Step | Hyp | Ref
| Expression |
1 | | nn0uz 11598 |
. . . 4
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11266 |
. . . 4
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | 1rp 11712 |
. . . . 5
⊢ 1 ∈
ℝ+ |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝜑 → 1 ∈
ℝ+) |
5 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑚) = (seq0( + , 𝐴)‘𝑚)) |
6 | | abelth.7 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐴) ⇝ 0) |
7 | 1, 2, 4, 5, 6 | climi0 14091 |
. . 3
⊢ (𝜑 → ∃𝑗 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1) |
8 | 7 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → ∃𝑗
∈ ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1) |
9 | | simprl 790 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑗 ∈ ℕ0) |
10 | | oveq2 6557 |
. . . . . 6
⊢ (𝑛 = 𝑖 → ((abs‘𝑋)↑𝑛) = ((abs‘𝑋)↑𝑖)) |
11 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛)) = (𝑛 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑛)) |
12 | | ovex 6577 |
. . . . . 6
⊢
((abs‘𝑋)↑𝑖) ∈ V |
13 | 10, 11, 12 | fvmpt 6191 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖)) |
14 | 13 | adantl 481 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖)) |
15 | | cnxmet 22386 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
16 | | 0cn 9911 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
17 | | rpxr 11716 |
. . . . . . . . 9
⊢ (1 ∈
ℝ+ → 1 ∈ ℝ*) |
18 | 3, 17 | ax-mp 5 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
19 | | blssm 22033 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (0(ball‘(abs ∘ −
))1) ⊆ ℂ) |
20 | 15, 16, 18, 19 | mp3an 1416 |
. . . . . . 7
⊢
(0(ball‘(abs ∘ − ))1) ⊆ ℂ |
21 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) |
22 | 20, 21 | sseldi 3566 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 𝑋 ∈ ℂ) |
23 | 22 | abscld 14023 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈
ℝ) |
24 | | reexpcl 12739 |
. . . . 5
⊢
(((abs‘𝑋)
∈ ℝ ∧ 𝑖
∈ ℕ0) → ((abs‘𝑋)↑𝑖) ∈ ℝ) |
25 | 23, 24 | sylan 487 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) →
((abs‘𝑋)↑𝑖) ∈
ℝ) |
26 | 14, 25 | eqeltrd 2688 |
. . 3
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))‘𝑖) ∈ ℝ) |
27 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑖)) |
28 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑘 = 𝑖 → (𝑋↑𝑘) = (𝑋↑𝑖)) |
29 | 27, 28 | oveq12d 6567 |
. . . . . 6
⊢ (𝑘 = 𝑖 → ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
30 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘))) |
31 | | ovex 6577 |
. . . . . 6
⊢ ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ V |
32 | 29, 30, 31 | fvmpt 6191 |
. . . . 5
⊢ (𝑖 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
33 | 32 | adantl 481 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
34 | | abelth.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
35 | 34 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℕ0) → (𝐴‘𝑥) ∈ ℂ) |
36 | 1, 2, 35 | serf 12691 |
. . . . . . 7
⊢ (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ) |
37 | 36 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , 𝐴):ℕ0⟶ℂ) |
38 | 37 | ffvelrnda 6267 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → (seq0( +
, 𝐴)‘𝑖) ∈
ℂ) |
39 | | expcl 12740 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ 𝑖 ∈ ℕ0)
→ (𝑋↑𝑖) ∈
ℂ) |
40 | 22, 39 | sylan 487 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → (𝑋↑𝑖) ∈ ℂ) |
41 | 38, 40 | mulcld 9939 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → ((seq0( +
, 𝐴)‘𝑖) · (𝑋↑𝑖)) ∈ ℂ) |
42 | 33, 41 | eqeltrd 2688 |
. . 3
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ ℕ0) → ((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) ∈ ℂ) |
43 | 23 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) ∈
ℂ) |
44 | | absidm 13911 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
45 | 22, 44 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) →
(abs‘(abs‘𝑋)) =
(abs‘𝑋)) |
46 | | eqid 2610 |
. . . . . . . . . 10
⊢ (abs
∘ − ) = (abs ∘ − ) |
47 | 46 | cnmetdval 22384 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑋(abs
∘ − )0) = (abs‘(𝑋 − 0))) |
48 | 22, 16, 47 | sylancl 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0))) |
49 | 22 | subid1d 10260 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 − 0) = 𝑋) |
50 | 49 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘(𝑋 − 0)) = (abs‘𝑋)) |
51 | 48, 50 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) = (abs‘𝑋)) |
52 | | elbl3 22007 |
. . . . . . . . . 10
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈
ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
53 | 15, 18, 52 | mpanl12 714 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ 𝑋
∈ ℂ) → (𝑋
∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) <
1)) |
54 | 16, 22, 53 | sylancr 694 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑋(abs ∘
− )0) < 1)) |
55 | 21, 54 | mpbid 221 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (𝑋(abs ∘ − )0) <
1) |
56 | 51, 55 | eqbrtrrd 4607 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → (abs‘𝑋) < 1) |
57 | 45, 56 | eqbrtrd 4605 |
. . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) →
(abs‘(abs‘𝑋))
< 1) |
58 | 43, 57, 14 | geolim 14440 |
. . . 4
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋)))) |
59 | | climrel 14071 |
. . . . 5
⊢ Rel
⇝ |
60 | 59 | releldmi 5283 |
. . . 4
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ ((abs‘𝑋)↑𝑛))) ⇝ (1 / (1 − (abs‘𝑋))) → seq0( + , (𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ ) |
61 | 58, 60 | syl 17 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))) ∈ dom ⇝ ) |
62 | | 1red 9934 |
. . 3
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → 1 ∈
ℝ) |
63 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → seq0( + , 𝐴):ℕ0⟶ℂ) |
64 | | eluznn0 11633 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ℕ0
∧ 𝑖 ∈
(ℤ≥‘𝑗)) → 𝑖 ∈ ℕ0) |
65 | 9, 64 | sylan 487 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → 𝑖 ∈ ℕ0) |
66 | 63, 65 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (seq0( + , 𝐴)‘𝑖) ∈ ℂ) |
67 | 65, 40 | syldan 486 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (𝑋↑𝑖) ∈ ℂ) |
68 | 66, 67 | absmuld 14041 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘((seq0( + ,
𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖)))) |
69 | 22 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → 𝑋 ∈ ℂ) |
70 | 69, 65 | absexpd 14039 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘(𝑋↑𝑖)) = ((abs‘𝑋)↑𝑖)) |
71 | 70 | oveq2d 6565 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((abs‘(seq0( + ,
𝐴)‘𝑖)) · (abs‘(𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖))) |
72 | 68, 71 | eqtrd 2644 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘((seq0( + ,
𝐴)‘𝑖) · (𝑋↑𝑖))) = ((abs‘(seq0( + , 𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖))) |
73 | 66 | abscld 14023 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘(seq0( + ,
𝐴)‘𝑖)) ∈ ℝ) |
74 | | 1red 9934 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → 1 ∈
ℝ) |
75 | 65, 25 | syldan 486 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((abs‘𝑋)↑𝑖) ∈ ℝ) |
76 | 67 | absge0d 14031 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → 0 ≤
(abs‘(𝑋↑𝑖))) |
77 | 76, 70 | breqtrd 4609 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → 0 ≤
((abs‘𝑋)↑𝑖)) |
78 | | simprr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1) |
79 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑖 → (seq0( + , 𝐴)‘𝑚) = (seq0( + , 𝐴)‘𝑖)) |
80 | 79 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑖 → (abs‘(seq0( + , 𝐴)‘𝑚)) = (abs‘(seq0( + , 𝐴)‘𝑖))) |
81 | 80 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑚 = 𝑖 → ((abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ↔ (abs‘(seq0( + , 𝐴)‘𝑖)) < 1)) |
82 | 81 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑚 ∈
(ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1 ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘(seq0( + ,
𝐴)‘𝑖)) < 1) |
83 | 78, 82 | sylan 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘(seq0( + ,
𝐴)‘𝑖)) < 1) |
84 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
85 | | ltle 10005 |
. . . . . . . 8
⊢
(((abs‘(seq0( + , 𝐴)‘𝑖)) ∈ ℝ ∧ 1 ∈ ℝ)
→ ((abs‘(seq0( + , 𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1)) |
86 | 73, 84, 85 | sylancl 693 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((abs‘(seq0( + ,
𝐴)‘𝑖)) < 1 → (abs‘(seq0( + , 𝐴)‘𝑖)) ≤ 1)) |
87 | 83, 86 | mpd 15 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘(seq0( + ,
𝐴)‘𝑖)) ≤ 1) |
88 | 73, 74, 75, 77, 87 | lemul1ad 10842 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((abs‘(seq0( + ,
𝐴)‘𝑖)) · ((abs‘𝑋)↑𝑖)) ≤ (1 · ((abs‘𝑋)↑𝑖))) |
89 | 72, 88 | eqbrtrd 4605 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘((seq0( + ,
𝐴)‘𝑖) · (𝑋↑𝑖))) ≤ (1 · ((abs‘𝑋)↑𝑖))) |
90 | 65, 32 | syl 17 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( +
, 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖) = ((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖))) |
91 | 90 | fveq2d 6107 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) = (abs‘((seq0( + , 𝐴)‘𝑖) · (𝑋↑𝑖)))) |
92 | 65, 13 | syl 17 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → ((𝑛 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑛))‘𝑖) = ((abs‘𝑋)↑𝑖)) |
93 | 92 | oveq2d 6565 |
. . . 4
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (1 · ((𝑛 ∈ ℕ0
↦ ((abs‘𝑋)↑𝑛))‘𝑖)) = (1 · ((abs‘𝑋)↑𝑖))) |
94 | 89, 91, 93 | 3brtr4d 4615 |
. . 3
⊢ ((((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) ∧ 𝑖 ∈ (ℤ≥‘𝑗)) → (abs‘((𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))‘𝑖)) ≤ (1 · ((𝑛 ∈ ℕ0 ↦
((abs‘𝑋)↑𝑛))‘𝑖))) |
95 | 1, 9, 26, 42, 61, 62, 94 | cvgcmpce 14391 |
. 2
⊢ (((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) ∧ (𝑗 ∈
ℕ0 ∧ ∀𝑚 ∈ (ℤ≥‘𝑗)(abs‘(seq0( + , 𝐴)‘𝑚)) < 1)) → seq0( + , (𝑘 ∈ ℕ0
↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |
96 | 8, 95 | rexlimddv 3017 |
1
⊢ ((𝜑 ∧ 𝑋 ∈ (0(ball‘(abs ∘ −
))1)) → seq0( + , (𝑘
∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋↑𝑘)))) ∈ dom ⇝ ) |