Step | Hyp | Ref
| Expression |
1 | | geomulcvg.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ0 ↦ (𝑘 · (𝐴↑𝑘))) |
2 | | elnn0 11294 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℕ
∨ 𝑘 =
0)) |
3 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐴 = 0) |
4 | 3 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → (𝐴↑𝑘) = (0↑𝑘)) |
5 | | 0exp 12895 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ →
(0↑𝑘) =
0) |
6 | 4, 5 | sylan9eq 2676 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝐴↑𝑘) = 0) |
7 | 6 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · (𝐴↑𝑘)) = (𝑘 · 0)) |
8 | | nncn 11028 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
9 | 8 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈
ℂ) |
10 | 9 | mul01d 10235 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · 0) =
0) |
11 | 7, 10 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ) → (𝑘 · (𝐴↑𝑘)) = 0) |
12 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝑘 = 0) |
13 | 12 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝑘 · (𝐴↑𝑘)) = (0 · (𝐴↑𝑘))) |
14 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝐴 ∈ ℂ) |
15 | | 0nn0 11307 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℕ0 |
16 | 12, 15 | syl6eqel 2709 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → 𝑘 ∈ ℕ0) |
17 | 14, 16 | expcld 13008 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝐴↑𝑘) ∈ ℂ) |
18 | 17 | mul02d 10234 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (0 · (𝐴↑𝑘)) = 0) |
19 | 13, 18 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 = 0) → (𝑘 · (𝐴↑𝑘)) = 0) |
20 | 11, 19 | jaodan 826 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ (𝑘 ∈ ℕ ∨ 𝑘 = 0)) → (𝑘 · (𝐴↑𝑘)) = 0) |
21 | 2, 20 | sylan2b 492 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) ∧ 𝑘 ∈ ℕ0)
→ (𝑘 · (𝐴↑𝑘)) = 0) |
22 | 21 | mpteq2dva 4744 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → (𝑘 ∈ ℕ0
↦ (𝑘 · (𝐴↑𝑘))) = (𝑘 ∈ ℕ0 ↦
0)) |
23 | 1, 22 | syl5eq 2668 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐹 = (𝑘 ∈ ℕ0 ↦
0)) |
24 | | fconstmpt 5163 |
. . . . . . 7
⊢
(ℕ0 × {0}) = (𝑘 ∈ ℕ0 ↦
0) |
25 | | nn0uz 11722 |
. . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) |
26 | 25 | xpeq1i 5135 |
. . . . . . 7
⊢
(ℕ0 × {0}) = ((ℤ≥‘0)
× {0}) |
27 | 24, 26 | eqtr3i 2646 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ 0) = ((ℤ≥‘0) × {0}) |
28 | 23, 27 | syl6eq 2672 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → 𝐹 =
((ℤ≥‘0) × {0})) |
29 | 28 | seqeq3d 12809 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) = seq0( + ,
((ℤ≥‘0) × {0}))) |
30 | | 0z 11388 |
. . . . 5
⊢ 0 ∈
ℤ |
31 | | serclim0 14308 |
. . . . 5
⊢ (0 ∈
ℤ → seq0( + , ((ℤ≥‘0) × {0}))
⇝ 0) |
32 | 30, 31 | ax-mp 5 |
. . . 4
⊢ seq0( + ,
((ℤ≥‘0) × {0})) ⇝ 0 |
33 | 29, 32 | syl6eqbr 4692 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) ⇝
0) |
34 | | seqex 12803 |
. . . 4
⊢ seq0( + ,
𝐹) ∈
V |
35 | | c0ex 10034 |
. . . 4
⊢ 0 ∈
V |
36 | 34, 35 | breldm 5329 |
. . 3
⊢ (seq0( +
, 𝐹) ⇝ 0 → seq0(
+ , 𝐹) ∈ dom ⇝
) |
37 | 33, 36 | syl 17 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 = 0) → seq0( + ,
𝐹) ∈ dom ⇝
) |
38 | | 1red 10055 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → 1 ∈
ℝ) |
39 | | abscl 14018 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(abs‘𝐴) ∈
ℝ) |
40 | 39 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℝ) |
41 | | peano2re 10209 |
. . . . . . . 8
⊢
((abs‘𝐴)
∈ ℝ → ((abs‘𝐴) + 1) ∈ ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) + 1)
∈ ℝ) |
43 | 42 | rehalfcld 11279 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℝ) |
44 | 43 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(((abs‘𝐴) + 1) / 2)
∈ ℝ) |
45 | | absrpcl 14028 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (abs‘𝐴) ∈
ℝ+) |
46 | 45 | adantlr 751 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(abs‘𝐴) ∈
ℝ+) |
47 | 44, 46 | rerpdivcld 11903 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴)) ∈
ℝ) |
48 | 40 | recnd 10068 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) ∈
ℂ) |
49 | 48 | mulid2d 10058 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 · (abs‘𝐴)) = (abs‘𝐴)) |
50 | | simpr 477 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
1) |
51 | | 1re 10039 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
52 | | avglt1 11270 |
. . . . . . . . 9
⊢
(((abs‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐴) < 1 ↔ (abs‘𝐴) < (((abs‘𝐴) + 1) / 2))) |
53 | 40, 51, 52 | sylancl 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) <
1 ↔ (abs‘𝐴) <
(((abs‘𝐴) + 1) /
2))) |
54 | 50, 53 | mpbid 222 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘𝐴) <
(((abs‘𝐴) + 1) /
2)) |
55 | 49, 54 | eqbrtrd 4675 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (1 · (abs‘𝐴)) < (((abs‘𝐴) + 1) / 2)) |
56 | 55 | adantr 481 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → (1
· (abs‘𝐴))
< (((abs‘𝐴) + 1) /
2)) |
57 | 38, 44, 46 | ltmuldivd 11919 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → ((1
· (abs‘𝐴))
< (((abs‘𝐴) + 1) /
2) ↔ 1 < ((((abs‘𝐴) + 1) / 2) / (abs‘𝐴)))) |
58 | 56, 57 | mpbid 222 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → 1 <
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))) |
59 | | expmulnbnd 12996 |
. . . 4
⊢ ((1
∈ ℝ ∧ ((((abs‘𝐴) + 1) / 2) / (abs‘𝐴)) ∈ ℝ ∧ 1 <
((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))) →
∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘)) |
60 | 38, 47, 58, 59 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘)) |
61 | | eluznn0 11757 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑛)) → 𝑘 ∈ ℕ0) |
62 | | nn0cn 11302 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℂ) |
63 | 62 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℂ) |
64 | 63 | mulid2d 10058 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (1 · 𝑘) =
𝑘) |
65 | 43 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℂ) |
66 | 65 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (((abs‘𝐴) + 1)
/ 2) ∈ ℂ) |
67 | 48 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℂ) |
68 | 46 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℝ+) |
69 | 68 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ≠
0) |
70 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℕ0) |
71 | 66, 67, 69, 70 | expdivd 13022 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (((((abs‘𝐴) +
1) / 2) / (abs‘𝐴))↑𝑘) = (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘))) |
72 | 64, 71 | breq12d 4666 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((1 · 𝑘) <
(((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) |
73 | | nn0re 11301 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
74 | 73 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℝ) |
75 | | reexpcl 12877 |
. . . . . . . . . . 11
⊢
(((((abs‘𝐴) +
1) / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) →
((((abs‘𝐴) + 1) /
2)↑𝑘) ∈
ℝ) |
76 | 44, 75 | sylan 488 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((((abs‘𝐴) +
1) / 2)↑𝑘) ∈
ℝ) |
77 | 40 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(abs‘𝐴) ∈
ℝ) |
78 | | reexpcl 12877 |
. . . . . . . . . . 11
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℕ0) → ((abs‘𝐴)↑𝑘) ∈ ℝ) |
79 | 77, 78 | sylan 488 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((abs‘𝐴)↑𝑘) ∈ ℝ) |
80 | 77 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ (abs‘𝐴) ∈
ℝ) |
81 | | nn0z 11400 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℤ) |
82 | 81 | adantl 482 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 𝑘 ∈
ℤ) |
83 | 68 | rpgt0d 11875 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 0 < (abs‘𝐴)) |
84 | | expgt0 12893 |
. . . . . . . . . . 11
⊢
(((abs‘𝐴)
∈ ℝ ∧ 𝑘
∈ ℤ ∧ 0 < (abs‘𝐴)) → 0 < ((abs‘𝐴)↑𝑘)) |
85 | 80, 82, 83, 84 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ 0 < ((abs‘𝐴)↑𝑘)) |
86 | | ltmuldiv 10896 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧
((((abs‘𝐴) + 1) /
2)↑𝑘) ∈ ℝ
∧ (((abs‘𝐴)↑𝑘) ∈ ℝ ∧ 0 <
((abs‘𝐴)↑𝑘))) → ((𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) |
87 | 74, 76, 79, 85, 86 | syl112anc 1330 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((𝑘 ·
((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ 𝑘 < (((((abs‘𝐴) + 1) / 2)↑𝑘) / ((abs‘𝐴)↑𝑘)))) |
88 | 72, 87 | bitr4d 271 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑘 ∈ ℕ0)
→ ((1 · 𝑘) <
(((((abs‘𝐴) + 1) / 2)
/ (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) |
89 | 61, 88 | sylan2 491 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ (𝑛 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑛))) → ((1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) |
90 | 89 | anassrs 680 |
. . . . . 6
⊢
(((((𝐴 ∈
ℂ ∧ (abs‘𝐴)
< 1) ∧ 𝐴 ≠ 0)
∧ 𝑛 ∈
ℕ0) ∧ 𝑘 ∈ (ℤ≥‘𝑛)) → ((1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ (𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) |
91 | 90 | ralbidva 2985 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) ↔ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) |
92 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → 𝑛 ∈ ℕ0) |
93 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → ((((abs‘𝐴) + 1) / 2)↑𝑘) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
94 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘)) = (𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘)) |
95 | | ovex 6678 |
. . . . . . . . . . 11
⊢
((((abs‘𝐴) +
1) / 2)↑𝑚) ∈
V |
96 | 93, 94, 95 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
97 | 96 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
98 | 43 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) →
(((abs‘𝐴) + 1) / 2)
∈ ℝ) |
99 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) |
100 | 98, 99 | reexpcld 13025 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) →
((((abs‘𝐴) + 1) /
2)↑𝑚) ∈
ℝ) |
101 | 97, 100 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚) ∈ ℝ) |
102 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → 𝑘 = 𝑚) |
103 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑘 = 𝑚 → (𝐴↑𝑘) = (𝐴↑𝑚)) |
104 | 102, 103 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑚 → (𝑘 · (𝐴↑𝑘)) = (𝑚 · (𝐴↑𝑚))) |
105 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑚 · (𝐴↑𝑚)) ∈ V |
106 | 104, 1, 105 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) |
107 | 106 | adantl 482 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) |
108 | | nn0cn 11302 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
109 | 108 | adantl 482 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) |
110 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → 𝐴 ∈ ℂ) |
111 | | expcl 12878 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ (𝐴↑𝑚) ∈
ℂ) |
112 | 110, 111 | sylan 488 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐴↑𝑚) ∈ ℂ) |
113 | 109, 112 | mulcld 10060 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝑚 · (𝐴↑𝑚)) ∈ ℂ) |
114 | 107, 113 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ ℕ0) → (𝐹‘𝑚) ∈ ℂ) |
115 | | 0red 10041 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ∈ ℝ) |
116 | | absge0 14027 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℂ → 0 ≤
(abs‘𝐴)) |
117 | 116 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ≤ (abs‘𝐴)) |
118 | 115, 40, 43, 117, 54 | lelttrd 10195 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 < (((abs‘𝐴) + 1) / 2)) |
119 | 115, 43, 118 | ltled 10185 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ 0 ≤ (((abs‘𝐴) + 1) / 2)) |
120 | 43, 119 | absidd 14161 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(((abs‘𝐴) + 1) / 2)) = (((abs‘𝐴) + 1) / 2)) |
121 | | avglt2 11271 |
. . . . . . . . . . . . . 14
⊢
(((abs‘𝐴)
∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝐴) < 1 ↔ (((abs‘𝐴) + 1) / 2) <
1)) |
122 | 40, 51, 121 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ ((abs‘𝐴) <
1 ↔ (((abs‘𝐴) +
1) / 2) < 1)) |
123 | 50, 122 | mpbid 222 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (((abs‘𝐴) + 1)
/ 2) < 1) |
124 | 120, 123 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ (abs‘(((abs‘𝐴) + 1) / 2)) < 1) |
125 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑛 → ((((abs‘𝐴) + 1) / 2)↑𝑘) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) |
126 | | ovex 6678 |
. . . . . . . . . . . . 13
⊢
((((abs‘𝐴) +
1) / 2)↑𝑛) ∈
V |
127 | 125, 94, 126 | fvmpt 6282 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))‘𝑛) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) |
128 | 127 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑛) = ((((abs‘𝐴) + 1) / 2)↑𝑛)) |
129 | 65, 124, 128 | geolim 14601 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ⇝ (1 / (1 −
(((abs‘𝐴) + 1) /
2)))) |
130 | | seqex 12803 |
. . . . . . . . . . 11
⊢ seq0( + ,
(𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ V |
131 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (1 / (1
− (((abs‘𝐴) +
1) / 2))) ∈ V |
132 | 130, 131 | breldm 5329 |
. . . . . . . . . 10
⊢ (seq0( +
, (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ⇝ (1 / (1 −
(((abs‘𝐴) + 1) / 2)))
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ dom ⇝ ) |
133 | 129, 132 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , (𝑘 ∈
ℕ0 ↦ ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∈ dom ⇝ ) |
134 | 133 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → seq0( + , (𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))) ∈ dom
⇝ ) |
135 | | 1red 10055 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → 1 ∈ ℝ) |
136 | | eluznn0 11757 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑛)) → 𝑚 ∈ ℕ0) |
137 | 92, 136 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℕ0) |
138 | 137 | nn0red 11352 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℝ) |
139 | | simplll 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐴 ∈ ℂ) |
140 | 139 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘𝐴) ∈
ℝ) |
141 | 140, 137 | reexpcld 13025 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((abs‘𝐴)↑𝑚) ∈ ℝ) |
142 | 138, 141 | remulcld 10070 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) ∈ ℝ) |
143 | 137, 100 | syldan 487 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((abs‘𝐴) + 1) / 2)↑𝑚) ∈
ℝ) |
144 | | simprr 796 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘)) |
145 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((abs‘𝐴)↑𝑘) = ((abs‘𝐴)↑𝑚)) |
146 | 102, 145 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (𝑘 · ((abs‘𝐴)↑𝑘)) = (𝑚 · ((abs‘𝐴)↑𝑚))) |
147 | 146, 93 | breq12d 4666 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ↔ (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚))) |
148 | 147 | rspccva 3308 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
149 | 144, 148 | sylan 488 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) < ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
150 | 142, 143,
149 | ltled 10185 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑚 · ((abs‘𝐴)↑𝑚)) ≤ ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
151 | 137 | nn0cnd 11353 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ ℂ) |
152 | 139, 137 | expcld 13008 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐴↑𝑚) ∈ ℂ) |
153 | 151, 152 | absmuld 14193 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) = ((abs‘𝑚) · (abs‘(𝐴↑𝑚)))) |
154 | 137 | nn0ge0d 11354 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 0 ≤ 𝑚) |
155 | 138, 154 | absidd 14161 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘𝑚) = 𝑚) |
156 | 139, 137 | absexpd 14191 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐴↑𝑚)) = ((abs‘𝐴)↑𝑚)) |
157 | 155, 156 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((abs‘𝑚) · (abs‘(𝐴↑𝑚))) = (𝑚 · ((abs‘𝐴)↑𝑚))) |
158 | 153, 157 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) = (𝑚 · ((abs‘𝐴)↑𝑚))) |
159 | 143 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((((abs‘𝐴) + 1) / 2)↑𝑚) ∈
ℂ) |
160 | 159 | mulid2d 10058 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (1 ·
((((abs‘𝐴) + 1) /
2)↑𝑚)) =
((((abs‘𝐴) + 1) /
2)↑𝑚)) |
161 | 150, 158,
160 | 3brtr4d 4685 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝑚 · (𝐴↑𝑚))) ≤ (1 · ((((abs‘𝐴) + 1) / 2)↑𝑚))) |
162 | 137, 106 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝐹‘𝑚) = (𝑚 · (𝐴↑𝑚))) |
163 | 162 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑚)) = (abs‘(𝑚 · (𝐴↑𝑚)))) |
164 | 137, 96 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑚) = ((((abs‘𝐴) + 1) / 2)↑𝑚)) |
165 | 164 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (1 · ((𝑘 ∈ ℕ0
↦ ((((abs‘𝐴) +
1) / 2)↑𝑘))‘𝑚)) = (1 · ((((abs‘𝐴) + 1) / 2)↑𝑚))) |
166 | 161, 163,
165 | 3brtr4d 4685 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (abs‘(𝐹‘𝑚)) ≤ (1 · ((𝑘 ∈ ℕ0 ↦
((((abs‘𝐴) + 1) /
2)↑𝑘))‘𝑚))) |
167 | 25, 92, 101, 114, 134, 135, 166 | cvgcmpce 14550 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
(𝑛 ∈
ℕ0 ∧ ∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘))) → seq0( + , 𝐹) ∈ dom ⇝ ) |
168 | 167 | expr 643 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝑛 ∈
ℕ0) → (∀𝑘 ∈ (ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) |
169 | 168 | adantlr 751 |
. . . . 5
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(𝑘 · ((abs‘𝐴)↑𝑘)) < ((((abs‘𝐴) + 1) / 2)↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) |
170 | 91, 169 | sylbid 230 |
. . . 4
⊢ ((((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) ∧ 𝑛 ∈ ℕ0)
→ (∀𝑘 ∈
(ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) |
171 | 170 | rexlimdva 3031 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) →
(∃𝑛 ∈
ℕ0 ∀𝑘 ∈ (ℤ≥‘𝑛)(1 · 𝑘) < (((((abs‘𝐴) + 1) / 2) / (abs‘𝐴))↑𝑘) → seq0( + , 𝐹) ∈ dom ⇝ )) |
172 | 60, 171 | mpd 15 |
. 2
⊢ (((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1) ∧
𝐴 ≠ 0) → seq0( + ,
𝐹) ∈ dom ⇝
) |
173 | 37, 172 | pm2.61dane 2881 |
1
⊢ ((𝐴 ∈ ℂ ∧
(abs‘𝐴) < 1)
→ seq0( + , 𝐹) ∈
dom ⇝ ) |