Metamath Proof Explorer

Theorem abelthlem3

Description: Lemma for abelth . (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Hypotheses abelth.1 ⊢φ→A:ℕ0⟶ℂ
abelth.2 ⊢φ→seq0+A∈dom⁡⇝
abelth.3 ⊢φ→M∈ℝ
abelth.4 ⊢φ→0≤M
abelth.5 ⊢S=z∈ℂ|1−z≤M⁢1−z
Assertion abelthlem3 ⊢φ∧X∈S→seq0+n∈ℕ0⟼A⁡n⁢Xn∈dom⁡⇝

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢φ→A:ℕ0⟶ℂ
2 abelth.2 ⊢φ→seq0+A∈dom⁡⇝
3 abelth.3 ⊢φ→M∈ℝ
4 abelth.4 ⊢φ→0≤M
5 abelth.5 ⊢S=z∈ℂ|1−z≤M⁢1−z
6 1 2 3 4 5 abelthlem2 ⊢φ→1∈S∧S∖1⊆0ball⁡abs∘−1
7 6 simprd ⊢φ→S∖1⊆0ball⁡abs∘−1
8 ssundif ⊢S⊆1∪0ball⁡abs∘−1↔S∖1⊆0ball⁡abs∘−1
9 7 8 sylibr ⊢φ→S⊆1∪0ball⁡abs∘−1
10 9 sselda ⊢φ∧X∈S→X∈1∪0ball⁡abs∘−1
11 elun ⊢X∈1∪0ball⁡abs∘−1↔X∈1∨X∈0ball⁡abs∘−1
12 10 11 sylib ⊢φ∧X∈S→X∈1∨X∈0ball⁡abs∘−1
13 1 feqmptd ⊢φ→A=n∈ℕ0⟼A⁡n
14 1 ffvelcdmda ⊢φ∧n∈ℕ0→A⁡n∈ℂ
15 14 mulridd ⊢φ∧n∈ℕ0→A⁡n⋅1=A⁡n
16 15 mpteq2dva ⊢φ→n∈ℕ0⟼A⁡n⋅1=n∈ℕ0⟼A⁡n
17 13 16 eqtr4d ⊢φ→A=n∈ℕ0⟼A⁡n⋅1
18 elsni ⊢X∈1→X=1
19 18 oveq1d ⊢X∈1→Xn=1n
20 nn0z ⊢n∈ℕ0→n∈ℤ
21 1exp ⊢n∈ℤ→1n=1
22 20 21 syl ⊢n∈ℕ0→1n=1
23 19 22 sylan9eq ⊢X∈1∧n∈ℕ0→Xn=1
24 23 oveq2d ⊢X∈1∧n∈ℕ0→A⁡n⁢Xn=A⁡n⋅1
25 24 mpteq2dva ⊢X∈1→n∈ℕ0⟼A⁡n⁢Xn=n∈ℕ0⟼A⁡n⋅1
26 25 eqcomd ⊢X∈1→n∈ℕ0⟼A⁡n⋅1=n∈ℕ0⟼A⁡n⁢Xn
27 17 26 sylan9eq ⊢φ∧X∈1→A=n∈ℕ0⟼A⁡n⁢Xn
28 27 seqeq3d ⊢φ∧X∈1→seq0+A=seq0+n∈ℕ0⟼A⁡n⁢Xn
29 2 adantr ⊢φ∧X∈1→seq0+A∈dom⁡⇝
30 28 29 eqeltrrd ⊢φ∧X∈1→seq0+n∈ℕ0⟼A⁡n⁢Xn∈dom⁡⇝
31 cnxmet ⊢abs∘−∈∞Met⁡ℂ
32 0cn ⊢0∈ℂ
33 1xr ⊢1∈ℝ*
34 blssm ⊢abs∘−∈∞Met⁡ℂ∧0∈ℂ∧1∈ℝ*→0ball⁡abs∘−1⊆ℂ
35 31 32 33 34 mp3an ⊢0ball⁡abs∘−1⊆ℂ
36 simpr ⊢φ∧X∈0ball⁡abs∘−1→X∈0ball⁡abs∘−1
37 35 36 sselid ⊢φ∧X∈0ball⁡abs∘−1→X∈ℂ
38 oveq1 ⊢z=X→zn=Xn
39 38 oveq2d ⊢z=X→A⁡n⁢zn=A⁡n⁢Xn
40 39 mpteq2dv ⊢z=X→n∈ℕ0⟼A⁡n⁢zn=n∈ℕ0⟼A⁡n⁢Xn
41 eqid ⊢z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn=z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn
42 nn0ex ⊢ℕ0∈V
43 42 mptex ⊢n∈ℕ0⟼A⁡n⁢Xn∈V
44 40 41 43 fvmpt ⊢X∈ℂ→z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡X=n∈ℕ0⟼A⁡n⁢Xn
45 37 44 syl ⊢φ∧X∈0ball⁡abs∘−1→z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡X=n∈ℕ0⟼A⁡n⁢Xn
46 45 seqeq3d ⊢φ∧X∈0ball⁡abs∘−1→seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡X=seq0+n∈ℕ0⟼A⁡n⁢Xn
47 1 adantr ⊢φ∧X∈0ball⁡abs∘−1→A:ℕ0⟶ℂ
48 eqid ⊢supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<=supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
49 37 abscld ⊢φ∧X∈0ball⁡abs∘−1→X∈ℝ
50 49 rexrd ⊢φ∧X∈0ball⁡abs∘−1→X∈ℝ*
51 1re ⊢1∈ℝ
52 rexr ⊢1∈ℝ→1∈ℝ*
53 51 52 mp1i ⊢φ∧X∈0ball⁡abs∘−1→1∈ℝ*
54 iccssxr ⊢0+∞⊆ℝ*
55 41 47 48 radcnvcl ⊢φ∧X∈0ball⁡abs∘−1→supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<∈0+∞
56 54 55 sselid ⊢φ∧X∈0ball⁡abs∘−1→supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<∈ℝ*
57 eqid ⊢abs∘−=abs∘−
58 57 cnmetdval ⊢X∈ℂ∧0∈ℂ→Xabs∘−0=X−0
59 37 32 58 sylancl ⊢φ∧X∈0ball⁡abs∘−1→Xabs∘−0=X−0
60 37 subid1d ⊢φ∧X∈0ball⁡abs∘−1→X−0=X
61 60 fveq2d ⊢φ∧X∈0ball⁡abs∘−1→X−0=X
62 59 61 eqtrd ⊢φ∧X∈0ball⁡abs∘−1→Xabs∘−0=X
63 elbl3 ⊢abs∘−∈∞Met⁡ℂ∧1∈ℝ*∧0∈ℂ∧X∈ℂ→X∈0ball⁡abs∘−1↔Xabs∘−0<1
64 31 33 63 mpanl12 ⊢0∈ℂ∧X∈ℂ→X∈0ball⁡abs∘−1↔Xabs∘−0<1
65 32 37 64 sylancr ⊢φ∧X∈0ball⁡abs∘−1→X∈0ball⁡abs∘−1↔Xabs∘−0<1
66 36 65 mpbid ⊢φ∧X∈0ball⁡abs∘−1→Xabs∘−0<1
67 62 66 eqbrtrrd ⊢φ∧X∈0ball⁡abs∘−1→X<1
68 1 2 abelthlem1 ⊢φ→1≤supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
69 68 adantr ⊢φ∧X∈0ball⁡abs∘−1→1≤supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
70 50 53 56 67 69 xrltletrd ⊢φ∧X∈0ball⁡abs∘−1→X<supr∈ℝ|seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡r∈dom⁡⇝ℝ*<
71 41 47 48 37 70 radcnvlt2 ⊢φ∧X∈0ball⁡abs∘−1→seq0+z∈ℂ⟼n∈ℕ0⟼A⁡n⁢zn⁡X∈dom⁡⇝
72 46 71 eqeltrrd ⊢φ∧X∈0ball⁡abs∘−1→seq0+n∈ℕ0⟼A⁡n⁢Xn∈dom⁡⇝
73 30 72 jaodan ⊢φ∧X∈1∨X∈0ball⁡abs∘−1→seq0+n∈ℕ0⟼A⁡n⁢Xn∈dom⁡⇝
74 12 73 syldan ⊢φ∧X∈S→seq0+n∈ℕ0⟼A⁡n⁢Xn∈dom⁡⇝