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 ⇝ )