Step | Hyp | Ref
| Expression |
1 | | ssrab2 4042 |
. . 3
โข {๐ โ โ โฃ (๐โ2) โฅ ๐} โ
โ |
2 | | breq2 5114 |
. . . . . . 7
โข (๐ = ๐ โ ((๐โ2) โฅ ๐ โ (๐โ2) โฅ ๐)) |
3 | 2 | rabbidv 3418 |
. . . . . 6
โข (๐ = ๐ โ {๐ โ โ โฃ (๐โ2) โฅ ๐} = {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
4 | 3 | supeq1d 9389 |
. . . . 5
โข (๐ = ๐ โ sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < ) = sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
5 | | prmreclem1.1 |
. . . . 5
โข ๐ = (๐ โ โ โฆ sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, <
)) |
6 | | ltso 11242 |
. . . . . 6
โข < Or
โ |
7 | 6 | supex 9406 |
. . . . 5
โข
sup({๐ โ
โ โฃ (๐โ2)
โฅ ๐}, โ, < )
โ V |
8 | 4, 5, 7 | fvmpt 6953 |
. . . 4
โข (๐ โ โ โ (๐โ๐) = sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
9 | | nnssz 12528 |
. . . . . 6
โข โ
โ โค |
10 | 1, 9 | sstri 3958 |
. . . . 5
โข {๐ โ โ โฃ (๐โ2) โฅ ๐} โ
โค |
11 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = 1 โ (๐โ2) = (1โ2)) |
12 | | sq1 14106 |
. . . . . . . . 9
โข
(1โ2) = 1 |
13 | 11, 12 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ = 1 โ (๐โ2) = 1) |
14 | 13 | breq1d 5120 |
. . . . . . 7
โข (๐ = 1 โ ((๐โ2) โฅ ๐ โ 1 โฅ ๐)) |
15 | | 1nn 12171 |
. . . . . . . 8
โข 1 โ
โ |
16 | 15 | a1i 11 |
. . . . . . 7
โข (๐ โ โ โ 1 โ
โ) |
17 | | nnz 12527 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
18 | | 1dvds 16160 |
. . . . . . . 8
โข (๐ โ โค โ 1 โฅ
๐) |
19 | 17, 18 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ 1 โฅ
๐) |
20 | 14, 16, 19 | elrabd 3652 |
. . . . . 6
โข (๐ โ โ โ 1 โ
{๐ โ โ โฃ
(๐โ2) โฅ ๐}) |
21 | 20 | ne0d 4300 |
. . . . 5
โข (๐ โ โ โ {๐ โ โ โฃ (๐โ2) โฅ ๐} โ โ
) |
22 | | nnz 12527 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ๐ง โ
โค) |
23 | | zsqcl 14041 |
. . . . . . . . . . 11
โข (๐ง โ โค โ (๐งโ2) โ
โค) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
โข (๐ง โ โ โ (๐งโ2) โ
โค) |
25 | | id 22 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
26 | | dvdsle 16199 |
. . . . . . . . . 10
โข (((๐งโ2) โ โค โง
๐ โ โ) โ
((๐งโ2) โฅ ๐ โ (๐งโ2) โค ๐)) |
27 | 24, 25, 26 | syl2anr 598 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ง โ โ) โ ((๐งโ2) โฅ ๐ โ (๐งโ2) โค ๐)) |
28 | | nnlesq 14116 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ๐ง โค (๐งโ2)) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ง โ โ) โ ๐ง โค (๐งโ2)) |
30 | | nnre 12167 |
. . . . . . . . . . . 12
โข (๐ง โ โ โ ๐ง โ
โ) |
31 | 30 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ง โ โ) โ ๐ง โ
โ) |
32 | 31 | resqcld 14037 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ง โ โ) โ (๐งโ2) โ
โ) |
33 | | nnre 12167 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
34 | 33 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ง โ โ) โ ๐ โ
โ) |
35 | | letr 11256 |
. . . . . . . . . . 11
โข ((๐ง โ โ โง (๐งโ2) โ โ โง
๐ โ โ) โ
((๐ง โค (๐งโ2) โง (๐งโ2) โค ๐) โ ๐ง โค ๐)) |
36 | 31, 32, 34, 35 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ง โ โ) โ ((๐ง โค (๐งโ2) โง (๐งโ2) โค ๐) โ ๐ง โค ๐)) |
37 | 29, 36 | mpand 694 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ง โ โ) โ ((๐งโ2) โค ๐ โ ๐ง โค ๐)) |
38 | 27, 37 | syld 47 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ง โ โ) โ ((๐งโ2) โฅ ๐ โ ๐ง โค ๐)) |
39 | 38 | ralrimiva 3144 |
. . . . . . 7
โข (๐ โ โ โ
โ๐ง โ โ
((๐งโ2) โฅ ๐ โ ๐ง โค ๐)) |
40 | | oveq1 7369 |
. . . . . . . . 9
โข (๐ = ๐ง โ (๐โ2) = (๐งโ2)) |
41 | 40 | breq1d 5120 |
. . . . . . . 8
โข (๐ = ๐ง โ ((๐โ2) โฅ ๐ โ (๐งโ2) โฅ ๐)) |
42 | 41 | ralrab 3656 |
. . . . . . 7
โข
(โ๐ง โ
{๐ โ โ โฃ
(๐โ2) โฅ ๐}๐ง โค ๐ โ โ๐ง โ โ ((๐งโ2) โฅ ๐ โ ๐ง โค ๐)) |
43 | 39, 42 | sylibr 233 |
. . . . . 6
โข (๐ โ โ โ
โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐) |
44 | | brralrspcev 5170 |
. . . . . 6
โข ((๐ โ โค โง
โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐) โ โ๐ฅ โ โค โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐ฅ) |
45 | 17, 43, 44 | syl2anc 585 |
. . . . 5
โข (๐ โ โ โ
โ๐ฅ โ โค
โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐ฅ) |
46 | | suprzcl2 12870 |
. . . . 5
โข (({๐ โ โ โฃ (๐โ2) โฅ ๐} โ โค โง {๐ โ โ โฃ (๐โ2) โฅ ๐} โ โ
โง
โ๐ฅ โ โค
โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐ฅ) โ sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < ) โ {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
47 | 10, 21, 45, 46 | mp3an2i 1467 |
. . . 4
โข (๐ โ โ โ
sup({๐ โ โ
โฃ (๐โ2) โฅ
๐}, โ, < ) โ
{๐ โ โ โฃ
(๐โ2) โฅ ๐}) |
48 | 8, 47 | eqeltrd 2838 |
. . 3
โข (๐ โ โ โ (๐โ๐) โ {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
49 | 1, 48 | sselid 3947 |
. 2
โข (๐ โ โ โ (๐โ๐) โ โ) |
50 | | oveq1 7369 |
. . . . . 6
โข (๐ง = (๐โ๐) โ (๐งโ2) = ((๐โ๐)โ2)) |
51 | 50 | breq1d 5120 |
. . . . 5
โข (๐ง = (๐โ๐) โ ((๐งโ2) โฅ ๐ โ ((๐โ๐)โ2) โฅ ๐)) |
52 | 41 | cbvrabv 3420 |
. . . . 5
โข {๐ โ โ โฃ (๐โ2) โฅ ๐} = {๐ง โ โ โฃ (๐งโ2) โฅ ๐} |
53 | 51, 52 | elrab2 3653 |
. . . 4
โข ((๐โ๐) โ {๐ โ โ โฃ (๐โ2) โฅ ๐} โ ((๐โ๐) โ โ โง ((๐โ๐)โ2) โฅ ๐)) |
54 | 48, 53 | sylib 217 |
. . 3
โข (๐ โ โ โ ((๐โ๐) โ โ โง ((๐โ๐)โ2) โฅ ๐)) |
55 | 54 | simprd 497 |
. 2
โข (๐ โ โ โ ((๐โ๐)โ2) โฅ ๐) |
56 | 49 | adantr 482 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ (๐โ๐) โ โ) |
57 | 56 | nncnd 12176 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ (๐โ๐) โ โ) |
58 | 57 | mulid1d 11179 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ((๐โ๐) ยท 1) = (๐โ๐)) |
59 | | eluz2gt1 12852 |
. . . . . . . 8
โข (๐พ โ
(โคโฅโ2) โ 1 < ๐พ) |
60 | 59 | adantl 483 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ 1 < ๐พ) |
61 | | 1red 11163 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ 1 โ โ) |
62 | | eluz2nn 12816 |
. . . . . . . . . 10
โข (๐พ โ
(โคโฅโ2) โ ๐พ โ โ) |
63 | 62 | adantl 483 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ๐พ โ โ) |
64 | 63 | nnred 12175 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ๐พ โ โ) |
65 | 56 | nnred 12175 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ (๐โ๐) โ โ) |
66 | 56 | nngt0d 12209 |
. . . . . . . 8
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ 0 < (๐โ๐)) |
67 | | ltmul2 12013 |
. . . . . . . 8
โข ((1
โ โ โง ๐พ
โ โ โง ((๐โ๐) โ โ โง 0 < (๐โ๐))) โ (1 < ๐พ โ ((๐โ๐) ยท 1) < ((๐โ๐) ยท ๐พ))) |
68 | 61, 64, 65, 66, 67 | syl112anc 1375 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ (1 < ๐พ โ ((๐โ๐) ยท 1) < ((๐โ๐) ยท ๐พ))) |
69 | 60, 68 | mpbid 231 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ((๐โ๐) ยท 1) < ((๐โ๐) ยท ๐พ)) |
70 | 58, 69 | eqbrtrrd 5134 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ (๐โ๐) < ((๐โ๐) ยท ๐พ)) |
71 | | nnmulcl 12184 |
. . . . . . . 8
โข (((๐โ๐) โ โ โง ๐พ โ โ) โ ((๐โ๐) ยท ๐พ) โ โ) |
72 | 49, 62, 71 | syl2an 597 |
. . . . . . 7
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ((๐โ๐) ยท ๐พ) โ โ) |
73 | 72 | nnred 12175 |
. . . . . 6
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ((๐โ๐) ยท ๐พ) โ โ) |
74 | 65, 73 | ltnled 11309 |
. . . . 5
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ((๐โ๐) < ((๐โ๐) ยท ๐พ) โ ยฌ ((๐โ๐) ยท ๐พ) โค (๐โ๐))) |
75 | 70, 74 | mpbid 231 |
. . . 4
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ยฌ ((๐โ๐) ยท ๐พ) โค (๐โ๐)) |
76 | 45 | ad2antrr 725 |
. . . . . 6
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ โ๐ฅ โ โค โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐ฅ) |
77 | | oveq1 7369 |
. . . . . . . 8
โข (๐ = ((๐โ๐) ยท ๐พ) โ (๐โ2) = (((๐โ๐) ยท ๐พ)โ2)) |
78 | 77 | breq1d 5120 |
. . . . . . 7
โข (๐ = ((๐โ๐) ยท ๐พ) โ ((๐โ2) โฅ ๐ โ (((๐โ๐) ยท ๐พ)โ2) โฅ ๐)) |
79 | 72 | adantr 482 |
. . . . . . 7
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐) ยท ๐พ) โ โ) |
80 | | simpr 486 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) |
81 | 63 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ๐พ โ โ) |
82 | 81 | nnsqcld 14154 |
. . . . . . . . . . 11
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐พโ2) โ โ) |
83 | | nnz 12527 |
. . . . . . . . . . 11
โข ((๐พโ2) โ โ โ
(๐พโ2) โ
โค) |
84 | 82, 83 | syl 17 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐พโ2) โ โค) |
85 | 49 | nnsqcld 14154 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ((๐โ๐)โ2) โ โ) |
86 | 9, 85 | sselid 3947 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐โ๐)โ2) โ โค) |
87 | 85 | nnne0d 12210 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ((๐โ๐)โ2) โ 0) |
88 | | dvdsval2 16146 |
. . . . . . . . . . . . 13
โข ((((๐โ๐)โ2) โ โค โง ((๐โ๐)โ2) โ 0 โง ๐ โ โค) โ (((๐โ๐)โ2) โฅ ๐ โ (๐ / ((๐โ๐)โ2)) โ โค)) |
89 | 86, 87, 17, 88 | syl3anc 1372 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (((๐โ๐)โ2) โฅ ๐ โ (๐ / ((๐โ๐)โ2)) โ โค)) |
90 | 55, 89 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ โ โ (๐ / ((๐โ๐)โ2)) โ โค) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐ / ((๐โ๐)โ2)) โ โค) |
92 | 86 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐)โ2) โ โค) |
93 | | dvdscmul 16172 |
. . . . . . . . . 10
โข (((๐พโ2) โ โค โง
(๐ / ((๐โ๐)โ2)) โ โค โง ((๐โ๐)โ2) โ โค) โ ((๐พโ2) โฅ (๐ / ((๐โ๐)โ2)) โ (((๐โ๐)โ2) ยท (๐พโ2)) โฅ (((๐โ๐)โ2) ยท (๐ / ((๐โ๐)โ2))))) |
94 | 84, 91, 92, 93 | syl3anc 1372 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐พโ2) โฅ (๐ / ((๐โ๐)โ2)) โ (((๐โ๐)โ2) ยท (๐พโ2)) โฅ (((๐โ๐)โ2) ยท (๐ / ((๐โ๐)โ2))))) |
95 | 80, 94 | mpd 15 |
. . . . . . . 8
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (((๐โ๐)โ2) ยท (๐พโ2)) โฅ (((๐โ๐)โ2) ยท (๐ / ((๐โ๐)โ2)))) |
96 | 57 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐โ๐) โ โ) |
97 | 81 | nncnd 12176 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ๐พ โ โ) |
98 | 96, 97 | sqmuld 14070 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (((๐โ๐) ยท ๐พ)โ2) = (((๐โ๐)โ2) ยท (๐พโ2))) |
99 | 98 | eqcomd 2743 |
. . . . . . . 8
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (((๐โ๐)โ2) ยท (๐พโ2)) = (((๐โ๐) ยท ๐พ)โ2)) |
100 | | nncn 12168 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
101 | 100 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ๐ โ โ) |
102 | 85 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐)โ2) โ โ) |
103 | 102 | nncnd 12176 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐)โ2) โ โ) |
104 | 87 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐)โ2) โ 0) |
105 | 101, 103,
104 | divcan2d 11940 |
. . . . . . . 8
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (((๐โ๐)โ2) ยท (๐ / ((๐โ๐)โ2))) = ๐) |
106 | 95, 99, 105 | 3brtr3d 5141 |
. . . . . . 7
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (((๐โ๐) ยท ๐พ)โ2) โฅ ๐) |
107 | 78, 79, 106 | elrabd 3652 |
. . . . . 6
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐) ยท ๐พ) โ {๐ โ โ โฃ (๐โ2) โฅ ๐}) |
108 | | suprzub 12871 |
. . . . . 6
โข (({๐ โ โ โฃ (๐โ2) โฅ ๐} โ โค โง
โ๐ฅ โ โค
โ๐ง โ {๐ โ โ โฃ (๐โ2) โฅ ๐}๐ง โค ๐ฅ โง ((๐โ๐) ยท ๐พ) โ {๐ โ โ โฃ (๐โ2) โฅ ๐}) โ ((๐โ๐) ยท ๐พ) โค sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
109 | 10, 76, 107, 108 | mp3an2i 1467 |
. . . . 5
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐) ยท ๐พ) โค sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
110 | 8 | ad2antrr 725 |
. . . . 5
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ (๐โ๐) = sup({๐ โ โ โฃ (๐โ2) โฅ ๐}, โ, < )) |
111 | 109, 110 | breqtrrd 5138 |
. . . 4
โข (((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โง (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) โ ((๐โ๐) ยท ๐พ) โค (๐โ๐)) |
112 | 75, 111 | mtand 815 |
. . 3
โข ((๐ โ โ โง ๐พ โ
(โคโฅโ2)) โ ยฌ (๐พโ2) โฅ (๐ / ((๐โ๐)โ2))) |
113 | 112 | ex 414 |
. 2
โข (๐ โ โ โ (๐พ โ
(โคโฅโ2) โ ยฌ (๐พโ2) โฅ (๐ / ((๐โ๐)โ2)))) |
114 | 49, 55, 113 | 3jca 1129 |
1
โข (๐ โ โ โ ((๐โ๐) โ โ โง ((๐โ๐)โ2) โฅ ๐ โง (๐พ โ (โคโฅโ2)
โ ยฌ (๐พโ2)
โฅ (๐ / ((๐โ๐)โ2))))) |