Step | Hyp | Ref
| Expression |
1 | | fzfid 13940 |
. . . . 5
β’ (π β (1...π) β Fin) |
2 | | diffi 9181 |
. . . . 5
β’
((1...π) β Fin
β ((1...π) β
β) β Fin) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β ((1...π) β β) β
Fin) |
4 | | vmaf 26630 |
. . . . . 6
β’
Ξ:ββΆβ |
5 | 4 | a1i 11 |
. . . . 5
β’ ((π β§ π β ((1...π) β β)) β
Ξ:ββΆβ) |
6 | | fz1ssnn 13534 |
. . . . . . . 8
β’
(1...π) β
β |
7 | 6 | a1i 11 |
. . . . . . 7
β’ (π β (1...π) β β) |
8 | 7 | ssdifssd 4142 |
. . . . . 6
β’ (π β ((1...π) β β) β
β) |
9 | 8 | sselda 3982 |
. . . . 5
β’ ((π β§ π β ((1...π) β β)) β π β
β) |
10 | 5, 9 | ffvelcdmd 7087 |
. . . 4
β’ ((π β§ π β ((1...π) β β)) β
(Ξβπ) β
β) |
11 | 3, 10 | fsumrecl 15682 |
. . 3
β’ (π β Ξ£π β ((1...π) β β)(Ξβπ) β
β) |
12 | | 2rp 12981 |
. . . . 5
β’ 2 β
β+ |
13 | 12 | a1i 11 |
. . . 4
β’ (π β 2 β
β+) |
14 | 13 | relogcld 26138 |
. . 3
β’ (π β (logβ2) β
β) |
15 | | 1nn0 12490 |
. . . . . 6
β’ 1 β
β0 |
16 | | 4re 12298 |
. . . . . . . 8
β’ 4 β
β |
17 | | 2re 12288 |
. . . . . . . . . 10
β’ 2 β
β |
18 | | 6re 12304 |
. . . . . . . . . . . 12
β’ 6 β
β |
19 | 18, 17 | pm3.2i 471 |
. . . . . . . . . . 11
β’ (6 β
β β§ 2 β β) |
20 | | dp2cl 32084 |
. . . . . . . . . . 11
β’ ((6
β β β§ 2 β β) β _62 β β) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . 10
β’ _62 β β |
22 | 17, 21 | pm3.2i 471 |
. . . . . . . . 9
β’ (2 β
β β§ _62 β
β) |
23 | | dp2cl 32084 |
. . . . . . . . 9
β’ ((2
β β β§ _62 β
β) β _2_62 β β) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . 8
β’ _2_62 β β |
25 | 16, 24 | pm3.2i 471 |
. . . . . . 7
β’ (4 β
β β§ _2_62 β β) |
26 | | dp2cl 32084 |
. . . . . . 7
β’ ((4
β β β§ _2_62 β β) β _4_2_62
β β) |
27 | 25, 26 | ax-mp 5 |
. . . . . 6
β’ _4_2_62
β β |
28 | | dpcl 32095 |
. . . . . 6
β’ ((1
β β0 β§ _4_2_62
β β) β (1._4_2_62) β β) |
29 | 15, 27, 28 | mp2an 690 |
. . . . 5
β’ (1._4_2_62)
β β |
30 | 29 | a1i 11 |
. . . 4
β’ (π β (1._4_2_62)
β β) |
31 | | hgt750lemc.n |
. . . . . 6
β’ (π β π β β) |
32 | 31 | nnred 12229 |
. . . . 5
β’ (π β π β β) |
33 | 31 | nnrpd 13016 |
. . . . . 6
β’ (π β π β
β+) |
34 | 33 | rpge0d 13022 |
. . . . 5
β’ (π β 0 β€ π) |
35 | 32, 34 | resqrtcld 15366 |
. . . 4
β’ (π β (ββπ) β
β) |
36 | 30, 35 | remulcld 11246 |
. . 3
β’ (π β ((1._4_2_62)
Β· (ββπ))
β β) |
37 | | 0nn0 12489 |
. . . . . 6
β’ 0 β
β0 |
38 | | 0re 11218 |
. . . . . . . 8
β’ 0 β
β |
39 | | 1re 11216 |
. . . . . . . . . . . 12
β’ 1 β
β |
40 | 38, 39 | pm3.2i 471 |
. . . . . . . . . . 11
β’ (0 β
β β§ 1 β β) |
41 | | dp2cl 32084 |
. . . . . . . . . . 11
β’ ((0
β β β§ 1 β β) β _01 β β) |
42 | 40, 41 | ax-mp 5 |
. . . . . . . . . 10
β’ _01 β β |
43 | 38, 42 | pm3.2i 471 |
. . . . . . . . 9
β’ (0 β
β β§ _01 β
β) |
44 | | dp2cl 32084 |
. . . . . . . . 9
β’ ((0
β β β§ _01 β
β) β _0_01 β β) |
45 | 43, 44 | ax-mp 5 |
. . . . . . . 8
β’ _0_01 β β |
46 | 38, 45 | pm3.2i 471 |
. . . . . . 7
β’ (0 β
β β§ _0_01 β β) |
47 | | dp2cl 32084 |
. . . . . . 7
β’ ((0
β β β§ _0_01 β β) β _0_0_01
β β) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
β’ _0_0_01
β β |
49 | | dpcl 32095 |
. . . . . 6
β’ ((0
β β0 β§ _0_0_01
β β) β (0._0_0_01) β β) |
50 | 37, 48, 49 | mp2an 690 |
. . . . 5
β’ (0._0_0_01)
β β |
51 | 50 | a1i 11 |
. . . 4
β’ (π β (0._0_0_01)
β β) |
52 | 51, 35 | remulcld 11246 |
. . 3
β’ (π β ((0._0_0_01)
Β· (ββπ))
β β) |
53 | 31 | nnzd 12587 |
. . . . . . 7
β’ (π β π β β€) |
54 | | chpvalz 33709 |
. . . . . . 7
β’ (π β β€ β
(Οβπ) =
Ξ£π β (1...π)(Ξβπ)) |
55 | 53, 54 | syl 17 |
. . . . . 6
β’ (π β (Οβπ) = Ξ£π β (1...π)(Ξβπ)) |
56 | | chtvalz 33710 |
. . . . . . . 8
β’ (π β β€ β
(ΞΈβπ) =
Ξ£π β ((1...π) β© β)(logβπ)) |
57 | 53, 56 | syl 17 |
. . . . . . 7
β’ (π β (ΞΈβπ) = Ξ£π β ((1...π) β© β)(logβπ)) |
58 | | inss2 4229 |
. . . . . . . . . . 11
β’
((1...π) β©
β) β β |
59 | 58 | a1i 11 |
. . . . . . . . . 10
β’ (π β ((1...π) β© β) β
β) |
60 | 59 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π β ((1...π) β© β)) β π β β) |
61 | | vmaprm 26628 |
. . . . . . . . 9
β’ (π β β β
(Ξβπ) =
(logβπ)) |
62 | 60, 61 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β ((1...π) β© β)) β
(Ξβπ) =
(logβπ)) |
63 | 62 | sumeq2dv 15651 |
. . . . . . 7
β’ (π β Ξ£π β ((1...π) β© β)(Ξβπ) = Ξ£π β ((1...π) β© β)(logβπ)) |
64 | 57, 63 | eqtr4d 2775 |
. . . . . 6
β’ (π β (ΞΈβπ) = Ξ£π β ((1...π) β© β)(Ξβπ)) |
65 | 55, 64 | oveq12d 7429 |
. . . . 5
β’ (π β ((Οβπ) β (ΞΈβπ)) = (Ξ£π β (1...π)(Ξβπ) β Ξ£π β ((1...π) β© β)(Ξβπ))) |
66 | | infi 9270 |
. . . . . . . 8
β’
((1...π) β Fin
β ((1...π) β©
β) β Fin) |
67 | 1, 66 | syl 17 |
. . . . . . 7
β’ (π β ((1...π) β© β) β
Fin) |
68 | 4 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β ((1...π) β© β)) β
Ξ:ββΆβ) |
69 | | inss1 4228 |
. . . . . . . . . . . 12
β’
((1...π) β©
β) β (1...π) |
70 | 69, 6 | sstri 3991 |
. . . . . . . . . . 11
β’
((1...π) β©
β) β β |
71 | 70 | a1i 11 |
. . . . . . . . . 10
β’ (π β ((1...π) β© β) β
β) |
72 | 71 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π β ((1...π) β© β)) β π β β) |
73 | 68, 72 | ffvelcdmd 7087 |
. . . . . . . 8
β’ ((π β§ π β ((1...π) β© β)) β
(Ξβπ) β
β) |
74 | 73 | recnd 11244 |
. . . . . . 7
β’ ((π β§ π β ((1...π) β© β)) β
(Ξβπ) β
β) |
75 | 67, 74 | fsumcl 15681 |
. . . . . 6
β’ (π β Ξ£π β ((1...π) β© β)(Ξβπ) β
β) |
76 | 10 | recnd 11244 |
. . . . . . 7
β’ ((π β§ π β ((1...π) β β)) β
(Ξβπ) β
β) |
77 | 3, 76 | fsumcl 15681 |
. . . . . 6
β’ (π β Ξ£π β ((1...π) β β)(Ξβπ) β
β) |
78 | | inindif 31792 |
. . . . . . . 8
β’
(((1...π) β©
β) β© ((1...π)
β β)) = β
|
79 | 78 | a1i 11 |
. . . . . . 7
β’ (π β (((1...π) β© β) β© ((1...π) β β)) =
β
) |
80 | | inundif 4478 |
. . . . . . . . 9
β’
(((1...π) β©
β) βͺ ((1...π)
β β)) = (1...π) |
81 | 80 | eqcomi 2741 |
. . . . . . . 8
β’
(1...π) =
(((1...π) β© β)
βͺ ((1...π) β
β)) |
82 | 81 | a1i 11 |
. . . . . . 7
β’ (π β (1...π) = (((1...π) β© β) βͺ ((1...π) β
β))) |
83 | 4 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β
Ξ:ββΆβ) |
84 | 7 | sselda 3982 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β π β β) |
85 | 83, 84 | ffvelcdmd 7087 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (Ξβπ) β β) |
86 | 85 | recnd 11244 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β (Ξβπ) β β) |
87 | 79, 82, 1, 86 | fsumsplit 15689 |
. . . . . 6
β’ (π β Ξ£π β (1...π)(Ξβπ) = (Ξ£π β ((1...π) β© β)(Ξβπ) + Ξ£π β ((1...π) β β)(Ξβπ))) |
88 | 75, 77, 87 | mvrladdd 11629 |
. . . . 5
β’ (π β (Ξ£π β (1...π)(Ξβπ) β Ξ£π β ((1...π) β© β)(Ξβπ)) = Ξ£π β ((1...π) β β)(Ξβπ)) |
89 | 65, 88 | eqtr2d 2773 |
. . . 4
β’ (π β Ξ£π β ((1...π) β β)(Ξβπ) = ((Οβπ) β (ΞΈβπ))) |
90 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π β (Οβπ₯) = (Οβπ)) |
91 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π β (ΞΈβπ₯) = (ΞΈβπ)) |
92 | 90, 91 | oveq12d 7429 |
. . . . . 6
β’ (π₯ = π β ((Οβπ₯) β (ΞΈβπ₯)) = ((Οβπ) β (ΞΈβπ))) |
93 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π β (ββπ₯) = (ββπ)) |
94 | 93 | oveq2d 7427 |
. . . . . 6
β’ (π₯ = π β ((1._4_2_62)
Β· (ββπ₯))
= ((1._4_2_62)
Β· (ββπ))) |
95 | 92, 94 | breq12d 5161 |
. . . . 5
β’ (π₯ = π β (((Οβπ₯) β (ΞΈβπ₯)) < ((1._4_2_62)
Β· (ββπ₯))
β ((Οβπ)
β (ΞΈβπ))
< ((1._4_2_62)
Β· (ββπ)))) |
96 | | ax-ros336 33727 |
. . . . . 6
β’
βπ₯ β
β+ ((Οβπ₯) β (ΞΈβπ₯)) < ((1._4_2_62)
Β· (ββπ₯)) |
97 | 96 | a1i 11 |
. . . . 5
β’ (π β βπ₯ β β+
((Οβπ₯) β
(ΞΈβπ₯)) <
((1._4_2_62)
Β· (ββπ₯))) |
98 | 95, 97, 33 | rspcdva 3613 |
. . . 4
β’ (π β ((Οβπ) β (ΞΈβπ)) < ((1._4_2_62)
Β· (ββπ))) |
99 | 89, 98 | eqbrtrd 5170 |
. . 3
β’ (π β Ξ£π β ((1...π) β β)(Ξβπ) < ((1._4_2_62)
Β· (ββπ))) |
100 | 39 | a1i 11 |
. . . 4
β’ (π β 1 β
β) |
101 | | log2le1 26462 |
. . . . 5
β’
(logβ2) < 1 |
102 | 101 | a1i 11 |
. . . 4
β’ (π β (logβ2) <
1) |
103 | | 10nn0 12697 |
. . . . . . . . 9
β’ ;10 β
β0 |
104 | | 7nn0 12496 |
. . . . . . . . 9
β’ 7 β
β0 |
105 | 103, 104 | nn0expcli 14056 |
. . . . . . . 8
β’ (;10β7) β
β0 |
106 | 105 | nn0rei 12485 |
. . . . . . 7
β’ (;10β7) β
β |
107 | 106 | a1i 11 |
. . . . . 6
β’ (π β (;10β7) β β) |
108 | 51, 107 | remulcld 11246 |
. . . . 5
β’ (π β ((0._0_0_01)
Β· (;10β7)) β
β) |
109 | 103 | nn0rei 12485 |
. . . . . . . . . . 11
β’ ;10 β β |
110 | | 0z 12571 |
. . . . . . . . . . 11
β’ 0 β
β€ |
111 | | 3z 12597 |
. . . . . . . . . . 11
β’ 3 β
β€ |
112 | 109, 110,
111 | 3pm3.2i 1339 |
. . . . . . . . . 10
β’ (;10 β β β§ 0 β
β€ β§ 3 β β€) |
113 | | 1lt10 12818 |
. . . . . . . . . . 11
β’ 1 <
;10 |
114 | | 3pos 12319 |
. . . . . . . . . . 11
β’ 0 <
3 |
115 | 113, 114 | pm3.2i 471 |
. . . . . . . . . 10
β’ (1 <
;10 β§ 0 <
3) |
116 | | ltexp2a 14133 |
. . . . . . . . . 10
β’ (((;10 β β β§ 0 β
β€ β§ 3 β β€) β§ (1 < ;10 β§ 0 < 3)) β (;10β0) < (;10β3)) |
117 | 112, 115,
116 | mp2an 690 |
. . . . . . . . 9
β’ (;10β0) < (;10β3) |
118 | 103 | numexp0 17011 |
. . . . . . . . . 10
β’ (;10β0) = 1 |
119 | 118 | eqcomi 2741 |
. . . . . . . . 9
β’ 1 =
(;10β0) |
120 | 109 | recni 11230 |
. . . . . . . . . . 11
β’ ;10 β β |
121 | | 10pos 12696 |
. . . . . . . . . . . 12
β’ 0 <
;10 |
122 | 38, 121 | gtneii 11328 |
. . . . . . . . . . 11
β’ ;10 β 0 |
123 | | 4z 12598 |
. . . . . . . . . . 11
β’ 4 β
β€ |
124 | | expm1 14080 |
. . . . . . . . . . 11
β’ ((;10 β β β§ ;10 β 0 β§ 4 β β€)
β (;10β(4 β 1)) =
((;10β4) / ;10)) |
125 | 120, 122,
123, 124 | mp3an 1461 |
. . . . . . . . . 10
β’ (;10β(4 β 1)) = ((;10β4) / ;10) |
126 | | 4m1e3 12343 |
. . . . . . . . . . 11
β’ (4
β 1) = 3 |
127 | 126 | oveq2i 7422 |
. . . . . . . . . 10
β’ (;10β(4 β 1)) = (;10β3) |
128 | | 4nn0 12493 |
. . . . . . . . . . . . 13
β’ 4 β
β0 |
129 | 103, 128 | nn0expcli 14056 |
. . . . . . . . . . . 12
β’ (;10β4) β
β0 |
130 | 129 | nn0cni 12486 |
. . . . . . . . . . 11
β’ (;10β4) β
β |
131 | | divrec2 11891 |
. . . . . . . . . . 11
β’ (((;10β4) β β β§ ;10 β β β§ ;10 β 0) β ((;10β4) / ;10) = ((1 / ;10) Β· (;10β4))) |
132 | 130, 120,
122, 131 | mp3an 1461 |
. . . . . . . . . 10
β’ ((;10β4) / ;10) = ((1 / ;10) Β· (;10β4)) |
133 | 125, 127,
132 | 3eqtr3ri 2769 |
. . . . . . . . 9
β’ ((1 /
;10) Β· (;10β4)) = (;10β3) |
134 | 117, 119,
133 | 3brtr4i 5178 |
. . . . . . . 8
β’ 1 <
((1 / ;10) Β· (;10β4)) |
135 | | 1rp 12980 |
. . . . . . . . . 10
β’ 1 β
β+ |
136 | 135 | dp0h 32106 |
. . . . . . . . 9
β’ (0.1) =
(1 / ;10) |
137 | 136 | oveq1i 7421 |
. . . . . . . 8
β’ ((0.1)
Β· (;10β4)) = ((1 /
;10) Β· (;10β4)) |
138 | 134, 137 | breqtrri 5175 |
. . . . . . 7
β’ 1 <
((0.1) Β· (;10β4)) |
139 | 138 | a1i 11 |
. . . . . 6
β’ (π β 1 < ((0.1) Β·
(;10β4))) |
140 | | 4p1e5 12360 |
. . . . . . . 8
β’ (4 + 1) =
5 |
141 | | 5nn0 12494 |
. . . . . . . . 9
β’ 5 β
β0 |
142 | 141 | nn0zi 12589 |
. . . . . . . 8
β’ 5 β
β€ |
143 | 37, 135, 140, 123, 142 | dpexpp1 32112 |
. . . . . . 7
β’ ((0.1)
Β· (;10β4)) = ((0._01) Β· (;10β5)) |
144 | 37, 135 | rpdp2cl 32086 |
. . . . . . . 8
β’ _01 β
β+ |
145 | | 5p1e6 12361 |
. . . . . . . 8
β’ (5 + 1) =
6 |
146 | | 6nn0 12495 |
. . . . . . . . 9
β’ 6 β
β0 |
147 | 146 | nn0zi 12589 |
. . . . . . . 8
β’ 6 β
β€ |
148 | 37, 144, 145, 142, 147 | dpexpp1 32112 |
. . . . . . 7
β’ ((0._01) Β· (;10β5)) = ((0._0_01)
Β· (;10β6)) |
149 | 37, 144 | rpdp2cl 32086 |
. . . . . . . 8
β’ _0_01 β β+ |
150 | | 6p1e7 12362 |
. . . . . . . 8
β’ (6 + 1) =
7 |
151 | 104 | nn0zi 12589 |
. . . . . . . 8
β’ 7 β
β€ |
152 | 37, 149, 150, 147, 151 | dpexpp1 32112 |
. . . . . . 7
β’ ((0._0_01) Β· (;10β6)) = ((0._0_0_01)
Β· (;10β7)) |
153 | 143, 148,
152 | 3eqtrri 2765 |
. . . . . 6
β’ ((0._0_0_01)
Β· (;10β7)) = ((0.1)
Β· (;10β4)) |
154 | 139, 153 | breqtrrdi 5190 |
. . . . 5
β’ (π β 1 < ((0._0_0_01)
Β· (;10β7))) |
155 | 37, 149 | rpdp2cl 32086 |
. . . . . . . 8
β’ _0_0_01
β β+ |
156 | 37, 155 | rpdpcl 32107 |
. . . . . . 7
β’ (0._0_0_01)
β β+ |
157 | 156 | a1i 11 |
. . . . . 6
β’ (π β (0._0_0_01)
β β+) |
158 | | 2nn0 12491 |
. . . . . . . . . . . 12
β’ 2 β
β0 |
159 | 158, 104 | deccl 12694 |
. . . . . . . . . . 11
β’ ;27 β
β0 |
160 | 103, 159 | nn0expcli 14056 |
. . . . . . . . . 10
β’ (;10β;27) β β0 |
161 | 160 | nn0rei 12485 |
. . . . . . . . 9
β’ (;10β;27) β β |
162 | 161 | a1i 11 |
. . . . . . . 8
β’ (π β (;10β;27) β β) |
163 | 160 | nn0ge0i 12501 |
. . . . . . . . 9
β’ 0 β€
(;10β;27) |
164 | 163 | a1i 11 |
. . . . . . . 8
β’ (π β 0 β€ (;10β;27)) |
165 | 162, 164 | resqrtcld 15366 |
. . . . . . 7
β’ (π β (ββ(;10β;27)) β β) |
166 | | expmul 14075 |
. . . . . . . . . . . . 13
β’ ((;10 β β β§ 7 β
β0 β§ 2 β β0) β (;10β(7 Β· 2)) = ((;10β7)β2)) |
167 | 120, 104,
158, 166 | mp3an 1461 |
. . . . . . . . . . . 12
β’ (;10β(7 Β· 2)) = ((;10β7)β2) |
168 | | 7t2e14 12788 |
. . . . . . . . . . . . 13
β’ (7
Β· 2) = ;14 |
169 | 168 | oveq2i 7422 |
. . . . . . . . . . . 12
β’ (;10β(7 Β· 2)) = (;10β;14) |
170 | 167, 169 | eqtr3i 2762 |
. . . . . . . . . . 11
β’ ((;10β7)β2) = (;10β;14) |
171 | 170 | fveq2i 6894 |
. . . . . . . . . 10
β’
(ββ((;10β7)β2)) = (ββ(;10β;14)) |
172 | | expgt0 14063 |
. . . . . . . . . . . . 13
β’ ((;10 β β β§ 7 β
β€ β§ 0 < ;10) β 0
< (;10β7)) |
173 | 109, 151,
121, 172 | mp3an 1461 |
. . . . . . . . . . . 12
β’ 0 <
(;10β7) |
174 | 38, 106, 173 | ltleii 11339 |
. . . . . . . . . . 11
β’ 0 β€
(;10β7) |
175 | | sqrtsq 15218 |
. . . . . . . . . . 11
β’ (((;10β7) β β β§ 0 β€
(;10β7)) β
(ββ((;10β7)β2)) = (;10β7)) |
176 | 106, 174,
175 | mp2an 690 |
. . . . . . . . . 10
β’
(ββ((;10β7)β2)) = (;10β7) |
177 | 171, 176 | eqtr3i 2762 |
. . . . . . . . 9
β’
(ββ(;10β;14)) = (;10β7) |
178 | 15, 128 | deccl 12694 |
. . . . . . . . . . . . 13
β’ ;14 β
β0 |
179 | 178 | nn0zi 12589 |
. . . . . . . . . . . 12
β’ ;14 β β€ |
180 | 159 | nn0zi 12589 |
. . . . . . . . . . . 12
β’ ;27 β β€ |
181 | 109, 179,
180 | 3pm3.2i 1339 |
. . . . . . . . . . 11
β’ (;10 β β β§ ;14 β β€ β§ ;27 β β€) |
182 | | 4lt10 12815 |
. . . . . . . . . . . . 13
β’ 4 <
;10 |
183 | | 1lt2 12385 |
. . . . . . . . . . . . 13
β’ 1 <
2 |
184 | 15, 158, 128, 104, 182, 183 | decltc 12708 |
. . . . . . . . . . . 12
β’ ;14 < ;27 |
185 | 113, 184 | pm3.2i 471 |
. . . . . . . . . . 11
β’ (1 <
;10 β§ ;14 < ;27) |
186 | | ltexp2a 14133 |
. . . . . . . . . . 11
β’ (((;10 β β β§ ;14 β β€ β§ ;27 β β€) β§ (1 < ;10 β§ ;14 < ;27)) β (;10β;14) < (;10β;27)) |
187 | 181, 185,
186 | mp2an 690 |
. . . . . . . . . 10
β’ (;10β;14) < (;10β;27) |
188 | 103, 178 | nn0expcli 14056 |
. . . . . . . . . . . . 13
β’ (;10β;14) β β0 |
189 | 188 | nn0rei 12485 |
. . . . . . . . . . . 12
β’ (;10β;14) β β |
190 | | expgt0 14063 |
. . . . . . . . . . . . . 14
β’ ((;10 β β β§ ;14 β β€ β§ 0 < ;10) β 0 < (;10β;14)) |
191 | 109, 179,
121, 190 | mp3an 1461 |
. . . . . . . . . . . . 13
β’ 0 <
(;10β;14) |
192 | 38, 189, 191 | ltleii 11339 |
. . . . . . . . . . . 12
β’ 0 β€
(;10β;14) |
193 | 189, 192 | pm3.2i 471 |
. . . . . . . . . . 11
β’ ((;10β;14) β β β§ 0 β€ (;10β;14)) |
194 | 161, 163 | pm3.2i 471 |
. . . . . . . . . . 11
β’ ((;10β;27) β β β§ 0 β€ (;10β;27)) |
195 | | sqrtlt 15210 |
. . . . . . . . . . 11
β’ ((((;10β;14) β β β§ 0 β€ (;10β;14)) β§ ((;10β;27) β β β§ 0 β€ (;10β;27))) β ((;10β;14) < (;10β;27) β (ββ(;10β;14)) < (ββ(;10β;27)))) |
196 | 193, 194,
195 | mp2an 690 |
. . . . . . . . . 10
β’ ((;10β;14) < (;10β;27) β (ββ(;10β;14)) < (ββ(;10β;27))) |
197 | 187, 196 | mpbi 229 |
. . . . . . . . 9
β’
(ββ(;10β;14)) < (ββ(;10β;27)) |
198 | 177, 197 | eqbrtrri 5171 |
. . . . . . . 8
β’ (;10β7) < (ββ(;10β;27)) |
199 | 198 | a1i 11 |
. . . . . . 7
β’ (π β (;10β7) < (ββ(;10β;27))) |
200 | | hgt750lemd.0 |
. . . . . . . 8
β’ (π β (;10β;27) β€ π) |
201 | 162, 164,
32, 34 | sqrtled 15375 |
. . . . . . . 8
β’ (π β ((;10β;27) β€ π β (ββ(;10β;27)) β€ (ββπ))) |
202 | 200, 201 | mpbid 231 |
. . . . . . 7
β’ (π β (ββ(;10β;27)) β€ (ββπ)) |
203 | 107, 165,
35, 199, 202 | ltletrd 11376 |
. . . . . 6
β’ (π β (;10β7) < (ββπ)) |
204 | 107, 35, 157, 203 | ltmul2dd 13074 |
. . . . 5
β’ (π β ((0._0_0_01)
Β· (;10β7)) <
((0._0_0_01)
Β· (ββπ))) |
205 | 100, 108,
52, 154, 204 | lttrd 11377 |
. . . 4
β’ (π β 1 < ((0._0_0_01)
Β· (ββπ))) |
206 | 14, 100, 52, 102, 205 | lttrd 11377 |
. . 3
β’ (π β (logβ2) <
((0._0_0_01)
Β· (ββπ))) |
207 | 11, 14, 36, 52, 99, 206 | lt2addd 11839 |
. 2
β’ (π β (Ξ£π β ((1...π) β β)(Ξβπ) + (logβ2)) <
(((1._4_2_62)
Β· (ββπ))
+ ((0._0_0_01)
Β· (ββπ)))) |
208 | | nfv 1917 |
. . 3
β’
β²ππ |
209 | | nfcv 2903 |
. . 3
β’
β²π(logβ2) |
210 | | 2prm 16631 |
. . . 4
β’ 2 β
β |
211 | 210 | a1i 11 |
. . 3
β’ (π β 2 β
β) |
212 | | elndif 4128 |
. . . 4
β’ (2 β
β β Β¬ 2 β ((1...π) β β)) |
213 | 211, 212 | syl 17 |
. . 3
β’ (π β Β¬ 2 β ((1...π) β
β)) |
214 | | fveq2 6891 |
. . . 4
β’ (π = 2 β
(Ξβπ) =
(Ξβ2)) |
215 | | vmaprm 26628 |
. . . . 5
β’ (2 β
β β (Ξβ2) = (logβ2)) |
216 | 210, 215 | ax-mp 5 |
. . . 4
β’
(Ξβ2) = (logβ2) |
217 | 214, 216 | eqtrdi 2788 |
. . 3
β’ (π = 2 β
(Ξβπ) =
(logβ2)) |
218 | | 2cnd 12292 |
. . . 4
β’ (π β 2 β
β) |
219 | | 2ne0 12318 |
. . . . 5
β’ 2 β
0 |
220 | 219 | a1i 11 |
. . . 4
β’ (π β 2 β 0) |
221 | 218, 220 | logcld 26086 |
. . 3
β’ (π β (logβ2) β
β) |
222 | 208, 209,
3, 211, 213, 76, 217, 221 | fsumsplitsn 15692 |
. 2
β’ (π β Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ) =
(Ξ£π β
((1...π) β
β)(Ξβπ)
+ (logβ2))) |
223 | 146, 12 | rpdp2cl 32086 |
. . . . . 6
β’ _62 β
β+ |
224 | 158, 223 | rpdp2cl 32086 |
. . . . 5
β’ _2_62 β β+ |
225 | | 3rp 12982 |
. . . . . . 7
β’ 3 β
β+ |
226 | 146, 225 | rpdp2cl 32086 |
. . . . . 6
β’ _63 β
β+ |
227 | 158, 226 | rpdp2cl 32086 |
. . . . 5
β’ _2_63 β β+ |
228 | | 1p0e1 12338 |
. . . . 5
β’ (1 + 0) =
1 |
229 | | 4cn 12299 |
. . . . . . 7
β’ 4 β
β |
230 | 229 | addridi 11403 |
. . . . . 6
β’ (4 + 0) =
4 |
231 | | 2cn 12289 |
. . . . . . . 8
β’ 2 β
β |
232 | 231 | addridi 11403 |
. . . . . . 7
β’ (2 + 0) =
2 |
233 | | 3nn0 12492 |
. . . . . . . 8
β’ 3 β
β0 |
234 | | eqid 2732 |
. . . . . . . . 9
β’ ;62 = ;62 |
235 | | eqid 2732 |
. . . . . . . . 9
β’ ;01 = ;01 |
236 | | 6cn 12305 |
. . . . . . . . . 10
β’ 6 β
β |
237 | 236 | addridi 11403 |
. . . . . . . . 9
β’ (6 + 0) =
6 |
238 | | 2p1e3 12356 |
. . . . . . . . 9
β’ (2 + 1) =
3 |
239 | 146, 158,
37, 15, 234, 235, 237, 238 | decadd 12733 |
. . . . . . . 8
β’ (;62 + ;01) = ;63 |
240 | 146, 158,
37, 15, 146, 233, 239 | dpadd 32115 |
. . . . . . 7
β’ ((6.2) +
(0.1)) = (6.3) |
241 | 146, 12, 37, 135, 146, 225, 158, 37, 232, 240 | dpadd2 32114 |
. . . . . 6
β’ ((2._62) + (0._01)) = (2._63) |
242 | 158, 223,
37, 144, 158, 226, 128, 37, 230, 241 | dpadd2 32114 |
. . . . 5
β’ ((4._2_62) + (0._0_01))
= (4._2_63) |
243 | 128, 224,
37, 149, 128, 227, 15, 37, 228, 242 | dpadd2 32114 |
. . . 4
β’ ((1._4_2_62) +
(0._0_0_01))
= (1._4_2_63) |
244 | 243 | oveq1i 7421 |
. . 3
β’
(((1._4_2_62) +
(0._0_0_01))
Β· (ββπ))
= ((1._4_2_63)
Β· (ββπ)) |
245 | 30 | recnd 11244 |
. . . 4
β’ (π β (1._4_2_62)
β β) |
246 | 51 | recnd 11244 |
. . . 4
β’ (π β (0._0_0_01)
β β) |
247 | 35 | recnd 11244 |
. . . 4
β’ (π β (ββπ) β
β) |
248 | 245, 246,
247 | adddird 11241 |
. . 3
β’ (π β (((1._4_2_62) +
(0._0_0_01))
Β· (ββπ))
= (((1._4_2_62)
Β· (ββπ))
+ ((0._0_0_01)
Β· (ββπ)))) |
249 | 244, 248 | eqtr3id 2786 |
. 2
β’ (π β ((1._4_2_63)
Β· (ββπ))
= (((1._4_2_62)
Β· (ββπ))
+ ((0._0_0_01)
Β· (ββπ)))) |
250 | 207, 222,
249 | 3brtr4d 5180 |
1
β’ (π β Ξ£π β (((1...π) β β) βͺ
{2})(Ξβπ) <
((1._4_2_63)
Β· (ββπ))) |