[GOAL]
⊢ |exp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10
[PROOFSTEP]
apply exp_approx_start
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)
[PROOFSTEP]
iterate 13 refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (2244083 / 825552)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 0 + 1 = ?m.664
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 = ?m.664
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑1 = ?m.675
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 1 1 ((2244083 / 825552 - 1) * 1)| ≤ |1| ^ 1 / ↑(Nat.factorial 1) * (1 / 10 ^ 10 * 1)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 1 + 1 = ?m.1007
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2 = ?m.1007
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑2 = ?m.1009
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 2 1 (((2244083 / 825552 - 1) * 1 - 1) * 2)| ≤ |1| ^ 2 / ↑(Nat.factorial 2) * (1 / 10 ^ 10 * 1 * 2)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 2 + 1 = ?m.1077
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 3 = ?m.1077
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑3 = ?m.1079
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 3 1 ((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    |1| ^ 3 / ↑(Nat.factorial 3) * (1 / 10 ^ 10 * 1 * 2 * 3)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 3 + 1 = ?m.1147
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 4 = ?m.1147
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑4 = ?m.1149
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 4 1 (((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    |1| ^ 4 / ↑(Nat.factorial 4) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 4 + 1 = ?m.1217
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 5 = ?m.1217
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑5 = ?m.1219
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 5 1 ((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 5 + 1 = ?m.1287
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 6 = ?m.1287
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑6 = ?m.1289
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 6 1 (((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 6 + 1 = ?m.1357
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 7 = ?m.1357
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑7 = ?m.1359
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 7 1 ((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 7 + 1 = ?m.1427
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 8 = ?m.1427
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑8 = ?m.1429
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 8 1
          (((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 8 + 1 = ?m.1497
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 9 = ?m.1497
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑9 = ?m.1499
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 9 1
          ((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
            9)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 9 + 1 = ?m.1567
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 10 = ?m.1567
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑10 = ?m.1569
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 10 1
          (((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) * 9 -
              1) *
            10)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 10 + 1 = ?m.1637
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 11 = ?m.1637
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑11 = ?m.1639
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 11 1
          ((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                    9 -
                  1) *
                10 -
              1) *
            11)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 11 + 1 = ?m.1707
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 12 = ?m.1707
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑12 = ?m.1709
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 12 1
          (((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                        9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 12 + 1 = ?m.1777
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 13 = ?m.1777
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑13 = ?m.1779
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 13 1
          ((((((((((((((2244083 / 825552 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) * 8 - 1) *
                            9 -
                          1) *
                        10 -
                      1) *
                    11 -
                  1) *
                12 -
              1) *
            13)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 10 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ |exp 1 - expNear 13 1 (5 / 7)| ≤ |1| ^ 13 / ↑(Nat.factorial 13) * (243243 / 390625)
[PROOFSTEP]
refine' exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) _
[GOAL]
⊢ 13 + 1 = ?m.2354
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 14 = ?m.2354
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑14 = ?m.2356
[PROOFSTEP]
norm_cast
[GOAL]
⊢ |1| ≤ 1
[PROOFSTEP]
simp
[GOAL]
case h
⊢ |1 - 5 / 7| ≤ 243243 / 390625 - |1| / 14 * ((14 + 1) / 14)
[PROOFSTEP]
rw [_root_.abs_one, abs_of_pos]
[GOAL]
case h
⊢ 1 - 5 / 7 ≤ 243243 / 390625 - 1 / 14 * ((14 + 1) / 14)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ 0 < 1 - 5 / 7
[PROOFSTEP]
norm_num1
[GOAL]
⊢ |exp 1 - 363916618873 / 133877442384| ≤ 1 / 10 ^ 20
[PROOFSTEP]
apply exp_approx_start
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
[PROOFSTEP]
iterate 21 refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
case h
⊢ |exp 1 - expNear 0 1 (363916618873 / 133877442384)| ≤ |1| ^ 0 / ↑(Nat.factorial 0) * (1 / 10 ^ 20)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 0 + 1 = ?m.3624
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 = ?m.3624
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑1 = ?m.3635
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 1 1 ((363916618873 / 133877442384 - 1) * 1)| ≤ |1| ^ 1 / ↑(Nat.factorial 1) * (1 / 10 ^ 20 * 1)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 1 + 1 = ?m.3967
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2 = ?m.3967
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑2 = ?m.3969
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 2 1 (((363916618873 / 133877442384 - 1) * 1 - 1) * 2)| ≤
    |1| ^ 2 / ↑(Nat.factorial 2) * (1 / 10 ^ 20 * 1 * 2)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 2 + 1 = ?m.4037
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 3 = ?m.4037
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑3 = ?m.4039
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 3 1 ((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3)| ≤
    |1| ^ 3 / ↑(Nat.factorial 3) * (1 / 10 ^ 20 * 1 * 2 * 3)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 3 + 1 = ?m.4107
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 4 = ?m.4107
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑4 = ?m.4109
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 4 1 (((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4)| ≤
    |1| ^ 4 / ↑(Nat.factorial 4) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 4 + 1 = ?m.4177
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 5 = ?m.4177
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑5 = ?m.4179
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 5 1 ((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5)| ≤
    |1| ^ 5 / ↑(Nat.factorial 5) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 5 + 1 = ?m.4247
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 6 = ?m.4247
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑6 = ?m.4249
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 - expNear 6 1 (((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6)| ≤
    |1| ^ 6 / ↑(Nat.factorial 6) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 6 + 1 = ?m.4317
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 7 = ?m.4317
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑7 = ?m.4319
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 7 1
          ((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7)| ≤
    |1| ^ 7 / ↑(Nat.factorial 7) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 7 + 1 = ?m.4387
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 8 = ?m.4387
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑8 = ?m.4389
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 8 1
          (((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
            8)| ≤
    |1| ^ 8 / ↑(Nat.factorial 8) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 8 + 1 = ?m.4457
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 9 = ?m.4457
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑9 = ?m.4459
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 9 1
          ((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                8 -
              1) *
            9)| ≤
    |1| ^ 9 / ↑(Nat.factorial 9) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 9 + 1 = ?m.4527
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 10 = ?m.4527
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑10 = ?m.4529
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 10 1
          (((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                    8 -
                  1) *
                9 -
              1) *
            10)| ≤
    |1| ^ 10 / ↑(Nat.factorial 10) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 10 + 1 = ?m.4597
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 11 = ?m.4597
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑11 = ?m.4599
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 11 1
          ((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                        8 -
                      1) *
                    9 -
                  1) *
                10 -
              1) *
            11)| ≤
    |1| ^ 11 / ↑(Nat.factorial 11) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 11 + 1 = ?m.4667
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 12 = ?m.4667
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑12 = ?m.4669
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 12 1
          (((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 - 1) *
                            8 -
                          1) *
                        9 -
                      1) *
                    10 -
                  1) *
                11 -
              1) *
            12)| ≤
    |1| ^ 12 / ↑(Nat.factorial 12) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 12 + 1 = ?m.4737
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 13 = ?m.4737
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑13 = ?m.4739
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 13 1
          ((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                  1) *
                                8 -
                              1) *
                            9 -
                          1) *
                        10 -
                      1) *
                    11 -
                  1) *
                12 -
              1) *
            13)| ≤
    |1| ^ 13 / ↑(Nat.factorial 13) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 13 + 1 = ?m.4807
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 14 = ?m.4807
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑14 = ?m.4809
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 14 1
          (((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                      1) *
                                    8 -
                                  1) *
                                9 -
                              1) *
                            10 -
                          1) *
                        11 -
                      1) *
                    12 -
                  1) *
                13 -
              1) *
            14)| ≤
    |1| ^ 14 / ↑(Nat.factorial 14) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 14 + 1 = ?m.4877
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 15 = ?m.4877
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑15 = ?m.4879
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 15 1
          ((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                          1) *
                                        8 -
                                      1) *
                                    9 -
                                  1) *
                                10 -
                              1) *
                            11 -
                          1) *
                        12 -
                      1) *
                    13 -
                  1) *
                14 -
              1) *
            15)| ≤
    |1| ^ 15 / ↑(Nat.factorial 15) * (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 15 + 1 = ?m.4947
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 16 = ?m.4947
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑16 = ?m.4949
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 16 1
          (((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                              1) *
                                            8 -
                                          1) *
                                        9 -
                                      1) *
                                    10 -
                                  1) *
                                11 -
                              1) *
                            12 -
                          1) *
                        13 -
                      1) *
                    14 -
                  1) *
                15 -
              1) *
            16)| ≤
    |1| ^ 16 / ↑(Nat.factorial 16) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 16 + 1 = ?m.5017
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 17 = ?m.5017
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑17 = ?m.5019
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 17 1
          ((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) * 7 -
                                                  1) *
                                                8 -
                                              1) *
                                            9 -
                                          1) *
                                        10 -
                                      1) *
                                    11 -
                                  1) *
                                12 -
                              1) *
                            13 -
                          1) *
                        14 -
                      1) *
                    15 -
                  1) *
                16 -
              1) *
            17)| ≤
    |1| ^ 17 / ↑(Nat.factorial 17) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 17 + 1 = ?m.5087
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 18 = ?m.5087
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑18 = ?m.5089
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 18 1
          (((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                        7 -
                                                      1) *
                                                    8 -
                                                  1) *
                                                9 -
                                              1) *
                                            10 -
                                          1) *
                                        11 -
                                      1) *
                                    12 -
                                  1) *
                                13 -
                              1) *
                            14 -
                          1) *
                        15 -
                      1) *
                    16 -
                  1) *
                17 -
              1) *
            18)| ≤
    |1| ^ 18 / ↑(Nat.factorial 18) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 18 + 1 = ?m.5157
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 19 = ?m.5157
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑19 = ?m.5159
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 19 1
          ((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                            7 -
                                                          1) *
                                                        8 -
                                                      1) *
                                                    9 -
                                                  1) *
                                                10 -
                                              1) *
                                            11 -
                                          1) *
                                        12 -
                                      1) *
                                    13 -
                                  1) *
                                14 -
                              1) *
                            15 -
                          1) *
                        16 -
                      1) *
                    17 -
                  1) *
                18 -
              1) *
            19)| ≤
    |1| ^ 19 / ↑(Nat.factorial 19) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 19 + 1 = ?m.5227
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 20 = ?m.5227
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑20 = ?m.5229
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 20 1
          (((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                7 -
                                                              1) *
                                                            8 -
                                                          1) *
                                                        9 -
                                                      1) *
                                                    10 -
                                                  1) *
                                                11 -
                                              1) *
                                            12 -
                                          1) *
                                        13 -
                                      1) *
                                    14 -
                                  1) *
                                15 -
                              1) *
                            16 -
                          1) *
                        17 -
                      1) *
                    18 -
                  1) *
                19 -
              1) *
            20)| ≤
    |1| ^ 20 / ↑(Nat.factorial 20) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20)
