Metamath Proof Explorer

Theorem lgamgulmlem4

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r ⊢φ→R∈ℕ
lgamgulm.u ⊢U=x∈ℂ|x≤R∧∀k∈ℕ01R≤x+k
lgamgulm.g ⊢G=m∈ℕ⟼z∈U⟼z⁢log⁡m+1m−log⁡zm+1
lgamgulm.t ⊢T=m∈ℕ⟼if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π
Assertion lgamgulmlem4 ⊢φ→seq1+T∈dom⁡⇝

Proof

Step Hyp Ref Expression
1 lgamgulm.r ⊢φ→R∈ℕ
2 lgamgulm.u ⊢U=x∈ℂ|x≤R∧∀k∈ℕ01R≤x+k
3 lgamgulm.g ⊢G=m∈ℕ⟼z∈U⟼z⁢log⁡m+1m−log⁡zm+1
4 lgamgulm.t ⊢T=m∈ℕ⟼if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π
5 2nn ⊢2∈ℕ
6 5 a1i ⊢φ→2∈ℕ
7 6 1 nnmulcld ⊢φ→2⁢R∈ℕ
8 7 nnzd ⊢φ→2⁢R∈ℤ
9 eluzle ⊢n∈ℤ≥2⁢R→2⁢R≤n
10 9 adantl ⊢φ∧n∈ℤ≥2⁢R→2⁢R≤n
11 10 iftrued ⊢φ∧n∈ℤ≥2⁢R→if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π=R⁢2⁢R+1n2
12 eluznn ⊢2⁢R∈ℕ∧n∈ℤ≥2⁢R→n∈ℕ
13 7 12 sylan ⊢φ∧n∈ℤ≥2⁢R→n∈ℕ
14 breq2 ⊢m=n→2⁢R≤m↔2⁢R≤n
15 oveq1 ⊢m=n→m2=n2
16 15 oveq2d ⊢m=n→2⁢R+1m2=2⁢R+1n2
17 16 oveq2d ⊢m=n→R⁢2⁢R+1m2=R⁢2⁢R+1n2
18 oveq1 ⊢m=n→m+1=n+1
19 id ⊢m=n→m=n
20 18 19 oveq12d ⊢m=n→m+1m=n+1n
21 20 fveq2d ⊢m=n→log⁡m+1m=log⁡n+1n
22 21 oveq2d ⊢m=n→R⁢log⁡m+1m=R⁢log⁡n+1n
23 oveq2 ⊢m=n→R+1⁢m=R+1⁢n
24 23 fveq2d ⊢m=n→log⁡R+1⁢m=log⁡R+1⁢n
25 24 oveq1d ⊢m=n→log⁡R+1⁢m+π=log⁡R+1⁢n+π
26 22 25 oveq12d ⊢m=n→R⁢log⁡m+1m+log⁡R+1⁢m+π=R⁢log⁡n+1n+log⁡R+1⁢n+π
27 14 17 26 ifbieq12d ⊢m=n→if2⁢R≤mR⁢2⁢R+1m2R⁢log⁡m+1m+log⁡R+1⁢m+π=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
28 ovex ⊢R⁢2⁢R+1n2∈V
29 ovex ⊢R⁢log⁡n+1n+log⁡R+1⁢n+π∈V
30 28 29 ifex ⊢if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π∈V
31 27 4 30 fvmpt ⊢n∈ℕ→T⁡n=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
32 13 31 syl ⊢φ∧n∈ℤ≥2⁢R→T⁡n=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
33 eqid ⊢m∈ℕ⟼R⁢2⁢R+1m2=m∈ℕ⟼R⁢2⁢R+1m2
34 17 33 28 fvmpt ⊢n∈ℕ→m∈ℕ⟼R⁢2⁢R+1m2⁡n=R⁢2⁢R+1n2
35 13 34 syl ⊢φ∧n∈ℤ≥2⁢R→m∈ℕ⟼R⁢2⁢R+1m2⁡n=R⁢2⁢R+1n2
36 11 32 35 3eqtr4d ⊢φ∧n∈ℤ≥2⁢R→T⁡n=m∈ℕ⟼R⁢2⁢R+1m2⁡n
37 8 36 seqfeq ⊢φ→seq2⁢R+T=seq2⁢R+m∈ℕ⟼R⁢2⁢R+1m2
38 nnuz ⊢ℕ=ℤ≥1
39 1zzd ⊢φ→1∈ℤ
40 1 nncnd ⊢φ→R∈ℂ
41 2cnd ⊢φ→2∈ℂ
42 1cnd ⊢φ→1∈ℂ
43 40 42 addcld ⊢φ→R+1∈ℂ
44 41 43 mulcld ⊢φ→2⁢R+1∈ℂ
45 40 44 mulcld ⊢φ→R⁢2⁢R+1∈ℂ
46 1lt2 ⊢1<2
47 2re ⊢2∈ℝ
48 rere ⊢2∈ℝ→ℜ⁡2=2
49 47 48 ax-mp ⊢ℜ⁡2=2
50 46 49 breqtrri ⊢1<ℜ⁡2
51 50 a1i ⊢φ→1<ℜ⁡2
52 oveq1 ⊢m=n→m−2=n−2
53 eqid ⊢m∈ℕ⟼m−2=m∈ℕ⟼m−2
54 ovex ⊢n−2∈V
55 52 53 54 fvmpt ⊢n∈ℕ→m∈ℕ⟼m−2⁡n=n−2
56 55 adantl ⊢φ∧n∈ℕ→m∈ℕ⟼m−2⁡n=n−2
57 41 51 56 zetacvg ⊢φ→seq1+m∈ℕ⟼m−2∈dom⁡⇝
58 climdm ⊢seq1+m∈ℕ⟼m−2∈dom⁡⇝↔seq1+m∈ℕ⟼m−2⇝⇝⁡seq1+m∈ℕ⟼m−2
59 57 58 sylib ⊢φ→seq1+m∈ℕ⟼m−2⇝⇝⁡seq1+m∈ℕ⟼m−2
60 simpr ⊢φ∧n∈ℕ→n∈ℕ
61 60 nncnd ⊢φ∧n∈ℕ→n∈ℂ
62 2cnd ⊢φ∧n∈ℕ→2∈ℂ
63 62 negcld ⊢φ∧n∈ℕ→−2∈ℂ
64 61 63 cxpcld ⊢φ∧n∈ℕ→n−2∈ℂ
65 56 64 eqeltrd ⊢φ∧n∈ℕ→m∈ℕ⟼m−2⁡n∈ℂ
66 40 adantr ⊢φ∧n∈ℕ→R∈ℂ
67 1cnd ⊢φ∧n∈ℕ→1∈ℂ
68 66 67 addcld ⊢φ∧n∈ℕ→R+1∈ℂ
69 62 68 mulcld ⊢φ∧n∈ℕ→2⁢R+1∈ℂ
70 66 69 mulcld ⊢φ∧n∈ℕ→R⁢2⁢R+1∈ℂ
71 61 sqcld ⊢φ∧n∈ℕ→n2∈ℂ
72 60 nnne0d ⊢φ∧n∈ℕ→n≠0
73 2z ⊢2∈ℤ
74 73 a1i ⊢φ∧n∈ℕ→2∈ℤ
75 61 72 74 expne0d ⊢φ∧n∈ℕ→n2≠0
76 70 71 75 divrecd ⊢φ∧n∈ℕ→R⁢2⁢R+1n2=R⁢2⁢R+1⁢1n2
77 66 69 71 75 divassd ⊢φ∧n∈ℕ→R⁢2⁢R+1n2=R⁢2⁢R+1n2
78 61 72 62 cxpnegd ⊢φ∧n∈ℕ→n−2=1n2
79 61 72 74 cxpexpzd ⊢φ∧n∈ℕ→n2=n2
80 79 oveq2d ⊢φ∧n∈ℕ→1n2=1n2
81 78 80 eqtr2d ⊢φ∧n∈ℕ→1n2=n−2
82 81 oveq2d ⊢φ∧n∈ℕ→R⁢2⁢R+1⁢1n2=R⁢2⁢R+1⁢n−2
83 76 77 82 3eqtr3d ⊢φ∧n∈ℕ→R⁢2⁢R+1n2=R⁢2⁢R+1⁢n−2
84 34 adantl ⊢φ∧n∈ℕ→m∈ℕ⟼R⁢2⁢R+1m2⁡n=R⁢2⁢R+1n2
85 56 oveq2d ⊢φ∧n∈ℕ→R⁢2⁢R+1⁢m∈ℕ⟼m−2⁡n=R⁢2⁢R+1⁢n−2
86 83 84 85 3eqtr4d ⊢φ∧n∈ℕ→m∈ℕ⟼R⁢2⁢R+1m2⁡n=R⁢2⁢R+1⁢m∈ℕ⟼m−2⁡n
87 38 39 45 59 65 86 isermulc2 ⊢φ→seq1+m∈ℕ⟼R⁢2⁢R+1m2⇝R⁢2⁢R+1⁢⇝⁡seq1+m∈ℕ⟼m−2
88 climrel ⊢Rel⁡⇝
89 88 releldmi ⊢seq1+m∈ℕ⟼R⁢2⁢R+1m2⇝R⁢2⁢R+1⁢⇝⁡seq1+m∈ℕ⟼m−2→seq1+m∈ℕ⟼R⁢2⁢R+1m2∈dom⁡⇝
90 87 89 syl ⊢φ→seq1+m∈ℕ⟼R⁢2⁢R+1m2∈dom⁡⇝
91 69 71 75 divcld ⊢φ∧n∈ℕ→2⁢R+1n2∈ℂ
92 66 91 mulcld ⊢φ∧n∈ℕ→R⁢2⁢R+1n2∈ℂ
93 84 92 eqeltrd ⊢φ∧n∈ℕ→m∈ℕ⟼R⁢2⁢R+1m2⁡n∈ℂ
94 38 7 93 iserex ⊢φ→seq1+m∈ℕ⟼R⁢2⁢R+1m2∈dom⁡⇝↔seq2⁢R+m∈ℕ⟼R⁢2⁢R+1m2∈dom⁡⇝
95 90 94 mpbid ⊢φ→seq2⁢R+m∈ℕ⟼R⁢2⁢R+1m2∈dom⁡⇝
96 37 95 eqeltrd ⊢φ→seq2⁢R+T∈dom⁡⇝
97 31 adantl ⊢φ∧n∈ℕ→T⁡n=if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π
98 1 adantr ⊢φ∧n∈ℕ→R∈ℕ
99 98 nnred ⊢φ∧n∈ℕ→R∈ℝ
100 47 a1i ⊢φ∧n∈ℕ→2∈ℝ
101 1red ⊢φ∧n∈ℕ→1∈ℝ
102 99 101 readdcld ⊢φ∧n∈ℕ→R+1∈ℝ
103 100 102 remulcld ⊢φ∧n∈ℕ→2⁢R+1∈ℝ
104 60 nnsqcld ⊢φ∧n∈ℕ→n2∈ℕ
105 103 104 nndivred ⊢φ∧n∈ℕ→2⁢R+1n2∈ℝ
106 99 105 remulcld ⊢φ∧n∈ℕ→R⁢2⁢R+1n2∈ℝ
107 60 peano2nnd ⊢φ∧n∈ℕ→n+1∈ℕ
108 107 nnrpd ⊢φ∧n∈ℕ→n+1∈ℝ+
109 60 nnrpd ⊢φ∧n∈ℕ→n∈ℝ+
110 108 109 rpdivcld ⊢φ∧n∈ℕ→n+1n∈ℝ+
111 110 relogcld ⊢φ∧n∈ℕ→log⁡n+1n∈ℝ
112 99 111 remulcld ⊢φ∧n∈ℕ→R⁢log⁡n+1n∈ℝ
113 98 peano2nnd ⊢φ∧n∈ℕ→R+1∈ℕ
114 113 nnrpd ⊢φ∧n∈ℕ→R+1∈ℝ+
115 114 109 rpmulcld ⊢φ∧n∈ℕ→R+1⁢n∈ℝ+
116 115 relogcld ⊢φ∧n∈ℕ→log⁡R+1⁢n∈ℝ
117 pire ⊢π∈ℝ
118 117 a1i ⊢φ∧n∈ℕ→π∈ℝ
119 116 118 readdcld ⊢φ∧n∈ℕ→log⁡R+1⁢n+π∈ℝ
120 112 119 readdcld ⊢φ∧n∈ℕ→R⁢log⁡n+1n+log⁡R+1⁢n+π∈ℝ
121 106 120 ifcld ⊢φ∧n∈ℕ→if2⁢R≤nR⁢2⁢R+1n2R⁢log⁡n+1n+log⁡R+1⁢n+π∈ℝ
122 97 121 eqeltrd ⊢φ∧n∈ℕ→T⁡n∈ℝ
123 122 recnd ⊢φ∧n∈ℕ→T⁡n∈ℂ
124 38 7 123 iserex ⊢φ→seq1+T∈dom⁡⇝↔seq2⁢R+T∈dom⁡⇝
125 96 124 mpbird ⊢φ→seq1+T∈dom⁡⇝