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

Theorem abelthlem7 24237
Description: Lemma for abelth 24240. (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 24233 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
8 abelthlem6.1 . . . . 5 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
98eldifad 3619 . . . 4 (𝜑𝑋𝑆)
107, 9ffvelrnd 6400 . . 3 (𝜑 → (𝐹𝑋) ∈ ℂ)
1110abscld 14219 . 2 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
12 ax-1cn 10032 . . . . . 6 1 ∈ ℂ
13 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 24236 . . . . . . 7 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
1514simpld 474 . . . . . 6 (𝜑𝑋 ∈ ℂ)
16 subcl 10318 . . . . . 6 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
1712, 15, 16sylancr 696 . . . . 5 (𝜑 → (1 − 𝑋) ∈ ℂ)
18 fzfid 12812 . . . . . 6 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19 elfznn0 12471 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
20 nn0uz 11760 . . . . . . . . . 10 0 = (ℤ‘0)
21 0zd 11427 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
221ffvelrnda 6399 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2320, 21, 22serf 12869 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
2423ffvelrnda 6399 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25 expcl 12918 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2615, 25sylan 487 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2724, 26mulcld 10098 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2819, 27sylan2 490 . . . . . 6 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2918, 28fsumcl 14508 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
3017, 29mulcld 10098 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
3130abscld 14219 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
32 eqid 2651 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
33 abelthlem7.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
3433nn0zd 11518 . . . . . 6 (𝜑𝑁 ∈ ℤ)
35 eluznn0 11795 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
3633, 35sylan 487 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
37 fveq2 6229 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38 oveq2 6698 . . . . . . . . 9 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
3937, 38oveq12d 6708 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
40 eqid 2651 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
41 ovex 6718 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
4239, 40, 41fvmpt 6321 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4336, 42syl 17 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4436, 27syldan 486 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
451, 2, 3, 4, 5abelthlem2 24231 . . . . . . . . . 10 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4645simprd 478 . . . . . . . . 9 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4746, 8sseldd 3637 . . . . . . . 8 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
481, 2, 3, 4, 5, 6, 13abelthlem5 24234 . . . . . . . 8 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4947, 48mpdan 703 . . . . . . 7 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5042adantl 481 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
5150, 27eqeltrd 2730 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
5220, 33, 51iserex 14431 . . . . . . 7 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ))
5349, 52mpbid 222 . . . . . 6 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5432, 34, 43, 44, 53isumcl 14536 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
5517, 54mulcld 10098 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
5655abscld 14219 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
5731, 56readdcld 10107 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ∈ ℝ)
58 peano2re 10247 . . . 4 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
593, 58syl 17 . . 3 (𝜑 → (𝑀 + 1) ∈ ℝ)
60 abelthlem7.2 . . . 4 (𝜑𝑅 ∈ ℝ+)
6160rpred 11910 . . 3 (𝜑𝑅 ∈ ℝ)
6259, 61remulcld 10108 . 2 (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 24235 . . . . 5 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6420, 32, 33, 50, 27, 49isumsplit 14616 . . . . . 6 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6564oveq2d 6706 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6617, 29, 54adddid 10102 . . . . 5 (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6763, 65, 663eqtrd 2689 . . . 4 (𝜑 → (𝐹𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6867fveq2d 6233 . . 3 (𝜑 → (abs‘(𝐹𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
6930, 55abstrid 14239 . . 3 (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
7068, 69eqbrtrd 4707 . 2 (𝜑 → (abs‘(𝐹𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
713, 61remulcld 10108 . . . 4 (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
7217abscld 14219 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
7324abscld 14219 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7419, 73sylan2 490 . . . . . . . 8 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7518, 74fsumrecl 14509 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76 peano2re 10247 . . . . . . 7 𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7775, 76syl 17 . . . . . 6 (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7872, 77remulcld 10108 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
7917, 29absmuld 14237 . . . . . 6 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
8029abscld 14219 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8117absge0d 14227 . . . . . . 7 (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
8227abscld 14219 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8319, 82sylan2 490 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8418, 83fsumrecl 14509 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8518, 28fsumabs 14577 . . . . . . . . . 10 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
8615abscld 14219 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑋) ∈ ℝ)
87 reexpcl 12917 . . . . . . . . . . . . . . 15 (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
8886, 87sylan 487 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89 1red 10093 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 1 ∈ ℝ)
9024absge0d 14227 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
9186adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ∈ ℝ)
9215absge0d 14227 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝑋))
9392adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘𝑋))
94 0cn 10070 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℂ
95 eqid 2651 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) = (abs ∘ − )
9695cnmetdval 22621 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9715, 94, 96sylancl 695 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9815subid1d 10419 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋 − 0) = 𝑋)
9998fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
10097, 99eqtrd 2685 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101 cnxmet 22623 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) ∈ (∞Met‘ℂ)
102 1rp 11874 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
103 rpxr 11878 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℝ+ → 1 ∈ ℝ*)
104102, 103ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
105 elbl3 22244 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
106101, 104, 105mpanl12 718 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10794, 15, 106sylancr 696 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10847, 107mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) < 1)
109100, 108eqbrtrrd 4709 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝑋) < 1)
110 1re 10077 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
111 ltle 10164 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
11286, 110, 111sylancl 695 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
113109, 112mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝑋) ≤ 1)
114113adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ≤ 1)
115 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
116 exple1 12960 . . . . . . . . . . . . . . 15 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11791, 93, 114, 115, 116syl31anc 1369 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11888, 89, 73, 90, 117lemul2ad 11002 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
11924, 26absmuld 14237 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))))
120 absexp 14088 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
12115, 120sylan 487 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
122121oveq2d 6706 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
123119, 122eqtr2d 2686 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
12473recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
125124mulid1d 10095 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
126118, 123, 1253brtr3d 4716 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12719, 126sylan2 490 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12818, 83, 74, 127fsumle 14575 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12980, 84, 75, 85, 128letrd 10232 . . . . . . . . 9 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
13075ltp1d 10992 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13180, 75, 77, 129, 130lelttrd 10233 . . . . . . . 8 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13280, 77, 131ltled 10223 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13380, 77, 72, 81, 132lemul2ad 11002 . . . . . 6 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
13479, 133eqbrtrd 4707 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
135 abelthlem7.5 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
136 0red 10079 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
13719, 90sylan2 490 . . . . . . . . 9 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
13818, 74, 137fsumge0 14571 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
139136, 75, 77, 138, 130lelttrd 10233 . . . . . . 7 (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
140 ltmuldiv 10934 . . . . . . 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))))
14172, 61, 77, 139, 140syl112anc 1370 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅 ↔ (abs‘(1 − 𝑋)) < (𝑅 / (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))))
142135, 141mpbird 247 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) < 𝑅)
14331, 78, 61, 134, 142lelttrd 10233 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) < 𝑅)
14417, 54absmuld 14237 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
14554abscld 14219 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
14639fveq2d 6233 . . . . . . . . . 10 (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
147 eqid 2651 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
148 fvex 6239 . . . . . . . . . 10 (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ V
149146, 147, 148fvmpt 6321 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15036, 149syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15144abscld 14219 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
152 uzid 11740 . . . . . . . . . 10 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
15334, 152syl 17 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑁))
154 oveq2 6698 . . . . . . . . . . . 12 (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
155 eqid 2651 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))
156 ovex 6718 . . . . . . . . . . . 12 ((abs‘𝑋)↑𝑛) ∈ V
157154, 155, 156fvmpt 6321 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15836, 157syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15936, 88syldan 486 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
160158, 159eqeltrd 2730 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
161151recnd 10106 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
162150, 161eqeltrd 2730 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) ∈ ℂ)
16386recnd 10106 . . . . . . . . . . 11 (𝜑 → (abs‘𝑋) ∈ ℂ)
164 absidm 14107 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
16515, 164syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
166165, 109eqbrtrd 4707 . . . . . . . . . . 11 (𝜑 → (abs‘(abs‘𝑋)) < 1)
167163, 166, 33, 158geolim2 14646 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
168 seqex 12843 . . . . . . . . . . 11 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ V
169 ovex 6718 . . . . . . . . . . 11 (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
170168, 169breldm 5361 . . . . . . . . . 10 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
171167, 170syl 17 . . . . . . . . 9 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
172119, 122eqtrd 2685 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17336, 172syldan 486 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17436, 73syldan 486 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
17561adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑅 ∈ ℝ)
17686adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘𝑋) ∈ ℝ)
17792adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ (abs‘𝑋))
178176, 36, 177expge0d 13066 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
179 abelthlem7.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
18037fveq2d 6233 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
181180breq1d 4695 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
182181rspccva 3339 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
183179, 182sylan 487 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
184174, 175, 183ltled 10223 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
185174, 175, 159, 178, 184lemul1ad 11001 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
186173, 185eqbrtrd 4707 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
187150fveq2d 6233 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
188 absidm 14107 . . . . . . . . . . . 12 (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
18944, 188syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
190187, 189eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
191158oveq2d 6706 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
192186, 190, 1913brtr4d 4717 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
19332, 153, 160, 162, 171, 61, 192cvgcmpce 14594 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ∈ dom ⇝ )
19432, 34, 150, 151, 193isumrecl 14540 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
195 eldifsni 4353 . . . . . . . . . . . 12 (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
1968, 195syl 17 . . . . . . . . . . 11 (𝜑𝑋 ≠ 1)
197196necomd 2878 . . . . . . . . . 10 (𝜑 → 1 ≠ 𝑋)
198 subeq0 10345 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
199198necon3bid 2867 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
20012, 15, 199sylancr 696 . . . . . . . . . 10 (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
201197, 200mpbird 247 . . . . . . . . 9 (𝜑 → (1 − 𝑋) ≠ 0)
20217, 201absrpcld 14231 . . . . . . . 8 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ+)
20371, 202rerpdivcld 11941 . . . . . . 7 (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
20432, 34, 43, 44, 53isumclim2 14533 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
20532, 34, 150, 161, 193isumclim2 14533 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20636, 51syldan 486 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
20743fveq2d 6233 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
208150, 207eqtr4d 2688 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)))
20932, 204, 205, 34, 206, 208iserabs 14591 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
21086, 33reexpcld 13065 . . . . . . . . . 10 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
211 difrp 11906 . . . . . . . . . . . 12 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
21286, 110, 211sylancl 695 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
213109, 212mpbid 222 . . . . . . . . . 10 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ+)
214210, 213rerpdivcld 11941 . . . . . . . . 9 (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
21561, 214remulcld 10108 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
216154oveq2d 6706 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
217 eqid 2651 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
218 ovex 6718 . . . . . . . . . . . 12 (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
219216, 217, 218fvmpt 6321 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
22036, 219syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
221175, 159remulcld 10108 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
22260rpcnd 11912 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
223160recnd 10106 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
224220, 191eqtr4d 2688 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
22532, 34, 222, 167, 223, 224isermulc2 14432 . . . . . . . . . . 11 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
226 seqex 12843 . . . . . . . . . . . 12 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
227 ovex 6718 . . . . . . . . . . . 12 (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
228226, 227breldm 5361 . . . . . . . . . . 11 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
229225, 228syl 17 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ dom ⇝ )
23032, 34, 150, 151, 220, 221, 186, 193, 229isumle 14620 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
231221recnd 10106 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
23232, 34, 220, 231, 225isumclim 14532 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
233230, 232breqtrd 4711 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
23460, 213rpdivcld 11927 . . . . . . . . . 10 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ+)
235234rpred 11910 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
236210recnd 10106 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
237213rpcnd 11912 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
238213rpne0d 11915 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
239222, 236, 237, 238div12d 10875 . . . . . . . . . 10 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
240 1red 10093 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
241234rpge0d 11914 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
242 exple1 12960 . . . . . . . . . . . . 13 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((abs‘𝑋)↑𝑁) ≤ 1)
24386, 92, 113, 33, 242syl31anc 1369 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
244210, 240, 235, 241, 243lemul1ad 11001 . . . . . . . . . . 11 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
245234rpcnd 11912 . . . . . . . . . . . 12 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
246245mulid2d 10096 . . . . . . . . . . 11 (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
247244, 246breqtrd 4711 . . . . . . . . . 10 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
248239, 247eqbrtrd 4707 . . . . . . . . 9 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
24914simprd 478 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
250 resubcl 10383 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
251110, 86, 250sylancr 696 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
2523, 251remulcld 10108 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
25372, 252, 60lemul2d 11954 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
254249, 253mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
2553recnd 10106 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℂ)
256222, 255, 237mul12d 10283 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
257222, 237mulcomd 10099 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
258257oveq2d 6706 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
259255, 237, 222mul12d 10283 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260256, 258, 2593eqtrd 2689 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
261254, 260breqtrd 4711 . . . . . . . . . . . 12 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
262251, 71remulcld 10108 . . . . . . . . . . . . 13 (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
26361, 262, 202lemuldivd 11959 . . . . . . . . . . . 12 (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
264261, 263mpbid 222 . . . . . . . . . . 11 (𝜑𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
26571recnd 10106 . . . . . . . . . . . 12 (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
26672recnd 10106 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
267202rpne0d 11915 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
268237, 265, 266, 267divassd 10874 . . . . . . . . . . 11 (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
269264, 268breqtrd 4711 . . . . . . . . . 10 (𝜑𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
270 posdif 10559 . . . . . . . . . . . . 13 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
27186, 110, 270sylancl 695 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
272109, 271mpbid 222 . . . . . . . . . . 11 (𝜑 → 0 < (1 − (abs‘𝑋)))
273 ledivmul 10937 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
27461, 203, 251, 272, 273syl112anc 1370 . . . . . . . . . 10 (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
275269, 274mpbird 247 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276215, 235, 203, 248, 275letrd 10232 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277194, 215, 203, 233, 276letrd 10232 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
278145, 194, 203, 209, 277letrd 10232 . . . . . 6 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
279145, 71, 202lemuldiv2d 11960 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
280278, 279mpbird 247 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
281144, 280eqbrtrd 4707 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
28231, 56, 61, 71, 143, 281ltleaddd 10686 . . 3 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
283 1cnd 10094 . . . . 5 (𝜑 → 1 ∈ ℂ)
284255, 283, 222adddird 10103 . . . 4 (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
285222mulid2d 10096 . . . . 5 (𝜑 → (1 · 𝑅) = 𝑅)
286285oveq2d 6706 . . . 4 (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
287265, 222addcomd 10276 . . . 4 (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
288284, 286, 2873eqtrd 2689 . . 3 (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
289282, 288breqtrrd 4713 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < ((𝑀 + 1) · 𝑅))
29011, 57, 62, 70, 289lelttrd 10233 1 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wne 2823  wral 2941  {crab 2945  cdif 3604  wss 3607  {csn 4210   class class class wbr 4685  cmpt 4762  dom cdm 5143  ccom 5147  wf 5922  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  *cxr 10111   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  0cn0 11330  cz 11415  cuz 11725  +crp 11870  ...cfz 12364  seqcseq 12841  cexp 12900  abscabs 14018  cli 14259  Σcsu 14460  ∞Metcxmt 19779  ballcbl 19781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-xadd 11985  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789
This theorem is referenced by:  abelthlem8  24238
  Copyright terms: Public domain W3C validator