[PROOFSTEP]
refine' exp_1_approx_succ_eq (by norm_num1; rfl) (by norm_cast) _
[GOAL]
⊢ 20 + 1 = ?m.5297
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 21 = ?m.5297
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑21 = ?m.5299
[PROOFSTEP]
norm_cast
[GOAL]
case h
⊢ |exp 1 -
        expNear 21 1
          ((((((((((((((((((((((363916618873 / 133877442384 - 1) * 1 - 1) * 2 - 1) * 3 - 1) * 4 - 1) * 5 - 1) * 6 - 1) *
                                                                    7 -
                                                                  1) *
                                                                8 -
                                                              1) *
                                                            9 -
                                                          1) *
                                                        10 -
                                                      1) *
                                                    11 -
                                                  1) *
                                                12 -
                                              1) *
                                            13 -
                                          1) *
                                        14 -
                                      1) *
                                    15 -
                                  1) *
                                16 -
                              1) *
                            17 -
                          1) *
                        18 -
                      1) *
                    19 -
                  1) *
                20 -
              1) *
            21)| ≤
    |1| ^ 21 / ↑(Nat.factorial 21) *
      (1 / 10 ^ 20 * 1 * 2 * 3 * 4 * 5 * 6 * 7 * 8 * 9 * 10 * 11 * 12 * 13 * 14 * 15 * 16 * 17 * 18 * 19 * 20 * 21)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ |exp 1 - expNear 21 1 (36295539 / 44271641)| ≤ |1| ^ 21 / ↑(Nat.factorial 21) * (311834363841 / 610351562500)
