Step | Hyp | Ref
| Expression |
1 | | 2nn 12231 |
. . . . . . 7
โข 2 โ
โ |
2 | 1 | a1i 11 |
. . . . . 6
โข (๐ โ 2 โ
โ) |
3 | | lgamgulm.r |
. . . . . 6
โข (๐ โ ๐
โ โ) |
4 | 2, 3 | nnmulcld 12211 |
. . . . 5
โข (๐ โ (2 ยท ๐
) โ
โ) |
5 | 4 | nnzd 12531 |
. . . 4
โข (๐ โ (2 ยท ๐
) โ
โค) |
6 | | eluzle 12781 |
. . . . . . 7
โข (๐ โ
(โคโฅโ(2 ยท ๐
)) โ (2 ยท ๐
) โค ๐) |
7 | 6 | adantl 483 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(2
ยท ๐
))) โ (2
ยท ๐
) โค ๐) |
8 | 7 | iftrued 4495 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ(2
ยท ๐
))) โ if((2
ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) = (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
9 | | eluznn 12848 |
. . . . . . 7
โข (((2
ยท ๐
) โ โ
โง ๐ โ
(โคโฅโ(2 ยท ๐
))) โ ๐ โ โ) |
10 | 4, 9 | sylan 581 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ(2
ยท ๐
))) โ ๐ โ
โ) |
11 | | breq2 5110 |
. . . . . . . 8
โข (๐ = ๐ โ ((2 ยท ๐
) โค ๐ โ (2 ยท ๐
) โค ๐)) |
12 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ2) = (๐โ2)) |
13 | 12 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ๐ โ ((2 ยท (๐
+ 1)) / (๐โ2)) = ((2 ยท (๐
+ 1)) / (๐โ2))) |
14 | 13 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) = (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
15 | | oveq1 7365 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (๐ + 1) = (๐ + 1)) |
16 | | id 22 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ๐ = ๐) |
17 | 15, 16 | oveq12d 7376 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐ + 1) / ๐) = ((๐ + 1) / ๐)) |
18 | 17 | fveq2d 6847 |
. . . . . . . . . 10
โข (๐ = ๐ โ (logโ((๐ + 1) / ๐)) = (logโ((๐ + 1) / ๐))) |
19 | 18 | oveq2d 7374 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐
ยท (logโ((๐ + 1) / ๐))) = (๐
ยท (logโ((๐ + 1) / ๐)))) |
20 | | oveq2 7366 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐
+ 1) ยท ๐) = ((๐
+ 1) ยท ๐)) |
21 | 20 | fveq2d 6847 |
. . . . . . . . . 10
โข (๐ = ๐ โ (logโ((๐
+ 1) ยท ๐)) = (logโ((๐
+ 1) ยท ๐))) |
22 | 21 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ = ๐ โ ((logโ((๐
+ 1) ยท ๐)) + ฯ) = ((logโ((๐
+ 1) ยท ๐)) + ฯ)) |
23 | 19, 22 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) = ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) |
24 | 11, 14, 23 | ifbieq12d 4515 |
. . . . . . 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 7391 |
. . . . . . . 8
โข (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ V |
27 | | ovex 7391 |
. . . . . . . 8
โข ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) โ V |
28 | 26, 27 | ifex 4537 |
. . . . . . 7
โข if((2
ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) โ V |
29 | 24, 25, 28 | fvmpt 6949 |
. . . . . 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 2733 |
. . . . . . 7
โข (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) = (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
32 | 14, 31, 26 | fvmpt 6949 |
. . . . . 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 13939 |
. . 3
โข (๐ โ seq(2 ยท ๐
)( + , ๐) = seq(2 ยท ๐
)( + , (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))))) |
36 | | nnuz 12811 |
. . . . . 6
โข โ =
(โคโฅโ1) |
37 | | 1zzd 12539 |
. . . . . 6
โข (๐ โ 1 โ
โค) |
38 | 3 | nncnd 12174 |
. . . . . . 7
โข (๐ โ ๐
โ โ) |
39 | | 2cnd 12236 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
40 | | 1cnd 11155 |
. . . . . . . . 9
โข (๐ โ 1 โ
โ) |
41 | 38, 40 | addcld 11179 |
. . . . . . . 8
โข (๐ โ (๐
+ 1) โ โ) |
42 | 39, 41 | mulcld 11180 |
. . . . . . 7
โข (๐ โ (2 ยท (๐
+ 1)) โ
โ) |
43 | 38, 42 | mulcld 11180 |
. . . . . 6
โข (๐ โ (๐
ยท (2 ยท (๐
+ 1))) โ โ) |
44 | | 1lt2 12329 |
. . . . . . . . . 10
โข 1 <
2 |
45 | | 2re 12232 |
. . . . . . . . . . 11
โข 2 โ
โ |
46 | | rere 15013 |
. . . . . . . . . . 11
โข (2 โ
โ โ (โโ2) = 2) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . . . 10
โข
(โโ2) = 2 |
48 | 44, 47 | breqtrri 5133 |
. . . . . . . . 9
โข 1 <
(โโ2) |
49 | 48 | a1i 11 |
. . . . . . . 8
โข (๐ โ 1 <
(โโ2)) |
50 | | oveq1 7365 |
. . . . . . . . . 10
โข (๐ = ๐ โ (๐โ๐-2) = (๐โ๐-2)) |
51 | | eqid 2733 |
. . . . . . . . . 10
โข (๐ โ โ โฆ (๐โ๐-2)) =
(๐ โ โ โฆ
(๐โ๐-2)) |
52 | | ovex 7391 |
. . . . . . . . . 10
โข (๐โ๐-2)
โ V |
53 | 50, 51, 52 | fvmpt 6949 |
. . . . . . . . 9
โข (๐ โ โ โ ((๐ โ โ โฆ (๐โ๐-2))โ๐) = (๐โ๐-2)) |
54 | 53 | adantl 483 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-2))โ๐) = (๐โ๐-2)) |
55 | 39, 49, 54 | zetacvg 26380 |
. . . . . . 7
โข (๐ โ seq1( + , (๐ โ โ โฆ (๐โ๐-2)))
โ dom โ ) |
56 | | climdm 15442 |
. . . . . . 7
โข (seq1( +
, (๐ โ โ โฆ
(๐โ๐-2))) โ dom
โ โ seq1( + , (๐
โ โ โฆ (๐โ๐-2))) โ (
โ โseq1( + , (๐
โ โ โฆ (๐โ๐-2))))) |
57 | 55, 56 | sylib 217 |
. . . . . 6
โข (๐ โ seq1( + , (๐ โ โ โฆ (๐โ๐-2)))
โ ( โ โseq1( + , (๐ โ โ โฆ (๐โ๐-2))))) |
58 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
59 | 58 | nncnd 12174 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
60 | | 2cnd 12236 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ 2 โ
โ) |
61 | 60 | negcld 11504 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ -2 โ
โ) |
62 | 59, 61 | cxpcld 26079 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐โ๐-2) โ
โ) |
63 | 54, 62 | eqeltrd 2834 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐โ๐-2))โ๐) โ
โ) |
64 | 38 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐
โ โ) |
65 | | 1cnd 11155 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ โ) โ 1 โ
โ) |
66 | 64, 65 | addcld 11179 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐
+ 1) โ โ) |
67 | 60, 66 | mulcld 11180 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (2 ยท (๐
+ 1)) โ
โ) |
68 | 64, 67 | mulcld 11180 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐
ยท (2 ยท (๐
+ 1))) โ โ) |
69 | 59 | sqcld 14055 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐โ2) โ โ) |
70 | 58 | nnne0d 12208 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐ โ 0) |
71 | | 2z 12540 |
. . . . . . . . . . 11
โข 2 โ
โค |
72 | 71 | a1i 11 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ 2 โ
โค) |
73 | 59, 70, 72 | expne0d 14063 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐โ2) โ 0) |
74 | 68, 69, 73 | divrecd 11939 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐
ยท (2 ยท (๐
+ 1))) / (๐โ2)) = ((๐
ยท (2 ยท (๐
+ 1))) ยท (1 / (๐โ2)))) |
75 | 64, 67, 69, 73 | divassd 11971 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐
ยท (2 ยท (๐
+ 1))) / (๐โ2)) = (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
76 | 59, 70, 60 | cxpnegd 26086 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐โ๐-2) = (1 / (๐โ๐2))) |
77 | 59, 70, 72 | cxpexpzd 26082 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐โ๐2) = (๐โ2)) |
78 | 77 | oveq2d 7374 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (1 / (๐โ๐2)) =
(1 / (๐โ2))) |
79 | 76, 78 | eqtr2d 2774 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (1 / (๐โ2)) = (๐โ๐-2)) |
80 | 79 | oveq2d 7374 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ((๐
ยท (2 ยท (๐
+ 1))) ยท (1 / (๐โ2))) = ((๐
ยท (2 ยท (๐
+ 1))) ยท (๐โ๐-2))) |
81 | 74, 75, 80 | 3eqtr3d 2781 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) = ((๐
ยท (2 ยท (๐
+ 1))) ยท (๐โ๐-2))) |
82 | 32 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))โ๐) = (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2)))) |
83 | 54 | oveq2d 7374 |
. . . . . . 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 15548 |
. . . . 5
โข (๐ โ seq1( + , (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))) โ ((๐
ยท (2 ยท (๐
+ 1))) ยท ( โ โseq1( + ,
(๐ โ โ โฆ
(๐โ๐-2)))))) |
86 | | climrel 15380 |
. . . . . 6
โข Rel
โ |
87 | 86 | releldmi 5904 |
. . . . 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 11936 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((2 ยท (๐
+ 1)) / (๐โ2)) โ โ) |
90 | 64, 89 | mulcld 11180 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ โ) |
91 | 82, 90 | eqeltrd 2834 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ ((๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))โ๐) โ โ) |
92 | 36, 4, 91 | iserex 15547 |
. . . 4
โข (๐ โ (seq1( + , (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))) โ dom โ โ seq(2
ยท ๐
)( + , (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))) โ dom โ
)) |
93 | 88, 92 | mpbid 231 |
. . 3
โข (๐ โ seq(2 ยท ๐
)( + , (๐ โ โ โฆ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))))) โ dom โ
) |
94 | 35, 93 | eqeltrd 2834 |
. 2
โข (๐ โ seq(2 ยท ๐
)( + , ๐) โ dom โ ) |
95 | 29 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (๐โ๐) = if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)))) |
96 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐
โ โ) |
97 | 96 | nnred 12173 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ๐
โ โ) |
98 | 45 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ 2 โ
โ) |
99 | | 1red 11161 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ 1 โ
โ) |
100 | 97, 99 | readdcld 11189 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (๐
+ 1) โ โ) |
101 | 98, 100 | remulcld 11190 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (2 ยท (๐
+ 1)) โ
โ) |
102 | 58 | nnsqcld 14153 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (๐โ2) โ โ) |
103 | 101, 102 | nndivred 12212 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((2 ยท (๐
+ 1)) / (๐โ2)) โ โ) |
104 | 97, 103 | remulcld 11190 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))) โ โ) |
105 | 58 | peano2nnd 12175 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ โ) |
106 | 105 | nnrpd 12960 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐ + 1) โ
โ+) |
107 | 58 | nnrpd 12960 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐ โ โ+) |
108 | 106, 107 | rpdivcld 12979 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((๐ + 1) / ๐) โ
โ+) |
109 | 108 | relogcld 25994 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (logโ((๐ + 1) / ๐)) โ โ) |
110 | 97, 109 | remulcld 11190 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (๐
ยท (logโ((๐ + 1) / ๐))) โ โ) |
111 | 96 | peano2nnd 12175 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐
+ 1) โ โ) |
112 | 111 | nnrpd 12960 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (๐
+ 1) โ
โ+) |
113 | 112, 107 | rpmulcld 12978 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((๐
+ 1) ยท ๐) โ
โ+) |
114 | 113 | relogcld 25994 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (logโ((๐
+ 1) ยท ๐)) โ
โ) |
115 | | pire 25831 |
. . . . . . . . 9
โข ฯ
โ โ |
116 | 115 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ฯ โ
โ) |
117 | 114, 116 | readdcld 11189 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((logโ((๐
+ 1) ยท ๐)) + ฯ) โ
โ) |
118 | 110, 117 | readdcld 11189 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ)) โ โ) |
119 | 104, 118 | ifcld 4533 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ if((2 ยท ๐
) โค ๐, (๐
ยท ((2 ยท (๐
+ 1)) / (๐โ2))), ((๐
ยท (logโ((๐ + 1) / ๐))) + ((logโ((๐
+ 1) ยท ๐)) + ฯ))) โ โ) |
120 | 95, 119 | eqeltrd 2834 |
. . . 4
โข ((๐ โง ๐ โ โ) โ (๐โ๐) โ โ) |
121 | 120 | recnd 11188 |
. . 3
โข ((๐ โง ๐ โ โ) โ (๐โ๐) โ โ) |
122 | 36, 4, 121 | iserex 15547 |
. 2
โข (๐ โ (seq1( + , ๐) โ dom โ โ
seq(2 ยท ๐
)( + ,
๐) โ dom โ
)) |
123 | 94, 122 | mpbird 257 |
1
โข (๐ โ seq1( + , ๐) โ dom โ
) |