Step | Hyp | Ref
| Expression |
1 | | nn0uz 11722 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11389 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ ℤ) |
3 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑛 → (2 · 𝑘) = (2 · 𝑛)) |
4 | 3 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑛 → ((2 · 𝑘) + 1) = ((2 · 𝑛) + 1)) |
5 | 4 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (3 · ((2 · 𝑘) + 1)) = (3 · ((2
· 𝑛) +
1))) |
6 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → (9↑𝑘) = (9↑𝑛)) |
7 | 5, 6 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)) = ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) |
8 | 7 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))) = (2 / ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛)))) |
9 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘)))) = (𝑘 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘)))) |
10 | | ovex 6678 |
. . . . . . . 8
⊢ (2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))
∈ V |
11 | 8, 9, 10 | fvmpt 6282 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
12 | 11 | adantl 482 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
13 | | 2re 11090 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
14 | | 3nn 11186 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ |
15 | | 2nn0 11309 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ0 |
16 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℕ0) |
17 | | nn0mulcl 11329 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ0 ∧ 𝑛 ∈ ℕ0) → (2
· 𝑛) ∈
ℕ0) |
18 | 15, 16, 17 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 · 𝑛) ∈
ℕ0) |
19 | | nn0p1nn 11332 |
. . . . . . . . . . 11
⊢ ((2
· 𝑛) ∈
ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 · 𝑛) + 1) ∈ ℕ) |
21 | | nnmulcl 11043 |
. . . . . . . . . 10
⊢ ((3
∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2
· 𝑛) + 1)) ∈
ℕ) |
22 | 14, 20, 21 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ) |
23 | | 9nn 11192 |
. . . . . . . . . 10
⊢ 9 ∈
ℕ |
24 | | nnexpcl 12873 |
. . . . . . . . . 10
⊢ ((9
∈ ℕ ∧ 𝑛
∈ ℕ0) → (9↑𝑛) ∈ ℕ) |
25 | 23, 16, 24 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (9↑𝑛) ∈ ℕ) |
26 | 22, 25 | nnmulcld 11068 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) |
27 | | nndivre 11056 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 ·
((2 · 𝑛) + 1))
· (9↑𝑛)))
∈ ℝ) |
28 | 13, 26, 27 | sylancr 695 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ) |
29 | 28 | recnd 10068 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ) |
30 | 9 | log2cnv 24671 |
. . . . . . 7
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2) |
31 | 30 | a1i 11 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2)) |
32 | 1, 2, 12, 29, 31 | isumclim 14488 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (log‘2)) |
33 | | eqid 2622 |
. . . . . 6
⊢
(ℤ≥‘𝑁) = (ℤ≥‘𝑁) |
34 | | id 22 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℕ0) |
35 | | seqex 12803 |
. . . . . . . 8
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ V |
36 | | fvex 6201 |
. . . . . . . 8
⊢
(log‘2) ∈ V |
37 | 35, 36 | breldm 5329 |
. . . . . . 7
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ⇝ (log‘2) → seq0( + ,
(𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ) |
38 | 30, 37 | mp1i 13 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ seq0( + , (𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ) |
39 | 1, 33, 34, 12, 29, 38 | isumsplit 14572 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
ℕ0 (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) + Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))) |
40 | 32, 39 | eqtr3d 2658 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (log‘2) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) + Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))))) |
41 | 40 | oveq1d 6665 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) =
((Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) +
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))))) |
42 | | fzfid 12772 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (0...(𝑁 − 1))
∈ Fin) |
43 | | elfznn0 12433 |
. . . . . 6
⊢ (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0) |
44 | 43, 29 | sylan2 491 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈ (0...(𝑁 − 1))) → (2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))
∈ ℂ) |
45 | 42, 44 | fsumcl 14464 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))
∈ ℂ) |
46 | | nn0z 11400 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
47 | | eluznn0 11757 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑛 ∈ ℕ0) |
48 | 47, 11 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘))))‘𝑛) = (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
49 | 47, 28 | syldan 487 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) ∈
ℝ) |
50 | 12, 29 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘))))‘𝑛) ∈ ℂ) |
51 | 1, 34, 50 | iserex 14387 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (seq0( + , (𝑘 ∈
ℕ0 ↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (2 / ((3
· ((2 · 𝑘) +
1)) · (9↑𝑘)))))
∈ dom ⇝ )) |
52 | 38, 51 | mpbid 222 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ (2 / ((3 · ((2 · 𝑘) + 1)) · (9↑𝑘))))) ∈ dom ⇝ ) |
53 | 33, 46, 48, 49, 52 | isumrecl 14496 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈
ℝ) |
54 | 53 | recnd 10068 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈
ℂ) |
55 | 45, 54 | pncan2d 10394 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ ((Σ𝑛 ∈
(0...(𝑁 − 1))(2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛))) +
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) =
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
56 | 41, 55 | eqtrd 2656 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) =
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
57 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 2 ∈ ℝ) |
58 | | 0le2 11111 |
. . . . . . 7
⊢ 0 ≤
2 |
59 | 58 | a1i 11 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 0 ≤ 2) |
60 | 26 | nnred 11035 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ) |
61 | 26 | nngt0d 11064 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 0 < ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) |
62 | | divge0 10892 |
. . . . . 6
⊢ (((2
∈ ℝ ∧ 0 ≤ 2) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 <
((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) → 0 ≤ (2 / ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛)))) |
63 | 57, 59, 60, 61, 62 | syl22anc 1327 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 0 ≤ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
64 | 47, 63 | syldan 487 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 ≤ (2 / ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛)))) |
65 | 33, 46, 48, 49, 52, 64 | isumge0 14497 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ Σ𝑛
∈ (ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
66 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑛 → ((1 / 9)↑𝑘) = ((1 / 9)↑𝑛)) |
67 | 66 | oveq2d 6666 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 /
9)↑𝑘)) = ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑛))) |
68 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘))) |
69 | | ovex 6678 |
. . . . . . . . 9
⊢ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑛)) ∈ V |
70 | 67, 68, 69 | fvmpt 6282 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 /
9)↑𝑛))) |
71 | 70 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 /
9)↑𝑛))) |
72 | | 9cn 11108 |
. . . . . . . . . . 11
⊢ 9 ∈
ℂ |
73 | 72 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 9 ∈ ℂ) |
74 | 23 | nnne0i 11055 |
. . . . . . . . . . 11
⊢ 9 ≠
0 |
75 | 74 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 9 ≠ 0) |
76 | | nn0z 11400 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) |
77 | 76 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 𝑛 ∈ ℤ) |
78 | 73, 75, 77 | exprecd 13016 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((1 / 9)↑𝑛) = (1 / (9↑𝑛))) |
79 | 78 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = ((2 / (3 · ((2
· 𝑁) + 1))) ·
(1 / (9↑𝑛)))) |
80 | | nn0mulcl 11329 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2
· 𝑁) ∈
ℕ0) |
81 | 15, 80 | mpan 706 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (2 · 𝑁)
∈ ℕ0) |
82 | | nn0p1nn 11332 |
. . . . . . . . . . . . . 14
⊢ ((2
· 𝑁) ∈
ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ) |
83 | 81, 82 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ ((2 · 𝑁) + 1)
∈ ℕ) |
84 | | nnmulcl 11043 |
. . . . . . . . . . . . 13
⊢ ((3
∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (3 ·
((2 · 𝑁) + 1))
∈ ℕ) |
85 | 14, 83, 84 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) |
86 | | nndivre 11056 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (3 · ((2 · 𝑁) + 1)) ∈ ℕ) → (2 / (3
· ((2 · 𝑁) +
1))) ∈ ℝ) |
87 | 13, 85, 86 | sylancr 695 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℝ) |
88 | 87 | recnd 10068 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ) |
89 | 88 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 / (3 · ((2 · 𝑁) + 1))) ∈ ℂ) |
90 | 25 | nncnd 11036 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (9↑𝑛) ∈ ℂ) |
91 | 25 | nnne0d 11065 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (9↑𝑛) ≠ 0) |
92 | 89, 90, 91 | divrecd 10804 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · (1 /
(9↑𝑛)))) |
93 | | 2cnd 11093 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → 2 ∈ ℂ) |
94 | 85 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℕ) |
95 | 94 | nncnd 11036 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (3 · ((2 · 𝑁) + 1)) ∈ ℂ) |
96 | 94 | nnne0d 11065 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (3 · ((2 · 𝑁) + 1)) ≠ 0) |
97 | 93, 95, 90, 96, 91 | divdiv1d 10832 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) / (9↑𝑛)) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))) |
98 | 79, 92, 97 | 3eqtr2d 2662 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑛)) = (2 / ((3 · ((2
· 𝑁) + 1)) ·
(9↑𝑛)))) |
99 | 71, 98 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))) |
100 | 47, 99 | syldan 487 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))‘𝑛) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))) |
101 | 94, 25 | nnmulcld 11068 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) |
102 | | nndivre 11056 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 ·
((2 · 𝑁) + 1))
· (9↑𝑛)))
∈ ℝ) |
103 | 13, 101, 102 | sylancr 695 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
ℕ0) → (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∈ ℝ) |
104 | 47, 103 | syldan 487 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 / ((3 · ((2 ·
𝑁) + 1)) ·
(9↑𝑛))) ∈
ℝ) |
105 | 81 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ∈
ℕ0) |
106 | 105 | nn0red 11352 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ∈ ℝ) |
107 | 15, 47, 17 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 · 𝑛) ∈
ℕ0) |
108 | 107 | nn0red 11352 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 · 𝑛) ∈ ℝ) |
109 | | 1red 10055 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 1 ∈ ℝ) |
110 | | eluzle 11700 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(ℤ≥‘𝑁) → 𝑁 ≤ 𝑛) |
111 | 110 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑁 ≤ 𝑛) |
112 | | nn0re 11301 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
113 | 112 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑁 ∈ ℝ) |
114 | 47 | nn0red 11352 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 𝑛 ∈ ℝ) |
115 | 13 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 2 ∈ ℝ) |
116 | | 2pos 11112 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
117 | 116 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 < 2) |
118 | | lemul2 10876 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ (2 ∈
ℝ ∧ 0 < 2)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛))) |
119 | 113, 114,
115, 117, 118 | syl112anc 1330 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (𝑁 ≤ 𝑛 ↔ (2 · 𝑁) ≤ (2 · 𝑛))) |
120 | 111, 119 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 · 𝑁) ≤ (2 · 𝑛)) |
121 | 106, 108,
109, 120 | leadd1dd 10641 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1)) |
122 | 83 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℕ) |
123 | 122 | nnred 11035 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑁) + 1) ∈ ℝ) |
124 | 47, 20 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℕ) |
125 | 124 | nnred 11035 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 · 𝑛) + 1) ∈ ℝ) |
126 | | 3re 11094 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
127 | 126 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 3 ∈ ℝ) |
128 | | 3pos 11114 |
. . . . . . . . . 10
⊢ 0 <
3 |
129 | 128 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 < 3) |
130 | | lemul2 10876 |
. . . . . . . . 9
⊢ ((((2
· 𝑁) + 1) ∈
ℝ ∧ ((2 · 𝑛) + 1) ∈ ℝ ∧ (3 ∈ ℝ
∧ 0 < 3)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2
· 𝑛) +
1)))) |
131 | 123, 125,
127, 129, 130 | syl112anc 1330 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (((2 · 𝑁) + 1) ≤ ((2 · 𝑛) + 1) ↔ (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2
· 𝑛) +
1)))) |
132 | 121, 131 | mpbid 222 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2
· 𝑛) +
1))) |
133 | 85 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈
ℕ) |
134 | 133 | nnred 11035 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (3 · ((2 · 𝑁) + 1)) ∈
ℝ) |
135 | 47, 22 | syldan 487 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈
ℕ) |
136 | 135 | nnred 11035 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (3 · ((2 · 𝑛) + 1)) ∈
ℝ) |
137 | 23, 47, 24 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℕ) |
138 | 137 | nnred 11035 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (9↑𝑛) ∈ ℝ) |
139 | 137 | nngt0d 11064 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 < (9↑𝑛)) |
140 | | lemul1 10875 |
. . . . . . . 8
⊢ (((3
· ((2 · 𝑁) +
1)) ∈ ℝ ∧ (3 · ((2 · 𝑛) + 1)) ∈ ℝ ∧ ((9↑𝑛) ∈ ℝ ∧ 0 <
(9↑𝑛))) → ((3
· ((2 · 𝑁) +
1)) ≤ (3 · ((2 · 𝑛) + 1)) ↔ ((3 · ((2 ·
𝑁) + 1)) ·
(9↑𝑛)) ≤ ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))) |
141 | 134, 136,
138, 139, 140 | syl112anc 1330 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) ≤ (3 · ((2
· 𝑛) + 1)) ↔
((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) |
142 | 132, 141 | mpbid 222 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛))) |
143 | 47, 101 | syldan 487 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈
ℕ) |
144 | 143 | nnred 11035 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ∈
ℝ) |
145 | 143 | nngt0d 11064 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 < ((3 · ((2 ·
𝑁) + 1)) ·
(9↑𝑛))) |
146 | 47, 60 | syldan 487 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈
ℝ) |
147 | 47, 61 | syldan 487 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → 0 < ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) |
148 | | lediv2 10913 |
. . . . . . 7
⊢ (((((3
· ((2 · 𝑁) +
1)) · (9↑𝑛))
∈ ℝ ∧ 0 < ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) ∧ (((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℝ ∧ 0 <
((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ↔ (2 / ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛))) ≤ (2 / ((3
· ((2 · 𝑁) +
1)) · (9↑𝑛))))) |
149 | 144, 145,
146, 147, 115, 117, 148 | syl222anc 1342 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)) ≤ ((3 · ((2
· 𝑛) + 1)) ·
(9↑𝑛)) ↔ (2 / ((3
· ((2 · 𝑛) +
1)) · (9↑𝑛)))
≤ (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))))) |
150 | 142, 149 | mpbid 222 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛))) ≤ (2 / ((3
· ((2 · 𝑁) +
1)) · (9↑𝑛)))) |
151 | | 9re 11107 |
. . . . . . . . . . . 12
⊢ 9 ∈
ℝ |
152 | 151, 74 | rereccli 10790 |
. . . . . . . . . . 11
⊢ (1 / 9)
∈ ℝ |
153 | 152 | recni 10052 |
. . . . . . . . . 10
⊢ (1 / 9)
∈ ℂ |
154 | 153 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (1 / 9) ∈ ℂ) |
155 | | 0re 10040 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
156 | | 9pos 11122 |
. . . . . . . . . . . . . 14
⊢ 0 <
9 |
157 | 151, 156 | recgt0ii 10929 |
. . . . . . . . . . . . 13
⊢ 0 < (1
/ 9) |
158 | 155, 152,
157 | ltleii 10160 |
. . . . . . . . . . . 12
⊢ 0 ≤ (1
/ 9) |
159 | | absid 14036 |
. . . . . . . . . . . 12
⊢ (((1 / 9)
∈ ℝ ∧ 0 ≤ (1 / 9)) → (abs‘(1 / 9)) = (1 /
9)) |
160 | 152, 158,
159 | mp2an 708 |
. . . . . . . . . . 11
⊢
(abs‘(1 / 9)) = (1 / 9) |
161 | | 1lt9 11229 |
. . . . . . . . . . . . 13
⊢ 1 <
9 |
162 | | recgt1i 10920 |
. . . . . . . . . . . . 13
⊢ ((9
∈ ℝ ∧ 1 < 9) → (0 < (1 / 9) ∧ (1 / 9) <
1)) |
163 | 151, 161,
162 | mp2an 708 |
. . . . . . . . . . . 12
⊢ (0 <
(1 / 9) ∧ (1 / 9) < 1) |
164 | 163 | simpri 478 |
. . . . . . . . . . 11
⊢ (1 / 9)
< 1 |
165 | 160, 164 | eqbrtri 4674 |
. . . . . . . . . 10
⊢
(abs‘(1 / 9)) < 1 |
166 | 165 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (abs‘(1 / 9)) < 1) |
167 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((1 / 9)↑𝑘)) =
(𝑘 ∈
ℕ0 ↦ ((1 / 9)↑𝑘)) |
168 | | ovex 6678 |
. . . . . . . . . . 11
⊢ ((1 /
9)↑𝑛) ∈
V |
169 | 66, 167, 168 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((1 / 9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛)) |
170 | 47, 169 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 /
9)↑𝑘))‘𝑛) = ((1 / 9)↑𝑛)) |
171 | 154, 166,
34, 170 | geolim2 14602 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((1 / 9)↑𝑘)))
⇝ (((1 / 9)↑𝑁) /
(1 − (1 / 9)))) |
172 | 72 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 9 ∈ ℂ) |
173 | 74 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 9 ≠ 0) |
174 | 172, 173,
46 | exprecd 13016 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((1 / 9)↑𝑁) =
(1 / (9↑𝑁))) |
175 | 72, 74 | dividi 10758 |
. . . . . . . . . . . . 13
⊢ (9 / 9) =
1 |
176 | 175 | oveq1i 6660 |
. . . . . . . . . . . 12
⊢ ((9 / 9)
− (1 / 9)) = (1 − (1 / 9)) |
177 | | ax-1cn 9994 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
178 | 72, 74 | pm3.2i 471 |
. . . . . . . . . . . . . 14
⊢ (9 ∈
ℂ ∧ 9 ≠ 0) |
179 | | divsubdir 10721 |
. . . . . . . . . . . . . 14
⊢ ((9
∈ ℂ ∧ 1 ∈ ℂ ∧ (9 ∈ ℂ ∧ 9 ≠ 0))
→ ((9 − 1) / 9) = ((9 / 9) − (1 / 9))) |
180 | 72, 177, 178, 179 | mp3an 1424 |
. . . . . . . . . . . . 13
⊢ ((9
− 1) / 9) = ((9 / 9) − (1 / 9)) |
181 | | df-9 11086 |
. . . . . . . . . . . . . . . 16
⊢ 9 = (8 +
1) |
182 | 181 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢ (9
− 1) = ((8 + 1) − 1) |
183 | | 8cn 11106 |
. . . . . . . . . . . . . . . 16
⊢ 8 ∈
ℂ |
184 | 183, 177 | pncan3oi 10297 |
. . . . . . . . . . . . . . 15
⊢ ((8 + 1)
− 1) = 8 |
185 | 182, 184 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ (9
− 1) = 8 |
186 | 185 | oveq1i 6660 |
. . . . . . . . . . . . 13
⊢ ((9
− 1) / 9) = (8 / 9) |
187 | 180, 186 | eqtr3i 2646 |
. . . . . . . . . . . 12
⊢ ((9 / 9)
− (1 / 9)) = (8 / 9) |
188 | 176, 187 | eqtr3i 2646 |
. . . . . . . . . . 11
⊢ (1
− (1 / 9)) = (8 / 9) |
189 | 188 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (1 − (1 / 9)) = (8 / 9)) |
190 | 174, 189 | oveq12d 6668 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (((1 / 9)↑𝑁) /
(1 − (1 / 9))) = ((1 / (9↑𝑁)) / (8 / 9))) |
191 | 177 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 1 ∈ ℂ) |
192 | | nnexpcl 12873 |
. . . . . . . . . . . 12
⊢ ((9
∈ ℕ ∧ 𝑁
∈ ℕ0) → (9↑𝑁) ∈ ℕ) |
193 | 23, 192 | mpan 706 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (9↑𝑁) ∈
ℕ) |
194 | 193 | nncnd 11036 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (9↑𝑁) ∈
ℂ) |
195 | 183, 72, 74 | divcli 10767 |
. . . . . . . . . . 11
⊢ (8 / 9)
∈ ℂ |
196 | 195 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (8 / 9) ∈ ℂ) |
197 | 193 | nnne0d 11065 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (9↑𝑁) ≠
0) |
198 | | 8nn 11191 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℕ |
199 | 198 | nnne0i 11055 |
. . . . . . . . . . . 12
⊢ 8 ≠
0 |
200 | 183, 72, 199, 74 | divne0i 10773 |
. . . . . . . . . . 11
⊢ (8 / 9)
≠ 0 |
201 | 200 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (8 / 9) ≠ 0) |
202 | 191, 194,
196, 197, 201 | divdiv32d 10826 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((1 / (9↑𝑁)) /
(8 / 9)) = ((1 / (8 / 9)) / (9↑𝑁))) |
203 | | recdiv 10731 |
. . . . . . . . . . . 12
⊢ (((8
∈ ℂ ∧ 8 ≠ 0) ∧ (9 ∈ ℂ ∧ 9 ≠ 0)) →
(1 / (8 / 9)) = (9 / 8)) |
204 | 183, 199,
72, 74, 203 | mp4an 709 |
. . . . . . . . . . 11
⊢ (1 / (8 /
9)) = (9 / 8) |
205 | 204 | oveq1i 6660 |
. . . . . . . . . 10
⊢ ((1 / (8
/ 9)) / (9↑𝑁)) = ((9 /
8) / (9↑𝑁)) |
206 | 183 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 8 ∈ ℂ) |
207 | 199 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ 8 ≠ 0) |
208 | 172, 206,
194, 207, 197 | divdiv1d 10832 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((9 / 8) / (9↑𝑁)) = (9 / (8 · (9↑𝑁)))) |
209 | 205, 208 | syl5eq 2668 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((1 / (8 / 9)) / (9↑𝑁)) = (9 / (8 · (9↑𝑁)))) |
210 | 190, 202,
209 | 3eqtrd 2660 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (((1 / 9)↑𝑁) /
(1 − (1 / 9))) = (9 / (8 · (9↑𝑁)))) |
211 | 171, 210 | breqtrd 4679 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((1 / 9)↑𝑘)))
⇝ (9 / (8 · (9↑𝑁)))) |
212 | | expcl 12878 |
. . . . . . . . 9
⊢ (((1 / 9)
∈ ℂ ∧ 𝑛
∈ ℕ0) → ((1 / 9)↑𝑛) ∈ ℂ) |
213 | 153, 47, 212 | sylancr 695 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((1 / 9)↑𝑛) ∈ ℂ) |
214 | 170, 213 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((1 /
9)↑𝑘))‘𝑛) ∈
ℂ) |
215 | 47, 70 | syl 17 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 /
9)↑𝑛))) |
216 | 170 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((2 / (3 · ((2 ·
𝑁) + 1))) · ((𝑘 ∈ ℕ0
↦ ((1 / 9)↑𝑘))‘𝑛)) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 /
9)↑𝑛))) |
217 | 215, 216 | eqtr4d 2659 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))‘𝑛) = ((2 / (3 · ((2 · 𝑁) + 1))) · ((𝑘 ∈ ℕ0
↦ ((1 / 9)↑𝑘))‘𝑛))) |
218 | 33, 46, 88, 211, 214, 217 | isermulc2 14388 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 ·
((2 · 𝑁) + 1)))
· (9 / (8 · (9↑𝑁))))) |
219 | | seqex 12803 |
. . . . . . 7
⊢ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))) ∈ V |
220 | | ovex 6678 |
. . . . . . 7
⊢ ((2 / (3
· ((2 · 𝑁) +
1))) · (9 / (8 · (9↑𝑁)))) ∈ V |
221 | 219, 220 | breldm 5329 |
. . . . . 6
⊢ (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((2 / (3
· ((2 · 𝑁) +
1))) · ((1 / 9)↑𝑘)))) ⇝ ((2 / (3 · ((2 ·
𝑁) + 1))) · (9 / (8
· (9↑𝑁))))
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝
) |
222 | 218, 221 | syl 17 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ∈ dom ⇝
) |
223 | 33, 46, 48, 49, 100, 104, 150, 52, 222 | isumle 14576 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛)))) |
224 | 104 | recnd 10068 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑛 ∈
(ℤ≥‘𝑁)) → (2 / ((3 · ((2 ·
𝑁) + 1)) ·
(9↑𝑛))) ∈
ℂ) |
225 | | 3cn 11095 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
226 | | 4cn 11098 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℂ |
227 | | 2cn 11091 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℂ |
228 | | 4ne0 11117 |
. . . . . . . . . . . 12
⊢ 4 ≠
0 |
229 | | 3ne0 11115 |
. . . . . . . . . . . 12
⊢ 3 ≠
0 |
230 | | 2ne0 11113 |
. . . . . . . . . . . 12
⊢ 2 ≠
0 |
231 | 225, 226,
227, 225, 228, 229, 230 | divdivdivi 10788 |
. . . . . . . . . . 11
⊢ ((3 / 4)
/ (2 / 3)) = ((3 · 3) / (4 · 2)) |
232 | | 3t3e9 11180 |
. . . . . . . . . . . 12
⊢ (3
· 3) = 9 |
233 | | 4t2e8 11181 |
. . . . . . . . . . . 12
⊢ (4
· 2) = 8 |
234 | 232, 233 | oveq12i 6662 |
. . . . . . . . . . 11
⊢ ((3
· 3) / (4 · 2)) = (9 / 8) |
235 | 231, 234 | eqtri 2644 |
. . . . . . . . . 10
⊢ ((3 / 4)
/ (2 / 3)) = (9 / 8) |
236 | 235 | oveq2i 6661 |
. . . . . . . . 9
⊢ ((2 / 3)
· ((3 / 4) / (2 / 3))) = ((2 / 3) · (9 / 8)) |
237 | 225, 226,
228 | divcli 10767 |
. . . . . . . . . 10
⊢ (3 / 4)
∈ ℂ |
238 | 227, 225,
229 | divcli 10767 |
. . . . . . . . . 10
⊢ (2 / 3)
∈ ℂ |
239 | 227, 225,
230, 229 | divne0i 10773 |
. . . . . . . . . 10
⊢ (2 / 3)
≠ 0 |
240 | 237, 238,
239 | divcan2i 10768 |
. . . . . . . . 9
⊢ ((2 / 3)
· ((3 / 4) / (2 / 3))) = (3 / 4) |
241 | 236, 240 | eqtr3i 2646 |
. . . . . . . 8
⊢ ((2 / 3)
· (9 / 8)) = (3 / 4) |
242 | 241 | oveq1i 6660 |
. . . . . . 7
⊢ (((2 / 3)
· (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) |
243 | | 2cnd 11093 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 2 ∈ ℂ) |
244 | 225 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 3 ∈ ℂ) |
245 | 83 | nncnd 11036 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((2 · 𝑁) + 1)
∈ ℂ) |
246 | 229 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 3 ≠ 0) |
247 | 83 | nnne0d 11065 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ((2 · 𝑁) + 1)
≠ 0) |
248 | 243, 244,
245, 246, 247 | divdiv1d 10832 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((2 / 3) / ((2 · 𝑁) + 1)) = (2 / (3 · ((2 ·
𝑁) + 1)))) |
249 | 248, 208 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = ((2 / (3 · ((2
· 𝑁) + 1))) ·
(9 / (8 · (9↑𝑁))))) |
250 | 238 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (2 / 3) ∈ ℂ) |
251 | 72, 183, 199 | divcli 10767 |
. . . . . . . . . 10
⊢ (9 / 8)
∈ ℂ |
252 | 251 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (9 / 8) ∈ ℂ) |
253 | 250, 245,
252, 194, 247, 197 | divmuldivd 10842 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (((2 / 3) / ((2 · 𝑁) + 1)) · ((9 / 8) / (9↑𝑁))) = (((2 / 3) · (9 /
8)) / (((2 · 𝑁) + 1)
· (9↑𝑁)))) |
254 | 249, 253 | eqtr3d 2658 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 ·
(9↑𝑁)))) = (((2 / 3)
· (9 / 8)) / (((2 · 𝑁) + 1) · (9↑𝑁)))) |
255 | 226 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ 4 ∈ ℂ) |
256 | 255, 245,
194 | mulassd 10063 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = (4 · (((2 · 𝑁) + 1) · (9↑𝑁)))) |
257 | 256 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))) |
258 | 83, 193 | nnmulcld 11068 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ (((2 · 𝑁) +
1) · (9↑𝑁))
∈ ℕ) |
259 | 258 | nncnd 11036 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (((2 · 𝑁) +
1) · (9↑𝑁))
∈ ℂ) |
260 | 228 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ 4 ≠ 0) |
261 | 258 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (((2 · 𝑁) +
1) · (9↑𝑁))
≠ 0) |
262 | 244, 255,
259, 260, 261 | divdiv1d 10832 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁))) = (3 / (4 · (((2 · 𝑁) + 1) · (9↑𝑁))))) |
263 | 257, 262 | eqtr4d 2659 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) = ((3 / 4) / (((2 · 𝑁) + 1) · (9↑𝑁)))) |
264 | 242, 254,
263 | 3eqtr4a 2682 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ ((2 / (3 · ((2 · 𝑁) + 1))) · (9 / (8 ·
(9↑𝑁)))) = (3 / ((4
· ((2 · 𝑁) +
1)) · (9↑𝑁)))) |
265 | 218, 264 | breqtrd 4679 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ seq𝑁( + , (𝑘 ∈ ℕ0
↦ ((2 / (3 · ((2 · 𝑁) + 1))) · ((1 / 9)↑𝑘)))) ⇝ (3 / ((4 ·
((2 · 𝑁) + 1))
· (9↑𝑁)))) |
266 | 33, 46, 100, 224, 265 | isumclim 14488 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑛))) = (3 / ((4 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))) |
267 | 223, 266 | breqtrd 4679 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))) |
268 | | 4nn 11187 |
. . . . . . 7
⊢ 4 ∈
ℕ |
269 | | nnmulcl 11043 |
. . . . . . 7
⊢ ((4
∈ ℕ ∧ ((2 · 𝑁) + 1) ∈ ℕ) → (4 ·
((2 · 𝑁) + 1))
∈ ℕ) |
270 | 268, 83, 269 | sylancr 695 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (4 · ((2 · 𝑁) + 1)) ∈ ℕ) |
271 | 270, 193 | nnmulcld 11068 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) |
272 | | nndivre 11056 |
. . . . 5
⊢ ((3
∈ ℝ ∧ ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ) → (3 / ((4 ·
((2 · 𝑁) + 1))
· (9↑𝑁)))
∈ ℝ) |
273 | 126, 271,
272 | sylancr 695 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ) |
274 | | elicc2 12238 |
. . . 4
⊢ ((0
∈ ℝ ∧ (3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))) ∈ ℝ) → (Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4
· ((2 · 𝑁) +
1)) · (9↑𝑁))))
↔ (Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))))) |
275 | 155, 273,
274 | sylancr 695 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ (Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4
· ((2 · 𝑁) +
1)) · (9↑𝑁))))
↔ (Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ ∧ 0 ≤
Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∧ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ≤ (3 / ((4 · ((2
· 𝑁) + 1)) ·
(9↑𝑁)))))) |
276 | 53, 65, 267, 275 | mpbir3and 1245 |
. 2
⊢ (𝑁 ∈ ℕ0
→ Σ𝑛 ∈
(ℤ≥‘𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ (0[,](3 / ((4
· ((2 · 𝑁) +
1)) · (9↑𝑁))))) |
277 | 56, 276 | eqeltrd 2701 |
1
⊢ (𝑁 ∈ ℕ0
→ ((log‘2) − Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 ·
𝑛) + 1)) ·
(9↑𝑛)))) ∈
(0[,](3 / ((4 · ((2 · 𝑁) + 1)) · (9↑𝑁))))) |