Step | Hyp | Ref
| Expression |
1 | | prmuz2 16579 |
. . 3
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
2 | | euclemma 16596 |
. . . . . 6
โข ((๐ โ โ โง ๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
3 | 2 | 3expb 1121 |
. . . . 5
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
4 | 3 | biimpd 228 |
. . . 4
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
5 | 4 | ralrimivva 3198 |
. . 3
โข (๐ โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
6 | 1, 5 | jca 513 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)))) |
7 | | simpl 484 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โ
(โคโฅโ2)) |
8 | | eluz2nn 12816 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
9 | 8 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โ) |
10 | 9 | nnzd 12533 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โค) |
11 | | iddvds 16159 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โฅ ๐) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โฅ ๐) |
13 | | nncn 12168 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
14 | 9, 13 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โ) |
15 | | nncn 12168 |
. . . . . . . . . . . 12
โข (๐ง โ โ โ ๐ง โ
โ) |
16 | 15 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ) |
17 | | nnne0 12194 |
. . . . . . . . . . . 12
โข (๐ง โ โ โ ๐ง โ 0) |
18 | 17 | ad2antrl 727 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ 0) |
19 | 14, 16, 18 | divcan1d 11939 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / ๐ง) ยท ๐ง) = ๐) |
20 | 12, 19 | breqtrrd 5138 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง)) |
21 | 20 | adantr 482 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง)) |
22 | | simprr 772 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โฅ ๐) |
23 | | simprl 770 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ) |
24 | | nndivdvds 16152 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ง โ โ) โ (๐ง โฅ ๐ โ (๐ / ๐ง) โ โ)) |
25 | 9, 23, 24 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ / ๐ง) โ โ)) |
26 | 22, 25 | mpbid 231 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / ๐ง) โ โ) |
27 | 26 | nnzd 12533 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / ๐ง) โ โค) |
28 | | nnz 12527 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ๐ง โ
โค) |
29 | 28 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โค) |
30 | 27, 29 | jca 513 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / ๐ง) โ โค โง ๐ง โ โค)) |
31 | | oveq1 7369 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ / ๐ง) โ (๐ฅ ยท ๐ฆ) = ((๐ / ๐ง) ยท ๐ฆ)) |
32 | 31 | breq2d 5122 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / ๐ง) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ฆ))) |
33 | | breq2 5114 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ / ๐ง) โ (๐ โฅ ๐ฅ โ ๐ โฅ (๐ / ๐ง))) |
34 | 33 | orbi1d 916 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / ๐ง) โ ((๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ))) |
35 | 32, 34 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฅ = (๐ / ๐ง) โ ((๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ)))) |
36 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ง โ ((๐ / ๐ง) ยท ๐ฆ) = ((๐ / ๐ง) ยท ๐ง)) |
37 | 36 | breq2d 5122 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ง โ (๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง))) |
38 | | breq2 5114 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ง โ (๐ โฅ ๐ฆ โ ๐ โฅ ๐ง)) |
39 | 38 | orbi2d 915 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ง โ ((๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
40 | 37, 39 | imbi12d 345 |
. . . . . . . . . 10
โข (๐ฆ = ๐ง โ ((๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ)) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)))) |
41 | 35, 40 | rspc2va 3594 |
. . . . . . . . 9
โข ((((๐ / ๐ง) โ โค โง ๐ง โ โค) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
42 | 30, 41 | sylan 581 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
43 | 21, 42 | mpd 15 |
. . . . . . 7
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)) |
44 | | dvdsle 16199 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง (๐ / ๐ง) โ โ) โ (๐ โฅ (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
45 | 10, 26, 44 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
46 | 14 | div1d 11930 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / 1) = ๐) |
47 | 46 | breq1d 5120 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / 1) โค (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
48 | 45, 47 | sylibrd 259 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ (๐ / 1) โค (๐ / ๐ง))) |
49 | | nnrp 12933 |
. . . . . . . . . . . . . 14
โข (๐ง โ โ โ ๐ง โ
โ+) |
50 | 49 | rpregt0d 12970 |
. . . . . . . . . . . . 13
โข (๐ง โ โ โ (๐ง โ โ โง 0 <
๐ง)) |
51 | 50 | ad2antrl 727 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โ โ โง 0 < ๐ง)) |
52 | | 1rp 12926 |
. . . . . . . . . . . . 13
โข 1 โ
โ+ |
53 | | rpregt0 12936 |
. . . . . . . . . . . . 13
โข (1 โ
โ+ โ (1 โ โ โง 0 < 1)) |
54 | 52, 53 | mp1i 13 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (1 โ โ โง 0 <
1)) |
55 | | nnrp 12933 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
56 | 9, 55 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ
โ+) |
57 | 56 | rpregt0d 12970 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โ โ โง 0 < ๐)) |
58 | | lediv2 12052 |
. . . . . . . . . . . 12
โข (((๐ง โ โ โง 0 <
๐ง) โง (1 โ โ
โง 0 < 1) โง (๐
โ โ โง 0 < ๐)) โ (๐ง โค 1 โ (๐ / 1) โค (๐ / ๐ง))) |
59 | 51, 54, 57, 58 | syl3anc 1372 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โค 1 โ (๐ / 1) โค (๐ / ๐ง))) |
60 | 48, 59 | sylibrd 259 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ง โค 1)) |
61 | | nnle1eq1 12190 |
. . . . . . . . . . 11
โข (๐ง โ โ โ (๐ง โค 1 โ ๐ง = 1)) |
62 | 61 | ad2antrl 727 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โค 1 โ ๐ง = 1)) |
63 | 60, 62 | sylibd 238 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ง = 1)) |
64 | | nnnn0 12427 |
. . . . . . . . . . . . 13
โข (๐ง โ โ โ ๐ง โ
โ0) |
65 | 64 | ad2antrl 727 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ0) |
66 | 65 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง โ โ0) |
67 | | nnnn0 12427 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
68 | 9, 67 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ
โ0) |
69 | 68 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ โ
โ0) |
70 | | simplrr 777 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง โฅ ๐) |
71 | | simpr 486 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ โฅ ๐ง) |
72 | | dvdseq 16203 |
. . . . . . . . . . 11
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง (๐ง โฅ ๐ โง ๐ โฅ ๐ง)) โ ๐ง = ๐) |
73 | 66, 69, 70, 71, 72 | syl22anc 838 |
. . . . . . . . . 10
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง = ๐) |
74 | 73 | ex 414 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ ๐ง โ ๐ง = ๐)) |
75 | 63, 74 | orim12d 964 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง) โ (๐ง = 1 โจ ๐ง = ๐))) |
76 | 75 | imp 408 |
. . . . . . 7
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)) โ (๐ง = 1 โจ ๐ง = ๐)) |
77 | 43, 76 | syldan 592 |
. . . . . 6
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ง = 1 โจ ๐ง = ๐)) |
78 | 77 | an32s 651 |
. . . . 5
โข (((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง = 1 โจ ๐ง = ๐)) |
79 | 78 | expr 458 |
. . . 4
โข (((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โง ๐ง โ โ) โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐))) |
80 | 79 | ralrimiva 3144 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ โ๐ง โ โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐))) |
81 | | isprm2 16565 |
. . 3
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ง โ โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐)))) |
82 | 7, 80, 81 | sylanbrc 584 |
. 2
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โ โ) |
83 | 6, 82 | impbii 208 |
1
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)))) |