Step | Hyp | Ref
| Expression |
1 | | 2nn 11782 |
. . . . . . 7
⊢ 2 ∈
ℕ |
2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 2 ∈
ℕ) |
3 | | lgamgulm.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ ℕ) |
4 | 2, 3 | nnmulcld 11762 |
. . . . 5
⊢ (𝜑 → (2 · 𝑅) ∈
ℕ) |
5 | 4 | nnzd 12160 |
. . . 4
⊢ (𝜑 → (2 · 𝑅) ∈
ℤ) |
6 | | eluzle 12330 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘(2 · 𝑅)) → (2 · 𝑅) ≤ 𝑛) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) → (2
· 𝑅) ≤ 𝑛) |
8 | 7 | iftrued 4419 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) → if((2
· 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
9 | | eluznn 12393 |
. . . . . . 7
⊢ (((2
· 𝑅) ∈ ℕ
∧ 𝑛 ∈
(ℤ≥‘(2 · 𝑅))) → 𝑛 ∈ ℕ) |
10 | 4, 9 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) → 𝑛 ∈
ℕ) |
11 | | breq2 5031 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((2 · 𝑅) ≤ 𝑚 ↔ (2 · 𝑅) ≤ 𝑛)) |
12 | | oveq1 7171 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑚↑2) = (𝑛↑2)) |
13 | 12 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((2 · (𝑅 + 1)) / (𝑚↑2)) = ((2 · (𝑅 + 1)) / (𝑛↑2))) |
14 | 13 | oveq2d 7180 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
15 | | oveq1 7171 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
16 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑚 = 𝑛 → 𝑚 = 𝑛) |
17 | 15, 16 | oveq12d 7182 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑚 + 1) / 𝑚) = ((𝑛 + 1) / 𝑛)) |
18 | 17 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑚 + 1) / 𝑚)) = (log‘((𝑛 + 1) / 𝑛))) |
19 | 18 | oveq2d 7180 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝑅 · (log‘((𝑚 + 1) / 𝑚))) = (𝑅 · (log‘((𝑛 + 1) / 𝑛)))) |
20 | | oveq2 7172 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → ((𝑅 + 1) · 𝑚) = ((𝑅 + 1) · 𝑛)) |
21 | 20 | fveq2d 6672 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (log‘((𝑅 + 1) · 𝑚)) = (log‘((𝑅 + 1) · 𝑛))) |
22 | 21 | oveq1d 7179 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → ((log‘((𝑅 + 1) · 𝑚)) + π) = ((log‘((𝑅 + 1) · 𝑛)) + π)) |
23 | 19, 22 | oveq12d 7182 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)) = ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) |
24 | 11, 14, 23 | ifbieq12d 4439 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π))) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
25 | | lgamgulm.t |
. . . . . . 7
⊢ 𝑇 = (𝑚 ∈ ℕ ↦ if((2 · 𝑅) ≤ 𝑚, (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))), ((𝑅 · (log‘((𝑚 + 1) / 𝑚))) + ((log‘((𝑅 + 1) · 𝑚)) + π)))) |
26 | | ovex 7197 |
. . . . . . . 8
⊢ (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ V |
27 | | ovex 7197 |
. . . . . . . 8
⊢ ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ V |
28 | 26, 27 | ifex 4461 |
. . . . . . 7
⊢ if((2
· 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ V |
29 | 24, 25, 28 | fvmpt 6769 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
30 | 10, 29 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
31 | | eqid 2738 |
. . . . . . 7
⊢ (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2)))) = (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2)))) |
32 | 14, 31, 26 | fvmpt 6769 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
33 | 10, 32 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) →
((𝑚 ∈ ℕ ↦
(𝑅 · ((2 ·
(𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
34 | 8, 30, 33 | 3eqtr4d 2783 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘(2
· 𝑅))) → (𝑇‘𝑛) = ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛)) |
35 | 5, 34 | seqfeq 13480 |
. . 3
⊢ (𝜑 → seq(2 · 𝑅)( + , 𝑇) = seq(2 · 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2)))))) |
36 | | nnuz 12356 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
37 | | 1zzd 12087 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℤ) |
38 | 3 | nncnd 11725 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) |
39 | | 2cnd 11787 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℂ) |
40 | | 1cnd 10707 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℂ) |
41 | 38, 40 | addcld 10731 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 + 1) ∈ ℂ) |
42 | 39, 41 | mulcld 10732 |
. . . . . . 7
⊢ (𝜑 → (2 · (𝑅 + 1)) ∈
ℂ) |
43 | 38, 42 | mulcld 10732 |
. . . . . 6
⊢ (𝜑 → (𝑅 · (2 · (𝑅 + 1))) ∈ ℂ) |
44 | | 1lt2 11880 |
. . . . . . . . . 10
⊢ 1 <
2 |
45 | | 2re 11783 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
46 | | rere 14564 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ → (ℜ‘2) = 2) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℜ‘2) = 2 |
48 | 44, 47 | breqtrri 5054 |
. . . . . . . . 9
⊢ 1 <
(ℜ‘2) |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 <
(ℜ‘2)) |
50 | | oveq1 7171 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑚↑𝑐-2) = (𝑛↑𝑐-2)) |
51 | | eqid 2738 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2)) =
(𝑚 ∈ ℕ ↦
(𝑚↑𝑐-2)) |
52 | | ovex 7197 |
. . . . . . . . . 10
⊢ (𝑛↑𝑐-2)
∈ V |
53 | 50, 51, 52 | fvmpt 6769 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → ((𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))‘𝑛) = (𝑛↑𝑐-2)) |
54 | 53 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))‘𝑛) = (𝑛↑𝑐-2)) |
55 | 39, 49, 54 | zetacvg 25744 |
. . . . . . 7
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2)))
∈ dom ⇝ ) |
56 | | climdm 14994 |
. . . . . . 7
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
(𝑚↑𝑐-2))) ∈ dom
⇝ ↔ seq1( + , (𝑚
∈ ℕ ↦ (𝑚↑𝑐-2))) ⇝ (
⇝ ‘seq1( + , (𝑚
∈ ℕ ↦ (𝑚↑𝑐-2))))) |
57 | 55, 56 | sylib 221 |
. . . . . 6
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2)))
⇝ ( ⇝ ‘seq1( + , (𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))))) |
58 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ) |
59 | 58 | nncnd 11725 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℂ) |
60 | | 2cnd 11787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈
ℂ) |
61 | 60 | negcld 11055 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → -2 ∈
ℂ) |
62 | 59, 61 | cxpcld 25443 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑𝑐-2) ∈
ℂ) |
63 | 54, 62 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))‘𝑛) ∈
ℂ) |
64 | 38 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℂ) |
65 | | 1cnd 10707 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℂ) |
66 | 64, 65 | addcld 10731 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℂ) |
67 | 60, 66 | mulcld 10732 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · (𝑅 + 1)) ∈
ℂ) |
68 | 64, 67 | mulcld 10732 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · (2 · (𝑅 + 1))) ∈ ℂ) |
69 | 59 | sqcld 13593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ∈ ℂ) |
70 | 58 | nnne0d 11759 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ≠ 0) |
71 | | 2z 12088 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
72 | 71 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈
ℤ) |
73 | 59, 70, 72 | expne0d 13601 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ≠ 0) |
74 | 68, 69, 73 | divrecd 11490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) / (𝑛↑2)) = ((𝑅 · (2 · (𝑅 + 1))) · (1 / (𝑛↑2)))) |
75 | 64, 67, 69, 73 | divassd 11522 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) / (𝑛↑2)) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
76 | 59, 70, 60 | cxpnegd 25450 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑𝑐-2) = (1 / (𝑛↑𝑐2))) |
77 | 59, 70, 72 | cxpexpzd 25446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑𝑐2) = (𝑛↑2)) |
78 | 77 | oveq2d 7180 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / (𝑛↑𝑐2)) =
(1 / (𝑛↑2))) |
79 | 76, 78 | eqtr2d 2774 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (1 / (𝑛↑2)) = (𝑛↑𝑐-2)) |
80 | 79 | oveq2d 7180 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) · (1 / (𝑛↑2))) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑𝑐-2))) |
81 | 74, 75, 80 | 3eqtr3d 2781 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑𝑐-2))) |
82 | 32 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2)))) |
83 | 54 | oveq2d 7180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (2 · (𝑅 + 1))) · ((𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))‘𝑛)) = ((𝑅 · (2 · (𝑅 + 1))) · (𝑛↑𝑐-2))) |
84 | 81, 82, 83 | 3eqtr4d 2783 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) = ((𝑅 · (2 · (𝑅 + 1))) · ((𝑚 ∈ ℕ ↦ (𝑚↑𝑐-2))‘𝑛))) |
85 | 36, 37, 43, 57, 63, 84 | isermulc2 15100 |
. . . . 5
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ⇝ ((𝑅 · (2 · (𝑅 + 1))) · ( ⇝ ‘seq1( + ,
(𝑚 ∈ ℕ ↦
(𝑚↑𝑐-2)))))) |
86 | | climrel 14932 |
. . . . . 6
⊢ Rel
⇝ |
87 | 86 | releldmi 5785 |
. . . . 5
⊢ (seq1( +
, (𝑚 ∈ ℕ ↦
(𝑅 · ((2 ·
(𝑅 + 1)) / (𝑚↑2))))) ⇝ ((𝑅 · (2 · (𝑅 + 1))) · ( ⇝
‘seq1( + , (𝑚 ∈
ℕ ↦ (𝑚↑𝑐-2))))) →
seq1( + , (𝑚 ∈ ℕ
↦ (𝑅 · ((2
· (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝
) |
88 | 85, 87 | syl 17 |
. . . 4
⊢ (𝜑 → seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝
) |
89 | 67, 69, 73 | divcld 11487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2 · (𝑅 + 1)) / (𝑛↑2)) ∈ ℂ) |
90 | 64, 89 | mulcld 10732 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ ℂ) |
91 | 82, 90 | eqeltrd 2833 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))‘𝑛) ∈ ℂ) |
92 | 36, 4, 91 | iserex 15099 |
. . . 4
⊢ (𝜑 → (seq1( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝ ↔ seq(2
· 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝
)) |
93 | 88, 92 | mpbid 235 |
. . 3
⊢ (𝜑 → seq(2 · 𝑅)( + , (𝑚 ∈ ℕ ↦ (𝑅 · ((2 · (𝑅 + 1)) / (𝑚↑2))))) ∈ dom ⇝
) |
94 | 35, 93 | eqeltrd 2833 |
. 2
⊢ (𝜑 → seq(2 · 𝑅)( + , 𝑇) ∈ dom ⇝ ) |
95 | 29 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) = if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)))) |
96 | 3 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℕ) |
97 | 96 | nnred 11724 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑅 ∈ ℝ) |
98 | 45 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 2 ∈
ℝ) |
99 | | 1red 10713 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 1 ∈
ℝ) |
100 | 97, 99 | readdcld 10741 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℝ) |
101 | 98, 100 | remulcld 10742 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (2 · (𝑅 + 1)) ∈
ℝ) |
102 | 58 | nnsqcld 13690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛↑2) ∈ ℕ) |
103 | 101, 102 | nndivred 11763 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((2 · (𝑅 + 1)) / (𝑛↑2)) ∈ ℝ) |
104 | 97, 103 | remulcld 10742 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))) ∈ ℝ) |
105 | 58 | peano2nnd 11726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈ ℕ) |
106 | 105 | nnrpd 12505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑛 + 1) ∈
ℝ+) |
107 | 58 | nnrpd 12505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℝ+) |
108 | 106, 107 | rpdivcld 12524 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑛 + 1) / 𝑛) ∈
ℝ+) |
109 | 108 | relogcld 25358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑛 + 1) / 𝑛)) ∈ ℝ) |
110 | 97, 109 | remulcld 10742 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 · (log‘((𝑛 + 1) / 𝑛))) ∈ ℝ) |
111 | 96 | peano2nnd 11726 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈ ℕ) |
112 | 111 | nnrpd 12505 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑅 + 1) ∈
ℝ+) |
113 | 112, 107 | rpmulcld 12523 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 + 1) · 𝑛) ∈
ℝ+) |
114 | 113 | relogcld 25358 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (log‘((𝑅 + 1) · 𝑛)) ∈
ℝ) |
115 | | pire 25195 |
. . . . . . . . 9
⊢ π
∈ ℝ |
116 | 115 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → π ∈
ℝ) |
117 | 114, 116 | readdcld 10741 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((log‘((𝑅 + 1) · 𝑛)) + π) ∈
ℝ) |
118 | 110, 117 | readdcld 10741 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π)) ∈ ℝ) |
119 | 104, 118 | ifcld 4457 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → if((2 · 𝑅) ≤ 𝑛, (𝑅 · ((2 · (𝑅 + 1)) / (𝑛↑2))), ((𝑅 · (log‘((𝑛 + 1) / 𝑛))) + ((log‘((𝑅 + 1) · 𝑛)) + π))) ∈ ℝ) |
120 | 95, 119 | eqeltrd 2833 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) ∈ ℝ) |
121 | 120 | recnd 10740 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝑇‘𝑛) ∈ ℂ) |
122 | 36, 4, 121 | iserex 15099 |
. 2
⊢ (𝜑 → (seq1( + , 𝑇) ∈ dom ⇝ ↔
seq(2 · 𝑅)( + ,
𝑇) ∈ dom ⇝
)) |
123 | 94, 122 | mpbird 260 |
1
⊢ (𝜑 → seq1( + , 𝑇) ∈ dom ⇝
) |