[PROOFSTEP]
refine' exp_approx_end' _ (by norm_num1; rfl) _ (by norm_cast) (by simp) _
[GOAL]
⊢ 21 + 1 = ?m.5994
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 22 = ?m.5994
[PROOFSTEP]
rfl
[GOAL]
⊢ ↑22 = ?m.5996
[PROOFSTEP]
norm_cast
[GOAL]
⊢ |1| ≤ 1
[PROOFSTEP]
simp
[GOAL]
case h
⊢ |1 - 36295539 / 44271641| ≤ 311834363841 / 610351562500 - |1| / 22 * ((22 + 1) / 22)
[PROOFSTEP]
rw [_root_.abs_one, abs_of_pos]
[GOAL]
case h
⊢ 1 - 36295539 / 44271641 ≤ 311834363841 / 610351562500 - 1 / 22 * ((22 + 1) / 22)
[PROOFSTEP]
norm_num1
[GOAL]
case h
⊢ 0 < 1 - 36295539 / 44271641
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 2.7182818283 < 2244083 / 825552 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 2.7182818286
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0.36787944116 < exp (-1)
[PROOFSTEP]
rw [exp_neg, lt_inv _ (exp_pos _)]
[GOAL]
⊢ exp 1 < 0.36787944116⁻¹
⊢ 0 < 0.36787944116
[PROOFSTEP]
refine' lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 exp_one_near_10).1) _
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹
⊢ 0 < 0.36787944116
[PROOFSTEP]
all_goals norm_num
[GOAL]
⊢ 1 / 10 ^ 10 + 2244083 / 825552 < 0.36787944116⁻¹
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 0.36787944116
[PROOFSTEP]
norm_num
[GOAL]
⊢ exp (-1) < 0.3678794412
[PROOFSTEP]
rw [exp_neg, inv_lt (exp_pos _)]
[GOAL]
⊢ 0.3678794412⁻¹ < exp 1
⊢ 0 < 0.3678794412
[PROOFSTEP]
refine' lt_of_lt_of_le _ (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)
[GOAL]
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10
⊢ 0 < 0.3678794412
[PROOFSTEP]
all_goals norm_num
[GOAL]
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0 < 0.3678794412
[PROOFSTEP]
norm_num
[GOAL]
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
[PROOFSTEP]
suffices |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
  by
  norm_num1 at *
  assumption
