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

Theorem abelthlem7 25797
Description: Lemma for abelth 25800. (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 25793 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
8 abelthlem6.1 . . . . 5 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
98eldifad 3922 . . . 4 (𝜑𝑋𝑆)
107, 9ffvelcdmd 7036 . . 3 (𝜑 → (𝐹𝑋) ∈ ℂ)
1110abscld 15321 . 2 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
12 ax-1cn 11109 . . . . . 6 1 ∈ ℂ
13 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 25796 . . . . . . 7 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
1514simpld 495 . . . . . 6 (𝜑𝑋 ∈ ℂ)
16 subcl 11400 . . . . . 6 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
1712, 15, 16sylancr 587 . . . . 5 (𝜑 → (1 − 𝑋) ∈ ℂ)
18 fzfid 13878 . . . . . 6 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19 elfznn0 13534 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
20 nn0uz 12805 . . . . . . . . . 10 0 = (ℤ‘0)
21 0zd 12511 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
221ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2320, 21, 22serf 13936 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
2423ffvelcdmda 7035 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25 expcl 13985 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2615, 25sylan 580 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2724, 26mulcld 11175 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2819, 27sylan2 593 . . . . . 6 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2918, 28fsumcl 15618 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
3017, 29mulcld 11175 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
3130abscld 15321 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
32 eqid 2736 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
33 abelthlem7.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
3433nn0zd 12525 . . . . . 6 (𝜑𝑁 ∈ ℤ)
35 eluznn0 12842 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
3633, 35sylan 580 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
37 fveq2 6842 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38 oveq2 7365 . . . . . . . . 9 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
3937, 38oveq12d 7375 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
40 eqid 2736 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
41 ovex 7390 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
4239, 40, 41fvmpt 6948 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4336, 42syl 17 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4436, 27syldan 591 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
451, 2, 3, 4, 5abelthlem2 25791 . . . . . . . . . 10 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4645simprd 496 . . . . . . . . 9 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4746, 8sseldd 3945 . . . . . . . 8 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
481, 2, 3, 4, 5, 6, 13abelthlem5 25794 . . . . . . . 8 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4947, 48mpdan 685 . . . . . . 7 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5042adantl 482 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
5150, 27eqeltrd 2838 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
5220, 33, 51iserex 15541 . . . . . . 7 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ))
5349, 52mpbid 231 . . . . . 6 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5432, 34, 43, 44, 53isumcl 15646 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
5517, 54mulcld 11175 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
5655abscld 15321 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
5731, 56readdcld 11184 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ∈ ℝ)
58 peano2re 11328 . . . 4 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
593, 58syl 17 . . 3 (𝜑 → (𝑀 + 1) ∈ ℝ)
60 abelthlem7.2 . . . 4 (𝜑𝑅 ∈ ℝ+)
6160rpred 12957 . . 3 (𝜑𝑅 ∈ ℝ)
6259, 61remulcld 11185 . 2 (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 25795 . . . . 5 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6420, 32, 33, 50, 27, 49isumsplit 15725 . . . . . 6 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6564oveq2d 7373 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6617, 29, 54adddid 11179 . . . . 5 (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6763, 65, 663eqtrd 2780 . . . 4 (𝜑 → (𝐹𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6867fveq2d 6846 . . 3 (𝜑 → (abs‘(𝐹𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
6930, 55abstrid 15341 . . 3 (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
7068, 69eqbrtrd 5127 . 2 (𝜑 → (abs‘(𝐹𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
713, 61remulcld 11185 . . . 4 (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
7217abscld 15321 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
7324abscld 15321 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7419, 73sylan2 593 . . . . . . . 8 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7518, 74fsumrecl 15619 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76 peano2re 11328 . . . . . . 7 𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7775, 76syl 17 . . . . . 6 (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7872, 77remulcld 11185 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
7917, 29absmuld 15339 . . . . . 6 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
8029abscld 15321 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8117absge0d 15329 . . . . . . 7 (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
8227abscld 15321 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8319, 82sylan2 593 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8418, 83fsumrecl 15619 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8518, 28fsumabs 15686 . . . . . . . . . 10 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
8615abscld 15321 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑋) ∈ ℝ)
87 reexpcl 13984 . . . . . . . . . . . . . . 15 (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
8886, 87sylan 580 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89 1red 11156 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 1 ∈ ℝ)
9024absge0d 15329 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
9186adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ∈ ℝ)
9215absge0d 15329 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝑋))
9392adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘𝑋))
94 0cn 11147 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℂ
95 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) = (abs ∘ − )
9695cnmetdval 24134 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9715, 94, 96sylancl 586 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9815subid1d 11501 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋 − 0) = 𝑋)
9998fveq2d 6846 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
10097, 99eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101 cnxmet 24136 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) ∈ (∞Met‘ℂ)
102 1xr 11214 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
103 elbl3 23745 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
104101, 102, 103mpanl12 700 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10594, 15, 104sylancr 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10647, 105mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) < 1)
107100, 106eqbrtrrd 5129 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝑋) < 1)
108 1re 11155 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
109 ltle 11243 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
11086, 108, 109sylancl 586 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
111107, 110mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝑋) ≤ 1)
112111adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ≤ 1)
113 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
114 exple1 14081 . . . . . . . . . . . . . . 15 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11591, 93, 112, 113, 114syl31anc 1373 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11688, 89, 73, 90, 115lemul2ad 12095 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
11724, 26absmuld 15339 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))))
118 absexp 15189 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
11915, 118sylan 580 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
120119oveq2d 7373 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
121117, 120eqtr2d 2777 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
12273recnd 11183 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
123122mulid1d 11172 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
124116, 121, 1233brtr3d 5136 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12519, 124sylan2 593 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12618, 83, 74, 125fsumle 15684 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12780, 84, 75, 85, 126letrd 11312 . . . . . . . . 9 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12875ltp1d 12085 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
12980, 75, 77, 127, 128lelttrd 11313 . . . . . . . 8 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13080, 77, 129ltled 11303 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13180, 77, 72, 81, 130lemul2ad 12095 . . . . . 6 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
13279, 131eqbrtrd 5127 . . . . 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 11158 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
13519, 90sylan2 593 . . . . . . . . 9 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
13618, 74, 135fsumge0 15680 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
137134, 75, 77, 136, 128lelttrd 11313 . . . . . . 7 (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
138 ltmuldiv 12028 . . . . . . 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 1374 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
140133, 139mpbird 256 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅)
14131, 78, 61, 132, 140lelttrd 11313 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) < 𝑅)
14217, 54absmuld 15339 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
14354abscld 15321 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
14439fveq2d 6846 . . . . . . . . . 10 (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
145 eqid 2736 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
146 fvex 6855 . . . . . . . . . 10 (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ V
147144, 145, 146fvmpt 6948 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
14836, 147syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
14944abscld 15321 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
150 uzid 12778 . . . . . . . . . 10 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
15134, 150syl 17 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑁))
152 oveq2 7365 . . . . . . . . . . . 12 (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
153 eqid 2736 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))
154 ovex 7390 . . . . . . . . . . . 12 ((abs‘𝑋)↑𝑛) ∈ V
155152, 153, 154fvmpt 6948 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15636, 155syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15736, 88syldan 591 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
158156, 157eqeltrd 2838 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
159149recnd 11183 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
160148, 159eqeltrd 2838 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) ∈ ℂ)
16186recnd 11183 . . . . . . . . . . 11 (𝜑 → (abs‘𝑋) ∈ ℂ)
162 absidm 15208 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
16315, 162syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
164163, 107eqbrtrd 5127 . . . . . . . . . . 11 (𝜑 → (abs‘(abs‘𝑋)) < 1)
165161, 164, 33, 156geolim2 15756 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
166 seqex 13908 . . . . . . . . . . 11 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ V
167 ovex 7390 . . . . . . . . . . 11 (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
168166, 167breldm 5864 . . . . . . . . . 10 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
169165, 168syl 17 . . . . . . . . 9 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
170117, 120eqtrd 2776 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17136, 170syldan 591 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17236, 73syldan 591 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
17361adantr 481 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑅 ∈ ℝ)
17486adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘𝑋) ∈ ℝ)
17592adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ (abs‘𝑋))
176174, 36, 175expge0d 14069 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
177 abelthlem7.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
17837fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
179178breq1d 5115 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
180179rspccva 3580 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
181177, 180sylan 580 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
182172, 173, 181ltled 11303 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
183172, 173, 157, 176, 182lemul1ad 12094 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
184171, 183eqbrtrd 5127 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
185148fveq2d 6846 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
186 absidm 15208 . . . . . . . . . . . 12 (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
18744, 186syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
188185, 187eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
189156oveq2d 7373 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
190184, 188, 1893brtr4d 5137 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
19132, 151, 158, 160, 169, 61, 190cvgcmpce 15703 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ∈ dom ⇝ )
19232, 34, 148, 149, 191isumrecl 15650 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
193 eldifsni 4750 . . . . . . . . . . . 12 (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
1948, 193syl 17 . . . . . . . . . . 11 (𝜑𝑋 ≠ 1)
195194necomd 2999 . . . . . . . . . 10 (𝜑 → 1 ≠ 𝑋)
196 subeq0 11427 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
197196necon3bid 2988 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
19812, 15, 197sylancr 587 . . . . . . . . . 10 (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
199195, 198mpbird 256 . . . . . . . . 9 (𝜑 → (1 − 𝑋) ≠ 0)
20017, 199absrpcld 15333 . . . . . . . 8 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ+)
20171, 200rerpdivcld 12988 . . . . . . 7 (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
20232, 34, 43, 44, 53isumclim2 15643 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
20332, 34, 148, 159, 191isumclim2 15643 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20436, 51syldan 591 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
20543fveq2d 6846 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
206148, 205eqtr4d 2779 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)))
20732, 202, 203, 34, 204, 206iserabs 15700 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20886, 33reexpcld 14068 . . . . . . . . . 10 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
209 difrp 12953 . . . . . . . . . . . 12 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
21086, 108, 209sylancl 586 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
211107, 210mpbid 231 . . . . . . . . . 10 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ+)
212208, 211rerpdivcld 12988 . . . . . . . . 9 (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
21361, 212remulcld 11185 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
214152oveq2d 7373 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
215 eqid 2736 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
216 ovex 7390 . . . . . . . . . . . 12 (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
217214, 215, 216fvmpt 6948 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
21836, 217syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
219173, 157remulcld 11185 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
22060rpcnd 12959 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
221158recnd 11183 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
222218, 189eqtr4d 2779 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
22332, 34, 220, 165, 221, 222isermulc2 15542 . . . . . . . . . . 11 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
224 seqex 13908 . . . . . . . . . . . 12 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
225 ovex 7390 . . . . . . . . . . . 12 (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
226224, 225breldm 5864 . . . . . . . . . . 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 15729 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
229219recnd 11183 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
23032, 34, 218, 229, 223isumclim 15642 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
231228, 230breqtrd 5131 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
23260, 211rpdivcld 12974 . . . . . . . . . 10 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ+)
233232rpred 12957 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
234208recnd 11183 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
235211rpcnd 12959 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
236211rpne0d 12962 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
237220, 234, 235, 236div12d 11967 . . . . . . . . . 10 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
238 1red 11156 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
239232rpge0d 12961 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
240 exple1 14081 . . . . . . . . . . . . 13 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((abs‘𝑋)↑𝑁) ≤ 1)
24186, 92, 111, 33, 240syl31anc 1373 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
242208, 238, 233, 239, 241lemul1ad 12094 . . . . . . . . . . 11 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
243232rpcnd 12959 . . . . . . . . . . . 12 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
244243mulid2d 11173 . . . . . . . . . . 11 (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
245242, 244breqtrd 5131 . . . . . . . . . 10 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
246237, 245eqbrtrd 5127 . . . . . . . . 9 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
24714simprd 496 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
248 resubcl 11465 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
249108, 86, 248sylancr 587 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
2503, 249remulcld 11185 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
25172, 250, 60lemul2d 13001 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
252247, 251mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
2533recnd 11183 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℂ)
254220, 253, 235mul12d 11364 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
255220, 235mulcomd 11176 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
256255oveq2d 7373 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
257253, 235, 220mul12d 11364 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
258254, 256, 2573eqtrd 2780 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
259252, 258breqtrd 5131 . . . . . . . . . . . 12 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260249, 71remulcld 11185 . . . . . . . . . . . . 13 (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
26161, 260, 200lemuldivd 13006 . . . . . . . . . . . 12 (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
262259, 261mpbid 231 . . . . . . . . . . 11 (𝜑𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
26371recnd 11183 . . . . . . . . . . . 12 (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
26472recnd 11183 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
265200rpne0d 12962 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
266235, 263, 264, 265divassd 11966 . . . . . . . . . . 11 (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
267262, 266breqtrd 5131 . . . . . . . . . 10 (𝜑𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
268 posdif 11648 . . . . . . . . . . . . 13 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
26986, 108, 268sylancl 586 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
270107, 269mpbid 231 . . . . . . . . . . 11 (𝜑 → 0 < (1 − (abs‘𝑋)))
271 ledivmul 12031 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
27261, 201, 249, 270, 271syl112anc 1374 . . . . . . . . . 10 (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
273267, 272mpbird 256 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
274213, 233, 201, 246, 273letrd 11312 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
275192, 213, 201, 231, 274letrd 11312 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276143, 192, 201, 207, 275letrd 11312 . . . . . 6 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277143, 71, 200lemuldiv2d 13007 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
278276, 277mpbird 256 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
279142, 278eqbrtrd 5127 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
28031, 56, 61, 71, 141, 279ltleaddd 11776 . . 3 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
281 1cnd 11150 . . . . 5 (𝜑 → 1 ∈ ℂ)
282253, 281, 220adddird 11180 . . . 4 (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
283220mulid2d 11173 . . . . 5 (𝜑 → (1 · 𝑅) = 𝑅)
284283oveq2d 7373 . . . 4 (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
285263, 220addcomd 11357 . . . 4 (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
286282, 284, 2853eqtrd 2780 . . 3 (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
287280, 286breqtrrd 5133 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < ((𝑀 + 1) · 𝑅))
28811, 57, 62, 70, 287lelttrd 11313 1 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  {crab 3407  cdif 3907  wss 3910  {csn 4586   class class class wbr 5105  cmpt 5188  dom cdm 5633  ccom 5637  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  0cn0 12413  cz 12499  cuz 12763  +crp 12915  ...cfz 13424  seqcseq 13906  cexp 13967  abscabs 15119  cli 15366  Σcsu 15570  ∞Metcxmet 20781  ballcbl 20783
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-xadd 13034  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791
This theorem is referenced by:  abelthlem8  25798
  Copyright terms: Public domain W3C validator