Step | Hyp | Ref
| Expression |
1 | | hgt750leme.n |
. . . . . 6
β’ (π β π β β) |
2 | 1 | nnnn0d 12529 |
. . . . 5
β’ (π β π β
β0) |
3 | | 3nn0 12487 |
. . . . . 6
β’ 3 β
β0 |
4 | 3 | a1i 11 |
. . . . 5
β’ (π β 3 β
β0) |
5 | | ssidd 4005 |
. . . . 5
β’ (π β β β
β) |
6 | 2, 4, 5 | reprfi2 33624 |
. . . 4
β’ (π β
(β(reprβ3)π)
β Fin) |
7 | | diffi 9176 |
. . . 4
β’
((β(reprβ3)π) β Fin β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))
β Fin) |
8 | 6, 7 | syl 17 |
. . 3
β’ (π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))
β Fin) |
9 | | vmaf 26613 |
. . . . . . 7
β’
Ξ:ββΆβ |
10 | 9 | a1i 11 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
Ξ:ββΆβ) |
11 | | ssidd 4005 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β β β
β) |
12 | 1 | nnzd 12582 |
. . . . . . . . 9
β’ (π β π β β€) |
13 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π β β€) |
14 | 3 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β 3 β
β0) |
15 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) |
16 | 15 | eldifad 3960 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π β (β(reprβ3)π)) |
17 | 11, 13, 14, 16 | reprf 33613 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π:(0..^3)βΆβ) |
18 | | c0ex 11205 |
. . . . . . . . . 10
β’ 0 β
V |
19 | 18 | tpid1 4772 |
. . . . . . . . 9
β’ 0 β
{0, 1, 2} |
20 | | fzo0to3tp 13715 |
. . . . . . . . 9
β’ (0..^3) =
{0, 1, 2} |
21 | 19, 20 | eleqtrri 2833 |
. . . . . . . 8
β’ 0 β
(0..^3) |
22 | 21 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β 0 β
(0..^3)) |
23 | 17, 22 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πβ0) β β) |
24 | 10, 23 | ffvelcdmd 7085 |
. . . . 5
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(Ξβ(πβ0)) β β) |
25 | | rge0ssre 13430 |
. . . . . 6
β’
(0[,)+β) β β |
26 | | hgt750leme.h |
. . . . . . . 8
β’ (π β π»:ββΆ(0[,)+β)) |
27 | 26 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β π»:ββΆ(0[,)+β)) |
28 | 27, 23 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (π»β(πβ0)) β
(0[,)+β)) |
29 | 25, 28 | sselid 3980 |
. . . . 5
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (π»β(πβ0)) β β) |
30 | 24, 29 | remulcld 11241 |
. . . 4
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
((Ξβ(πβ0)) Β· (π»β(πβ0))) β β) |
31 | | 1ex 11207 |
. . . . . . . . . . 11
β’ 1 β
V |
32 | 31 | tpid2 4774 |
. . . . . . . . . 10
β’ 1 β
{0, 1, 2} |
33 | 32, 20 | eleqtrri 2833 |
. . . . . . . . 9
β’ 1 β
(0..^3) |
34 | 33 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β 1 β
(0..^3)) |
35 | 17, 34 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πβ1) β β) |
36 | 10, 35 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(Ξβ(πβ1)) β β) |
37 | | hgt750leme.k |
. . . . . . . . 9
β’ (π β πΎ:ββΆ(0[,)+β)) |
38 | 37 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β πΎ:ββΆ(0[,)+β)) |
39 | 38, 35 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πΎβ(πβ1)) β
(0[,)+β)) |
40 | 25, 39 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πΎβ(πβ1)) β β) |
41 | 36, 40 | remulcld 11241 |
. . . . 5
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
((Ξβ(πβ1)) Β· (πΎβ(πβ1))) β β) |
42 | | 2ex 12286 |
. . . . . . . . . . 11
β’ 2 β
V |
43 | 42 | tpid3 4777 |
. . . . . . . . . 10
β’ 2 β
{0, 1, 2} |
44 | 43, 20 | eleqtrri 2833 |
. . . . . . . . 9
β’ 2 β
(0..^3) |
45 | 44 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β 2 β
(0..^3)) |
46 | 17, 45 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πβ2) β β) |
47 | 10, 46 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(Ξβ(πβ2)) β β) |
48 | 38, 46 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πΎβ(πβ2)) β
(0[,)+β)) |
49 | 25, 48 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β (πΎβ(πβ2)) β β) |
50 | 47, 49 | remulcld 11241 |
. . . . 5
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
((Ξβ(πβ2)) Β· (πΎβ(πβ2))) β β) |
51 | 41, 50 | remulcld 11241 |
. . . 4
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2)))) β β) |
52 | 30, 51 | remulcld 11241 |
. . 3
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
53 | 8, 52 | fsumrecl 15677 |
. 2
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β
β) |
54 | | 3re 12289 |
. . . 4
β’ 3 β
β |
55 | 54 | a1i 11 |
. . 3
β’ (π β 3 β
β) |
56 | | 1nn0 12485 |
. . . . . . . . 9
β’ 1 β
β0 |
57 | | 0nn0 12484 |
. . . . . . . . . 10
β’ 0 β
β0 |
58 | | 7nn0 12491 |
. . . . . . . . . . 11
β’ 7 β
β0 |
59 | | 9nn0 12493 |
. . . . . . . . . . . 12
β’ 9 β
β0 |
60 | | 5nn0 12489 |
. . . . . . . . . . . . . 14
β’ 5 β
β0 |
61 | | 5nn 12295 |
. . . . . . . . . . . . . . 15
β’ 5 β
β |
62 | | nnrp 12982 |
. . . . . . . . . . . . . . 15
β’ (5 β
β β 5 β β+) |
63 | 61, 62 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ 5 β
β+ |
64 | 60, 63 | rpdp2cl 32036 |
. . . . . . . . . . . . 13
β’ _55 β
β+ |
65 | 59, 64 | rpdp2cl 32036 |
. . . . . . . . . . . 12
β’ _9_55 β β+ |
66 | 59, 65 | rpdp2cl 32036 |
. . . . . . . . . . 11
β’ _9_9_55
β β+ |
67 | 58, 66 | rpdp2cl 32036 |
. . . . . . . . . 10
β’ _7_9_9_55
β β+ |
68 | 57, 67 | rpdp2cl 32036 |
. . . . . . . . 9
β’ _0_7_9_9_55
β β+ |
69 | 56, 68 | rpdpcl 32057 |
. . . . . . . 8
β’ (1._0_7_9_9_55)
β β+ |
70 | 69 | a1i 11 |
. . . . . . 7
β’ (π β (1._0_7_9_9_55)
β β+) |
71 | 70 | rpred 13013 |
. . . . . 6
β’ (π β (1._0_7_9_9_55)
β β) |
72 | 71 | resqcld 14087 |
. . . . 5
β’ (π β ((1._0_7_9_9_55)β2) β β) |
73 | | 4nn0 12488 |
. . . . . . . . 9
β’ 4 β
β0 |
74 | | 4nn 12292 |
. . . . . . . . . . 11
β’ 4 β
β |
75 | | nnrp 12982 |
. . . . . . . . . . 11
β’ (4 β
β β 4 β β+) |
76 | 74, 75 | ax-mp 5 |
. . . . . . . . . 10
β’ 4 β
β+ |
77 | 56, 76 | rpdp2cl 32036 |
. . . . . . . . 9
β’ _14 β
β+ |
78 | 73, 77 | rpdp2cl 32036 |
. . . . . . . 8
β’ _4_14 β β+ |
79 | 56, 78 | rpdpcl 32057 |
. . . . . . 7
β’ (1._4_14) β β+ |
80 | 79 | a1i 11 |
. . . . . 6
β’ (π β (1._4_14)
β β+) |
81 | 80 | rpred 13013 |
. . . . 5
β’ (π β (1._4_14)
β β) |
82 | 72, 81 | remulcld 11241 |
. . . 4
β’ (π β (((1._0_7_9_9_55)β2) Β· (1._4_14))
β β) |
83 | | fveq1 6888 |
. . . . . . . . . 10
β’ (π = π β (πβ0) = (πβ0)) |
84 | 83 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = π β ((πβ0) β (π β© β) β (πβ0) β (π β© β))) |
85 | 84 | notbid 318 |
. . . . . . . 8
β’ (π = π β (Β¬ (πβ0) β (π β© β) β Β¬ (πβ0) β (π β©
β))) |
86 | 85 | cbvrabv 3443 |
. . . . . . 7
β’ {π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)} =
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β©
β)} |
87 | 86 | ssrab3 4080 |
. . . . . 6
β’ {π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
β (β(reprβ3)π) |
88 | | ssfi 9170 |
. . . . . 6
β’
(((β(reprβ3)π) β Fin β§ {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)} β
(β(reprβ3)π))
β {π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
β Fin) |
89 | 6, 87, 88 | sylancl 587 |
. . . . 5
β’ (π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)} β
Fin) |
90 | 9 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
Ξ:ββΆβ) |
91 | | ssidd 4005 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β β
β β) |
92 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β π β
β€) |
93 | 3 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β 3
β β0) |
94 | 87 | a1i 11 |
. . . . . . . . . 10
β’ (π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)} β
(β(reprβ3)π)) |
95 | 94 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β π β
(β(reprβ3)π)) |
96 | 91, 92, 93, 95 | reprf 33613 |
. . . . . . . 8
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β π:(0..^3)βΆβ) |
97 | 21 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β 0
β (0..^3)) |
98 | 96, 97 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β (πβ0) β
β) |
99 | 90, 98 | ffvelcdmd 7085 |
. . . . . 6
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
(Ξβ(πβ0)) β β) |
100 | 33 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β 1
β (0..^3)) |
101 | 96, 100 | ffvelcdmd 7085 |
. . . . . . . 8
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β (πβ1) β
β) |
102 | 90, 101 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
(Ξβ(πβ1)) β β) |
103 | 44 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β 2
β (0..^3)) |
104 | 96, 103 | ffvelcdmd 7085 |
. . . . . . . 8
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β (πβ2) β
β) |
105 | 90, 104 | ffvelcdmd 7085 |
. . . . . . 7
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
(Ξβ(πβ2)) β β) |
106 | 102, 105 | remulcld 11241 |
. . . . . 6
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
((Ξβ(πβ1)) Β· (Ξβ(πβ2))) β
β) |
107 | 99, 106 | remulcld 11241 |
. . . . 5
β’ ((π β§ π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}) β
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β β) |
108 | 89, 107 | fsumrecl 15677 |
. . . 4
β’ (π β Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β β) |
109 | 82, 108 | remulcld 11241 |
. . 3
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β
β) |
110 | 55, 109 | remulcld 11241 |
. 2
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) β
β) |
111 | | 4re 12293 |
. . . . . . . . . 10
β’ 4 β
β |
112 | | 8re 12305 |
. . . . . . . . . 10
β’ 8 β
β |
113 | 111, 112 | pm3.2i 472 |
. . . . . . . . 9
β’ (4 β
β β§ 8 β β) |
114 | | dp2cl 32034 |
. . . . . . . . 9
β’ ((4
β β β§ 8 β β) β _48 β β) |
115 | 113, 114 | ax-mp 5 |
. . . . . . . 8
β’ _48 β β |
116 | 54, 115 | pm3.2i 472 |
. . . . . . 7
β’ (3 β
β β§ _48 β
β) |
117 | | dp2cl 32034 |
. . . . . . 7
β’ ((3
β β β§ _48 β
β) β _3_48 β β) |
118 | 116, 117 | ax-mp 5 |
. . . . . 6
β’ _3_48 β β |
119 | | dpcl 32045 |
. . . . . 6
β’ ((7
β β0 β§ _3_48
β β) β (7._3_48) β β) |
120 | 58, 118, 119 | mp2an 691 |
. . . . 5
β’ (7._3_48) β β |
121 | 120 | a1i 11 |
. . . 4
β’ (π β (7._3_48)
β β) |
122 | 1 | nnrpd 13011 |
. . . . . 6
β’ (π β π β
β+) |
123 | 122 | relogcld 26123 |
. . . . 5
β’ (π β (logβπ) β
β) |
124 | 1 | nnred 12224 |
. . . . . 6
β’ (π β π β β) |
125 | 122 | rpge0d 13017 |
. . . . . 6
β’ (π β 0 β€ π) |
126 | 124, 125 | resqrtcld 15361 |
. . . . 5
β’ (π β (ββπ) β
β) |
127 | 122 | rpsqrtcld 15355 |
. . . . . 6
β’ (π β (ββπ) β
β+) |
128 | 127 | rpne0d 13018 |
. . . . 5
β’ (π β (ββπ) β 0) |
129 | 123, 126,
128 | redivcld 12039 |
. . . 4
β’ (π β ((logβπ) / (ββπ)) β
β) |
130 | 121, 129 | remulcld 11241 |
. . 3
β’ (π β ((7._3_48)
Β· ((logβπ) /
(ββπ))) β
β) |
131 | 124 | resqcld 14087 |
. . 3
β’ (π β (πβ2) β β) |
132 | 130, 131 | remulcld 11241 |
. 2
β’ (π β (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2)) β
β) |
133 | | 0re 11213 |
. . . . . . . . . . 11
β’ 0 β
β |
134 | | 7re 12302 |
. . . . . . . . . . . . 13
β’ 7 β
β |
135 | | 9re 12308 |
. . . . . . . . . . . . . . 15
β’ 9 β
β |
136 | | 5re 12296 |
. . . . . . . . . . . . . . . . . . 19
β’ 5 β
β |
137 | 136, 136 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
β’ (5 β
β β§ 5 β β) |
138 | | dp2cl 32034 |
. . . . . . . . . . . . . . . . . 18
β’ ((5
β β β§ 5 β β) β _55 β β) |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ _55 β β |
140 | 135, 139 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’ (9 β
β β§ _55 β
β) |
141 | | dp2cl 32034 |
. . . . . . . . . . . . . . . 16
β’ ((9
β β β§ _55 β
β) β _9_55 β β) |
142 | 140, 141 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ _9_55 β β |
143 | 135, 142 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (9 β
β β§ _9_55 β β) |
144 | | dp2cl 32034 |
. . . . . . . . . . . . . 14
β’ ((9
β β β§ _9_55 β β) β _9_9_55
β β) |
145 | 143, 144 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ _9_9_55
β β |
146 | 134, 145 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (7 β
β β§ _9_9_55
β β) |
147 | | dp2cl 32034 |
. . . . . . . . . . . 12
β’ ((7
β β β§ _9_9_55 β β) β _7_9_9_55
β β) |
148 | 146, 147 | ax-mp 5 |
. . . . . . . . . . 11
β’ _7_9_9_55
β β |
149 | 133, 148 | pm3.2i 472 |
. . . . . . . . . 10
β’ (0 β
β β§ _7_9_9_55
β β) |
150 | | dp2cl 32034 |
. . . . . . . . . 10
β’ ((0
β β β§ _7_9_9_55
β β) β _0_7_9_9_55
β β) |
151 | 149, 150 | ax-mp 5 |
. . . . . . . . 9
β’ _0_7_9_9_55
β β |
152 | | dpcl 32045 |
. . . . . . . . 9
β’ ((1
β β0 β§ _0_7_9_9_55
β β) β (1._0_7_9_9_55)
β β) |
153 | 56, 151, 152 | mp2an 691 |
. . . . . . . 8
β’ (1._0_7_9_9_55)
β β |
154 | 153 | a1i 11 |
. . . . . . 7
β’ (π β (1._0_7_9_9_55)
β β) |
155 | 154 | resqcld 14087 |
. . . . . 6
β’ (π β ((1._0_7_9_9_55)β2) β β) |
156 | | 1re 11211 |
. . . . . . . . . . . 12
β’ 1 β
β |
157 | 156, 111 | pm3.2i 472 |
. . . . . . . . . . 11
β’ (1 β
β β§ 4 β β) |
158 | | dp2cl 32034 |
. . . . . . . . . . 11
β’ ((1
β β β§ 4 β β) β _14 β β) |
159 | 157, 158 | ax-mp 5 |
. . . . . . . . . 10
β’ _14 β β |
160 | 111, 159 | pm3.2i 472 |
. . . . . . . . 9
β’ (4 β
β β§ _14 β
β) |
161 | | dp2cl 32034 |
. . . . . . . . 9
β’ ((4
β β β§ _14 β
β) β _4_14 β β) |
162 | 160, 161 | ax-mp 5 |
. . . . . . . 8
β’ _4_14 β β |
163 | | dpcl 32045 |
. . . . . . . 8
β’ ((1
β β0 β§ _4_14
β β) β (1._4_14) β β) |
164 | 56, 162, 163 | mp2an 691 |
. . . . . . 7
β’ (1._4_14) β β |
165 | 164 | a1i 11 |
. . . . . 6
β’ (π β (1._4_14)
β β) |
166 | 155, 165 | remulcld 11241 |
. . . . 5
β’ (π β (((1._0_7_9_9_55)β2) Β· (1._4_14))
β β) |
167 | 36, 47 | remulcld 11241 |
. . . . . . 7
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
((Ξβ(πβ1)) Β· (Ξβ(πβ2))) β
β) |
168 | 24, 167 | remulcld 11241 |
. . . . . 6
β’ ((π β§ π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))) β
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β β) |
169 | 8, 168 | fsumrecl 15677 |
. . . . 5
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))((Ξβ(πβ0)) Β·
((Ξβ(πβ1)) Β· (Ξβ(πβ2)))) β
β) |
170 | 166, 169 | remulcld 11241 |
. . . 4
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β
β) |
171 | 55, 108 | remulcld 11241 |
. . . . 5
β’ (π β (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β
β) |
172 | 166, 171 | remulcld 11241 |
. . . 4
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) β
β) |
173 | | hgt750leme.1 |
. . . . 5
β’ ((π β§ π β β) β (πΎβπ) β€ (1._0_7_9_9_55)) |
174 | | hgt750leme.2 |
. . . . 5
β’ ((π β§ π β β) β (π»βπ) β€ (1._4_14)) |
175 | 8, 154, 165, 26, 37, 23, 35, 46, 173, 174 | hgt750lemf 33654 |
. . . 4
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) |
176 | | hgt750leme.o |
. . . . . 6
β’ π = {π§ β β€ β£ Β¬ 2 β₯ π§} |
177 | | 2re 12283 |
. . . . . . . 8
β’ 2 β
β |
178 | 177 | a1i 11 |
. . . . . . 7
β’ (π β 2 β
β) |
179 | | 10nn0 12692 |
. . . . . . . . . 10
β’ ;10 β
β0 |
180 | | 2nn0 12486 |
. . . . . . . . . . 11
β’ 2 β
β0 |
181 | 180, 58 | deccl 12689 |
. . . . . . . . . 10
β’ ;27 β
β0 |
182 | 179, 181 | nn0expcli 14051 |
. . . . . . . . 9
β’ (;10β;27) β β0 |
183 | 182 | nn0rei 12480 |
. . . . . . . 8
β’ (;10β;27) β β |
184 | 183 | a1i 11 |
. . . . . . 7
β’ (π β (;10β;27) β β) |
185 | 179 | numexp1 17007 |
. . . . . . . . . 10
β’ (;10β1) = ;10 |
186 | 179 | nn0rei 12480 |
. . . . . . . . . 10
β’ ;10 β β |
187 | 185, 186 | eqeltri 2830 |
. . . . . . . . 9
β’ (;10β1) β
β |
188 | 187 | a1i 11 |
. . . . . . . 8
β’ (π β (;10β1) β β) |
189 | | 1nn 12220 |
. . . . . . . . . . 11
β’ 1 β
β |
190 | | 2lt9 12414 |
. . . . . . . . . . . 12
β’ 2 <
9 |
191 | 177, 135,
190 | ltleii 11334 |
. . . . . . . . . . 11
β’ 2 β€
9 |
192 | 189, 57, 180, 191 | declei 12710 |
. . . . . . . . . 10
β’ 2 β€
;10 |
193 | 192, 185 | breqtrri 5175 |
. . . . . . . . 9
β’ 2 β€
(;10β1) |
194 | 193 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β€ (;10β1)) |
195 | | 1z 12589 |
. . . . . . . . . . . 12
β’ 1 β
β€ |
196 | 181 | nn0zi 12584 |
. . . . . . . . . . . 12
β’ ;27 β β€ |
197 | 186, 195,
196 | 3pm3.2i 1340 |
. . . . . . . . . . 11
β’ (;10 β β β§ 1 β
β€ β§ ;27 β
β€) |
198 | | 1lt10 12813 |
. . . . . . . . . . 11
β’ 1 <
;10 |
199 | 197, 198 | pm3.2i 472 |
. . . . . . . . . 10
β’ ((;10 β β β§ 1 β
β€ β§ ;27 β β€)
β§ 1 < ;10) |
200 | | 2nn 12282 |
. . . . . . . . . . 11
β’ 2 β
β |
201 | | 1lt9 12415 |
. . . . . . . . . . . 12
β’ 1 <
9 |
202 | 156, 135,
201 | ltleii 11334 |
. . . . . . . . . . 11
β’ 1 β€
9 |
203 | 200, 58, 56, 202 | declei 12710 |
. . . . . . . . . 10
β’ 1 β€
;27 |
204 | | leexp2 14133 |
. . . . . . . . . . 11
β’ (((;10 β β β§ 1 β
β€ β§ ;27 β β€)
β§ 1 < ;10) β (1 β€
;27 β (;10β1) β€ (;10β;27))) |
205 | 204 | biimpa 478 |
. . . . . . . . . 10
β’ ((((;10 β β β§ 1 β
β€ β§ ;27 β β€)
β§ 1 < ;10) β§ 1 β€
;27) β (;10β1) β€ (;10β;27)) |
206 | 199, 203,
205 | mp2an 691 |
. . . . . . . . 9
β’ (;10β1) β€ (;10β;27) |
207 | 206 | a1i 11 |
. . . . . . . 8
β’ (π β (;10β1) β€ (;10β;27)) |
208 | 178, 188,
184, 194, 207 | letrd 11368 |
. . . . . . 7
β’ (π β 2 β€ (;10β;27)) |
209 | | hgt750leme.0 |
. . . . . . 7
β’ (π β (;10β;27) β€ π) |
210 | 178, 184,
124, 208, 209 | letrd 11368 |
. . . . . 6
β’ (π β 2 β€ π) |
211 | | eqid 2733 |
. . . . . 6
β’ (π β {π β (β(reprβ3)π) β£ Β¬ (πβπ) β (π β© β)} β¦ (π β if(π = 0, ( I βΎ (0..^3)),
((pmTrspβ(0..^3))β{π, 0})))) = (π β {π β (β(reprβ3)π) β£ Β¬ (πβπ) β (π β© β)} β¦ (π β if(π = 0, ( I βΎ (0..^3)),
((pmTrspβ(0..^3))β{π, 0})))) |
212 | 176, 1, 210, 86, 211 | hgt750lema 33658 |
. . . . 5
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))((Ξβ(πβ0)) Β·
((Ξβ(πβ1)) Β· (Ξβ(πβ2)))) β€ (3 Β·
Ξ£π β {π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) |
213 | | 2z 12591 |
. . . . . . . . 9
β’ 2 β
β€ |
214 | 213 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β
β€) |
215 | 70, 214 | rpexpcld 14207 |
. . . . . . 7
β’ (π β ((1._0_7_9_9_55)β2) β
β+) |
216 | 215, 80 | rpmulcld 13029 |
. . . . . 6
β’ (π β (((1._0_7_9_9_55)β2) Β· (1._4_14))
β β+) |
217 | 169, 171,
216 | lemul2d 13057 |
. . . . 5
β’ (π β (Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))((Ξβ(πβ0)) Β·
((Ξβ(πβ1)) Β· (Ξβ(πβ2)))) β€ (3 Β·
Ξ£π β {π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))))) |
218 | 212, 217 | mpbid 231 |
. . . 4
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
((β(reprβ3)π)
β ((π β©
β)(reprβ3)π))((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))))) |
219 | 53, 170, 172, 175, 218 | letrd 11368 |
. . 3
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))))) |
220 | 154 | recnd 11239 |
. . . . . 6
β’ (π β (1._0_7_9_9_55)
β β) |
221 | 220 | sqcld 14106 |
. . . . 5
β’ (π β ((1._0_7_9_9_55)β2) β β) |
222 | 165 | recnd 11239 |
. . . . 5
β’ (π β (1._4_14)
β β) |
223 | 221, 222 | mulcld 11231 |
. . . 4
β’ (π β (((1._0_7_9_9_55)β2) Β· (1._4_14))
β β) |
224 | | 3cn 12290 |
. . . . 5
β’ 3 β
β |
225 | 224 | a1i 11 |
. . . 4
β’ (π β 3 β
β) |
226 | 108 | recnd 11239 |
. . . 4
β’ (π β Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β β) |
227 | 223, 225,
226 | mul12d 11420 |
. . 3
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (3 Β· Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) = (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))))) |
228 | 219, 227 | breqtrd 5174 |
. 2
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β€ (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))))) |
229 | | fzfi 13934 |
. . . . . . . . . . 11
β’
(1...π) β
Fin |
230 | | diffi 9176 |
. . . . . . . . . . 11
β’
((1...π) β Fin
β ((1...π) β
β) β Fin) |
231 | 229, 230 | ax-mp 5 |
. . . . . . . . . 10
β’
((1...π) β
β) β Fin |
232 | | snfi 9041 |
. . . . . . . . . 10
β’ {2}
β Fin |
233 | | unfi 9169 |
. . . . . . . . . 10
β’
((((1...π) β
β) β Fin β§ {2} β Fin) β (((1...π) β β) βͺ {2}) β
Fin) |
234 | 231, 232,
233 | mp2an 691 |
. . . . . . . . 9
β’
(((1...π) β
β) βͺ {2}) β Fin |
235 | 234 | a1i 11 |
. . . . . . . 8
β’ (π β (((1...π) β β) βͺ {2}) β
Fin) |
236 | 9 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (((1...π) β β) βͺ {2})) β
Ξ:ββΆβ) |
237 | | fz1ssnn 13529 |
. . . . . . . . . . . . 13
β’
(1...π) β
β |
238 | 237 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (1...π) β β) |
239 | 238 | ssdifssd 4142 |
. . . . . . . . . . 11
β’ (π β ((1...π) β β) β
β) |
240 | 200 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 2 β
β) |
241 | 240 | snssd 4812 |
. . . . . . . . . . 11
β’ (π β {2} β
β) |
242 | 239, 241 | unssd 4186 |
. . . . . . . . . 10
β’ (π β (((1...π) β β) βͺ {2}) β
β) |
243 | 242 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π β (((1...π) β β) βͺ {2})) β π β
β) |
244 | 236, 243 | ffvelcdmd 7085 |
. . . . . . . 8
β’ ((π β§ π β (((1...π) β β) βͺ {2})) β
(Ξβπ) β
β) |
245 | 235, 244 | fsumrecl 15677 |
. . . . . . 7
β’ (π β Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
β β) |
246 | | chpvalz 33629 |
. . . . . . . . 9
β’ (π β β€ β
(Οβπ) =
Ξ£π β (1...π)(Ξβπ)) |
247 | 12, 246 | syl 17 |
. . . . . . . 8
β’ (π β (Οβπ) = Ξ£π β (1...π)(Ξβπ)) |
248 | | chpf 26617 |
. . . . . . . . . 10
β’
Ο:ββΆβ |
249 | 248 | a1i 11 |
. . . . . . . . 9
β’ (π β
Ο:ββΆβ) |
250 | 249, 124 | ffvelcdmd 7085 |
. . . . . . . 8
β’ (π β (Οβπ) β
β) |
251 | 247, 250 | eqeltrrd 2835 |
. . . . . . 7
β’ (π β Ξ£π β (1...π)(Ξβπ) β β) |
252 | 245, 251 | remulcld 11241 |
. . . . . 6
β’ (π β (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ)) β β) |
253 | 123, 252 | remulcld 11241 |
. . . . 5
β’ (π β ((logβπ) Β· (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ))) β β) |
254 | 82, 253 | remulcld 11241 |
. . . 4
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))) β β) |
255 | 55, 254 | remulcld 11241 |
. . 3
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))) β β) |
256 | 176, 1, 210, 86 | hgt750lemb 33657 |
. . . . 5
β’ (π β Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β€ ((logβπ) Β· (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ)))) |
257 | 108, 253,
216 | lemul2d 13057 |
. . . . 5
β’ (π β (Ξ£π β {π β (β(reprβ3)π) β£ Β¬ (πβ0) β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))) β€ ((logβπ) Β· (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ))) β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))))) |
258 | 256, 257 | mpbid 231 |
. . . 4
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))) |
259 | | 3rp 12977 |
. . . . . 6
β’ 3 β
β+ |
260 | 259 | a1i 11 |
. . . . 5
β’ (π β 3 β
β+) |
261 | 109, 254,
260 | lemul2d 13057 |
. . . 4
β’ (π β (((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2))))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))) β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) β€ (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))))) |
262 | 258, 261 | mpbid 231 |
. . 3
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) β€ (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))))) |
263 | | 6re 12299 |
. . . . . . . . . . . . . . . . 17
β’ 6 β
β |
264 | 263, 54 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’ (6 β
β β§ 3 β β) |
265 | | dp2cl 32034 |
. . . . . . . . . . . . . . . 16
β’ ((6
β β β§ 3 β β) β _63 β β) |
266 | 264, 265 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ _63 β β |
267 | 177, 266 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (2 β
β β§ _63 β
β) |
268 | | dp2cl 32034 |
. . . . . . . . . . . . . 14
β’ ((2
β β β§ _63 β
β) β _2_63 β β) |
269 | 267, 268 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ _2_63 β β |
270 | 111, 269 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (4 β
β β§ _2_63 β β) |
271 | | dp2cl 32034 |
. . . . . . . . . . . 12
β’ ((4
β β β§ _2_63 β β) β _4_2_63
β β) |
272 | 270, 271 | ax-mp 5 |
. . . . . . . . . . 11
β’ _4_2_63
β β |
273 | | dpcl 32045 |
. . . . . . . . . . 11
β’ ((1
β β0 β§ _4_2_63
β β) β (1._4_2_63) β β) |
274 | 56, 272, 273 | mp2an 691 |
. . . . . . . . . 10
β’ (1._4_2_63)
β β |
275 | 274 | a1i 11 |
. . . . . . . . 9
β’ (π β (1._4_2_63)
β β) |
276 | 275, 126 | remulcld 11241 |
. . . . . . . 8
β’ (π β ((1._4_2_63)
Β· (ββπ))
β β) |
277 | 112, 54 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . 18
β’ (8 β
β β§ 3 β β) |
278 | | dp2cl 32034 |
. . . . . . . . . . . . . . . . . 18
β’ ((8
β β β§ 3 β β) β _83 β β) |
279 | 277, 278 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ _83 β β |
280 | 112, 279 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’ (8 β
β β§ _83 β
β) |
281 | | dp2cl 32034 |
. . . . . . . . . . . . . . . 16
β’ ((8
β β β§ _83 β
β) β _8_83 β β) |
282 | 280, 281 | ax-mp 5 |
. . . . . . . . . . . . . . 15
β’ _8_83 β β |
283 | 54, 282 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (3 β
β β§ _8_83 β β) |
284 | | dp2cl 32034 |
. . . . . . . . . . . . . 14
β’ ((3
β β β§ _8_83 β β) β _3_8_83
β β) |
285 | 283, 284 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ _3_8_83
β β |
286 | 133, 285 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (0 β
β β§ _3_8_83
β β) |
287 | | dp2cl 32034 |
. . . . . . . . . . . 12
β’ ((0
β β β§ _3_8_83 β β) β _0_3_8_83
β β) |
288 | 286, 287 | ax-mp 5 |
. . . . . . . . . . 11
β’ _0_3_8_83
β β |
289 | | dpcl 32045 |
. . . . . . . . . . 11
β’ ((1
β β0 β§ _0_3_8_83
β β) β (1._0_3_8_83)
β β) |
290 | 56, 288, 289 | mp2an 691 |
. . . . . . . . . 10
β’ (1._0_3_8_83)
β β |
291 | 290 | a1i 11 |
. . . . . . . . 9
β’ (π β (1._0_3_8_83)
β β) |
292 | 291, 124 | remulcld 11241 |
. . . . . . . 8
β’ (π β ((1._0_3_8_83)
Β· π) β
β) |
293 | 276, 292 | remulcld 11241 |
. . . . . . 7
β’ (π β (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)) β
β) |
294 | 123, 293 | remulcld 11241 |
. . . . . 6
β’ (π β ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) β
β) |
295 | 82, 294 | remulcld 11241 |
. . . . 5
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))) β
β) |
296 | 55, 295 | remulcld 11241 |
. . . 4
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) β
β) |
297 | | vmage0 26615 |
. . . . . . . . . . 11
β’ (π β β β 0 β€
(Ξβπ)) |
298 | 243, 297 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (((1...π) β β) βͺ {2})) β 0 β€
(Ξβπ)) |
299 | 235, 244,
298 | fsumge0 15738 |
. . . . . . . . 9
β’ (π β 0 β€ Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)) |
300 | 1, 209 | hgt750lemd 33649 |
. . . . . . . . 9
β’ (π β Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ) <
((1._4_2_63)
Β· (ββπ))) |
301 | | fzfid 13935 |
. . . . . . . . . 10
β’ (π β (1...π) β Fin) |
302 | 9 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β
Ξ:ββΆβ) |
303 | 238 | sselda 3982 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β π β β) |
304 | 302, 303 | ffvelcdmd 7085 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (Ξβπ) β β) |
305 | | vmage0 26615 |
. . . . . . . . . . 11
β’ (π β β β 0 β€
(Ξβπ)) |
306 | 303, 305 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β 0 β€ (Ξβπ)) |
307 | 301, 304,
306 | fsumge0 15738 |
. . . . . . . . 9
β’ (π β 0 β€ Ξ£π β (1...π)(Ξβπ)) |
308 | 1 | hgt750lemc 33648 |
. . . . . . . . 9
β’ (π β Ξ£π β (1...π)(Ξβπ) < ((1._0_3_8_83)
Β· π)) |
309 | 245, 276,
251, 292, 299, 300, 307, 308 | ltmul12ad 12152 |
. . . . . . . 8
β’ (π β (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ)) < (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) |
310 | 252, 293,
309 | ltled 11359 |
. . . . . . 7
β’ (π β (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ)) β€ (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) |
311 | 156 | a1i 11 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
312 | | 1lt2 12380 |
. . . . . . . . . . 11
β’ 1 <
2 |
313 | 312 | a1i 11 |
. . . . . . . . . 10
β’ (π β 1 < 2) |
314 | 311, 178,
124, 313, 210 | ltletrd 11371 |
. . . . . . . . 9
β’ (π β 1 < π) |
315 | 124, 314 | rplogcld 26129 |
. . . . . . . 8
β’ (π β (logβπ) β
β+) |
316 | 252, 293,
315 | lemul2d 13057 |
. . . . . . 7
β’ (π β ((Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ)) β€ (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)) β
((logβπ) Β·
(Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))) β€ ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) |
317 | 310, 316 | mpbid 231 |
. . . . . 6
β’ (π β ((logβπ) Β· (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ))) β€ ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))) |
318 | 253, 294,
216 | lemul2d 13057 |
. . . . . 6
β’ (π β (((logβπ) Β· (Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ)
Β· Ξ£π β
(1...π)(Ξβπ))) β€ ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) β
((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))))) |
319 | 317, 318 | mpbid 231 |
. . . . 5
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) |
320 | 254, 295,
260 | lemul2d 13057 |
. . . . 5
β’ (π β (((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ)))) β€ ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))) β (3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))) β€ (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))))) |
321 | 319, 320 | mpbid 231 |
. . . 4
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))) β€ (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))))) |
322 | 153 | resqcli 14147 |
. . . . . . . . . 10
β’ ((1._0_7_9_9_55)β2) β β |
323 | 322, 164 | remulcli 11227 |
. . . . . . . . 9
β’
(((1._0_7_9_9_55)β2) Β· (1._4_14))
β β |
324 | 274, 290 | remulcli 11227 |
. . . . . . . . 9
β’ ((1._4_2_63)
Β· (1._0_3_8_83))
β β |
325 | 323, 324 | remulcli 11227 |
. . . . . . . 8
β’
((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
β β |
326 | 54, 325 | remulcli 11227 |
. . . . . . 7
β’ (3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) β β |
327 | | hgt750lem2 33653 |
. . . . . . 7
β’ (3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) < (7._3_48) |
328 | 326, 120,
327 | ltleii 11334 |
. . . . . 6
β’ (3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) β€ (7._3_48) |
329 | 326 | a1i 11 |
. . . . . . 7
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) β β) |
330 | 315, 127 | rpdivcld 13030 |
. . . . . . . 8
β’ (π β ((logβπ) / (ββπ)) β
β+) |
331 | 122, 214 | rpexpcld 14207 |
. . . . . . . 8
β’ (π β (πβ2) β
β+) |
332 | 330, 331 | rpmulcld 13029 |
. . . . . . 7
β’ (π β (((logβπ) / (ββπ)) Β· (πβ2)) β
β+) |
333 | 329, 121,
332 | lemul1d 13056 |
. . . . . 6
β’ (π β ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) β€ (7._3_48)
β ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((logβπ) / (ββπ)) Β· (πβ2))) β€ ((7._3_48)
Β· (((logβπ) /
(ββπ)) Β·
(πβ2))))) |
334 | 328, 333 | mpbii 232 |
. . . . 5
β’ (π β ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((logβπ) / (ββπ)) Β· (πβ2))) β€ ((7._3_48)
Β· (((logβπ) /
(ββπ)) Β·
(πβ2)))) |
335 | 275 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β (1._4_2_63)
β β) |
336 | 126 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β (ββπ) β
β) |
337 | 291 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β (1._0_3_8_83)
β β) |
338 | 124 | recnd 11239 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
339 | 335, 336,
337, 338 | mul4d 11423 |
. . . . . . . . . . . . 13
β’ (π β (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)) = (((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π))) |
340 | 339 | oveq2d 7422 |
. . . . . . . . . . . 12
β’ (π β ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) =
((logβπ) Β·
(((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π)))) |
341 | 123 | recnd 11239 |
. . . . . . . . . . . . 13
β’ (π β (logβπ) β
β) |
342 | 335, 337 | mulcld 11231 |
. . . . . . . . . . . . . 14
β’ (π β ((1._4_2_63)
Β· (1._0_3_8_83))
β β) |
343 | 336, 338 | mulcld 11231 |
. . . . . . . . . . . . . 14
β’ (π β ((ββπ) Β· π) β β) |
344 | 342, 343 | mulcld 11231 |
. . . . . . . . . . . . 13
β’ (π β (((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π)) β
β) |
345 | 341, 344 | mulcomd 11232 |
. . . . . . . . . . . 12
β’ (π β ((logβπ) Β· (((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π))) = ((((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π)) Β·
(logβπ))) |
346 | 340, 345 | eqtrd 2773 |
. . . . . . . . . . 11
β’ (π β ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) = ((((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π)) Β·
(logβπ))) |
347 | 342, 343,
341 | mulassd 11234 |
. . . . . . . . . . 11
β’ (π β ((((1._4_2_63)
Β· (1._0_3_8_83))
Β· ((ββπ)
Β· π)) Β·
(logβπ)) = (((1._4_2_63)
Β· (1._0_3_8_83))
Β· (((ββπ) Β· π) Β· (logβπ)))) |
348 | 346, 347 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β ((logβπ) Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))) = (((1._4_2_63)
Β· (1._0_3_8_83))
Β· (((ββπ) Β· π) Β· (logβπ)))) |
349 | 348 | oveq2d 7422 |
. . . . . . . . 9
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))) =
((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (((1._4_2_63)
Β· (1._0_3_8_83))
Β· (((ββπ) Β· π) Β· (logβπ))))) |
350 | 82 | recnd 11239 |
. . . . . . . . . 10
β’ (π β (((1._0_7_9_9_55)β2) Β· (1._4_14))
β β) |
351 | 343, 341 | mulcld 11231 |
. . . . . . . . . 10
β’ (π β (((ββπ) Β· π) Β· (logβπ)) β β) |
352 | 350, 342,
351 | mulassd 11234 |
. . . . . . . . 9
β’ (π β (((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
Β· (((ββπ) Β· π) Β· (logβπ))) = ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· (((1._4_2_63)
Β· (1._0_3_8_83))
Β· (((ββπ) Β· π) Β· (logβπ))))) |
353 | 349, 352 | eqtr4d 2776 |
. . . . . . . 8
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π)))) =
(((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
Β· (((ββπ) Β· π) Β· (logβπ)))) |
354 | 353 | oveq2d 7422 |
. . . . . . 7
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) = (3
Β· (((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
Β· (((ββπ) Β· π) Β· (logβπ))))) |
355 | 55 | recnd 11239 |
. . . . . . . 8
β’ (π β 3 β
β) |
356 | 350, 342 | mulcld 11231 |
. . . . . . . 8
β’ (π β ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
β β) |
357 | 355, 356,
351 | mulassd 11234 |
. . . . . . 7
β’ (π β ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((ββπ) Β· π) Β· (logβπ))) = (3 Β· (((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))
Β· (((ββπ) Β· π) Β· (logβπ))))) |
358 | 354, 357 | eqtr4d 2776 |
. . . . . 6
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) = ((3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((ββπ) Β· π) Β· (logβπ)))) |
359 | 131 | recnd 11239 |
. . . . . . . . 9
β’ (π β (πβ2) β β) |
360 | 341, 336,
359, 128 | div32d 12010 |
. . . . . . . 8
β’ (π β (((logβπ) / (ββπ)) Β· (πβ2)) = ((logβπ) Β· ((πβ2) / (ββπ)))) |
361 | 359, 336,
128 | divcld 11987 |
. . . . . . . . 9
β’ (π β ((πβ2) / (ββπ)) β β) |
362 | 341, 361 | mulcomd 11232 |
. . . . . . . 8
β’ (π β ((logβπ) Β· ((πβ2) / (ββπ))) = (((πβ2) / (ββπ)) Β· (logβπ))) |
363 | 338 | sqvald 14105 |
. . . . . . . . . . . 12
β’ (π β (πβ2) = (π Β· π)) |
364 | 363 | oveq1d 7421 |
. . . . . . . . . . 11
β’ (π β ((πβ2) / (ββπ)) = ((π Β· π) / (ββπ))) |
365 | 338, 338,
336, 128 | divassd 12022 |
. . . . . . . . . . 11
β’ (π β ((π Β· π) / (ββπ)) = (π Β· (π / (ββπ)))) |
366 | | divsqrtid 33595 |
. . . . . . . . . . . . 13
β’ (π β β+
β (π /
(ββπ)) =
(ββπ)) |
367 | 122, 366 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π / (ββπ)) = (ββπ)) |
368 | 367 | oveq2d 7422 |
. . . . . . . . . . 11
β’ (π β (π Β· (π / (ββπ))) = (π Β· (ββπ))) |
369 | 364, 365,
368 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (π β ((πβ2) / (ββπ)) = (π Β· (ββπ))) |
370 | 338, 336 | mulcomd 11232 |
. . . . . . . . . 10
β’ (π β (π Β· (ββπ)) = ((ββπ) Β· π)) |
371 | 369, 370 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ((πβ2) / (ββπ)) = ((ββπ) Β· π)) |
372 | 371 | oveq1d 7421 |
. . . . . . . 8
β’ (π β (((πβ2) / (ββπ)) Β· (logβπ)) = (((ββπ) Β· π) Β· (logβπ))) |
373 | 360, 362,
372 | 3eqtrrd 2778 |
. . . . . . 7
β’ (π β (((ββπ) Β· π) Β· (logβπ)) = (((logβπ) / (ββπ)) Β· (πβ2))) |
374 | 373 | oveq2d 7422 |
. . . . . 6
β’ (π β ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((ββπ) Β· π) Β· (logβπ))) = ((3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((logβπ) / (ββπ)) Β· (πβ2)))) |
375 | 358, 374 | eqtrd 2773 |
. . . . 5
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) = ((3
Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((1._4_2_63)
Β· (1._0_3_8_83)))) Β· (((logβπ) / (ββπ)) Β· (πβ2)))) |
376 | 121 | recnd 11239 |
. . . . . 6
β’ (π β (7._3_48)
β β) |
377 | 129 | recnd 11239 |
. . . . . 6
β’ (π β ((logβπ) / (ββπ)) β
β) |
378 | 376, 377,
359 | mulassd 11234 |
. . . . 5
β’ (π β (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2)) =
((7._3_48) Β· (((logβπ) / (ββπ)) Β· (πβ2)))) |
379 | 334, 375,
378 | 3brtr4d 5180 |
. . . 4
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (((1._4_2_63)
Β· (ββπ))
Β· ((1._0_3_8_83)
Β· π))))) β€
(((7._3_48) Β· ((logβπ) / (ββπ))) Β· (πβ2))) |
380 | 255, 296,
132, 321, 379 | letrd 11368 |
. . 3
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· ((logβπ)
Β· (Ξ£π β
(((1...π) β β)
βͺ {2})(Ξβπ) Β· Ξ£π β (1...π)(Ξβπ))))) β€ (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2))) |
381 | 110, 255,
132, 262, 380 | letrd 11368 |
. 2
β’ (π β (3 Β· ((((1._0_7_9_9_55)β2) Β· (1._4_14))
Β· Ξ£π β
{π β
(β(reprβ3)π)
β£ Β¬ (πβ0)
β (π β© β)}
((Ξβ(πβ0)) Β· ((Ξβ(πβ1)) Β·
(Ξβ(πβ2)))))) β€ (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2))) |
382 | 53, 110, 132, 228, 381 | letrd 11368 |
1
β’ (π β Ξ£π β ((β(reprβ3)π) β ((π β© β)(reprβ3)π))(((Ξβ(πβ0)) Β· (π»β(πβ0))) Β· (((Ξβ(πβ1)) Β· (πΎβ(πβ1))) Β· ((Ξβ(πβ2)) Β· (πΎβ(πβ2))))) β€ (((7._3_48)
Β· ((logβπ) /
(ββπ)))
Β· (πβ2))) |