Proof of Theorem aaliou3lem3
Step | Hyp | Ref
| Expression |
1 | | eqid 2826 |
. . 3
⊢
(ℤ≥‘𝐴) = (ℤ≥‘𝐴) |
2 | | nnz 11728 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
3 | | uzid 11984 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
(ℤ≥‘𝐴)) |
5 | | aaliou3lem.a |
. . . 4
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑐
− 𝐴)))) |
6 | 5 | aaliou3lem1 24497 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℝ) |
7 | | aaliou3lem.b |
. . . . . 6
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) |
8 | 5, 7 | aaliou3lem2 24498 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏))) |
9 | | 0xr 10404 |
. . . . . 6
⊢ 0 ∈
ℝ* |
10 | | elioc2 12525 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐺‘𝑏) ∈ ℝ) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) |
11 | 9, 6, 10 | sylancr 583 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) |
12 | 8, 11 | mpbid 224 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏))) |
13 | 12 | simp1d 1178 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ ℝ) |
14 | | halfcn 11574 |
. . . . . 6
⊢ (1 / 2)
∈ ℂ |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (1 / 2)
∈ ℂ) |
16 | | halfre 11573 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
17 | | halfgt0 11575 |
. . . . . . . . 9
⊢ 0 < (1
/ 2) |
18 | 16, 17 | elrpii 12116 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ+ |
19 | | rprege0 12130 |
. . . . . . . 8
⊢ ((1 / 2)
∈ ℝ+ → ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 /
2))) |
20 | | absid 14414 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
21 | 18, 19, 20 | mp2b 10 |
. . . . . . 7
⊢
(abs‘(1 / 2)) = (1 / 2) |
22 | | halflt1 11577 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
23 | 21, 22 | eqbrtri 4895 |
. . . . . 6
⊢
(abs‘(1 / 2)) < 1 |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(abs‘(1 / 2)) < 1) |
25 | | 2rp 12118 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
26 | | nnnn0 11627 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
27 | | faccl 13364 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (!‘𝐴) ∈
ℕ) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) |
29 | 28 | nnzd 11810 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) |
30 | 29 | znegcld 11813 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
-(!‘𝐴) ∈
ℤ) |
31 | | rpexpcl 13174 |
. . . . . . 7
⊢ ((2
∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) →
(2↑-(!‘𝐴))
∈ ℝ+) |
32 | 25, 30, 31 | sylancr 583 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℝ+) |
33 | 32 | rpcnd 12159 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℂ) |
34 | 2, 15, 24, 33, 5 | geolim3 24494 |
. . . 4
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 /
2)))) |
35 | | seqex 13098 |
. . . . 5
⊢ seq𝐴( + , 𝐺) ∈ V |
36 | | ovex 6938 |
. . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) ∈
V |
37 | 35, 36 | breldm 5562 |
. . . 4
⊢ (seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 / 2))) →
seq𝐴( + , 𝐺) ∈ dom ⇝ ) |
38 | 34, 37 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ∈ dom ⇝ ) |
39 | 12 | simp2d 1179 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 < (𝐹‘𝑏)) |
40 | 13, 39 | elrpd 12154 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈
ℝ+) |
41 | 40 | rpge0d 12161 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 ≤ (𝐹‘𝑏)) |
42 | 12 | simp3d 1180 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) |
43 | 1, 4, 6, 13, 38, 41, 42 | cvgcmp 14923 |
. 2
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐹) ∈ dom ⇝ ) |
44 | | eqidd 2827 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) = (𝐹‘𝑏)) |
45 | 1, 1, 4, 44, 40, 43 | isumrpcl 14950 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈
ℝ+) |
46 | | eqidd 2827 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) = (𝐺‘𝑏)) |
47 | 1, 2, 44, 13, 46, 6, 42, 43, 38 | isumle 14951 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐺‘𝑏)) |
48 | 6 | recnd 10386 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℂ) |
49 | 1, 2, 46, 48, 34 | isumclim 14864 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = ((2↑-(!‘𝐴)) / (1 − (1 / 2)))) |
50 | | 1mhlfehlf 11578 |
. . . . . 6
⊢ (1
− (1 / 2)) = (1 / 2) |
51 | 50 | oveq2i 6917 |
. . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) =
((2↑-(!‘𝐴)) / (1
/ 2)) |
52 | | 2cn 11427 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
53 | | mulcl 10337 |
. . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ 2 ∈ ℂ)
→ ((2↑-(!‘𝐴)) · 2) ∈
ℂ) |
54 | 33, 52, 53 | sylancl 582 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· 2) ∈ ℂ) |
55 | 54 | div1d 11120 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(((2↑-(!‘𝐴))
· 2) / 1) = ((2↑-(!‘𝐴)) · 2)) |
56 | | 1rp 12117 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
57 | | rpcnne0 12133 |
. . . . . . . . 9
⊢ (1 ∈
ℝ+ → (1 ∈ ℂ ∧ 1 ≠ 0)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢ (1 ∈
ℂ ∧ 1 ≠ 0) |
59 | | 2cnne0 11569 |
. . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
60 | | divdiv2 11064 |
. . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ (1 ∈ ℂ
∧ 1 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
61 | 58, 59, 60 | mp3an23 1583 |
. . . . . . 7
⊢
((2↑-(!‘𝐴)) ∈ ℂ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
62 | 33, 61 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
63 | | mulcom 10339 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ (2↑-(!‘𝐴)) ∈ ℂ) → (2 ·
(2↑-(!‘𝐴))) =
((2↑-(!‘𝐴))
· 2)) |
64 | 52, 33, 63 | sylancr 583 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (2
· (2↑-(!‘𝐴))) = ((2↑-(!‘𝐴)) · 2)) |
65 | 55, 62, 64 | 3eqtr4d 2872 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (2 · (2↑-(!‘𝐴)))) |
66 | 51, 65 | syl5eq 2874 |
. . . 4
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
− (1 / 2))) = (2 · (2↑-(!‘𝐴)))) |
67 | 49, 66 | eqtrd 2862 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = (2 · (2↑-(!‘𝐴)))) |
68 | 47, 67 | breqtrd 4900 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴)))) |
69 | 43, 45, 68 | 3jca 1164 |
1
⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴))))) |