[GOAL]
this : |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10 ^ 10
[PROOFSTEP]
norm_num1 at *
[GOAL]
this : |log 2 - 287209 / 414355| ≤ 1 / 10000000000
⊢ |log 2 - 287209 / 414355| ≤ 1 / 10000000000
[PROOFSTEP]
assumption
[GOAL]
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
have t : |(2⁻¹ : ℝ)| = 2⁻¹ := by rw [abs_of_pos]; norm_num
[GOAL]
⊢ |2⁻¹| = 2⁻¹
[PROOFSTEP]
rw [abs_of_pos]
[GOAL]
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
have z := Real.abs_log_sub_add_sum_range_le (show |(2⁻¹ : ℝ)| < 1 by rw [t]; norm_num) 34
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ |2⁻¹| < 1
[PROOFSTEP]
rw [t]
[GOAL]
t : |2⁻¹| = 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun i => 2⁻¹ ^ (i + 1) / (↑i + 1)) + log (1 - 2⁻¹)| ≤ |2⁻¹| ^ (34 + 1) / (1 - |2⁻¹|)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
rw [t] at z 
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun i => 2⁻¹ ^ (i + 1) / (↑i + 1)) + log (1 - 2⁻¹)| ≤ 2⁻¹ ^ (34 + 1) / (1 - 2⁻¹)
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
norm_num1 at z 
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |(Finset.sum (range 34) fun x => (1 / 2) ^ (x + 1) / (↑x + 1)) + log (1 / 2)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
rw [one_div (2 : ℝ), log_inv, ← sub_eq_add_neg, _root_.abs_sub_comm] at z 
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |log 2 - 287209 / 414355| ≤ 1 / 17179869184 + (1 / 10 ^ 10 - 1 / 2 ^ 34)
[PROOFSTEP]
apply le_trans (_root_.abs_sub_le _ _ _) (add_le_add z _)
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |(Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)) - 287209 / 414355| ≤ 1 / 10 ^ 10 - 1 / 2 ^ 34
[PROOFSTEP]
simp_rw [sum_range_succ]
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |(Finset.sum (range 0) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)) + 2⁻¹ ^ (0 + 1) / (↑0 + 1) + 2⁻¹ ^ (1 + 1) / (↑1 + 1) +
                                                                        2⁻¹ ^ (2 + 1) / (↑2 + 1) +
                                                                      2⁻¹ ^ (3 + 1) / (↑3 + 1) +
                                                                    2⁻¹ ^ (4 + 1) / (↑4 + 1) +
                                                                  2⁻¹ ^ (5 + 1) / (↑5 + 1) +
                                                                2⁻¹ ^ (6 + 1) / (↑6 + 1) +
                                                              2⁻¹ ^ (7 + 1) / (↑7 + 1) +
                                                            2⁻¹ ^ (8 + 1) / (↑8 + 1) +
                                                          2⁻¹ ^ (9 + 1) / (↑9 + 1) +
                                                        2⁻¹ ^ (10 + 1) / (↑10 + 1) +
                                                      2⁻¹ ^ (11 + 1) / (↑11 + 1) +
                                                    2⁻¹ ^ (12 + 1) / (↑12 + 1) +
                                                  2⁻¹ ^ (13 + 1) / (↑13 + 1) +
                                                2⁻¹ ^ (14 + 1) / (↑14 + 1) +
                                              2⁻¹ ^ (15 + 1) / (↑15 + 1) +
                                            2⁻¹ ^ (16 + 1) / (↑16 + 1) +
                                          2⁻¹ ^ (17 + 1) / (↑17 + 1) +
                                        2⁻¹ ^ (18 + 1) / (↑18 + 1) +
                                      2⁻¹ ^ (19 + 1) / (↑19 + 1) +
                                    2⁻¹ ^ (20 + 1) / (↑20 + 1) +
                                  2⁻¹ ^ (21 + 1) / (↑21 + 1) +
                                2⁻¹ ^ (22 + 1) / (↑22 + 1) +
                              2⁻¹ ^ (23 + 1) / (↑23 + 1) +
                            2⁻¹ ^ (24 + 1) / (↑24 + 1) +
                          2⁻¹ ^ (25 + 1) / (↑25 + 1) +
                        2⁻¹ ^ (26 + 1) / (↑26 + 1) +
                      2⁻¹ ^ (27 + 1) / (↑27 + 1) +
                    2⁻¹ ^ (28 + 1) / (↑28 + 1) +
                  2⁻¹ ^ (29 + 1) / (↑29 + 1) +
                2⁻¹ ^ (30 + 1) / (↑30 + 1) +
              2⁻¹ ^ (31 + 1) / (↑31 + 1) +
            2⁻¹ ^ (32 + 1) / (↑32 + 1) +
          2⁻¹ ^ (33 + 1) / (↑33 + 1) -
        287209 / 414355| ≤
    1 / 10 ^ 10 - 1 / 2 ^ 34
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ |30417026706710207 / 51397301678363663775930777600| ≤ 7011591 / 167772160000000000
[PROOFSTEP]
rw [abs_of_pos]
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ 30417026706710207 / 51397301678363663775930777600 ≤ 7011591 / 167772160000000000
[PROOFSTEP]
norm_num
[GOAL]
t : |2⁻¹| = 2⁻¹
z : |log 2 - Finset.sum (range 34) fun x => 2⁻¹ ^ (x + 1) / (↑x + 1)| ≤ 1 / 17179869184
⊢ 0 < 30417026706710207 / 51397301678363663775930777600
[PROOFSTEP]
norm_num
[GOAL]
⊢ 0.6931471803 < 287209 / 414355 - 1 / 10 ^ 10
[PROOFSTEP]
norm_num1
[GOAL]
⊢ 1 / 10 ^ 10 + 287209 / 414355 < 0.6931471808
[PROOFSTEP]
norm_num
