Proof of Theorem aaliou3lem3
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . 3
⊢
(ℤ≥‘𝐴) = (ℤ≥‘𝐴) |
2 | | nnz 11276 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) |
3 | | uzid 11578 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
(ℤ≥‘𝐴)) |
5 | | aaliou3lem.a |
. . . 4
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑐
− 𝐴)))) |
6 | 5 | aaliou3lem1 23901 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℝ) |
7 | | aaliou3lem.b |
. . . . . 6
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) |
8 | 5, 7 | aaliou3lem2 23902 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏))) |
9 | | 0xr 9965 |
. . . . . 6
⊢ 0 ∈
ℝ* |
10 | | elioc2 12107 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐺‘𝑏) ∈ ℝ) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) |
11 | 9, 6, 10 | sylancr 694 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) |
12 | 8, 11 | mpbid 221 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏))) |
13 | 12 | simp1d 1066 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ ℝ) |
14 | | halfcn 11124 |
. . . . . 6
⊢ (1 / 2)
∈ ℂ |
15 | 14 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (1 / 2)
∈ ℂ) |
16 | | halfre 11123 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
17 | | halfgt0 11125 |
. . . . . . . . 9
⊢ 0 < (1
/ 2) |
18 | 16, 17 | elrpii 11711 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ+ |
19 | | rprege0 11723 |
. . . . . . . 8
⊢ ((1 / 2)
∈ ℝ+ → ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 /
2))) |
20 | | absid 13884 |
. . . . . . . 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 11127 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
23 | 21, 22 | eqbrtri 4604 |
. . . . . 6
⊢
(abs‘(1 / 2)) < 1 |
24 | 23 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(abs‘(1 / 2)) < 1) |
25 | | 2rp 11713 |
. . . . . . 7
⊢ 2 ∈
ℝ+ |
26 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) |
27 | | faccl 12932 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0
→ (!‘𝐴) ∈
ℕ) |
28 | 26, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) |
29 | 28 | nnzd 11357 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) |
30 | 29 | znegcld 11360 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
-(!‘𝐴) ∈
ℤ) |
31 | | rpexpcl 12741 |
. . . . . . 7
⊢ ((2
∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) →
(2↑-(!‘𝐴))
∈ ℝ+) |
32 | 25, 30, 31 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℝ+) |
33 | 32 | rpcnd 11750 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℂ) |
34 | 2, 15, 24, 33, 5 | geolim3 23898 |
. . . 4
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 /
2)))) |
35 | | seqex 12665 |
. . . . 5
⊢ seq𝐴( + , 𝐺) ∈ V |
36 | | ovex 6577 |
. . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) ∈
V |
37 | 35, 36 | breldm 5251 |
. . . 4
⊢ (seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 / 2))) →
seq𝐴( + , 𝐺) ∈ dom ⇝ ) |
38 | 34, 37 | syl 17 |
. . 3
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ∈ dom ⇝ ) |
39 | 12 | simp2d 1067 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 < (𝐹‘𝑏)) |
40 | 13, 39 | elrpd 11745 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈
ℝ+) |
41 | 40 | rpge0d 11752 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 ≤ (𝐹‘𝑏)) |
42 | 12 | simp3d 1068 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) |
43 | 1, 4, 6, 13, 38, 41, 42 | cvgcmp 14389 |
. 2
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐹) ∈ dom ⇝ ) |
44 | | eqidd 2611 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) = (𝐹‘𝑏)) |
45 | 1, 1, 4, 44, 40, 43 | isumrpcl 14414 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈
ℝ+) |
46 | | eqidd 2611 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) = (𝐺‘𝑏)) |
47 | 1, 2, 44, 13, 46, 6, 42, 43, 38 | isumle 14415 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐺‘𝑏)) |
48 | 6 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℂ) |
49 | 1, 2, 46, 48, 34 | isumclim 14330 |
. . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = ((2↑-(!‘𝐴)) / (1 − (1 / 2)))) |
50 | | 1mhlfehlf 11128 |
. . . . . 6
⊢ (1
− (1 / 2)) = (1 / 2) |
51 | 50 | oveq2i 6560 |
. . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) =
((2↑-(!‘𝐴)) / (1
/ 2)) |
52 | | 2cn 10968 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
53 | | mulcl 9899 |
. . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ 2 ∈ ℂ)
→ ((2↑-(!‘𝐴)) · 2) ∈
ℂ) |
54 | 33, 52, 53 | sylancl 693 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· 2) ∈ ℂ) |
55 | 54 | div1d 10672 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(((2↑-(!‘𝐴))
· 2) / 1) = ((2↑-(!‘𝐴)) · 2)) |
56 | | 1rp 11712 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
57 | | rpcnne0 11726 |
. . . . . . . . 9
⊢ (1 ∈
ℝ+ → (1 ∈ ℂ ∧ 1 ≠ 0)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢ (1 ∈
ℂ ∧ 1 ≠ 0) |
59 | | 2cnne0 11119 |
. . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
60 | | divdiv2 10616 |
. . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ (1 ∈ ℂ
∧ 1 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
61 | 58, 59, 60 | mp3an23 1408 |
. . . . . . 7
⊢
((2↑-(!‘𝐴)) ∈ ℂ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
62 | 33, 61 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) |
63 | | mulcom 9901 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ (2↑-(!‘𝐴)) ∈ ℂ) → (2 ·
(2↑-(!‘𝐴))) =
((2↑-(!‘𝐴))
· 2)) |
64 | 52, 33, 63 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (2
· (2↑-(!‘𝐴))) = ((2↑-(!‘𝐴)) · 2)) |
65 | 55, 62, 64 | 3eqtr4d 2654 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (2 · (2↑-(!‘𝐴)))) |
66 | 51, 65 | syl5eq 2656 |
. . . 4
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
− (1 / 2))) = (2 · (2↑-(!‘𝐴)))) |
67 | 49, 66 | eqtrd 2644 |
. . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = (2 · (2↑-(!‘𝐴)))) |
68 | 47, 67 | breqtrd 4609 |
. 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴)))) |
69 | 43, 45, 68 | 3jca 1235 |
1
⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴))))) |