Step | Hyp | Ref
| Expression |
1 | | eluz2nn 12816 |
. 2
โข (๐ โ
(โคโฅโ2) โ ๐ โ โ) |
2 | | eleq1 2826 |
. . . 4
โข (๐ฅ = 1 โ (๐ฅ โ (โคโฅโ2)
โ 1 โ (โคโฅโ2))) |
3 | 2 | imbi1d 342 |
. . 3
โข (๐ฅ = 1 โ ((๐ฅ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฅ) โ (1 โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฅ))) |
4 | | eleq1 2826 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ฅ โ (โคโฅโ2)
โ ๐ฆ โ
(โคโฅโ2))) |
5 | | breq2 5114 |
. . . . 5
โข (๐ฅ = ๐ฆ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ฆ)) |
6 | 5 | rexbidv 3176 |
. . . 4
โข (๐ฅ = ๐ฆ โ (โ๐ โ โ ๐ โฅ ๐ฅ โ โ๐ โ โ ๐ โฅ ๐ฆ)) |
7 | 4, 6 | imbi12d 345 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ฅ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฅ) โ (๐ฆ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฆ))) |
8 | | eleq1 2826 |
. . . 4
โข (๐ฅ = ๐ง โ (๐ฅ โ (โคโฅโ2)
โ ๐ง โ
(โคโฅโ2))) |
9 | | breq2 5114 |
. . . . 5
โข (๐ฅ = ๐ง โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐ง)) |
10 | 9 | rexbidv 3176 |
. . . 4
โข (๐ฅ = ๐ง โ (โ๐ โ โ ๐ โฅ ๐ฅ โ โ๐ โ โ ๐ โฅ ๐ง)) |
11 | 8, 10 | imbi12d 345 |
. . 3
โข (๐ฅ = ๐ง โ ((๐ฅ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฅ) โ (๐ง โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ง))) |
12 | | eleq1 2826 |
. . . 4
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (๐ฅ โ (โคโฅโ2)
โ (๐ฆ ยท ๐ง) โ
(โคโฅโ2))) |
13 | | breq2 5114 |
. . . . 5
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (๐ โฅ ๐ฅ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
14 | 13 | rexbidv 3176 |
. . . 4
โข (๐ฅ = (๐ฆ ยท ๐ง) โ (โ๐ โ โ ๐ โฅ ๐ฅ โ โ๐ โ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
15 | 12, 14 | imbi12d 345 |
. . 3
โข (๐ฅ = (๐ฆ ยท ๐ง) โ ((๐ฅ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฅ) โ ((๐ฆ ยท ๐ง) โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ (๐ฆ ยท ๐ง)))) |
16 | | eleq1 2826 |
. . . 4
โข (๐ฅ = ๐ โ (๐ฅ โ (โคโฅโ2)
โ ๐ โ
(โคโฅโ2))) |
17 | | breq2 5114 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ โฅ ๐ฅ โ ๐ โฅ ๐)) |
18 | 17 | rexbidv 3176 |
. . . 4
โข (๐ฅ = ๐ โ (โ๐ โ โ ๐ โฅ ๐ฅ โ โ๐ โ โ ๐ โฅ ๐)) |
19 | 16, 18 | imbi12d 345 |
. . 3
โข (๐ฅ = ๐ โ ((๐ฅ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ฅ) โ (๐ โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐))) |
20 | | 1m1e0 12232 |
. . . . 5
โข (1
โ 1) = 0 |
21 | | uz2m1nn 12855 |
. . . . 5
โข (1 โ
(โคโฅโ2) โ (1 โ 1) โ
โ) |
22 | 20, 21 | eqeltrrid 2843 |
. . . 4
โข (1 โ
(โคโฅโ2) โ 0 โ โ) |
23 | | 0nnn 12196 |
. . . . 5
โข ยฌ 0
โ โ |
24 | 23 | pm2.21i 119 |
. . . 4
โข (0 โ
โ โ โ๐
โ โ ๐ โฅ
๐ฅ) |
25 | 22, 24 | syl 17 |
. . 3
โข (1 โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฅ) |
26 | | prmz 16558 |
. . . . . 6
โข (๐ฅ โ โ โ ๐ฅ โ
โค) |
27 | | iddvds 16159 |
. . . . . 6
โข (๐ฅ โ โค โ ๐ฅ โฅ ๐ฅ) |
28 | 26, 27 | syl 17 |
. . . . 5
โข (๐ฅ โ โ โ ๐ฅ โฅ ๐ฅ) |
29 | | breq1 5113 |
. . . . . 6
โข (๐ = ๐ฅ โ (๐ โฅ ๐ฅ โ ๐ฅ โฅ ๐ฅ)) |
30 | 29 | rspcev 3584 |
. . . . 5
โข ((๐ฅ โ โ โง ๐ฅ โฅ ๐ฅ) โ โ๐ โ โ ๐ โฅ ๐ฅ) |
31 | 28, 30 | mpdan 686 |
. . . 4
โข (๐ฅ โ โ โ
โ๐ โ โ
๐ โฅ ๐ฅ) |
32 | 31 | a1d 25 |
. . 3
โข (๐ฅ โ โ โ (๐ฅ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฅ)) |
33 | | simpl 484 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ ๐ฆ โ
(โคโฅโ2)) |
34 | | eluzelz 12780 |
. . . . . . . . . 10
โข (๐ฆ โ
(โคโฅโ2) โ ๐ฆ โ โค) |
35 | 34 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ฆ โ
โค) |
36 | | eluzelz 12780 |
. . . . . . . . . 10
โข (๐ง โ
(โคโฅโ2) โ ๐ง โ โค) |
37 | 36 | ad2antlr 726 |
. . . . . . . . 9
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ง โ
โค) |
38 | | dvdsmul1 16167 |
. . . . . . . . 9
โข ((๐ฆ โ โค โง ๐ง โ โค) โ ๐ฆ โฅ (๐ฆ ยท ๐ง)) |
39 | 35, 37, 38 | syl2anc 585 |
. . . . . . . 8
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ฆ โฅ (๐ฆ ยท ๐ง)) |
40 | | prmz 16558 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โค) |
41 | 40 | adantl 483 |
. . . . . . . . 9
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ๐ โ
โค) |
42 | 35, 37 | zmulcld 12620 |
. . . . . . . . 9
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ (๐ฆ ยท ๐ง) โ
โค) |
43 | | dvdstr 16183 |
. . . . . . . . 9
โข ((๐ โ โค โง ๐ฆ โ โค โง (๐ฆ ยท ๐ง) โ โค) โ ((๐ โฅ ๐ฆ โง ๐ฆ โฅ (๐ฆ ยท ๐ง)) โ ๐ โฅ (๐ฆ ยท ๐ง))) |
44 | 41, 35, 42, 43 | syl3anc 1372 |
. . . . . . . 8
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ ((๐ โฅ ๐ฆ โง ๐ฆ โฅ (๐ฆ ยท ๐ง)) โ ๐ โฅ (๐ฆ ยท ๐ง))) |
45 | 39, 44 | mpan2d 693 |
. . . . . . 7
โข (((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โง ๐ โ โ)
โ (๐ โฅ ๐ฆ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
46 | 45 | reximdva 3166 |
. . . . . 6
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (โ๐ โ
โ ๐ โฅ ๐ฆ โ โ๐ โ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
47 | 33, 46 | embantd 59 |
. . . . 5
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ ((๐ฆ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฆ) โ โ๐ โ โ ๐ โฅ (๐ฆ ยท ๐ง))) |
48 | 47 | a1dd 50 |
. . . 4
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ ((๐ฆ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฆ) โ ((๐ฆ ยท ๐ง) โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ (๐ฆ ยท ๐ง)))) |
49 | 48 | adantrd 493 |
. . 3
โข ((๐ฆ โ
(โคโฅโ2) โง ๐ง โ (โคโฅโ2))
โ (((๐ฆ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐ฆ) โง (๐ง โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ ๐ง)) โ ((๐ฆ ยท ๐ง) โ (โคโฅโ2)
โ โ๐ โ
โ ๐ โฅ (๐ฆ ยท ๐ง)))) |
50 | 3, 7, 11, 15, 19, 25, 32, 49 | prmind 16569 |
. 2
โข (๐ โ โ โ (๐ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐)) |
51 | 1, 50 | mpcom 38 |
1
โข (๐ โ
(โคโฅโ2) โ โ๐ โ โ ๐ โฅ ๐) |