Bounds on specific values of the exponential

theorem Real.exp_one_near_10 : |exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10

theorem Real.exp_one_near_20 : |exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20

theorem Real.exp_one_gt_d9 : 2.7182818283 < exp 1

theorem Real.exp_one_lt_d9 : exp 1 < 2.7182818286

theorem Real.exp_one_gt_two : 2 < exp 1

theorem Real.exp_one_lt_three : exp 1 < 3

theorem Real.floor_exp_one_eq_two : ⌊exp 1⌋ = 2

theorem Real.ceil_exp_one_eq_three : ⌈exp 1⌉ = 3

theorem Real.round_exp_one_eq_three : round (exp 1) = 3

theorem Real.exp_neg_one_gt_d9 : 0.36787944116 < exp (-1)

theorem Real.exp_neg_one_lt_d9 : exp (-1) < 0.3678794412

theorem Real.exp_neg_one_lt_half : exp (-1) < 1 / 2

theorem Real.log_two_near_10 : |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10

theorem Real.log_two_gt_d9 : 0.6931471803 < log 2

theorem Real.log_two_lt_d9 : log 2 < 0.6931471808

theorem Real.log_three_near_10 : |log 3 - 109861228867 / 100000000000| ≤ 1 / 10 ^ 10

theorem Real.log_three_gt_d9 : 1.0986122885 < log 3

theorem Real.log_three_lt_d9 : log 3 < 1.0986122888

theorem Real.log_five_near_10 : |log 5 - 160943791243 / 100000000000| ≤ 1 / 10 ^ 10

theorem Real.log_five_gt_d9 : 1.6094379123 < log 5

theorem Real.log_five_lt_d9 : log 5 < 1.6094379126