Step | Hyp | Ref
| Expression |
1 | | aks4d1p3.1 |
. . . . . 6
β’ (π β π β
(β€β₯β3)) |
2 | | aks4d1p3.2 |
. . . . . 6
β’ π΄ = ((πβ(ββ(2 logb
π΅))) Β· βπ β (1...(ββ((2
logb π)β2)))((πβπ) β 1)) |
3 | | aks4d1p3.3 |
. . . . . 6
β’ π΅ = (ββ((2
logb π)β5)) |
4 | 1, 2, 3 | aks4d1p1 41457 |
. . . . 5
β’ (π β π΄ < (2βπ΅)) |
5 | 4 | adantr 480 |
. . . 4
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β π΄ < (2βπ΅)) |
6 | | 2re 12290 |
. . . . . . . . 9
β’ 2 β
β |
7 | 6 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β
β) |
8 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (π β π΅ = (ββ((2 logb π)β5))) |
9 | | 2pos 12319 |
. . . . . . . . . . . . . . 15
β’ 0 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 < 2) |
11 | | eluzelz 12836 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β3) β π β β€) |
12 | 1, 11 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β β€) |
13 | 12 | zred 12670 |
. . . . . . . . . . . . . 14
β’ (π β π β β) |
14 | | 0red 11221 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β
β) |
15 | | 3re 12296 |
. . . . . . . . . . . . . . . 16
β’ 3 β
β |
16 | 15 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 3 β
β) |
17 | | 3pos 12321 |
. . . . . . . . . . . . . . . 16
β’ 0 <
3 |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π β 0 < 3) |
19 | | eluzle 12839 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β3) β 3 β€ π) |
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β 3 β€ π) |
21 | 14, 16, 13, 18, 20 | ltletrd 11378 |
. . . . . . . . . . . . . 14
β’ (π β 0 < π) |
22 | | 1red 11219 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 β
β) |
23 | | 1lt2 12387 |
. . . . . . . . . . . . . . . . 17
β’ 1 <
2 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 < 2) |
25 | 22, 24 | ltned 11354 |
. . . . . . . . . . . . . . 15
β’ (π β 1 β 2) |
26 | 25 | necomd 2990 |
. . . . . . . . . . . . . 14
β’ (π β 2 β 1) |
27 | 7, 10, 13, 21, 26 | relogbcld 41354 |
. . . . . . . . . . . . 13
β’ (π β (2 logb π) β
β) |
28 | | 5nn0 12496 |
. . . . . . . . . . . . . 14
β’ 5 β
β0 |
29 | 28 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β 5 β
β0) |
30 | 27, 29 | reexpcld 14133 |
. . . . . . . . . . . 12
β’ (π β ((2 logb π)β5) β
β) |
31 | | ceilcl 13813 |
. . . . . . . . . . . 12
β’ (((2
logb π)β5)
β β β (ββ((2 logb π)β5)) β β€) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
β’ (π β (ββ((2
logb π)β5))
β β€) |
33 | 8, 32 | eqeltrd 2827 |
. . . . . . . . . 10
β’ (π β π΅ β β€) |
34 | 32 | zred 12670 |
. . . . . . . . . . . 12
β’ (π β (ββ((2
logb π)β5))
β β) |
35 | 8, 34 | eqeltrd 2827 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
36 | | 7re 12309 |
. . . . . . . . . . . . . . 15
β’ 7 β
β |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 7 β
β) |
38 | | 7pos 12327 |
. . . . . . . . . . . . . . 15
β’ 0 <
7 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β 0 < 7) |
40 | 13, 20 | 3lexlogpow5ineq3 41438 |
. . . . . . . . . . . . . 14
β’ (π β 7 < ((2 logb
π)β5)) |
41 | 14, 37, 30, 39, 40 | lttrd 11379 |
. . . . . . . . . . . . 13
β’ (π β 0 < ((2 logb
π)β5)) |
42 | | ceilge 13816 |
. . . . . . . . . . . . . 14
β’ (((2
logb π)β5)
β β β ((2 logb π)β5) β€ (ββ((2
logb π)β5))) |
43 | 30, 42 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β ((2 logb π)β5) β€
(ββ((2 logb π)β5))) |
44 | 14, 30, 34, 41, 43 | ltletrd 11378 |
. . . . . . . . . . . 12
β’ (π β 0 < (ββ((2
logb π)β5))) |
45 | 44, 8 | breqtrrd 5169 |
. . . . . . . . . . 11
β’ (π β 0 < π΅) |
46 | 14, 35, 45 | ltled 11366 |
. . . . . . . . . 10
β’ (π β 0 β€ π΅) |
47 | 33, 46 | jca 511 |
. . . . . . . . 9
β’ (π β (π΅ β β€ β§ 0 β€ π΅)) |
48 | | elnn0z 12575 |
. . . . . . . . 9
β’ (π΅ β β0
β (π΅ β β€
β§ 0 β€ π΅)) |
49 | 47, 48 | sylibr 233 |
. . . . . . . 8
β’ (π β π΅ β
β0) |
50 | 7, 49 | reexpcld 14133 |
. . . . . . 7
β’ (π β (2βπ΅) β β) |
51 | 50 | adantr 480 |
. . . . . 6
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (2βπ΅) β β) |
52 | | elfznn 13536 |
. . . . . . . . . . . . 13
β’ (π β (1...π΅) β π β β) |
53 | 52 | adantl 481 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π΅)) β π β β) |
54 | 53 | nnzd 12589 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π΅)) β π β β€) |
55 | 54 | ex 412 |
. . . . . . . . . 10
β’ (π β (π β (1...π΅) β π β β€)) |
56 | 55 | ssrdv 3983 |
. . . . . . . . 9
β’ (π β (1...π΅) β β€) |
57 | | fzfid 13944 |
. . . . . . . . 9
β’ (π β (1...π΅) β Fin) |
58 | | lcmfcl 16572 |
. . . . . . . . 9
β’
(((1...π΅) β
β€ β§ (1...π΅)
β Fin) β (lcmβ(1...π΅)) β
β0) |
59 | 56, 57, 58 | syl2anc 583 |
. . . . . . . 8
β’ (π β
(lcmβ(1...π΅))
β β0) |
60 | 59 | nn0red 12537 |
. . . . . . 7
β’ (π β
(lcmβ(1...π΅))
β β) |
61 | 60 | adantr 480 |
. . . . . 6
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (lcmβ(1...π΅)) β
β) |
62 | 2 | a1i 11 |
. . . . . . . . 9
β’ (π β π΄ = ((πβ(ββ(2 logb
π΅))) Β· βπ β (1...(ββ((2
logb π)β2)))((πβπ) β 1))) |
63 | | elnnz 12572 |
. . . . . . . . . . . 12
β’ (π β β β (π β β€ β§ 0 <
π)) |
64 | 12, 21, 63 | sylanbrc 582 |
. . . . . . . . . . 11
β’ (π β π β β) |
65 | 7, 10, 35, 45, 26 | relogbcld 41354 |
. . . . . . . . . . . . . 14
β’ (π β (2 logb π΅) β
β) |
66 | 65 | flcld 13769 |
. . . . . . . . . . . . 13
β’ (π β (ββ(2
logb π΅)) β
β€) |
67 | 7, 10, 7, 10, 26 | relogbcld 41354 |
. . . . . . . . . . . . . . 15
β’ (π β (2 logb 2)
β β) |
68 | | 0le1 11741 |
. . . . . . . . . . . . . . . . 17
β’ 0 β€
1 |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β 0 β€ 1) |
70 | 7 | recnd 11246 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 2 β
β) |
71 | 14, 10 | gtned 11353 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 2 β 0) |
72 | | logbid1 26655 |
. . . . . . . . . . . . . . . . . 18
β’ ((2
β β β§ 2 β 0 β§ 2 β 1) β (2 logb 2) =
1) |
73 | 70, 71, 26, 72 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
β’ (π β (2 logb 2) =
1) |
74 | 73 | eqcomd 2732 |
. . . . . . . . . . . . . . . 16
β’ (π β 1 = (2 logb
2)) |
75 | 69, 74 | breqtrd 5167 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β€ (2 logb
2)) |
76 | | 2z 12598 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β€ |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β 2 β
β€) |
78 | 7 | leidd 11784 |
. . . . . . . . . . . . . . . 16
β’ (π β 2 β€ 2) |
79 | | 2lt7 12406 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 <
7 |
80 | 79 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 2 < 7) |
81 | 7, 37, 80 | ltled 11366 |
. . . . . . . . . . . . . . . . 17
β’ (π β 2 β€ 7) |
82 | 37, 30, 34, 40, 43 | ltletrd 11378 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 7 < (ββ((2
logb π)β5))) |
83 | 82, 8 | breqtrrd 5169 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 7 < π΅) |
84 | 37, 35, 83 | ltled 11366 |
. . . . . . . . . . . . . . . . 17
β’ (π β 7 β€ π΅) |
85 | 7, 37, 35, 81, 84 | letrd 11375 |
. . . . . . . . . . . . . . . 16
β’ (π β 2 β€ π΅) |
86 | 77, 78, 7, 10, 35, 45, 85 | logblebd 41357 |
. . . . . . . . . . . . . . 15
β’ (π β (2 logb 2) β€
(2 logb π΅)) |
87 | 14, 67, 65, 75, 86 | letrd 11375 |
. . . . . . . . . . . . . 14
β’ (π β 0 β€ (2 logb
π΅)) |
88 | | 0zd 12574 |
. . . . . . . . . . . . . . 15
β’ (π β 0 β
β€) |
89 | | flge 13776 |
. . . . . . . . . . . . . . 15
β’ (((2
logb π΅) β
β β§ 0 β β€) β (0 β€ (2 logb π΅) β 0 β€
(ββ(2 logb π΅)))) |
90 | 65, 88, 89 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ (π β (0 β€ (2 logb
π΅) β 0 β€
(ββ(2 logb π΅)))) |
91 | 87, 90 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (π β 0 β€ (ββ(2
logb π΅))) |
92 | 66, 91 | jca 511 |
. . . . . . . . . . . 12
β’ (π β ((ββ(2
logb π΅)) β
β€ β§ 0 β€ (ββ(2 logb π΅)))) |
93 | | elnn0z 12575 |
. . . . . . . . . . . 12
β’
((ββ(2 logb π΅)) β β0 β
((ββ(2 logb π΅)) β β€ β§ 0 β€
(ββ(2 logb π΅)))) |
94 | 92, 93 | sylibr 233 |
. . . . . . . . . . 11
β’ (π β (ββ(2
logb π΅)) β
β0) |
95 | 64, 94 | nnexpcld 14213 |
. . . . . . . . . 10
β’ (π β (πβ(ββ(2 logb
π΅))) β
β) |
96 | | fzfid 13944 |
. . . . . . . . . . 11
β’ (π β (1...(ββ((2
logb π)β2))) β Fin) |
97 | 12 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β π β β€) |
98 | | elfznn 13536 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...(ββ((2
logb π)β2))) β π β β) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β π β β) |
100 | 99 | nnnn0d 12536 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β π β β0) |
101 | | zexpcl 14047 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β0)
β (πβπ) β
β€) |
102 | 97, 100, 101 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (πβπ) β β€) |
103 | | 1zzd 12597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 β
β€) |
104 | 102, 103 | zsubcld 12675 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β ((πβπ) β 1) β β€) |
105 | | 1cnd 11213 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 β
β) |
106 | 105 | addridd 11418 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (1 + 0) =
1) |
107 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 β
β) |
108 | | 1nn0 12492 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β0 |
109 | 108 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 β
β0) |
110 | 13, 109 | reexpcld 14133 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πβ1) β β) |
111 | 110 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (πβ1) β β) |
112 | 102 | zred 12670 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (πβπ) β β) |
113 | | 1lt3 12389 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 <
3 |
114 | 113 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β 1 < 3) |
115 | 22, 16, 13, 114, 20 | ltletrd 11378 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 < π) |
116 | 13 | recnd 11246 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β) |
117 | 116 | exp1d 14111 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πβ1) = π) |
118 | 117 | eqcomd 2732 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π = (πβ1)) |
119 | 115, 118 | breqtrd 5167 |
. . . . . . . . . . . . . . . . 17
β’ (π β 1 < (πβ1)) |
120 | 119 | adantr 480 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 < (πβ1)) |
121 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β π β β) |
122 | 64 | nnge1d 12264 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 β€ π) |
123 | 122 | adantr 480 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 β€ π) |
124 | | elfzuz 13503 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...(ββ((2
logb π)β2))) β π β
(β€β₯β1)) |
125 | 124 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β π β
(β€β₯β1)) |
126 | 121, 123,
125 | leexp2ad 14222 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (πβ1) β€ (πβπ)) |
127 | 107, 111,
112, 120, 126 | ltletrd 11378 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 1 < (πβπ)) |
128 | 106, 127 | eqbrtrd 5163 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (1 + 0) < (πβπ)) |
129 | 14 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 0 β
β) |
130 | 107, 129,
112 | ltaddsub2d 11819 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β ((1 + 0) < (πβπ) β 0 < ((πβπ) β 1))) |
131 | 128, 130 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β 0 < ((πβπ) β 1)) |
132 | 104, 131 | jca 511 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β (((πβπ) β 1) β β€ β§ 0 <
((πβπ) β 1))) |
133 | | elnnz 12572 |
. . . . . . . . . . . 12
β’ (((πβπ) β 1) β β β (((πβπ) β 1) β β€ β§ 0 <
((πβπ) β 1))) |
134 | 132, 133 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...(ββ((2
logb π)β2)))) β ((πβπ) β 1) β β) |
135 | 96, 134 | fprodnncl 15905 |
. . . . . . . . . 10
β’ (π β βπ β (1...(ββ((2
logb π)β2)))((πβπ) β 1) β β) |
136 | 95, 135 | nnmulcld 12269 |
. . . . . . . . 9
β’ (π β ((πβ(ββ(2 logb
π΅))) Β· βπ β (1...(ββ((2
logb π)β2)))((πβπ) β 1)) β
β) |
137 | 62, 136 | eqeltrd 2827 |
. . . . . . . 8
β’ (π β π΄ β β) |
138 | 137 | nnred 12231 |
. . . . . . 7
β’ (π β π΄ β β) |
139 | 138 | adantr 480 |
. . . . . 6
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β π΄ β β) |
140 | 1, 2, 3 | aks4d1p2 41458 |
. . . . . . 7
β’ (π β (2βπ΅) β€ (lcmβ(1...π΅))) |
141 | 140 | adantr 480 |
. . . . . 6
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (2βπ΅) β€ (lcmβ(1...π΅))) |
142 | 137 | nnzd 12589 |
. . . . . . . . . . 11
β’ (π β π΄ β β€) |
143 | 142 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β π΄ β β€) |
144 | 56 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (1...π΅) β β€) |
145 | | fzfid 13944 |
. . . . . . . . . 10
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (1...π΅) β Fin) |
146 | | lcmfdvdsb 16587 |
. . . . . . . . . 10
β’ ((π΄ β β€ β§ (1...π΅) β β€ β§
(1...π΅) β Fin) β
(βπ β
(1...π΅)π β₯ π΄ β (lcmβ(1...π΅)) β₯ π΄)) |
147 | 143, 144,
145, 146 | syl3anc 1368 |
. . . . . . . . 9
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (βπ β (1...π΅)π β₯ π΄ β (lcmβ(1...π΅)) β₯ π΄)) |
148 | 147 | biimpd 228 |
. . . . . . . 8
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (βπ β (1...π΅)π β₯ π΄ β (lcmβ(1...π΅)) β₯ π΄)) |
149 | 148 | syldbl2 838 |
. . . . . . 7
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (lcmβ(1...π΅)) β₯ π΄) |
150 | 59 | nn0zd 12588 |
. . . . . . . . 9
β’ (π β
(lcmβ(1...π΅))
β β€) |
151 | 150 | adantr 480 |
. . . . . . . 8
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (lcmβ(1...π΅)) β
β€) |
152 | 137 | adantr 480 |
. . . . . . . 8
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β π΄ β β) |
153 | | dvdsle 16260 |
. . . . . . . 8
β’
(((lcmβ(1...π΅)) β β€ β§ π΄ β β) β
((lcmβ(1...π΅))
β₯ π΄ β
(lcmβ(1...π΅))
β€ π΄)) |
154 | 151, 152,
153 | syl2anc 583 |
. . . . . . 7
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β ((lcmβ(1...π΅)) β₯ π΄ β (lcmβ(1...π΅)) β€ π΄)) |
155 | 149, 154 | mpd 15 |
. . . . . 6
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (lcmβ(1...π΅)) β€ π΄) |
156 | 51, 61, 139, 141, 155 | letrd 11375 |
. . . . 5
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β (2βπ΅) β€ π΄) |
157 | 51, 139 | lenltd 11364 |
. . . . 5
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β ((2βπ΅) β€ π΄ β Β¬ π΄ < (2βπ΅))) |
158 | 156, 157 | mpbid 231 |
. . . 4
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β Β¬ π΄ < (2βπ΅)) |
159 | 5, 158 | pm2.21dd 194 |
. . 3
β’ ((π β§ βπ β (1...π΅)π β₯ π΄) β Β¬ βπ β (1...π΅)π β₯ π΄) |
160 | | simpr 484 |
. . 3
β’ ((π β§ Β¬ βπ β (1...π΅)π β₯ π΄) β Β¬ βπ β (1...π΅)π β₯ π΄) |
161 | 159, 160 | pm2.61dan 810 |
. 2
β’ (π β Β¬ βπ β (1...π΅)π β₯ π΄) |
162 | | rexnal 3094 |
. 2
β’
(βπ β
(1...π΅) Β¬ π β₯ π΄ β Β¬ βπ β (1...π΅)π β₯ π΄) |
163 | 161, 162 | sylibr 233 |
1
β’ (π β βπ β (1...π΅) Β¬ π β₯ π΄) |