Step | Hyp | Ref
| Expression |
1 | | prmuz2 12133 |
. . 3
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
2 | | euclemma 12148 |
. . . . . 6
โข ((๐ โ โ โง ๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
3 | 2 | 3expb 1204 |
. . . . 5
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
4 | 3 | biimpd 144 |
. . . 4
โข ((๐ โ โ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
5 | 4 | ralrimivva 2559 |
. . 3
โข (๐ โ โ โ
โ๐ฅ โ โค
โ๐ฆ โ โค
(๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) |
6 | 1, 5 | jca 306 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)))) |
7 | | simpl 109 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โ
(โคโฅโ2)) |
8 | | eluz2nn 9568 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
9 | 8 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โ) |
10 | 9 | nnzd 9376 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โค) |
11 | | iddvds 11813 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โฅ ๐) |
12 | 10, 11 | syl 14 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โฅ ๐) |
13 | | nncn 8929 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
14 | 9, 13 | syl 14 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ โ) |
15 | | nncn 8929 |
. . . . . . . . . . . 12
โข (๐ง โ โ โ ๐ง โ
โ) |
16 | 15 | ad2antrl 490 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ) |
17 | | nnap0 8950 |
. . . . . . . . . . . 12
โข (๐ง โ โ โ ๐ง # 0) |
18 | 17 | ad2antrl 490 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง # 0) |
19 | 14, 16, 18 | divcanap1d 8750 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / ๐ง) ยท ๐ง) = ๐) |
20 | 12, 19 | breqtrrd 4033 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง)) |
21 | 20 | adantr 276 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง)) |
22 | | simprr 531 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โฅ ๐) |
23 | | simprl 529 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ) |
24 | | nndivdvds 11805 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐ง โ โ) โ (๐ง โฅ ๐ โ (๐ / ๐ง) โ โ)) |
25 | 9, 23, 24 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โฅ ๐ โ (๐ / ๐ง) โ โ)) |
26 | 22, 25 | mpbid 147 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / ๐ง) โ โ) |
27 | 26 | nnzd 9376 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / ๐ง) โ โค) |
28 | | nnz 9274 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ๐ง โ
โค) |
29 | 28 | ad2antrl 490 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โค) |
30 | 27, 29 | jca 306 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / ๐ง) โ โค โง ๐ง โ โค)) |
31 | | oveq1 5884 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ / ๐ง) โ (๐ฅ ยท ๐ฆ) = ((๐ / ๐ง) ยท ๐ฆ)) |
32 | 31 | breq2d 4017 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / ๐ง) โ (๐ โฅ (๐ฅ ยท ๐ฆ) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ฆ))) |
33 | | breq2 4009 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ / ๐ง) โ (๐ โฅ ๐ฅ โ ๐ โฅ (๐ / ๐ง))) |
34 | 33 | orbi1d 791 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ / ๐ง) โ ((๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ))) |
35 | 32, 34 | imbi12d 234 |
. . . . . . . . . 10
โข (๐ฅ = (๐ / ๐ง) โ ((๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ)))) |
36 | | oveq2 5885 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ง โ ((๐ / ๐ง) ยท ๐ฆ) = ((๐ / ๐ง) ยท ๐ง)) |
37 | 36 | breq2d 4017 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ง โ (๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ ๐ โฅ ((๐ / ๐ง) ยท ๐ง))) |
38 | | breq2 4009 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ง โ (๐ โฅ ๐ฆ โ ๐ โฅ ๐ง)) |
39 | 38 | orbi2d 790 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ง โ ((๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
40 | 37, 39 | imbi12d 234 |
. . . . . . . . . 10
โข (๐ฆ = ๐ง โ ((๐ โฅ ((๐ / ๐ง) ยท ๐ฆ) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ฆ)) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)))) |
41 | 35, 40 | rspc2va 2857 |
. . . . . . . . 9
โข ((((๐ / ๐ง) โ โค โง ๐ง โ โค) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
42 | 30, 41 | sylan 283 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ ((๐ / ๐ง) ยท ๐ง) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง))) |
43 | 21, 42 | mpd 13 |
. . . . . . 7
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)) |
44 | | dvdsle 11852 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง (๐ / ๐ง) โ โ) โ (๐ โฅ (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
45 | 10, 26, 44 | syl2anc 411 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
46 | 14 | div1d 8739 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ / 1) = ๐) |
47 | 46 | breq1d 4015 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ / 1) โค (๐ / ๐ง) โ ๐ โค (๐ / ๐ง))) |
48 | 45, 47 | sylibrd 169 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ (๐ / 1) โค (๐ / ๐ง))) |
49 | | nnrp 9665 |
. . . . . . . . . . . . . 14
โข (๐ง โ โ โ ๐ง โ
โ+) |
50 | 49 | rpregt0d 9705 |
. . . . . . . . . . . . 13
โข (๐ง โ โ โ (๐ง โ โ โง 0 <
๐ง)) |
51 | 50 | ad2antrl 490 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โ โ โง 0 < ๐ง)) |
52 | | 1rp 9659 |
. . . . . . . . . . . . 13
โข 1 โ
โ+ |
53 | | rpregt0 9669 |
. . . . . . . . . . . . 13
โข (1 โ
โ+ โ (1 โ โ โง 0 < 1)) |
54 | 52, 53 | mp1i 10 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (1 โ โ โง 0 <
1)) |
55 | | nnrp 9665 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ ๐ โ
โ+) |
56 | 9, 55 | syl 14 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ
โ+) |
57 | 56 | rpregt0d 9705 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โ โ โง 0 < ๐)) |
58 | | lediv2 8850 |
. . . . . . . . . . . 12
โข (((๐ง โ โ โง 0 <
๐ง) โง (1 โ โ
โง 0 < 1) โง (๐
โ โ โง 0 < ๐)) โ (๐ง โค 1 โ (๐ / 1) โค (๐ / ๐ง))) |
59 | 51, 54, 57, 58 | syl3anc 1238 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โค 1 โ (๐ / 1) โค (๐ / ๐ง))) |
60 | 48, 59 | sylibrd 169 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ง โค 1)) |
61 | | nnle1eq1 8945 |
. . . . . . . . . . 11
โข (๐ง โ โ โ (๐ง โค 1 โ ๐ง = 1)) |
62 | 61 | ad2antrl 490 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง โค 1 โ ๐ง = 1)) |
63 | 60, 62 | sylibd 149 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ (๐ / ๐ง) โ ๐ง = 1)) |
64 | | nnnn0 9185 |
. . . . . . . . . . . . 13
โข (๐ง โ โ โ ๐ง โ
โ0) |
65 | 64 | ad2antrl 490 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ง โ โ0) |
66 | 65 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง โ โ0) |
67 | | nnnn0 9185 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ0) |
68 | 9, 67 | syl 14 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ๐ โ
โ0) |
69 | 68 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ โ
โ0) |
70 | | simplrr 536 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง โฅ ๐) |
71 | | simpr 110 |
. . . . . . . . . . 11
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ โฅ ๐ง) |
72 | | dvdseq 11856 |
. . . . . . . . . . 11
โข (((๐ง โ โ0
โง ๐ โ
โ0) โง (๐ง โฅ ๐ โง ๐ โฅ ๐ง)) โ ๐ง = ๐) |
73 | 66, 69, 70, 71, 72 | syl22anc 1239 |
. . . . . . . . . 10
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง ๐ โฅ ๐ง) โ ๐ง = ๐) |
74 | 73 | ex 115 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ โฅ ๐ง โ ๐ง = ๐)) |
75 | 63, 74 | orim12d 786 |
. . . . . . . 8
โข ((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ ((๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง) โ (๐ง = 1 โจ ๐ง = ๐))) |
76 | 75 | imp 124 |
. . . . . . 7
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง (๐ โฅ (๐ / ๐ง) โจ ๐ โฅ ๐ง)) โ (๐ง = 1 โจ ๐ง = ๐)) |
77 | 43, 76 | syldan 282 |
. . . . . 6
โข (((๐ โ
(โคโฅโ2) โง (๐ง โ โ โง ๐ง โฅ ๐)) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ (๐ง = 1 โจ ๐ง = ๐)) |
78 | 77 | an32s 568 |
. . . . 5
โข (((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โง (๐ง โ โ โง ๐ง โฅ ๐)) โ (๐ง = 1 โจ ๐ง = ๐)) |
79 | 78 | expr 375 |
. . . 4
โข (((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โง ๐ง โ โ) โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐))) |
80 | 79 | ralrimiva 2550 |
. . 3
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ โ๐ง โ โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐))) |
81 | | isprm2 12119 |
. . 3
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ง โ โ (๐ง โฅ ๐ โ (๐ง = 1 โจ ๐ง = ๐)))) |
82 | 7, 80, 81 | sylanbrc 417 |
. 2
โข ((๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ))) โ ๐ โ โ) |
83 | 6, 82 | impbii 126 |
1
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โง โ๐ฅ โ โค โ๐ฆ โ โค (๐ โฅ (๐ฅ ยท ๐ฆ) โ (๐ โฅ ๐ฅ โจ ๐ โฅ ๐ฆ)))) |