MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelthlem7 Structured version   Visualization version   GIF version

Theorem abelthlem7 25011
Description: Lemma for abelth 25014. (Contributed by Mario Carneiro, 2-Apr-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
abelth.7 (𝜑 → seq0( + , 𝐴) ⇝ 0)
abelthlem6.1 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
abelthlem7.2 (𝜑𝑅 ∈ ℝ+)
abelthlem7.3 (𝜑𝑁 ∈ ℕ0)
abelthlem7.4 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
abelthlem7.5 (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
Assertion
Ref Expression
abelthlem7 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Distinct variable groups:   𝑘,𝑛,𝑥,𝑧,𝑀   𝑅,𝑘,𝑛,𝑥,𝑧   𝑘,𝑋,𝑛,𝑥,𝑧   𝐴,𝑘,𝑛,𝑥,𝑧   𝑘,𝑁,𝑛   𝜑,𝑘,𝑛,𝑥   𝑆,𝑘,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑘,𝑛)   𝑁(𝑥,𝑧)

Proof of Theorem abelthlem7
StepHypRef Expression
1 abelth.1 . . . . 5 (𝜑𝐴:ℕ0⟶ℂ)
2 abelth.2 . . . . 5 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
3 abelth.3 . . . . 5 (𝜑𝑀 ∈ ℝ)
4 abelth.4 . . . . 5 (𝜑 → 0 ≤ 𝑀)
5 abelth.5 . . . . 5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
6 abelth.6 . . . . 5 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
71, 2, 3, 4, 5, 6abelthlem4 25007 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
8 abelthlem6.1 . . . . 5 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
98eldifad 3922 . . . 4 (𝜑𝑋𝑆)
107, 9ffvelrnd 6825 . . 3 (𝜑 → (𝐹𝑋) ∈ ℂ)
1110abscld 14775 . 2 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
12 ax-1cn 10572 . . . . . 6 1 ∈ ℂ
13 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 25010 . . . . . . 7 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
1514simpld 498 . . . . . 6 (𝜑𝑋 ∈ ℂ)
16 subcl 10862 . . . . . 6 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
1712, 15, 16sylancr 590 . . . . 5 (𝜑 → (1 − 𝑋) ∈ ℂ)
18 fzfid 13324 . . . . . 6 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19 elfznn0 12983 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
20 nn0uz 12258 . . . . . . . . . 10 0 = (ℤ‘0)
21 0zd 11971 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
221ffvelrnda 6824 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2320, 21, 22serf 13382 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
2423ffvelrnda 6824 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25 expcl 13431 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2615, 25sylan 583 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2724, 26mulcld 10638 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2819, 27sylan2 595 . . . . . 6 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2918, 28fsumcl 15069 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
3017, 29mulcld 10638 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
3130abscld 14775 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
32 eqid 2821 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
33 abelthlem7.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
3433nn0zd 12063 . . . . . 6 (𝜑𝑁 ∈ ℤ)
35 eluznn0 12295 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
3633, 35sylan 583 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
37 fveq2 6643 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38 oveq2 7138 . . . . . . . . 9 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
3937, 38oveq12d 7148 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
40 eqid 2821 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
41 ovex 7163 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
4239, 40, 41fvmpt 6741 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4336, 42syl 17 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4436, 27syldan 594 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
451, 2, 3, 4, 5abelthlem2 25005 . . . . . . . . . 10 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4645simprd 499 . . . . . . . . 9 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4746, 8sseldd 3944 . . . . . . . 8 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
481, 2, 3, 4, 5, 6, 13abelthlem5 25008 . . . . . . . 8 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4947, 48mpdan 686 . . . . . . 7 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5042adantl 485 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
5150, 27eqeltrd 2912 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
5220, 33, 51iserex 14992 . . . . . . 7 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ))
5349, 52mpbid 235 . . . . . 6 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5432, 34, 43, 44, 53isumcl 15095 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
5517, 54mulcld 10638 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
5655abscld 14775 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
5731, 56readdcld 10647 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ∈ ℝ)
58 peano2re 10790 . . . 4 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
593, 58syl 17 . . 3 (𝜑 → (𝑀 + 1) ∈ ℝ)
60 abelthlem7.2 . . . 4 (𝜑𝑅 ∈ ℝ+)
6160rpred 12409 . . 3 (𝜑𝑅 ∈ ℝ)
6259, 61remulcld 10648 . 2 (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 25009 . . . . 5 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6420, 32, 33, 50, 27, 49isumsplit 15174 . . . . . 6 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6564oveq2d 7146 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6617, 29, 54adddid 10642 . . . . 5 (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6763, 65, 663eqtrd 2860 . . . 4 (𝜑 → (𝐹𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6867fveq2d 6647 . . 3 (𝜑 → (abs‘(𝐹𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
6930, 55abstrid 14795 . . 3 (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
7068, 69eqbrtrd 5061 . 2 (𝜑 → (abs‘(𝐹𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
713, 61remulcld 10648 . . . 4 (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
7217abscld 14775 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
7324abscld 14775 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7419, 73sylan2 595 . . . . . . . 8 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7518, 74fsumrecl 15070 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76 peano2re 10790 . . . . . . 7 𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7775, 76syl 17 . . . . . 6 (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7872, 77remulcld 10648 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
7917, 29absmuld 14793 . . . . . 6 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
8029abscld 14775 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8117absge0d 14783 . . . . . . 7 (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
8227abscld 14775 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8319, 82sylan2 595 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8418, 83fsumrecl 15070 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8518, 28fsumabs 15135 . . . . . . . . . 10 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
8615abscld 14775 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑋) ∈ ℝ)
87 reexpcl 13430 . . . . . . . . . . . . . . 15 (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
8886, 87sylan 583 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89 1red 10619 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 1 ∈ ℝ)
9024absge0d 14783 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
9186adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ∈ ℝ)
9215absge0d 14783 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝑋))
9392adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘𝑋))
94 0cn 10610 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℂ
95 eqid 2821 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) = (abs ∘ − )
9695cnmetdval 23354 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9715, 94, 96sylancl 589 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9815subid1d 10963 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋 − 0) = 𝑋)
9998fveq2d 6647 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
10097, 99eqtrd 2856 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101 cnxmet 23356 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) ∈ (∞Met‘ℂ)
102 1xr 10677 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
103 elbl3 22977 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
104101, 102, 103mpanl12 701 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10594, 15, 104sylancr 590 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10647, 105mpbid 235 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) < 1)
107100, 106eqbrtrrd 5063 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝑋) < 1)
108 1re 10618 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
109 ltle 10706 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
11086, 108, 109sylancl 589 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
111107, 110mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝑋) ≤ 1)
112111adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ≤ 1)
113 simpr 488 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
114 exple1 13524 . . . . . . . . . . . . . . 15 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11591, 93, 112, 113, 114syl31anc 1370 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11688, 89, 73, 90, 115lemul2ad 11557 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
11724, 26absmuld 14793 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))))
118 absexp 14643 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
11915, 118sylan 583 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
120119oveq2d 7146 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
121117, 120eqtr2d 2857 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
12273recnd 10646 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
123122mulid1d 10635 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
124116, 121, 1233brtr3d 5070 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12519, 124sylan2 595 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12618, 83, 74, 125fsumle 15133 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12780, 84, 75, 85, 126letrd 10774 . . . . . . . . 9 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12875ltp1d 11547 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
12980, 75, 77, 127, 128lelttrd 10775 . . . . . . . 8 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13080, 77, 129ltled 10765 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13180, 77, 72, 81, 130lemul2ad 11557 . . . . . 6 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
13279, 131eqbrtrd 5061 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
133 abelthlem7.5 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
134 0red 10621 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
13519, 90sylan2 595 . . . . . . . . 9 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
13618, 74, 135fsumge0 15129 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
137134, 75, 77, 136, 128lelttrd 10775 . . . . . . 7 (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
138 ltmuldiv 11490 . . . . . . 7 (((abs‘(1 − 𝑋)) ∈ ℝ ∧ 𝑅 ∈ ℝ ∧ ((Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ ∧ 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))) → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
13972, 61, 77, 137, 138syl112anc 1371 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
140133, 139mpbird 260 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅)
14131, 78, 61, 132, 140lelttrd 10775 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) < 𝑅)
14217, 54absmuld 14793 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
14354abscld 14775 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
14439fveq2d 6647 . . . . . . . . . 10 (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
145 eqid 2821 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
146 fvex 6656 . . . . . . . . . 10 (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ V
147144, 145, 146fvmpt 6741 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
14836, 147syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
14944abscld 14775 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
150 uzid 12236 . . . . . . . . . 10 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
15134, 150syl 17 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑁))
152 oveq2 7138 . . . . . . . . . . . 12 (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
153 eqid 2821 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))
154 ovex 7163 . . . . . . . . . . . 12 ((abs‘𝑋)↑𝑛) ∈ V
155152, 153, 154fvmpt 6741 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15636, 155syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15736, 88syldan 594 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
158156, 157eqeltrd 2912 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
159149recnd 10646 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
160148, 159eqeltrd 2912 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) ∈ ℂ)
16186recnd 10646 . . . . . . . . . . 11 (𝜑 → (abs‘𝑋) ∈ ℂ)
162 absidm 14662 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
16315, 162syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
164163, 107eqbrtrd 5061 . . . . . . . . . . 11 (𝜑 → (abs‘(abs‘𝑋)) < 1)
165161, 164, 33, 156geolim2 15206 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
166 seqex 13354 . . . . . . . . . . 11 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ V
167 ovex 7163 . . . . . . . . . . 11 (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
168166, 167breldm 5750 . . . . . . . . . 10 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
169165, 168syl 17 . . . . . . . . 9 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
170117, 120eqtrd 2856 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17136, 170syldan 594 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17236, 73syldan 594 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
17361adantr 484 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑅 ∈ ℝ)
17486adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘𝑋) ∈ ℝ)
17592adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ (abs‘𝑋))
176174, 36, 175expge0d 13512 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
177 abelthlem7.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
17837fveq2d 6647 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
179178breq1d 5049 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
180179rspccva 3599 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
181177, 180sylan 583 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
182172, 173, 181ltled 10765 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
183172, 173, 157, 176, 182lemul1ad 11556 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
184171, 183eqbrtrd 5061 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
185148fveq2d 6647 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
186 absidm 14662 . . . . . . . . . . . 12 (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
18744, 186syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
188185, 187eqtrd 2856 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
189156oveq2d 7146 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
190184, 188, 1893brtr4d 5071 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
19132, 151, 158, 160, 169, 61, 190cvgcmpce 15152 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ∈ dom ⇝ )
19232, 34, 148, 149, 191isumrecl 15099 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
193 eldifsni 4695 . . . . . . . . . . . 12 (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
1948, 193syl 17 . . . . . . . . . . 11 (𝜑𝑋 ≠ 1)
195194necomd 3062 . . . . . . . . . 10 (𝜑 → 1 ≠ 𝑋)
196 subeq0 10889 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
197196necon3bid 3051 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
19812, 15, 197sylancr 590 . . . . . . . . . 10 (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
199195, 198mpbird 260 . . . . . . . . 9 (𝜑 → (1 − 𝑋) ≠ 0)
20017, 199absrpcld 14787 . . . . . . . 8 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ+)
20171, 200rerpdivcld 12440 . . . . . . 7 (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
20232, 34, 43, 44, 53isumclim2 15092 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
20332, 34, 148, 159, 191isumclim2 15092 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20436, 51syldan 594 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
20543fveq2d 6647 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
206148, 205eqtr4d 2859 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)))
20732, 202, 203, 34, 204, 206iserabs 15149 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20886, 33reexpcld 13511 . . . . . . . . . 10 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
209 difrp 12405 . . . . . . . . . . . 12 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
21086, 108, 209sylancl 589 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
211107, 210mpbid 235 . . . . . . . . . 10 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ+)
212208, 211rerpdivcld 12440 . . . . . . . . 9 (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
21361, 212remulcld 10648 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
214152oveq2d 7146 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
215 eqid 2821 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
216 ovex 7163 . . . . . . . . . . . 12 (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
217214, 215, 216fvmpt 6741 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
21836, 217syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
219173, 157remulcld 10648 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
22060rpcnd 12411 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
221158recnd 10646 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
222218, 189eqtr4d 2859 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
22332, 34, 220, 165, 221, 222isermulc2 14993 . . . . . . . . . . 11 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
224 seqex 13354 . . . . . . . . . . . 12 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
225 ovex 7163 . . . . . . . . . . . 12 (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
226224, 225breldm 5750 . . . . . . . . . . 11 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
227223, 226syl 17 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
22832, 34, 148, 149, 218, 219, 184, 191, 227isumle 15178 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
229219recnd 10646 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
23032, 34, 218, 229, 223isumclim 15091 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
231228, 230breqtrd 5065 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
23260, 211rpdivcld 12426 . . . . . . . . . 10 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ+)
233232rpred 12409 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
234208recnd 10646 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
235211rpcnd 12411 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
236211rpne0d 12414 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
237220, 234, 235, 236div12d 11429 . . . . . . . . . 10 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
238 1red 10619 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
239232rpge0d 12413 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
240 exple1 13524 . . . . . . . . . . . . 13 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((abs‘𝑋)↑𝑁) ≤ 1)
24186, 92, 111, 33, 240syl31anc 1370 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
242208, 238, 233, 239, 241lemul1ad 11556 . . . . . . . . . . 11 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
243232rpcnd 12411 . . . . . . . . . . . 12 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
244243mulid2d 10636 . . . . . . . . . . 11 (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
245242, 244breqtrd 5065 . . . . . . . . . 10 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
246237, 245eqbrtrd 5061 . . . . . . . . 9 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
24714simprd 499 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
248 resubcl 10927 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
249108, 86, 248sylancr 590 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
2503, 249remulcld 10648 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
25172, 250, 60lemul2d 12453 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
252247, 251mpbid 235 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
2533recnd 10646 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℂ)
254220, 253, 235mul12d 10826 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
255220, 235mulcomd 10639 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
256255oveq2d 7146 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
257253, 235, 220mul12d 10826 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
258254, 256, 2573eqtrd 2860 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
259252, 258breqtrd 5065 . . . . . . . . . . . 12 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260249, 71remulcld 10648 . . . . . . . . . . . . 13 (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
26161, 260, 200lemuldivd 12458 . . . . . . . . . . . 12 (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
262259, 261mpbid 235 . . . . . . . . . . 11 (𝜑𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
26371recnd 10646 . . . . . . . . . . . 12 (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
26472recnd 10646 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
265200rpne0d 12414 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
266235, 263, 264, 265divassd 11428 . . . . . . . . . . 11 (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
267262, 266breqtrd 5065 . . . . . . . . . 10 (𝜑𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
268 posdif 11110 . . . . . . . . . . . . 13 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
26986, 108, 268sylancl 589 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
270107, 269mpbid 235 . . . . . . . . . . 11 (𝜑 → 0 < (1 − (abs‘𝑋)))
271 ledivmul 11493 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
27261, 201, 249, 270, 271syl112anc 1371 . . . . . . . . . 10 (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
273267, 272mpbird 260 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
274213, 233, 201, 246, 273letrd 10774 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
275192, 213, 201, 231, 274letrd 10774 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276143, 192, 201, 207, 275letrd 10774 . . . . . 6 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277143, 71, 200lemuldiv2d 12459 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
278276, 277mpbird 260 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
279142, 278eqbrtrd 5061 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
28031, 56, 61, 71, 141, 279ltleaddd 11238 . . 3 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
281 1cnd 10613 . . . . 5 (𝜑 → 1 ∈ ℂ)
282253, 281, 220adddird 10643 . . . 4 (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
283220mulid2d 10636 . . . . 5 (𝜑 → (1 · 𝑅) = 𝑅)
284283oveq2d 7146 . . . 4 (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
285263, 220addcomd 10819 . . . 4 (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
286282, 284, 2853eqtrd 2860 . . 3 (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
287280, 286breqtrrd 5067 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < ((𝑀 + 1) · 𝑅))
28811, 57, 62, 70, 287lelttrd 10775 1 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3007  wral 3126  {crab 3130  cdif 3907  wss 3910  {csn 4540   class class class wbr 5039  cmpt 5119  dom cdm 5528  ccom 5532  wf 6324  cfv 6328  (class class class)co 7130  cc 10512  cr 10513  0cc0 10514  1c1 10515   + caddc 10517   · cmul 10519  *cxr 10651   < clt 10652  cle 10653  cmin 10847   / cdiv 11274  0cn0 11875  cz 11959  cuz 12221  +crp 12367  ...cfz 12875  seqcseq 13352  cexp 13413  abscabs 14572  cli 14820  Σcsu 15021  ∞Metcxmet 20505  ballcbl 20507
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-rep 5163  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-inf2 9080  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592  ax-addf 10593  ax-mulf 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-int 4850  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-se 5488  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-1st 7664  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-1o 8077  df-oadd 8081  df-er 8264  df-map 8383  df-pm 8384  df-en 8485  df-dom 8486  df-sdom 8487  df-fin 8488  df-sup 8882  df-inf 8883  df-oi 8950  df-card 9344  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-n0 11876  df-z 11960  df-uz 12222  df-rp 12368  df-xadd 12486  df-ico 12722  df-icc 12723  df-fz 12876  df-fzo 13017  df-fl 13145  df-seq 13353  df-exp 13414  df-hash 13675  df-shft 14405  df-cj 14437  df-re 14438  df-im 14439  df-sqrt 14573  df-abs 14574  df-limsup 14807  df-clim 14824  df-rlim 14825  df-sum 15022  df-psmet 20512  df-xmet 20513  df-met 20514  df-bl 20515
This theorem is referenced by:  abelthlem8  25012
  Copyright terms: Public domain W3C validator