Step | Hyp | Ref
| Expression |
1 | | aks4d1p7.1 |
. . . . . 6
โข (๐ โ ๐ โ
(โคโฅโ3)) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) โ ๐ โ
(โคโฅโ3)) |
3 | | aks4d1p7.2 |
. . . . 5
โข ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)) |
4 | | aks4d1p7.3 |
. . . . 5
โข ๐ต = (โโ((2
logb ๐)โ5)) |
5 | | aks4d1p7.4 |
. . . . 5
โข ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) |
6 | | breq1 5109 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โฅ ๐
โ ๐ โฅ ๐
)) |
7 | | breq1 5109 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โฅ ๐ โ ๐ โฅ ๐)) |
8 | 6, 7 | imbi12d 345 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โฅ ๐
โ ๐ โฅ ๐) โ (๐ โฅ ๐
โ ๐ โฅ ๐))) |
9 | 8 | cbvralvw 3224 |
. . . . . . 7
โข
(โ๐ โ
โ (๐ โฅ ๐
โ ๐ โฅ ๐) โ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
10 | 9 | biimpi 215 |
. . . . . 6
โข
(โ๐ โ
โ (๐ โฅ ๐
โ ๐ โฅ ๐) โ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
11 | 10 | adantl 483 |
. . . . 5
โข ((๐ โง โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) โ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
12 | 2, 3, 4, 5, 11 | aks4d1p7d1 40585 |
. . . 4
โข ((๐ โง โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) โ ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) |
13 | 5 | a1i 11 |
. . . . . . . . 9
โข (๐ โ ๐
= inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < )) |
14 | | ltso 11240 |
. . . . . . . . . . 11
โข < Or
โ |
15 | 14 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ < Or
โ) |
16 | | fzfid 13884 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐ต) โ Fin) |
17 | | ssrab2 4038 |
. . . . . . . . . . . . 13
โข {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ (1...๐ต) |
18 | 17 | a1i 11 |
. . . . . . . . . . . 12
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ (1...๐ต)) |
19 | 16, 18 | ssfid 9214 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin) |
20 | 1, 3, 4 | aks4d1p3 40581 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ (1...๐ต) ยฌ ๐ โฅ ๐ด) |
21 | | rabn0 4346 |
. . . . . . . . . . . 12
โข ({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
โ โ๐ โ (1...๐ต) ยฌ ๐ โฅ ๐ด) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
) |
23 | | elfznn 13476 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐ต) โ ๐ โ โ) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...๐ต)) โ ๐ โ โ) |
25 | 24 | nnred 12173 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...๐ต)) โ ๐ โ โ) |
26 | 25 | ex 414 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ (1...๐ต) โ ๐ โ โ)) |
27 | 26 | ssrdv 3951 |
. . . . . . . . . . . 12
โข (๐ โ (1...๐ต) โ โ) |
28 | 18, 27 | sstrd 3955 |
. . . . . . . . . . 11
โข (๐ โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ) |
29 | 19, 22, 28 | 3jca 1129 |
. . . . . . . . . 10
โข (๐ โ ({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ)) |
30 | | fiinfcl 9442 |
. . . . . . . . . 10
โข (( <
Or โ โง ({๐ โ
(1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ Fin โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ
โง {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ โ)) โ inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}) |
31 | 15, 29, 30 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ inf({๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}, โ, < ) โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}) |
32 | 13, 31 | eqeltrd 2834 |
. . . . . . . 8
โข (๐ โ ๐
โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด}) |
33 | | breq1 5109 |
. . . . . . . . . 10
โข (๐ = ๐
โ (๐ โฅ ๐ด โ ๐
โฅ ๐ด)) |
34 | 33 | notbid 318 |
. . . . . . . . 9
โข (๐ = ๐
โ (ยฌ ๐ โฅ ๐ด โ ยฌ ๐
โฅ ๐ด)) |
35 | 34 | elrab 3646 |
. . . . . . . 8
โข (๐
โ {๐ โ (1...๐ต) โฃ ยฌ ๐ โฅ ๐ด} โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
36 | 32, 35 | sylib 217 |
. . . . . . 7
โข (๐ โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
37 | 36 | simprd 497 |
. . . . . 6
โข (๐ โ ยฌ ๐
โฅ ๐ด) |
38 | 1, 3, 4, 5 | aks4d1p4 40582 |
. . . . . . . . . . . . 13
โข (๐ โ (๐
โ (1...๐ต) โง ยฌ ๐
โฅ ๐ด)) |
39 | 38 | simpld 496 |
. . . . . . . . . . . 12
โข (๐ โ ๐
โ (1...๐ต)) |
40 | 39 | elfzelzd 13448 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โค) |
41 | | eluzelz 12778 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ3) โ ๐ โ โค) |
42 | 1, 41 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ โค) |
43 | | 2re 12232 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 2 โ
โ) |
45 | | 2pos 12261 |
. . . . . . . . . . . . . . . . 17
โข 0 <
2 |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < 2) |
47 | 4 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต = (โโ((2 logb ๐)โ5))) |
48 | 42 | zred 12612 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ โ โ) |
49 | | 0red 11163 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 0 โ
โ) |
50 | | 3re 12238 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 3 โ
โ |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 3 โ
โ) |
52 | | 3pos 12263 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 <
3 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 0 < 3) |
54 | | eluzle 12781 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ
(โคโฅโ3) โ 3 โค ๐) |
55 | 1, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 3 โค ๐) |
56 | 49, 51, 48, 53, 55 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 0 < ๐) |
57 | | 1red 11161 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 โ
โ) |
58 | | 1lt2 12329 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 1 <
2 |
59 | 58 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ 1 < 2) |
60 | 57, 59 | ltned 11296 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ 1 โ 2) |
61 | 60 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ 2 โ 1) |
62 | 44, 46, 48, 56, 61 | relogbcld 40476 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (2 logb ๐) โ
โ) |
63 | | 5nn0 12438 |
. . . . . . . . . . . . . . . . . . . . 21
โข 5 โ
โ0 |
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 5 โ
โ0) |
65 | 62, 64 | reexpcld 14074 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((2 logb ๐)โ5) โ
โ) |
66 | 65 | ceilcld 13754 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โค) |
67 | 66 | zred 12612 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (โโ((2
logb ๐)โ5))
โ โ) |
68 | 47, 67 | eqeltrd 2834 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ โ) |
69 | | 9re 12257 |
. . . . . . . . . . . . . . . . . 18
โข 9 โ
โ |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 9 โ
โ) |
71 | | 9pos 12271 |
. . . . . . . . . . . . . . . . . 18
โข 0 <
9 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 < 9) |
73 | 48, 55 | 3lexlogpow5ineq4 40559 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 9 < ((2 logb
๐)โ5)) |
74 | 65 | ceilged 13757 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ((2 logb ๐)โ5) โค
(โโ((2 logb ๐)โ5))) |
75 | 70, 65, 67, 73, 74 | ltletrd 11320 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 9 < (โโ((2
logb ๐)โ5))) |
76 | 75, 47 | breqtrrd 5134 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 9 < ๐ต) |
77 | 49, 70, 68, 72, 76 | lttrd 11321 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 < ๐ต) |
78 | 44, 46, 68, 77, 61 | relogbcld 40476 |
. . . . . . . . . . . . . . 15
โข (๐ โ (2 logb ๐ต) โ
โ) |
79 | 78 | flcld 13709 |
. . . . . . . . . . . . . 14
โข (๐ โ (โโ(2
logb ๐ต)) โ
โค) |
80 | 44 | recnd 11188 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โ
โ) |
81 | 49, 46 | gtned 11295 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 2 โ 0) |
82 | | logb1 26135 |
. . . . . . . . . . . . . . . . . 18
โข ((2
โ โ โง 2 โ 0 โง 2 โ 1) โ (2 logb 1) =
0) |
83 | 80, 81, 61, 82 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (2 logb 1) =
0) |
84 | 83 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 = (2 logb
1)) |
85 | | 2z 12540 |
. . . . . . . . . . . . . . . . . 18
โข 2 โ
โค |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โ
โค) |
87 | 44 | leidd 11726 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 2 โค 2) |
88 | | 0lt1 11682 |
. . . . . . . . . . . . . . . . . 18
โข 0 <
1 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 0 < 1) |
90 | | 1lt9 12364 |
. . . . . . . . . . . . . . . . . . . 20
โข 1 <
9 |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 1 < 9) |
92 | 57, 70, 91 | ltled 11308 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 1 โค 9) |
93 | 70, 68, 76 | ltled 11308 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ 9 โค ๐ต) |
94 | 57, 70, 68, 92, 93 | letrd 11317 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ 1 โค ๐ต) |
95 | 86, 87, 57, 89, 68, 77, 94 | logblebd 40479 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 logb 1) โค
(2 logb ๐ต)) |
96 | 84, 95 | eqbrtrd 5128 |
. . . . . . . . . . . . . . 15
โข (๐ โ 0 โค (2 logb
๐ต)) |
97 | | 0zd 12516 |
. . . . . . . . . . . . . . . 16
โข (๐ โ 0 โ
โค) |
98 | | flge 13716 |
. . . . . . . . . . . . . . . 16
โข (((2
logb ๐ต) โ
โ โง 0 โ โค) โ (0 โค (2 logb ๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
99 | 78, 97, 98 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ (0 โค (2 logb
๐ต) โ 0 โค
(โโ(2 logb ๐ต)))) |
100 | 96, 99 | mpbid 231 |
. . . . . . . . . . . . . 14
โข (๐ โ 0 โค (โโ(2
logb ๐ต))) |
101 | 79, 100 | jca 513 |
. . . . . . . . . . . . 13
โข (๐ โ ((โโ(2
logb ๐ต)) โ
โค โง 0 โค (โโ(2 logb ๐ต)))) |
102 | | elnn0z 12517 |
. . . . . . . . . . . . 13
โข
((โโ(2 logb ๐ต)) โ โ0 โ
((โโ(2 logb ๐ต)) โ โค โง 0 โค
(โโ(2 logb ๐ต)))) |
103 | 101, 102 | sylibr 233 |
. . . . . . . . . . . 12
โข (๐ โ (โโ(2
logb ๐ต)) โ
โ0) |
104 | 42, 103 | zexpcld 13999 |
. . . . . . . . . . 11
โข (๐ โ (๐โ(โโ(2 logb
๐ต))) โ
โค) |
105 | | fzfid 13884 |
. . . . . . . . . . . 12
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ Fin) |
106 | 42 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โค) |
107 | | elfznn 13476 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...(โโ((2
logb ๐)โ2))) โ ๐ โ โ) |
108 | 107 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ) |
109 | 108 | nnnn0d 12478 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ๐ โ โ0) |
110 | 106, 109 | zexpcld 13999 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ (๐โ๐) โ โค) |
111 | | 1zzd 12539 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ 1 โ
โค) |
112 | 110, 111 | zsubcld 12617 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (1...(โโ((2
logb ๐)โ2)))) โ ((๐โ๐) โ 1) โ โค) |
113 | 105, 112 | fprodzcl 15842 |
. . . . . . . . . . 11
โข (๐ โ โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1) โ โค) |
114 | | dvdsmultr1 16183 |
. . . . . . . . . . 11
โข ((๐
โ โค โง (๐โ(โโ(2
logb ๐ต))) โ
โค โง โ๐
โ (1...(โโ((2 logb ๐)โ2)))((๐โ๐) โ 1) โ โค) โ (๐
โฅ (๐โ(โโ(2 logb
๐ต))) โ ๐
โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)))) |
115 | 40, 104, 113, 114 | syl3anc 1372 |
. . . . . . . . . 10
โข (๐ โ (๐
โฅ (๐โ(โโ(2 logb
๐ต))) โ ๐
โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)))) |
116 | 115 | imp 408 |
. . . . . . . . 9
โข ((๐ โง ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) โ ๐
โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
117 | 3 | a1i 11 |
. . . . . . . . . . 11
โข (๐ โ ๐ด = ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1))) |
118 | 117 | breq2d 5118 |
. . . . . . . . . 10
โข (๐ โ (๐
โฅ ๐ด โ ๐
โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)))) |
119 | 118 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) โ (๐
โฅ ๐ด โ ๐
โฅ ((๐โ(โโ(2 logb
๐ต))) ยท โ๐ โ (1...(โโ((2
logb ๐)โ2)))((๐โ๐) โ 1)))) |
120 | 116, 119 | mpbird 257 |
. . . . . . . 8
โข ((๐ โง ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) โ ๐
โฅ ๐ด) |
121 | 120 | ex 414 |
. . . . . . 7
โข (๐ โ (๐
โฅ (๐โ(โโ(2 logb
๐ต))) โ ๐
โฅ ๐ด)) |
122 | 121 | con3d 152 |
. . . . . 6
โข (๐ โ (ยฌ ๐
โฅ ๐ด โ ยฌ ๐
โฅ (๐โ(โโ(2 logb
๐ต))))) |
123 | 37, 122 | mpd 15 |
. . . . 5
โข (๐ โ ยฌ ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) |
124 | 123 | adantr 482 |
. . . 4
โข ((๐ โง โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) โ ยฌ ๐
โฅ (๐โ(โโ(2 logb
๐ต)))) |
125 | 12, 124 | pm2.65da 816 |
. . 3
โข (๐ โ ยฌ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
126 | | ianor 981 |
. . . . . . . 8
โข (ยฌ
(๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ (ยฌ ๐ โฅ ๐
โจ ยฌ ยฌ ๐ โฅ ๐)) |
127 | | notnotb 315 |
. . . . . . . . . 10
โข (๐ โฅ ๐ โ ยฌ ยฌ ๐ โฅ ๐) |
128 | 127 | orbi2i 912 |
. . . . . . . . 9
โข ((ยฌ
๐ โฅ ๐
โจ ๐ โฅ ๐) โ (ยฌ ๐ โฅ ๐
โจ ยฌ ยฌ ๐ โฅ ๐)) |
129 | 128 | bicomi 223 |
. . . . . . . 8
โข ((ยฌ
๐ โฅ ๐
โจ ยฌ ยฌ ๐ โฅ ๐) โ (ยฌ ๐ โฅ ๐
โจ ๐ โฅ ๐)) |
130 | 126, 129 | bitri 275 |
. . . . . . 7
โข (ยฌ
(๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ (ยฌ ๐ โฅ ๐
โจ ๐ โฅ ๐)) |
131 | | df-or 847 |
. . . . . . 7
โข ((ยฌ
๐ โฅ ๐
โจ ๐ โฅ ๐) โ (ยฌ ยฌ ๐ โฅ ๐
โ ๐ โฅ ๐)) |
132 | 130, 131 | bitri 275 |
. . . . . 6
โข (ยฌ
(๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ (ยฌ ยฌ ๐ โฅ ๐
โ ๐ โฅ ๐)) |
133 | | notnotb 315 |
. . . . . . . 8
โข (๐ โฅ ๐
โ ยฌ ยฌ ๐ โฅ ๐
) |
134 | 133 | imbi1i 350 |
. . . . . . 7
โข ((๐ โฅ ๐
โ ๐ โฅ ๐) โ (ยฌ ยฌ ๐ โฅ ๐
โ ๐ โฅ ๐)) |
135 | 134 | bicomi 223 |
. . . . . 6
โข ((ยฌ
ยฌ ๐ โฅ ๐
โ ๐ โฅ ๐) โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
136 | 132, 135 | bitri 275 |
. . . . 5
โข (ยฌ
(๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
137 | 136 | ralbii 3093 |
. . . 4
โข
(โ๐ โ
โ ยฌ (๐ โฅ
๐
โง ยฌ ๐ โฅ ๐) โ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
138 | 137 | notbii 320 |
. . 3
โข (ยฌ
โ๐ โ โ
ยฌ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ ยฌ โ๐ โ โ (๐ โฅ ๐
โ ๐ โฅ ๐)) |
139 | 125, 138 | sylibr 233 |
. 2
โข (๐ โ ยฌ โ๐ โ โ ยฌ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐)) |
140 | | ralnex 3072 |
. . . 4
โข
(โ๐ โ
โ ยฌ (๐ โฅ
๐
โง ยฌ ๐ โฅ ๐) โ ยฌ โ๐ โ โ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐)) |
141 | 140 | con2bii 358 |
. . 3
โข
(โ๐ โ
โ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ ยฌ โ๐ โ โ ยฌ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐)) |
142 | 141 | bicomi 223 |
. 2
โข (ยฌ
โ๐ โ โ
ยฌ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐) โ โ๐ โ โ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐)) |
143 | 139, 142 | sylib 217 |
1
โข (๐ โ โ๐ โ โ (๐ โฅ ๐
โง ยฌ ๐ โฅ ๐)) |