Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11266 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | 1rp 11712 |
. . . 4
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ+) |
5 | | radcnvlem2.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℂ) |
6 | | pser.g |
. . . . 5
⊢ 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑥↑𝑛)))) |
7 | 6 | pserval2 23969 |
. . . 4
⊢ ((𝑌 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ ((𝐺‘𝑌)‘𝑘) = ((𝐴‘𝑘) · (𝑌↑𝑘))) |
8 | 5, 7 | sylan 487 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑌)‘𝑘) = ((𝐴‘𝑘) · (𝑌↑𝑘))) |
9 | | fvex 6113 |
. . . . 5
⊢ (𝐺‘𝑌) ∈ V |
10 | 9 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐺‘𝑌) ∈ V) |
11 | | radcnvlem2.c |
. . . 4
⊢ (𝜑 → seq0( + , (𝐺‘𝑌)) ∈ dom ⇝ ) |
12 | | radcnv.a |
. . . . . 6
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
13 | 6, 12, 5 | psergf 23970 |
. . . . 5
⊢ (𝜑 → (𝐺‘𝑌):ℕ0⟶ℂ) |
14 | 13 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐺‘𝑌)‘𝑘) ∈ ℂ) |
15 | 1, 2, 10, 11, 14 | serf0 14259 |
. . 3
⊢ (𝜑 → (𝐺‘𝑌) ⇝ 0) |
16 | 1, 2, 4, 8, 15 | climi0 14091 |
. 2
⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1) |
17 | | simprl 790 |
. . 3
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → 𝑗 ∈ ℕ0) |
18 | | nn0re 11178 |
. . . . . . 7
⊢ (𝑖 ∈ ℕ0
→ 𝑖 ∈
ℝ) |
19 | 18 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑖 ∈ ℕ0) → 𝑖 ∈
ℝ) |
20 | | psergf.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ ℂ) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → 𝑋 ∈ ℂ) |
22 | 21 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (abs‘𝑋) ∈
ℝ) |
23 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → 𝑌 ∈ ℂ) |
24 | 23 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (abs‘𝑌) ∈
ℝ) |
25 | | 0red 9920 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℝ) |
26 | 20 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑋) ∈
ℝ) |
27 | 5 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑌) ∈
ℝ) |
28 | 20 | absge0d 14031 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (abs‘𝑋)) |
29 | | radcnvlem2.a |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘𝑋) < (abs‘𝑌)) |
30 | 25, 26, 27, 28, 29 | lelttrd 10074 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (abs‘𝑌)) |
31 | 30 | gt0ne0d 10471 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝑌) ≠ 0) |
32 | 31 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (abs‘𝑌) ≠ 0) |
33 | 22, 24, 32 | redivcld 10732 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → ((abs‘𝑋) / (abs‘𝑌)) ∈ ℝ) |
34 | | reexpcl 12739 |
. . . . . . 7
⊢
((((abs‘𝑋) /
(abs‘𝑌)) ∈
ℝ ∧ 𝑖 ∈
ℕ0) → (((abs‘𝑋) / (abs‘𝑌))↑𝑖) ∈ ℝ) |
35 | 33, 34 | sylan 487 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑖 ∈ ℕ0) →
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖) ∈
ℝ) |
36 | 19, 35 | remulcld 9949 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑖 ∈ ℕ0) → (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖)) ∈ ℝ) |
37 | | eqid 2610 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖))) = (𝑖 ∈ ℕ0 ↦ (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖))) |
38 | 36, 37 | fmptd 6292 |
. . . 4
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (𝑖 ∈ ℕ0 ↦ (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖))):ℕ0⟶ℝ) |
39 | 38 | ffvelrnda 6267 |
. . 3
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ ℕ0) → ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖)))‘𝑚) ∈ ℝ) |
40 | | nn0re 11178 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
41 | 40 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℝ) |
42 | 6, 12, 20 | psergf 23970 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺‘𝑋):ℕ0⟶ℂ) |
43 | 42 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐺‘𝑋)‘𝑚) ∈ ℂ) |
44 | 43 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(abs‘((𝐺‘𝑋)‘𝑚)) ∈ ℝ) |
45 | 41, 44 | remulcld 9949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) ∈ ℝ) |
46 | | radcnvlem1.h |
. . . . . . 7
⊢ 𝐻 = (𝑚 ∈ ℕ0 ↦ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
47 | 45, 46 | fmptd 6292 |
. . . . . 6
⊢ (𝜑 → 𝐻:ℕ0⟶ℝ) |
48 | 47 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → 𝐻:ℕ0⟶ℝ) |
49 | 48 | ffvelrnda 6267 |
. . . 4
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ ℕ0) → (𝐻‘𝑚) ∈ ℝ) |
50 | 49 | recnd 9947 |
. . 3
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ ℕ0) → (𝐻‘𝑚) ∈ ℂ) |
51 | 26, 27, 31 | redivcld 10732 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝑋) / (abs‘𝑌)) ∈ ℝ) |
52 | 51 | recnd 9947 |
. . . . 5
⊢ (𝜑 → ((abs‘𝑋) / (abs‘𝑌)) ∈ ℂ) |
53 | | divge0 10771 |
. . . . . . . 8
⊢
((((abs‘𝑋)
∈ ℝ ∧ 0 ≤ (abs‘𝑋)) ∧ ((abs‘𝑌) ∈ ℝ ∧ 0 <
(abs‘𝑌))) → 0
≤ ((abs‘𝑋) /
(abs‘𝑌))) |
54 | 26, 28, 27, 30, 53 | syl22anc 1319 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ ((abs‘𝑋) / (abs‘𝑌))) |
55 | 51, 54 | absidd 14009 |
. . . . . 6
⊢ (𝜑 →
(abs‘((abs‘𝑋) /
(abs‘𝑌))) =
((abs‘𝑋) /
(abs‘𝑌))) |
56 | 27 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝑌) ∈
ℂ) |
57 | 56 | mulid1d 9936 |
. . . . . . . 8
⊢ (𝜑 → ((abs‘𝑌) · 1) = (abs‘𝑌)) |
58 | 29, 57 | breqtrrd 4611 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝑋) < ((abs‘𝑌) · 1)) |
59 | | 1red 9934 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
60 | | ltdivmul 10777 |
. . . . . . . 8
⊢
(((abs‘𝑋)
∈ ℝ ∧ 1 ∈ ℝ ∧ ((abs‘𝑌) ∈ ℝ ∧ 0 <
(abs‘𝑌))) →
(((abs‘𝑋) /
(abs‘𝑌)) < 1
↔ (abs‘𝑋) <
((abs‘𝑌) ·
1))) |
61 | 26, 59, 27, 30, 60 | syl112anc 1322 |
. . . . . . 7
⊢ (𝜑 → (((abs‘𝑋) / (abs‘𝑌)) < 1 ↔ (abs‘𝑋) < ((abs‘𝑌) · 1))) |
62 | 58, 61 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → ((abs‘𝑋) / (abs‘𝑌)) < 1) |
63 | 55, 62 | eqbrtrd 4605 |
. . . . 5
⊢ (𝜑 →
(abs‘((abs‘𝑋) /
(abs‘𝑌))) <
1) |
64 | 37 | geomulcvg 14446 |
. . . . 5
⊢
((((abs‘𝑋) /
(abs‘𝑌)) ∈
ℂ ∧ (abs‘((abs‘𝑋) / (abs‘𝑌))) < 1) → seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖)))) ∈ dom ⇝
) |
65 | 52, 63, 64 | syl2anc 691 |
. . . 4
⊢ (𝜑 → seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖)))) ∈ dom ⇝
) |
66 | 65 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → seq0( + , (𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖)))) ∈ dom ⇝
) |
67 | | 1red 9934 |
. . 3
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → 1 ∈
ℝ) |
68 | 42 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝐺‘𝑋):ℕ0⟶ℂ) |
69 | | eluznn0 11633 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑗)) → 𝑚 ∈ ℕ0) |
70 | 17, 69 | sylan 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℕ0) |
71 | 68, 70 | ffvelrnd 6268 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝐺‘𝑋)‘𝑚) ∈ ℂ) |
72 | 71 | abscld 14023 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐺‘𝑋)‘𝑚)) ∈ ℝ) |
73 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘𝑋) / (abs‘𝑌)) ∈ ℝ) |
74 | 73, 70 | reexpcld 12887 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (((abs‘𝑋) / (abs‘𝑌))↑𝑚) ∈ ℝ) |
75 | 70 | nn0red 11229 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℝ) |
76 | 70 | nn0ge0d 11231 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 ≤ 𝑚) |
77 | 12 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝐴:ℕ0⟶ℂ) |
78 | 77, 70 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝐴‘𝑚) ∈ ℂ) |
79 | 5 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑌 ∈ ℂ) |
80 | 79, 70 | expcld 12870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑌↑𝑚) ∈ ℂ) |
81 | 78, 80 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝐴‘𝑚) · (𝑌↑𝑚)) ∈ ℂ) |
82 | 81 | abscld 14023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) ∈ ℝ) |
83 | | 1red 9934 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 1 ∈
ℝ) |
84 | 20 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑋 ∈ ℂ) |
85 | 84 | abscld 14023 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘𝑋) ∈
ℝ) |
86 | 85, 70 | reexpcld 12887 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘𝑋)↑𝑚) ∈ ℝ) |
87 | 84 | absge0d 14031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 ≤
(abs‘𝑋)) |
88 | 85, 70, 87 | expge0d 12888 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 ≤
((abs‘𝑋)↑𝑚)) |
89 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → ∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1) |
90 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝐴‘𝑘) = (𝐴‘𝑚)) |
91 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑚 → (𝑌↑𝑘) = (𝑌↑𝑚)) |
92 | 90, 91 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑚 → ((𝐴‘𝑘) · (𝑌↑𝑘)) = ((𝐴‘𝑚) · (𝑌↑𝑚))) |
93 | 92 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑚 → (abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) = (abs‘((𝐴‘𝑚) · (𝑌↑𝑚)))) |
94 | 93 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝑚 → ((abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1 ↔ (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) < 1)) |
95 | 94 | rspccva 3281 |
. . . . . . . . . . . 12
⊢
((∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1 ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) < 1) |
96 | 89, 95 | sylan 487 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) < 1) |
97 | | 1re 9918 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
98 | | ltle 10005 |
. . . . . . . . . . . 12
⊢
(((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) < 1 → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) ≤ 1)) |
99 | 82, 97, 98 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) < 1 → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) ≤ 1)) |
100 | 96, 99 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) ≤ 1) |
101 | 82, 83, 86, 88, 100 | lemul1ad 10842 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · ((abs‘𝑋)↑𝑚)) ≤ (1 · ((abs‘𝑋)↑𝑚))) |
102 | 84, 70 | expcld 12870 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑋↑𝑚) ∈ ℂ) |
103 | 78, 102 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝐴‘𝑚) · (𝑋↑𝑚)) ∈ ℂ) |
104 | 103, 80 | absmuld 14041 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝐴‘𝑚) · (𝑋↑𝑚)) · (𝑌↑𝑚))) = ((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · (abs‘(𝑌↑𝑚)))) |
105 | 81, 102 | absmuld 14041 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝐴‘𝑚) · (𝑌↑𝑚)) · (𝑋↑𝑚))) = ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · (abs‘(𝑋↑𝑚)))) |
106 | 78, 80, 102 | mul32d 10125 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (((𝐴‘𝑚) · (𝑌↑𝑚)) · (𝑋↑𝑚)) = (((𝐴‘𝑚) · (𝑋↑𝑚)) · (𝑌↑𝑚))) |
107 | 106 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝐴‘𝑚) · (𝑌↑𝑚)) · (𝑋↑𝑚))) = (abs‘(((𝐴‘𝑚) · (𝑋↑𝑚)) · (𝑌↑𝑚)))) |
108 | 84, 70 | absexpd 14039 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝑋↑𝑚)) = ((abs‘𝑋)↑𝑚)) |
109 | 108 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · (abs‘(𝑋↑𝑚))) = ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · ((abs‘𝑋)↑𝑚))) |
110 | 105, 107,
109 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(((𝐴‘𝑚) · (𝑋↑𝑚)) · (𝑌↑𝑚))) = ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · ((abs‘𝑋)↑𝑚))) |
111 | 79, 70 | absexpd 14039 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝑌↑𝑚)) = ((abs‘𝑌)↑𝑚)) |
112 | 111 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · (abs‘(𝑌↑𝑚))) = ((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · ((abs‘𝑌)↑𝑚))) |
113 | 104, 110,
112 | 3eqtr3d 2652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑌↑𝑚))) · ((abs‘𝑋)↑𝑚)) = ((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · ((abs‘𝑌)↑𝑚))) |
114 | 86 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘𝑋)↑𝑚) ∈ ℂ) |
115 | 114 | mulid2d 9937 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (1 ·
((abs‘𝑋)↑𝑚)) = ((abs‘𝑋)↑𝑚)) |
116 | 101, 113,
115 | 3brtr3d 4614 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · ((abs‘𝑌)↑𝑚)) ≤ ((abs‘𝑋)↑𝑚)) |
117 | 103 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) ∈ ℝ) |
118 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘𝑌) ∈
ℝ) |
119 | 118, 70 | reexpcld 12887 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((abs‘𝑌)↑𝑚) ∈ ℝ) |
120 | | eluzelz 11573 |
. . . . . . . . . . 11
⊢ (𝑚 ∈
(ℤ≥‘𝑗) → 𝑚 ∈ ℤ) |
121 | 120 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 𝑚 ∈ ℤ) |
122 | 30 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 <
(abs‘𝑌)) |
123 | | expgt0 12755 |
. . . . . . . . . 10
⊢
(((abs‘𝑌)
∈ ℝ ∧ 𝑚
∈ ℤ ∧ 0 < (abs‘𝑌)) → 0 < ((abs‘𝑌)↑𝑚)) |
124 | 118, 121,
122, 123 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 <
((abs‘𝑌)↑𝑚)) |
125 | | lemuldiv 10782 |
. . . . . . . . 9
⊢
(((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) ∈ ℝ ∧ ((abs‘𝑋)↑𝑚) ∈ ℝ ∧ (((abs‘𝑌)↑𝑚) ∈ ℝ ∧ 0 <
((abs‘𝑌)↑𝑚))) → (((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · ((abs‘𝑌)↑𝑚)) ≤ ((abs‘𝑋)↑𝑚) ↔ (abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) ≤ (((abs‘𝑋)↑𝑚) / ((abs‘𝑌)↑𝑚)))) |
126 | 117, 86, 119, 124, 125 | syl112anc 1322 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (((abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) · ((abs‘𝑌)↑𝑚)) ≤ ((abs‘𝑋)↑𝑚) ↔ (abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) ≤ (((abs‘𝑋)↑𝑚) / ((abs‘𝑌)↑𝑚)))) |
127 | 116, 126 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐴‘𝑚) · (𝑋↑𝑚))) ≤ (((abs‘𝑋)↑𝑚) / ((abs‘𝑌)↑𝑚))) |
128 | 6 | pserval2 23969 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 𝑚 ∈ ℕ0)
→ ((𝐺‘𝑋)‘𝑚) = ((𝐴‘𝑚) · (𝑋↑𝑚))) |
129 | 84, 70, 128 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝐺‘𝑋)‘𝑚) = ((𝐴‘𝑚) · (𝑋↑𝑚))) |
130 | 129 | fveq2d 6107 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐺‘𝑋)‘𝑚)) = (abs‘((𝐴‘𝑚) · (𝑋↑𝑚)))) |
131 | 22 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (abs‘𝑋) ∈
ℂ) |
132 | 131 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘𝑋) ∈
ℂ) |
133 | 24 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → (abs‘𝑌) ∈
ℂ) |
134 | 133 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘𝑌) ∈
ℂ) |
135 | 31 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘𝑌) ≠ 0) |
136 | 132, 134,
135, 70 | expdivd 12884 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (((abs‘𝑋) / (abs‘𝑌))↑𝑚) = (((abs‘𝑋)↑𝑚) / ((abs‘𝑌)↑𝑚))) |
137 | 127, 130,
136 | 3brtr4d 4615 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘((𝐺‘𝑋)‘𝑚)) ≤ (((abs‘𝑋) / (abs‘𝑌))↑𝑚)) |
138 | 72, 74, 75, 76, 137 | lemul2ad 10843 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) ≤ (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) |
139 | 75, 72 | remulcld 9949 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) ∈ ℝ) |
140 | 71 | absge0d 14031 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 ≤
(abs‘((𝐺‘𝑋)‘𝑚))) |
141 | 75, 72, 76, 140 | mulge0d 10483 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → 0 ≤ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
142 | 139, 141 | absidd 14009 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) = (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
143 | 75, 74 | remulcld 9949 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚)) ∈ ℝ) |
144 | 143 | recnd 9947 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚)) ∈ ℂ) |
145 | 144 | mulid2d 9937 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (1 · (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) = (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) |
146 | 138, 142,
145 | 3brtr4d 4615 |
. . . 4
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) ≤ (1 · (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚)))) |
147 | | ovex 6577 |
. . . . . 6
⊢ (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))) ∈ V |
148 | 46 | fvmpt2 6200 |
. . . . . 6
⊢ ((𝑚 ∈ ℕ0
∧ (𝑚 ·
(abs‘((𝐺‘𝑋)‘𝑚))) ∈ V) → (𝐻‘𝑚) = (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
149 | 70, 147, 148 | sylancl 693 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (𝐻‘𝑚) = (𝑚 · (abs‘((𝐺‘𝑋)‘𝑚)))) |
150 | 149 | fveq2d 6107 |
. . . 4
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝐻‘𝑚)) = (abs‘(𝑚 · (abs‘((𝐺‘𝑋)‘𝑚))))) |
151 | | id 22 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → 𝑖 = 𝑚) |
152 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑖 = 𝑚 → (((abs‘𝑋) / (abs‘𝑌))↑𝑖) = (((abs‘𝑋) / (abs‘𝑌))↑𝑚)) |
153 | 151, 152 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖)) = (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) |
154 | | ovex 6577 |
. . . . . . 7
⊢ (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚)) ∈ V |
155 | 153, 37, 154 | fvmpt 6191 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ ((𝑖 ∈
ℕ0 ↦ (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖)))‘𝑚) = (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) |
156 | 70, 155 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → ((𝑖 ∈ ℕ0 ↦ (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖)))‘𝑚) = (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚))) |
157 | 156 | oveq2d 6565 |
. . . 4
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (1 · ((𝑖 ∈ ℕ0
↦ (𝑖 ·
(((abs‘𝑋) /
(abs‘𝑌))↑𝑖)))‘𝑚)) = (1 · (𝑚 · (((abs‘𝑋) / (abs‘𝑌))↑𝑚)))) |
158 | 146, 150,
157 | 3brtr4d 4615 |
. . 3
⊢ (((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) ∧ 𝑚 ∈ (ℤ≥‘𝑗)) → (abs‘(𝐻‘𝑚)) ≤ (1 · ((𝑖 ∈ ℕ0 ↦ (𝑖 · (((abs‘𝑋) / (abs‘𝑌))↑𝑖)))‘𝑚))) |
159 | 1, 17, 39, 50, 66, 67, 158 | cvgcmpce 14391 |
. 2
⊢ ((𝜑 ∧ (𝑗 ∈ ℕ0 ∧
∀𝑘 ∈
(ℤ≥‘𝑗)(abs‘((𝐴‘𝑘) · (𝑌↑𝑘))) < 1)) → seq0( + , 𝐻) ∈ dom ⇝
) |
160 | 16, 159 | rexlimddv 3017 |
1
⊢ (𝜑 → seq0( + , 𝐻) ∈ dom ⇝
) |