Metamath Proof Explorer


Theorem lgamgulmlem4

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

Ref Expression
Hypotheses lgamgulm.r ( 𝜑𝑅 ∈ ℕ )
lgamgulm.u 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
lgamgulm.g 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
lgamgulm.t 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
Assertion lgamgulmlem4 ( 𝜑 → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )

Proof

Step Hyp Ref Expression
1 lgamgulm.r ( 𝜑𝑅 ∈ ℕ )
2 lgamgulm.u 𝑈 = { 𝑥 ∈ ℂ ∣ ( ( abs ‘ 𝑥 ) ≤ 𝑅 ∧ ∀ 𝑘 ∈ ℕ0 ( 1 / 𝑅 ) ≤ ( abs ‘ ( 𝑥 + 𝑘 ) ) ) }
3 lgamgulm.g 𝐺 = ( 𝑚 ∈ ℕ ↦ ( 𝑧𝑈 ↦ ( ( 𝑧 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) − ( log ‘ ( ( 𝑧 / 𝑚 ) + 1 ) ) ) ) )
4 lgamgulm.t 𝑇 = ( 𝑚 ∈ ℕ ↦ if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) )
5 2nn 2 ∈ ℕ
6 5 a1i ( 𝜑 → 2 ∈ ℕ )
7 6 1 nnmulcld ( 𝜑 → ( 2 · 𝑅 ) ∈ ℕ )
8 7 nnzd ( 𝜑 → ( 2 · 𝑅 ) ∈ ℤ )
9 eluzle ( 𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) → ( 2 · 𝑅 ) ≤ 𝑛 )
10 9 adantl ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → ( 2 · 𝑅 ) ≤ 𝑛 )
11 10 iftrued ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
12 eluznn ( ( ( 2 · 𝑅 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → 𝑛 ∈ ℕ )
13 7 12 sylan ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → 𝑛 ∈ ℕ )
14 breq2 ( 𝑚 = 𝑛 → ( ( 2 · 𝑅 ) ≤ 𝑚 ↔ ( 2 · 𝑅 ) ≤ 𝑛 ) )
15 oveq1 ( 𝑚 = 𝑛 → ( 𝑚 ↑ 2 ) = ( 𝑛 ↑ 2 ) )
16 15 oveq2d ( 𝑚 = 𝑛 → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) = ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) )
17 16 oveq2d ( 𝑚 = 𝑛 → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
18 oveq1 ( 𝑚 = 𝑛 → ( 𝑚 + 1 ) = ( 𝑛 + 1 ) )
19 id ( 𝑚 = 𝑛𝑚 = 𝑛 )
20 18 19 oveq12d ( 𝑚 = 𝑛 → ( ( 𝑚 + 1 ) / 𝑚 ) = ( ( 𝑛 + 1 ) / 𝑛 ) )
21 20 fveq2d ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) = ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) )
22 21 oveq2d ( 𝑚 = 𝑛 → ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) = ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) )
23 oveq2 ( 𝑚 = 𝑛 → ( ( 𝑅 + 1 ) · 𝑚 ) = ( ( 𝑅 + 1 ) · 𝑛 ) )
24 23 fveq2d ( 𝑚 = 𝑛 → ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) = ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) )
25 24 oveq1d ( 𝑚 = 𝑛 → ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) = ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) )
26 22 25 oveq12d ( 𝑚 = 𝑛 → ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) = ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) )
27 14 17 26 ifbieq12d ( 𝑚 = 𝑛 → if ( ( 2 · 𝑅 ) ≤ 𝑚 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑚 + 1 ) / 𝑚 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑚 ) ) + π ) ) ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
28 ovex ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) ∈ V
29 ovex ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ∈ V
30 28 29 ifex if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) ∈ V
31 27 4 30 fvmpt ( 𝑛 ∈ ℕ → ( 𝑇𝑛 ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
32 13 31 syl ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → ( 𝑇𝑛 ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
33 eqid ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) )
34 17 33 28 fvmpt ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
35 13 34 syl ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
36 11 32 35 3eqtr4d ( ( 𝜑𝑛 ∈ ( ℤ ‘ ( 2 · 𝑅 ) ) ) → ( 𝑇𝑛 ) = ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) )
37 8 36 seqfeq ( 𝜑 → seq ( 2 · 𝑅 ) ( + , 𝑇 ) = seq ( 2 · 𝑅 ) ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) )
38 nnuz ℕ = ( ℤ ‘ 1 )
39 1zzd ( 𝜑 → 1 ∈ ℤ )
40 1 nncnd ( 𝜑𝑅 ∈ ℂ )
41 2cnd ( 𝜑 → 2 ∈ ℂ )
42 1cnd ( 𝜑 → 1 ∈ ℂ )
43 40 42 addcld ( 𝜑 → ( 𝑅 + 1 ) ∈ ℂ )
44 41 43 mulcld ( 𝜑 → ( 2 · ( 𝑅 + 1 ) ) ∈ ℂ )
45 40 44 mulcld ( 𝜑 → ( 𝑅 · ( 2 · ( 𝑅 + 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 ( 𝑚 = 𝑛 → ( 𝑚𝑐 - 2 ) = ( 𝑛𝑐 - 2 ) )
53 eqid ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) = ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) )
54 ovex ( 𝑛𝑐 - 2 ) ∈ V
55 52 53 54 fvmpt ( 𝑛 ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ‘ 𝑛 ) = ( 𝑛𝑐 - 2 ) )
56 55 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ‘ 𝑛 ) = ( 𝑛𝑐 - 2 ) )
57 41 51 56 zetacvg ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ∈ dom ⇝ )
58 climdm ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ∈ dom ⇝ ↔ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ) )
59 57 58 sylib ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ⇝ ( ⇝ ‘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ) )
60 simpr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
61 60 nncnd ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℂ )
62 2cnd ( ( 𝜑𝑛 ∈ ℕ ) → 2 ∈ ℂ )
63 62 negcld ( ( 𝜑𝑛 ∈ ℕ ) → - 2 ∈ ℂ )
64 61 63 cxpcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛𝑐 - 2 ) ∈ ℂ )
65 56 64 eqeltrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ‘ 𝑛 ) ∈ ℂ )
66 40 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑅 ∈ ℂ )
67 1cnd ( ( 𝜑𝑛 ∈ ℕ ) → 1 ∈ ℂ )
68 66 67 addcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℂ )
69 62 68 mulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 2 · ( 𝑅 + 1 ) ) ∈ ℂ )
70 66 69 mulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) ∈ ℂ )
71 61 sqcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
72 60 nnne0d ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ≠ 0 )
73 2z 2 ∈ ℤ
74 73 a1i ( ( 𝜑𝑛 ∈ ℕ ) → 2 ∈ ℤ )
75 61 72 74 expne0d ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛 ↑ 2 ) ≠ 0 )
76 70 71 75 divrecd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) / ( 𝑛 ↑ 2 ) ) = ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( 1 / ( 𝑛 ↑ 2 ) ) ) )
77 66 69 71 75 divassd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) / ( 𝑛 ↑ 2 ) ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
78 61 72 62 cxpnegd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛𝑐 - 2 ) = ( 1 / ( 𝑛𝑐 2 ) ) )
79 61 72 74 cxpexpzd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛𝑐 2 ) = ( 𝑛 ↑ 2 ) )
80 79 oveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1 / ( 𝑛𝑐 2 ) ) = ( 1 / ( 𝑛 ↑ 2 ) ) )
81 78 80 eqtr2d ( ( 𝜑𝑛 ∈ ℕ ) → ( 1 / ( 𝑛 ↑ 2 ) ) = ( 𝑛𝑐 - 2 ) )
82 81 oveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( 1 / ( 𝑛 ↑ 2 ) ) ) = ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( 𝑛𝑐 - 2 ) ) )
83 76 77 82 3eqtr3d ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) = ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( 𝑛𝑐 - 2 ) ) )
84 34 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) = ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) )
85 56 oveq2d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ‘ 𝑛 ) ) = ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( 𝑛𝑐 - 2 ) ) )
86 83 84 85 3eqtr4d ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) = ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ‘ 𝑛 ) ) )
87 38 39 45 59 65 86 isermulc2 ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ⇝ ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( ⇝ ‘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ) ) )
88 climrel Rel ⇝
89 88 releldmi ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ⇝ ( ( 𝑅 · ( 2 · ( 𝑅 + 1 ) ) ) · ( ⇝ ‘ seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑚𝑐 - 2 ) ) ) ) ) → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ∈ dom ⇝ )
90 87 89 syl ( 𝜑 → seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ∈ dom ⇝ )
91 69 71 75 divcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ∈ ℂ )
92 66 91 mulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) ∈ ℂ )
93 84 92 eqeltrd ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ‘ 𝑛 ) ∈ ℂ )
94 38 7 93 iserex ( 𝜑 → ( seq 1 ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ∈ dom ⇝ ↔ seq ( 2 · 𝑅 ) ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ∈ dom ⇝ ) )
95 90 94 mpbid ( 𝜑 → seq ( 2 · 𝑅 ) ( + , ( 𝑚 ∈ ℕ ↦ ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑚 ↑ 2 ) ) ) ) ) ∈ dom ⇝ )
96 37 95 eqeltrd ( 𝜑 → seq ( 2 · 𝑅 ) ( + , 𝑇 ) ∈ dom ⇝ )
97 31 adantl ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑇𝑛 ) = if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) )
98 1 adantr ( ( 𝜑𝑛 ∈ ℕ ) → 𝑅 ∈ ℕ )
99 98 nnred ( ( 𝜑𝑛 ∈ ℕ ) → 𝑅 ∈ ℝ )
100 47 a1i ( ( 𝜑𝑛 ∈ ℕ ) → 2 ∈ ℝ )
101 1red ( ( 𝜑𝑛 ∈ ℕ ) → 1 ∈ ℝ )
102 99 101 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℝ )
103 100 102 remulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 2 · ( 𝑅 + 1 ) ) ∈ ℝ )
104 60 nnsqcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛 ↑ 2 ) ∈ ℕ )
105 103 104 nndivred ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ∈ ℝ )
106 99 105 remulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) ∈ ℝ )
107 60 peano2nnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℕ )
108 107 nnrpd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑛 + 1 ) ∈ ℝ+ )
109 60 nnrpd ( ( 𝜑𝑛 ∈ ℕ ) → 𝑛 ∈ ℝ+ )
110 108 109 rpdivcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) / 𝑛 ) ∈ ℝ+ )
111 110 relogcld ( ( 𝜑𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ∈ ℝ )
112 99 111 remulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) ∈ ℝ )
113 98 peano2nnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℕ )
114 113 nnrpd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑅 + 1 ) ∈ ℝ+ )
115 114 109 rpmulcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 + 1 ) · 𝑛 ) ∈ ℝ+ )
116 115 relogcld ( ( 𝜑𝑛 ∈ ℕ ) → ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) ∈ ℝ )
117 pire π ∈ ℝ
118 117 a1i ( ( 𝜑𝑛 ∈ ℕ ) → π ∈ ℝ )
119 116 118 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ∈ ℝ )
120 112 119 readdcld ( ( 𝜑𝑛 ∈ ℕ ) → ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ∈ ℝ )
121 106 120 ifcld ( ( 𝜑𝑛 ∈ ℕ ) → if ( ( 2 · 𝑅 ) ≤ 𝑛 , ( 𝑅 · ( ( 2 · ( 𝑅 + 1 ) ) / ( 𝑛 ↑ 2 ) ) ) , ( ( 𝑅 · ( log ‘ ( ( 𝑛 + 1 ) / 𝑛 ) ) ) + ( ( log ‘ ( ( 𝑅 + 1 ) · 𝑛 ) ) + π ) ) ) ∈ ℝ )
122 97 121 eqeltrd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑇𝑛 ) ∈ ℝ )
123 122 recnd ( ( 𝜑𝑛 ∈ ℕ ) → ( 𝑇𝑛 ) ∈ ℂ )
124 38 7 123 iserex ( 𝜑 → ( seq 1 ( + , 𝑇 ) ∈ dom ⇝ ↔ seq ( 2 · 𝑅 ) ( + , 𝑇 ) ∈ dom ⇝ ) )
125 96 124 mpbird ( 𝜑 → seq 1 ( + , 𝑇 ) ∈ dom ⇝ )