| Step | Hyp | Ref
| Expression |
| 1 | | nn0uz 12920 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
| 2 | | 0nn0 12541 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
| 3 | 2 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 0 ∈ ℕ0) |
| 4 | | 1e0p1 12775 |
. . . . . 6
⊢ 1 = (0 +
1) |
| 5 | | 0z 12624 |
. . . . . . 7
⊢ 0 ∈
ℤ |
| 6 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑛 = 0 → (!‘𝑛) =
(!‘0)) |
| 7 | | fac0 14315 |
. . . . . . . . . . . 12
⊢
(!‘0) = 1 |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝑛 = 0 → (!‘𝑛) = 1) |
| 9 | 8 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1)) |
| 10 | | ax-1cn 11213 |
. . . . . . . . . . 11
⊢ 1 ∈
ℂ |
| 11 | 10 | div1i 11995 |
. . . . . . . . . 10
⊢ (1 / 1) =
1 |
| 12 | 9, 11 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (𝑛 = 0 → (1 / (!‘𝑛)) = 1) |
| 13 | | erelem1.2 |
. . . . . . . . 9
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 /
(!‘𝑛))) |
| 14 | | 1ex 11257 |
. . . . . . . . 9
⊢ 1 ∈
V |
| 15 | 12, 13, 14 | fvmpt 7016 |
. . . . . . . 8
⊢ (0 ∈
ℕ0 → (𝐺‘0) = 1) |
| 16 | 2, 15 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (𝐺‘0) =
1) |
| 17 | 5, 16 | seq1i 14056 |
. . . . . 6
⊢ (⊤
→ (seq0( + , 𝐺)‘0) = 1) |
| 18 | | 1nn0 12542 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
| 19 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑛 = 1 → (!‘𝑛) =
(!‘1)) |
| 20 | | fac1 14316 |
. . . . . . . . . . 11
⊢
(!‘1) = 1 |
| 21 | 19, 20 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (𝑛 = 1 → (!‘𝑛) = 1) |
| 22 | 21 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1)) |
| 23 | 22, 11 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑛 = 1 → (1 / (!‘𝑛)) = 1) |
| 24 | 23, 13, 14 | fvmpt 7016 |
. . . . . . 7
⊢ (1 ∈
ℕ0 → (𝐺‘1) = 1) |
| 25 | 18, 24 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝐺‘1) =
1) |
| 26 | 1, 3, 4, 17, 25 | seqp1d 14059 |
. . . . 5
⊢ (⊤
→ (seq0( + , 𝐺)‘1) = (1 + 1)) |
| 27 | | df-2 12329 |
. . . . 5
⊢ 2 = (1 +
1) |
| 28 | 26, 27 | eqtr4di 2795 |
. . . 4
⊢ (⊤
→ (seq0( + , 𝐺)‘1) = 2) |
| 29 | 18 | a1i 11 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℕ0) |
| 30 | | nn0z 12638 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
| 31 | | 1exp 14132 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ (1↑𝑛) =
1) |
| 33 | 32 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((1↑𝑛) /
(!‘𝑛)) = (1 /
(!‘𝑛))) |
| 34 | 33 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ ((1↑𝑛) /
(!‘𝑛))) = (𝑛 ∈ ℕ0
↦ (1 / (!‘𝑛))) |
| 35 | 13, 34 | eqtr4i 2768 |
. . . . . . . 8
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦
((1↑𝑛) /
(!‘𝑛))) |
| 36 | 35 | efcvg 16121 |
. . . . . . 7
⊢ (1 ∈
ℂ → seq0( + , 𝐺)
⇝ (exp‘1)) |
| 37 | 10, 36 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ seq0( + , 𝐺) ⇝
(exp‘1)) |
| 38 | | df-e 16104 |
. . . . . 6
⊢ e =
(exp‘1) |
| 39 | 37, 38 | breqtrrdi 5185 |
. . . . 5
⊢ (⊤
→ seq0( + , 𝐺) ⇝
e) |
| 40 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘)) |
| 41 | 40 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘))) |
| 42 | | ovex 7464 |
. . . . . . . 8
⊢ (1 /
(!‘𝑘)) ∈
V |
| 43 | 41, 13, 42 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (𝐺‘𝑘) = (1 / (!‘𝑘))) |
| 44 | 43 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (𝐺‘𝑘) = (1 / (!‘𝑘))) |
| 45 | | faccl 14322 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
| 46 | 45 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (!‘𝑘) ∈ ℕ) |
| 47 | 46 | nnrecred 12317 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ) |
| 48 | 44, 47 | eqeltrd 2841 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (𝐺‘𝑘) ∈ ℝ) |
| 49 | 46 | nnred 12281 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (!‘𝑘) ∈ ℝ) |
| 50 | 46 | nngt0d 12315 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 0 < (!‘𝑘)) |
| 51 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 52 | | 0le1 11786 |
. . . . . . . 8
⊢ 0 ≤
1 |
| 53 | | divge0 12137 |
. . . . . . . 8
⊢ (((1
∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 /
(!‘𝑘))) |
| 54 | 51, 52, 53 | mpanl12 702 |
. . . . . . 7
⊢
(((!‘𝑘) ∈
ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘))) |
| 55 | 49, 50, 54 | syl2anc 584 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 0 ≤ (1 / (!‘𝑘))) |
| 56 | 55, 44 | breqtrrd 5171 |
. . . . 5
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 0 ≤ (𝐺‘𝑘)) |
| 57 | 1, 29, 39, 48, 56 | climserle 15699 |
. . . 4
⊢ (⊤
→ (seq0( + , 𝐺)‘1) ≤ e) |
| 58 | 28, 57 | eqbrtrrd 5167 |
. . 3
⊢ (⊤
→ 2 ≤ e) |
| 59 | 58 | mptru 1547 |
. 2
⊢ 2 ≤
e |
| 60 | | nnuz 12921 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
| 61 | | 1zzd 12648 |
. . . . . 6
⊢ (⊤
→ 1 ∈ ℤ) |
| 62 | 48 | recnd 11289 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
| 63 | 1, 3, 62, 39 | clim2ser 15691 |
. . . . . . 7
⊢ (⊤
→ seq(0 + 1)( + , 𝐺)
⇝ (e − (seq0( + , 𝐺)‘0))) |
| 64 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 65 | | seqeq1 14045 |
. . . . . . . 8
⊢ ((0 + 1)
= 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)) |
| 66 | 64, 65 | ax-mp 5 |
. . . . . . 7
⊢ seq(0 +
1)( + , 𝐺) = seq1( + ,
𝐺) |
| 67 | 17 | mptru 1547 |
. . . . . . . 8
⊢ (seq0( +
, 𝐺)‘0) =
1 |
| 68 | 67 | oveq2i 7442 |
. . . . . . 7
⊢ (e
− (seq0( + , 𝐺)‘0)) = (e − 1) |
| 69 | 63, 66, 68 | 3brtr3g 5176 |
. . . . . 6
⊢ (⊤
→ seq1( + , 𝐺) ⇝
(e − 1)) |
| 70 | | 2cnd 12344 |
. . . . . . . 8
⊢ (⊤
→ 2 ∈ ℂ) |
| 71 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘)) |
| 72 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛)) =
(𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)) |
| 73 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ ((1 /
2)↑𝑘) ∈
V |
| 74 | 71, 72, 73 | fvmpt 7016 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
| 75 | 74 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
| 76 | | halfre 12480 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ |
| 77 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 𝑘 ∈ ℕ0) |
| 78 | | reexpcl 14119 |
. . . . . . . . . . . . 13
⊢ (((1 / 2)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ) |
| 79 | 76, 77, 78 | sylancr 587 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ) |
| 80 | 79 | recnd 11289 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ) |
| 81 | 75, 80 | eqeltrd 2841 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑘) ∈
ℂ) |
| 82 | | 1lt2 12437 |
. . . . . . . . . . . . . 14
⊢ 1 <
2 |
| 83 | | 2re 12340 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
| 84 | | 0le2 12368 |
. . . . . . . . . . . . . . 15
⊢ 0 ≤
2 |
| 85 | | absid 15335 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2) |
| 86 | 83, 84, 85 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
(abs‘2) = 2 |
| 87 | 82, 86 | breqtrri 5170 |
. . . . . . . . . . . . 13
⊢ 1 <
(abs‘2) |
| 88 | 87 | a1i 11 |
. . . . . . . . . . . 12
⊢ (⊤
→ 1 < (abs‘2)) |
| 89 | 70, 88, 75 | georeclim 15908 |
. . . . . . . . . . 11
⊢ (⊤
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 −
1))) |
| 90 | | 2m1e1 12392 |
. . . . . . . . . . . . 13
⊢ (2
− 1) = 1 |
| 91 | 90 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (2 / (2
− 1)) = (2 / 1) |
| 92 | | 2cn 12341 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
| 93 | 92 | div1i 11995 |
. . . . . . . . . . . 12
⊢ (2 / 1) =
2 |
| 94 | 91, 93 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (2 / (2
− 1)) = 2 |
| 95 | 89, 94 | breqtrdi 5184 |
. . . . . . . . . 10
⊢ (⊤
→ seq0( + , (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2) |
| 96 | 1, 3, 81, 95 | clim2ser 15691 |
. . . . . . . . 9
⊢ (⊤
→ seq(0 + 1)( + , (𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛)))‘0))) |
| 97 | | seqeq1 14045 |
. . . . . . . . . 10
⊢ ((0 + 1)
= 1 → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))) = seq1( + ,
(𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)))) |
| 98 | 64, 97 | ax-mp 5 |
. . . . . . . . 9
⊢ seq(0 +
1)( + , (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))) = seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))) |
| 99 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 /
2)↑0)) |
| 100 | | ovex 7464 |
. . . . . . . . . . . . . . . . 17
⊢ ((1 /
2)↑0) ∈ V |
| 101 | 99, 72, 100 | fvmpt 7016 |
. . . . . . . . . . . . . . . 16
⊢ (0 ∈
ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘0) = ((1
/ 2)↑0)) |
| 102 | 2, 101 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛))‘0) = ((1 /
2)↑0) |
| 103 | | halfcn 12481 |
. . . . . . . . . . . . . . . 16
⊢ (1 / 2)
∈ ℂ |
| 104 | | exp0 14106 |
. . . . . . . . . . . . . . . 16
⊢ ((1 / 2)
∈ ℂ → ((1 / 2)↑0) = 1) |
| 105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((1 /
2)↑0) = 1 |
| 106 | 102, 105 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
↦ ((1 / 2)↑𝑛))‘0) = 1 |
| 107 | 106 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ((𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1) |
| 108 | 5, 107 | seq1i 14056 |
. . . . . . . . . . . 12
⊢ (⊤
→ (seq0( + , (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1) |
| 109 | 108 | mptru 1547 |
. . . . . . . . . . 11
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1 |
| 110 | 109 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (2
− (seq0( + , (𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 −
1) |
| 111 | 110, 90 | eqtri 2765 |
. . . . . . . . 9
⊢ (2
− (seq0( + , (𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1 |
| 112 | 96, 98, 111 | 3brtr3g 5176 |
. . . . . . . 8
⊢ (⊤
→ seq1( + , (𝑛 ∈
ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1) |
| 113 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 114 | 113, 81 | sylan2 593 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ) |
| 115 | 71 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 /
2)↑𝑘))) |
| 116 | | erelem1.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 /
2)↑𝑛))) |
| 117 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (2
· ((1 / 2)↑𝑘))
∈ V |
| 118 | 115, 116,
117 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (2 · ((1 / 2)↑𝑘))) |
| 119 | 118 | adantl 481 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) = (2 · ((1 / 2)↑𝑘))) |
| 120 | 113, 75 | sylan2 593 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ) → ((𝑛
∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘)) |
| 121 | 120 | oveq2d 7447 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑘)) = (2 · ((1 /
2)↑𝑘))) |
| 122 | 119, 121 | eqtr4d 2780 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 /
2)↑𝑛))‘𝑘))) |
| 123 | 60, 61, 70, 112, 114, 122 | isermulc2 15694 |
. . . . . . 7
⊢ (⊤
→ seq1( + , 𝐹) ⇝
(2 · 1)) |
| 124 | | 2t1e2 12429 |
. . . . . . 7
⊢ (2
· 1) = 2 |
| 125 | 123, 124 | breqtrdi 5184 |
. . . . . 6
⊢ (⊤
→ seq1( + , 𝐹) ⇝
2) |
| 126 | 113, 48 | sylan2 593 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ∈ ℝ) |
| 127 | | remulcl 11240 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 /
2)↑𝑘)) ∈
ℝ) |
| 128 | 83, 79, 127 | sylancr 587 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ) |
| 129 | 113, 128 | sylan2 593 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ) |
| 130 | 119, 129 | eqeltrd 2841 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐹‘𝑘) ∈ ℝ) |
| 131 | | faclbnd2 14330 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((2↑𝑘) / 2)
≤ (!‘𝑘)) |
| 132 | 131 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘)) |
| 133 | | 2nn 12339 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ |
| 134 | | nnexpcl 14115 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) |
| 135 | 133, 77, 134 | sylancr 587 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) |
| 136 | 135 | nnrpd 13075 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈
ℝ+) |
| 137 | 136 | rphalfcld 13089 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((2↑𝑘) / 2) ∈
ℝ+) |
| 138 | 46 | nnrpd 13075 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (!‘𝑘) ∈
ℝ+) |
| 139 | 137, 138 | lerecd 13096 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))) |
| 140 | 132, 139 | mpbid 232 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))) |
| 141 | | 2cnd 12344 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 2 ∈ ℂ) |
| 142 | 135 | nncnd 12282 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℂ) |
| 143 | 135 | nnne0d 12316 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ≠ 0) |
| 144 | 141, 142,
143 | divrecd 12046 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘)))) |
| 145 | | 2ne0 12370 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
| 146 | | recdiv 11973 |
. . . . . . . . . . . 12
⊢
((((2↑𝑘) ∈
ℂ ∧ (2↑𝑘)
≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘))) |
| 147 | 92, 145, 146 | mpanr12 705 |
. . . . . . . . . . 11
⊢
(((2↑𝑘) ∈
ℂ ∧ (2↑𝑘)
≠ 0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘))) |
| 148 | 142, 143,
147 | syl2anc 584 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘))) |
| 149 | 145 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 2 ≠ 0) |
| 150 | | nn0z 12638 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
| 151 | 150 | adantl 481 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → 𝑘 ∈ ℤ) |
| 152 | 141, 149,
151 | exprecd 14194 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘))) |
| 153 | 152 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘)))) |
| 154 | 144, 148,
153 | 3eqtr4rd 2788 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2))) |
| 155 | 140, 154 | breqtrrd 5171 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑘
∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘))) |
| 156 | 113, 155 | sylan2 593 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘))) |
| 157 | 113, 44 | sylan2 593 |
. . . . . . 7
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) = (1 / (!‘𝑘))) |
| 158 | 156, 157,
119 | 3brtr4d 5175 |
. . . . . 6
⊢
((⊤ ∧ 𝑘
∈ ℕ) → (𝐺‘𝑘) ≤ (𝐹‘𝑘)) |
| 159 | 60, 61, 69, 125, 126, 130, 158 | iserle 15696 |
. . . . 5
⊢ (⊤
→ (e − 1) ≤ 2) |
| 160 | 159 | mptru 1547 |
. . . 4
⊢ (e
− 1) ≤ 2 |
| 161 | | ere 16125 |
. . . . 5
⊢ e ∈
ℝ |
| 162 | 161, 51, 83 | lesubaddi 11821 |
. . . 4
⊢ ((e
− 1) ≤ 2 ↔ e ≤ (2 + 1)) |
| 163 | 160, 162 | mpbi 230 |
. . 3
⊢ e ≤ (2
+ 1) |
| 164 | | df-3 12330 |
. . 3
⊢ 3 = (2 +
1) |
| 165 | 163, 164 | breqtrri 5170 |
. 2
⊢ e ≤
3 |
| 166 | 59, 165 | pm3.2i 470 |
1
⊢ (2 ≤ e
∧ e ≤ 3) |