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

Theorem abelthlem7 24383
Description: Lemma for abelth 24386. (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 24379 . . . 4 (𝜑𝐹:𝑆⟶ℂ)
8 abelthlem6.1 . . . . 5 (𝜑𝑋 ∈ (𝑆 ∖ {1}))
98eldifad 3719 . . . 4 (𝜑𝑋𝑆)
107, 9ffvelrnd 6515 . . 3 (𝜑 → (𝐹𝑋) ∈ ℂ)
1110abscld 14366 . 2 (𝜑 → (abs‘(𝐹𝑋)) ∈ ℝ)
12 ax-1cn 10178 . . . . . 6 1 ∈ ℂ
13 abelth.7 . . . . . . . 8 (𝜑 → seq0( + , 𝐴) ⇝ 0)
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 24382 . . . . . . 7 (𝜑 → (𝑋 ∈ ℂ ∧ (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋)))))
1514simpld 477 . . . . . 6 (𝜑𝑋 ∈ ℂ)
16 subcl 10464 . . . . . 6 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (1 − 𝑋) ∈ ℂ)
1712, 15, 16sylancr 698 . . . . 5 (𝜑 → (1 − 𝑋) ∈ ℂ)
18 fzfid 12958 . . . . . 6 (𝜑 → (0...(𝑁 − 1)) ∈ Fin)
19 elfznn0 12618 . . . . . . 7 (𝑛 ∈ (0...(𝑁 − 1)) → 𝑛 ∈ ℕ0)
20 nn0uz 11907 . . . . . . . . . 10 0 = (ℤ‘0)
21 0zd 11573 . . . . . . . . . 10 (𝜑 → 0 ∈ ℤ)
221ffvelrnda 6514 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ0) → (𝐴𝑛) ∈ ℂ)
2320, 21, 22serf 13015 . . . . . . . . 9 (𝜑 → seq0( + , 𝐴):ℕ0⟶ℂ)
2423ffvelrnda 6514 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (seq0( + , 𝐴)‘𝑛) ∈ ℂ)
25 expcl 13064 . . . . . . . . 9 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2615, 25sylan 489 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (𝑋𝑛) ∈ ℂ)
2724, 26mulcld 10244 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2819, 27sylan2 492 . . . . . 6 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
2918, 28fsumcl 14655 . . . . 5 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
3017, 29mulcld 10244 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
3130abscld 14366 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
32 eqid 2752 . . . . . 6 (ℤ𝑁) = (ℤ𝑁)
33 abelthlem7.3 . . . . . . 7 (𝜑𝑁 ∈ ℕ0)
3433nn0zd 11664 . . . . . 6 (𝜑𝑁 ∈ ℤ)
35 eluznn0 11942 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
3633, 35sylan 489 . . . . . . 7 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑛 ∈ ℕ0)
37 fveq2 6344 . . . . . . . . 9 (𝑘 = 𝑛 → (seq0( + , 𝐴)‘𝑘) = (seq0( + , 𝐴)‘𝑛))
38 oveq2 6813 . . . . . . . . 9 (𝑘 = 𝑛 → (𝑋𝑘) = (𝑋𝑛))
3937, 38oveq12d 6823 . . . . . . . 8 (𝑘 = 𝑛 → ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
40 eqid 2752 . . . . . . . 8 (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))
41 ovex 6833 . . . . . . . 8 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ V
4239, 40, 41fvmpt 6436 . . . . . . 7 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4336, 42syl 17 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
4436, 27syldan 488 . . . . . 6 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
451, 2, 3, 4, 5abelthlem2 24377 . . . . . . . . . 10 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
4645simprd 482 . . . . . . . . 9 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
4746, 8sseldd 3737 . . . . . . . 8 (𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1))
481, 2, 3, 4, 5, 6, 13abelthlem5 24380 . . . . . . . 8 ((𝜑𝑋 ∈ (0(ball‘(abs ∘ − ))1)) → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
4947, 48mpdan 705 . . . . . . 7 (𝜑 → seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5042adantl 473 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) = ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
5150, 27eqeltrd 2831 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
5220, 33, 51iserex 14578 . . . . . . 7 (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ↔ seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ ))
5349, 52mpbid 222 . . . . . 6 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ∈ dom ⇝ )
5432, 34, 43, 44, 53isumcl 14683 . . . . 5 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ)
5517, 54mulcld 10244 . . . 4 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
5655abscld 14366 . . 3 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ∈ ℝ)
5731, 56readdcld 10253 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ∈ ℝ)
58 peano2re 10393 . . . 4 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
593, 58syl 17 . . 3 (𝜑 → (𝑀 + 1) ∈ ℝ)
60 abelthlem7.2 . . . 4 (𝜑𝑅 ∈ ℝ+)
6160rpred 12057 . . 3 (𝜑𝑅 ∈ ℝ)
6259, 61remulcld 10254 . 2 (𝜑 → ((𝑀 + 1) · 𝑅) ∈ ℝ)
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 24381 . . . . 5 (𝜑 → (𝐹𝑋) = ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6420, 32, 33, 50, 27, 49isumsplit 14763 . . . . . 6 (𝜑 → Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) = (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
6564oveq2d 6821 . . . . 5 (𝜑 → ((1 − 𝑋) · Σ𝑛 ∈ ℕ0 ((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6617, 29, 54adddid 10248 . . . . 5 (𝜑 → ((1 − 𝑋) · (Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) + Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6763, 65, 663eqtrd 2790 . . . 4 (𝜑 → (𝐹𝑋) = (((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
6867fveq2d 6348 . . 3 (𝜑 → (abs‘(𝐹𝑋)) = (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
6930, 55abstrid 14386 . . 3 (𝜑 → (abs‘(((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) + ((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
7068, 69eqbrtrd 4818 . 2 (𝜑 → (abs‘(𝐹𝑋)) ≤ ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))))
713, 61remulcld 10254 . . . 4 (𝜑 → (𝑀 · 𝑅) ∈ ℝ)
7217abscld 14366 . . . . . 6 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ)
7324abscld 14366 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7419, 73sylan2 492 . . . . . . . 8 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
7518, 74fsumrecl 14656 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
76 peano2re 10393 . . . . . . 7 𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7775, 76syl 17 . . . . . 6 (𝜑 → (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1) ∈ ℝ)
7872, 77remulcld 10254 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)) ∈ ℝ)
7917, 29absmuld 14384 . . . . . 6 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
8029abscld 14366 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8117absge0d 14374 . . . . . . 7 (𝜑 → 0 ≤ (abs‘(1 − 𝑋)))
8227abscld 14366 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8319, 82sylan2 492 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8418, 83fsumrecl 14656 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
8518, 28fsumabs 14724 . . . . . . . . . 10 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
8615abscld 14366 . . . . . . . . . . . . . . 15 (𝜑 → (abs‘𝑋) ∈ ℝ)
87 reexpcl 13063 . . . . . . . . . . . . . . 15 (((abs‘𝑋) ∈ ℝ ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
8886, 87sylan 489 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
89 1red 10239 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 1 ∈ ℝ)
9024absge0d 14374 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
9186adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ∈ ℝ)
9215absge0d 14374 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (abs‘𝑋))
9392adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 0 ≤ (abs‘𝑋))
94 0cn 10216 . . . . . . . . . . . . . . . . . . . 20 0 ∈ ℂ
95 eqid 2752 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) = (abs ∘ − )
9695cnmetdval 22767 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9715, 94, 96sylancl 697 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘(𝑋 − 0)))
9815subid1d 10565 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑋 − 0) = 𝑋)
9998fveq2d 6348 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘(𝑋 − 0)) = (abs‘𝑋))
10097, 99eqtrd 2786 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) = (abs‘𝑋))
101 cnxmet 22769 . . . . . . . . . . . . . . . . . . . . 21 (abs ∘ − ) ∈ (∞Met‘ℂ)
102 1rp 12021 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℝ+
103 rpxr 12025 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ ℝ+ → 1 ∈ ℝ*)
104102, 103ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ ℝ*
105 elbl3 22390 . . . . . . . . . . . . . . . . . . . . 21 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ*) ∧ (0 ∈ ℂ ∧ 𝑋 ∈ ℂ)) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
106101, 104, 105mpanl12 720 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ ℂ ∧ 𝑋 ∈ ℂ) → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10794, 15, 106sylancr 698 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑋 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑋(abs ∘ − )0) < 1))
10847, 107mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋(abs ∘ − )0) < 1)
109100, 108eqbrtrrd 4820 . . . . . . . . . . . . . . . . 17 (𝜑 → (abs‘𝑋) < 1)
110 1re 10223 . . . . . . . . . . . . . . . . . 18 1 ∈ ℝ
111 ltle 10310 . . . . . . . . . . . . . . . . . 18 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
11286, 110, 111sylancl 697 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝑋) < 1 → (abs‘𝑋) ≤ 1))
113109, 112mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → (abs‘𝑋) ≤ 1)
114113adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘𝑋) ≤ 1)
115 simpr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
116 exple1 13106 . . . . . . . . . . . . . . 15 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11791, 93, 114, 115, 116syl31anc 1476 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘𝑋)↑𝑛) ≤ 1)
11888, 89, 73, 90, 117lemul2ad 11148 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1))
11924, 26absmuld 14384 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))))
120 absexp 14235 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℂ ∧ 𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
12115, 120sylan 489 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ0) → (abs‘(𝑋𝑛)) = ((abs‘𝑋)↑𝑛))
122121oveq2d 6821 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · (abs‘(𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
123119, 122eqtr2d 2787 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
12473recnd 10252 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ0) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℂ)
125124mulid1d 10241 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ0) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · 1) = (abs‘(seq0( + , 𝐴)‘𝑛)))
126118, 123, 1253brtr3d 4827 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12719, 126sylan2 492 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
12818, 83, 74, 127fsumle 14722 . . . . . . . . . 10 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
12980, 84, 75, 85, 128letrd 10378 . . . . . . . . 9 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
13075ltp1d 11138 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13180, 75, 77, 129, 130lelttrd 10379 . . . . . . . 8 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13280, 77, 131ltled 10369 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
13380, 77, 72, 81, 132lemul2ad 11148 . . . . . 6 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ ((abs‘(1 − 𝑋)) · (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1)))
13479, 133eqbrtrd 4818 . . . . 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 10225 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
13719, 90sylan2 492 . . . . . . . . 9 ((𝜑𝑛 ∈ (0...(𝑁 − 1))) → 0 ≤ (abs‘(seq0( + , 𝐴)‘𝑛)))
13818, 74, 137fsumge0 14718 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)))
139136, 75, 77, 138, 130lelttrd 10379 . . . . . . 7 (𝜑 → 0 < (Σ𝑛 ∈ (0...(𝑁 − 1))(abs‘(seq0( + , 𝐴)‘𝑛)) + 1))
140 ltmuldiv 11080 . . . . . . 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 1477 . . . . . 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 10379 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) < 𝑅)
14417, 54absmuld 14384 . . . . 5 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
14554abscld 14366 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
14639fveq2d 6348 . . . . . . . . . 10 (𝑘 = 𝑛 → (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
147 eqid 2752 . . . . . . . . . 10 (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) = (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))
148 fvex 6354 . . . . . . . . . 10 (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ V
149146, 147, 148fvmpt 6436 . . . . . . . . 9 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15036, 149syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
15144abscld 14366 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
152 uzid 11886 . . . . . . . . . 10 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
15334, 152syl 17 . . . . . . . . 9 (𝜑𝑁 ∈ (ℤ𝑁))
154 oveq2 6813 . . . . . . . . . . . 12 (𝑘 = 𝑛 → ((abs‘𝑋)↑𝑘) = ((abs‘𝑋)↑𝑛))
155 eqid 2752 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘)) = (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))
156 ovex 6833 . . . . . . . . . . . 12 ((abs‘𝑋)↑𝑛) ∈ V
157154, 155, 156fvmpt 6436 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15836, 157syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) = ((abs‘𝑋)↑𝑛))
15936, 88syldan 488 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘𝑋)↑𝑛) ∈ ℝ)
160158, 159eqeltrd 2831 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℝ)
161151recnd 10252 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℂ)
162150, 161eqeltrd 2831 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) ∈ ℂ)
16386recnd 10252 . . . . . . . . . . 11 (𝜑 → (abs‘𝑋) ∈ ℂ)
164 absidm 14254 . . . . . . . . . . . . 13 (𝑋 ∈ ℂ → (abs‘(abs‘𝑋)) = (abs‘𝑋))
16515, 164syl 17 . . . . . . . . . . . 12 (𝜑 → (abs‘(abs‘𝑋)) = (abs‘𝑋))
166165, 109eqbrtrd 4818 . . . . . . . . . . 11 (𝜑 → (abs‘(abs‘𝑋)) < 1)
167163, 166, 33, 158geolim2 14793 . . . . . . . . . 10 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))))
168 seqex 12989 . . . . . . . . . . 11 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ V
169 ovex 6833 . . . . . . . . . . 11 (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ V
170168, 169breldm 5476 . . . . . . . . . 10 (seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ⇝ (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
171167, 170syl 17 . . . . . . . . 9 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))) ∈ dom ⇝ )
172119, 122eqtrd 2786 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ0) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17336, 172syldan 488 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) = ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)))
17436, 73syldan 488 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ∈ ℝ)
17561adantr 472 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 𝑅 ∈ ℝ)
17686adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘𝑋) ∈ ℝ)
17792adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ (abs‘𝑋))
178176, 36, 177expge0d 13212 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → 0 ≤ ((abs‘𝑋)↑𝑛))
179 abelthlem7.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅)
18037fveq2d 6348 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑛 → (abs‘(seq0( + , 𝐴)‘𝑘)) = (abs‘(seq0( + , 𝐴)‘𝑛)))
181180breq1d 4806 . . . . . . . . . . . . . . 15 (𝑘 = 𝑛 → ((abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅 ↔ (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅))
182181rspccva 3440 . . . . . . . . . . . . . 14 ((∀𝑘 ∈ (ℤ𝑁)(abs‘(seq0( + , 𝐴)‘𝑘)) < 𝑅𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
183179, 182sylan 489 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) < 𝑅)
184174, 175, 183ltled 10369 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(seq0( + , 𝐴)‘𝑛)) ≤ 𝑅)
185174, 175, 159, 178, 184lemul1ad 11147 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((abs‘(seq0( + , 𝐴)‘𝑛)) · ((abs‘𝑋)↑𝑛)) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
186173, 185eqbrtrd 4818 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · ((abs‘𝑋)↑𝑛)))
187150fveq2d 6348 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))))
188 absidm 14254 . . . . . . . . . . . 12 (((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)) ∈ ℂ → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
18944, 188syl 17 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
190187, 189eqtrd 2786 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
191158oveq2d 6821 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
192186, 190, 1913brtr4d 4828 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛)) ≤ (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
19332, 153, 160, 162, 171, 61, 192cvgcmpce 14741 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ∈ dom ⇝ )
19432, 34, 150, 151, 193isumrecl 14687 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ∈ ℝ)
195 eldifsni 4458 . . . . . . . . . . . 12 (𝑋 ∈ (𝑆 ∖ {1}) → 𝑋 ≠ 1)
1968, 195syl 17 . . . . . . . . . . 11 (𝜑𝑋 ≠ 1)
197196necomd 2979 . . . . . . . . . 10 (𝜑 → 1 ≠ 𝑋)
198 subeq0 10491 . . . . . . . . . . . 12 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) = 0 ↔ 1 = 𝑋))
199198necon3bid 2968 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑋 ∈ ℂ) → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
20012, 15, 199sylancr 698 . . . . . . . . . 10 (𝜑 → ((1 − 𝑋) ≠ 0 ↔ 1 ≠ 𝑋))
201197, 200mpbird 247 . . . . . . . . 9 (𝜑 → (1 − 𝑋) ≠ 0)
20217, 201absrpcld 14378 . . . . . . . 8 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℝ+)
20371, 202rerpdivcld 12088 . . . . . . 7 (𝜑 → ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ)
20432, 34, 43, 44, 53isumclim2 14680 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))) ⇝ Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))
20532, 34, 150, 161, 193isumclim2 14680 . . . . . . . 8 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))) ⇝ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
20636, 51syldan 488 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛) ∈ ℂ)
20743fveq2d 6348 . . . . . . . . 9 ((𝜑𝑛 ∈ (ℤ𝑁)) → (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)) = (abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
208150, 207eqtr4d 2789 . . . . . . . 8 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (abs‘((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘))))‘𝑛) = (abs‘((𝑘 ∈ ℕ0 ↦ ((seq0( + , 𝐴)‘𝑘) · (𝑋𝑘)))‘𝑛)))
20932, 204, 205, 34, 206, 208iserabs 14738 . . . . . . 7 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))
21086, 33reexpcld 13211 . . . . . . . . . 10 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℝ)
211 difrp 12053 . . . . . . . . . . . 12 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
21286, 110, 211sylancl 697 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋) < 1 ↔ (1 − (abs‘𝑋)) ∈ ℝ+))
213109, 212mpbid 222 . . . . . . . . . 10 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ+)
214210, 213rerpdivcld 12088 . . . . . . . . 9 (𝜑 → (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋))) ∈ ℝ)
21561, 214remulcld 10254 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ ℝ)
216154oveq2d 6821 . . . . . . . . . . . 12 (𝑘 = 𝑛 → (𝑅 · ((abs‘𝑋)↑𝑘)) = (𝑅 · ((abs‘𝑋)↑𝑛)))
217 eqid 2752 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘))) = (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))
218 ovex 6833 . . . . . . . . . . . 12 (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ V
219216, 217, 218fvmpt 6436 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
22036, 219syl 17 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((abs‘𝑋)↑𝑛)))
221175, 159remulcld 10254 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℝ)
22260rpcnd 12059 . . . . . . . . . . . 12 (𝜑𝑅 ∈ ℂ)
223160recnd 10252 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛) ∈ ℂ)
224220, 191eqtr4d 2789 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (ℤ𝑁)) → ((𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))‘𝑛) = (𝑅 · ((𝑘 ∈ ℕ0 ↦ ((abs‘𝑋)↑𝑘))‘𝑛)))
22532, 34, 222, 167, 223, 224isermulc2 14579 . . . . . . . . . . 11 (𝜑 → seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ⇝ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
226 seqex 12989 . . . . . . . . . . . 12 seq𝑁( + , (𝑘 ∈ ℕ0 ↦ (𝑅 · ((abs‘𝑋)↑𝑘)))) ∈ V
227 ovex 6833 . . . . . . . . . . . 12 (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ∈ V
228226, 227breldm 5476 . . . . . . . . . . 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 14767 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)))
231221recnd 10252 . . . . . . . . . 10 ((𝜑𝑛 ∈ (ℤ𝑁)) → (𝑅 · ((abs‘𝑋)↑𝑛)) ∈ ℂ)
23232, 34, 220, 231, 225isumclim 14679 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(𝑅 · ((abs‘𝑋)↑𝑛)) = (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
233230, 232breqtrd 4822 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))))
23460, 213rpdivcld 12074 . . . . . . . . . 10 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ+)
235234rpred 12057 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℝ)
236210recnd 10252 . . . . . . . . . . 11 (𝜑 → ((abs‘𝑋)↑𝑁) ∈ ℂ)
237213rpcnd 12059 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ∈ ℂ)
238213rpne0d 12062 . . . . . . . . . . 11 (𝜑 → (1 − (abs‘𝑋)) ≠ 0)
239222, 236, 237, 238div12d 11021 . . . . . . . . . 10 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) = (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))))
240 1red 10239 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℝ)
241234rpge0d 12061 . . . . . . . . . . . 12 (𝜑 → 0 ≤ (𝑅 / (1 − (abs‘𝑋))))
242 exple1 13106 . . . . . . . . . . . . 13 ((((abs‘𝑋) ∈ ℝ ∧ 0 ≤ (abs‘𝑋) ∧ (abs‘𝑋) ≤ 1) ∧ 𝑁 ∈ ℕ0) → ((abs‘𝑋)↑𝑁) ≤ 1)
24386, 92, 113, 33, 242syl31anc 1476 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋)↑𝑁) ≤ 1)
244210, 240, 235, 241, 243lemul1ad 11147 . . . . . . . . . . 11 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (1 · (𝑅 / (1 − (abs‘𝑋)))))
245234rpcnd 12059 . . . . . . . . . . . 12 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ∈ ℂ)
246245mulid2d 10242 . . . . . . . . . . 11 (𝜑 → (1 · (𝑅 / (1 − (abs‘𝑋)))) = (𝑅 / (1 − (abs‘𝑋))))
247244, 246breqtrd 4822 . . . . . . . . . 10 (𝜑 → (((abs‘𝑋)↑𝑁) · (𝑅 / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
248239, 247eqbrtrd 4818 . . . . . . . . 9 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ (𝑅 / (1 − (abs‘𝑋))))
24914simprd 482 . . . . . . . . . . . . . 14 (𝜑 → (abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))))
250 resubcl 10529 . . . . . . . . . . . . . . . . 17 ((1 ∈ ℝ ∧ (abs‘𝑋) ∈ ℝ) → (1 − (abs‘𝑋)) ∈ ℝ)
251110, 86, 250sylancr 698 . . . . . . . . . . . . . . . 16 (𝜑 → (1 − (abs‘𝑋)) ∈ ℝ)
2523, 251remulcld 10254 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 · (1 − (abs‘𝑋))) ∈ ℝ)
25372, 252, 60lemul2d 12101 . . . . . . . . . . . . . 14 (𝜑 → ((abs‘(1 − 𝑋)) ≤ (𝑀 · (1 − (abs‘𝑋))) ↔ (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋))))))
254249, 253mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ (𝑅 · (𝑀 · (1 − (abs‘𝑋)))))
2553recnd 10252 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℂ)
256222, 255, 237mul12d 10429 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = (𝑀 · (𝑅 · (1 − (abs‘𝑋)))))
257222, 237mulcomd 10245 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 · (1 − (abs‘𝑋))) = ((1 − (abs‘𝑋)) · 𝑅))
258257oveq2d 6821 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · (𝑅 · (1 − (abs‘𝑋)))) = (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)))
259255, 237, 222mul12d 10429 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 · ((1 − (abs‘𝑋)) · 𝑅)) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
260256, 258, 2593eqtrd 2790 . . . . . . . . . . . . 13 (𝜑 → (𝑅 · (𝑀 · (1 − (abs‘𝑋)))) = ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
261254, 260breqtrd 4822 . . . . . . . . . . . 12 (𝜑 → (𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)))
262251, 71remulcld 10254 . . . . . . . . . . . . 13 (𝜑 → ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ∈ ℝ)
26361, 262, 202lemuldivd 12106 . . . . . . . . . . . 12 (𝜑 → ((𝑅 · (abs‘(1 − 𝑋))) ≤ ((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) ↔ 𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋)))))
264261, 263mpbid 222 . . . . . . . . . . 11 (𝜑𝑅 ≤ (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))))
26571recnd 10252 . . . . . . . . . . . 12 (𝜑 → (𝑀 · 𝑅) ∈ ℂ)
26672recnd 10252 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ∈ ℂ)
267202rpne0d 12062 . . . . . . . . . . . 12 (𝜑 → (abs‘(1 − 𝑋)) ≠ 0)
268237, 265, 266, 267divassd 11020 . . . . . . . . . . 11 (𝜑 → (((1 − (abs‘𝑋)) · (𝑀 · 𝑅)) / (abs‘(1 − 𝑋))) = ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
269264, 268breqtrd 4822 . . . . . . . . . 10 (𝜑𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
270 posdif 10705 . . . . . . . . . . . . 13 (((abs‘𝑋) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
27186, 110, 270sylancl 697 . . . . . . . . . . . 12 (𝜑 → ((abs‘𝑋) < 1 ↔ 0 < (1 − (abs‘𝑋))))
272109, 271mpbid 222 . . . . . . . . . . 11 (𝜑 → 0 < (1 − (abs‘𝑋)))
273 ledivmul 11083 . . . . . . . . . . 11 ((𝑅 ∈ ℝ ∧ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ∈ ℝ ∧ ((1 − (abs‘𝑋)) ∈ ℝ ∧ 0 < (1 − (abs‘𝑋)))) → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
27461, 203, 251, 272, 273syl112anc 1477 . . . . . . . . . 10 (𝜑 → ((𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))) ↔ 𝑅 ≤ ((1 − (abs‘𝑋)) · ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))))
275269, 274mpbird 247 . . . . . . . . 9 (𝜑 → (𝑅 / (1 − (abs‘𝑋))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
276215, 235, 203, 248, 275letrd 10378 . . . . . . . 8 (𝜑 → (𝑅 · (((abs‘𝑋)↑𝑁) / (1 − (abs‘𝑋)))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
277194, 215, 203, 233, 276letrd 10378 . . . . . . 7 (𝜑 → Σ𝑛 ∈ (ℤ𝑁)(abs‘((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
278145, 194, 203, 209, 277letrd 10378 . . . . . 6 (𝜑 → (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋))))
279145, 71, 202lemuldiv2d 12107 . . . . . 6 (𝜑 → (((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅) ↔ (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))) ≤ ((𝑀 · 𝑅) / (abs‘(1 − 𝑋)))))
280278, 279mpbird 247 . . . . 5 (𝜑 → ((abs‘(1 − 𝑋)) · (abs‘Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
281144, 280eqbrtrd 4818 . . . 4 (𝜑 → (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) ≤ (𝑀 · 𝑅))
28231, 56, 61, 71, 143, 281ltleaddd 10832 . . 3 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < (𝑅 + (𝑀 · 𝑅)))
283 1cnd 10240 . . . . 5 (𝜑 → 1 ∈ ℂ)
284255, 283, 222adddird 10249 . . . 4 (𝜑 → ((𝑀 + 1) · 𝑅) = ((𝑀 · 𝑅) + (1 · 𝑅)))
285222mulid2d 10242 . . . . 5 (𝜑 → (1 · 𝑅) = 𝑅)
286285oveq2d 6821 . . . 4 (𝜑 → ((𝑀 · 𝑅) + (1 · 𝑅)) = ((𝑀 · 𝑅) + 𝑅))
287265, 222addcomd 10422 . . . 4 (𝜑 → ((𝑀 · 𝑅) + 𝑅) = (𝑅 + (𝑀 · 𝑅)))
288284, 286, 2873eqtrd 2790 . . 3 (𝜑 → ((𝑀 + 1) · 𝑅) = (𝑅 + (𝑀 · 𝑅)))
289282, 288breqtrrd 4824 . 2 (𝜑 → ((abs‘((1 − 𝑋) · Σ𝑛 ∈ (0...(𝑁 − 1))((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛)))) + (abs‘((1 − 𝑋) · Σ𝑛 ∈ (ℤ𝑁)((seq0( + , 𝐴)‘𝑛) · (𝑋𝑛))))) < ((𝑀 + 1) · 𝑅))
29011, 57, 62, 70, 289lelttrd 10379 1 (𝜑 → (abs‘(𝐹𝑋)) < ((𝑀 + 1) · 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wne 2924  wral 3042  {crab 3046  cdif 3704  wss 3707  {csn 4313   class class class wbr 4796  cmpt 4873  dom cdm 5258  ccom 5262  wf 6037  cfv 6041  (class class class)co 6805  cc 10118  cr 10119  0cc0 10120  1c1 10121   + caddc 10123   · cmul 10125  *cxr 10257   < clt 10258  cle 10259  cmin 10450   / cdiv 10868  0cn0 11476  cz 11561  cuz 11871  +crp 12017  ...cfz 12511  seqcseq 12987  cexp 13046  abscabs 14165  cli 14406  Σcsu 14607  ∞Metcxmt 19925  ballcbl 19927
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-n0 11477  df-z 11562  df-uz 11872  df-rp 12018  df-xadd 12132  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-seq 12988  df-exp 13047  df-hash 13304  df-shft 13998  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-limsup 14393  df-clim 14410  df-rlim 14411  df-sum 14608  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935
This theorem is referenced by:  abelthlem8  24384
  Copyright terms: Public domain W3C validator