Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
2 | | elfzoelz 13581 |
. . . . 5
โข (๐ โ (1..^๐) โ ๐ โ โค) |
3 | 2 | adantl 483 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โค) |
4 | | prmnn 16558 |
. . . . 5
โข (๐ โ โ โ ๐ โ
โ) |
5 | | prmz 16559 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
โค) |
6 | | fzoval 13582 |
. . . . . . . 8
โข (๐ โ โค โ
(1..^๐) = (1...(๐ โ 1))) |
7 | 5, 6 | syl 17 |
. . . . . . 7
โข (๐ โ โ โ
(1..^๐) = (1...(๐ โ 1))) |
8 | 7 | eleq2d 2820 |
. . . . . 6
โข (๐ โ โ โ (๐ โ (1..^๐) โ ๐ โ (1...(๐ โ 1)))) |
9 | 8 | biimpa 478 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ (1...(๐ โ 1))) |
10 | | fzm1ndvds 16212 |
. . . . 5
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐) |
11 | 4, 9, 10 | syl2an2r 684 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ยฌ ๐ โฅ ๐) |
12 | | eqid 2733 |
. . . . . . 7
โข ((๐โ(๐ โ 2)) mod ๐) = ((๐โ(๐ โ 2)) mod ๐) |
13 | 12 | modprminv 16679 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ (((๐โ(๐ โ 2)) mod ๐) โ (1...(๐ โ 1)) โง ((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1)) |
14 | 13 | simpld 496 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ ((๐โ(๐ โ 2)) mod ๐) โ (1...(๐ โ 1))) |
15 | 13 | simprd 497 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ ((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1) |
16 | | 1eluzge0 12825 |
. . . . . . . . . . 11
โข 1 โ
(โคโฅโ0) |
17 | | fzss1 13489 |
. . . . . . . . . . 11
โข (1 โ
(โคโฅโ0) โ (1...(๐ โ 1)) โ (0...(๐ โ 1))) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . 10
โข (๐ โ โ โ
(1...(๐ โ 1)) โ
(0...(๐ โ
1))) |
19 | 18 | sseld 3947 |
. . . . . . . . 9
โข (๐ โ โ โ (๐ โ (1...(๐ โ 1)) โ ๐ โ (0...(๐ โ 1)))) |
20 | 19 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ (๐ โ (1...(๐ โ 1)) โ ๐ โ (0...(๐ โ 1)))) |
21 | 20 | imdistani 570 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โง ๐ โ (1...(๐ โ 1))) โ ((๐ โ โ โง ๐ โ โค โง ยฌ ๐ โฅ ๐) โง ๐ โ (0...(๐ โ 1)))) |
22 | 12 | modprminveq 16680 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ ((๐ โ (0...(๐ โ 1)) โง ((๐ ยท ๐ ) mod ๐) = 1) โ ๐ = ((๐โ(๐ โ 2)) mod ๐))) |
23 | 22 | biimpa 478 |
. . . . . . . . 9
โข (((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โง (๐ โ (0...(๐ โ 1)) โง ((๐ ยท ๐ ) mod ๐) = 1)) โ ๐ = ((๐โ(๐ โ 2)) mod ๐)) |
24 | 23 | eqcomd 2739 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โง (๐ โ (0...(๐ โ 1)) โง ((๐ ยท ๐ ) mod ๐) = 1)) โ ((๐โ(๐ โ 2)) mod ๐) = ๐ ) |
25 | 24 | expr 458 |
. . . . . . 7
โข (((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โง ๐ โ (0...(๐ โ 1))) โ (((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )) |
26 | 21, 25 | syl 17 |
. . . . . 6
โข (((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โง ๐ โ (1...(๐ โ 1))) โ (((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )) |
27 | 26 | ralrimiva 3140 |
. . . . 5
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )) |
28 | 14, 15, 27 | jca32 517 |
. . . 4
โข ((๐ โ โ โง ๐ โ โค โง ยฌ
๐ โฅ ๐) โ (((๐โ(๐ โ 2)) mod ๐) โ (1...(๐ โ 1)) โง (((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )))) |
29 | 1, 3, 11, 28 | syl3anc 1372 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (((๐โ(๐ โ 2)) mod ๐) โ (1...(๐ โ 1)) โง (((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )))) |
30 | | oveq2 7369 |
. . . . . . 7
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (๐ ยท ๐) = (๐ ยท ((๐โ(๐ โ 2)) mod ๐))) |
31 | 30 | oveq1d 7376 |
. . . . . 6
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ ((๐ ยท ๐) mod ๐) = ((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐)) |
32 | 31 | eqeq1d 2735 |
. . . . 5
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (((๐ ยท ๐) mod ๐) = 1 โ ((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1)) |
33 | | eqeq1 2737 |
. . . . . . 7
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (๐ = ๐ โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )) |
34 | 33 | imbi2d 341 |
. . . . . 6
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ ((((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ ) โ (((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ ))) |
35 | 34 | ralbidv 3171 |
. . . . 5
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ (โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ ) โ โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ ))) |
36 | 32, 35 | anbi12d 632 |
. . . 4
โข (๐ = ((๐โ(๐ โ 2)) mod ๐) โ ((((๐ ยท ๐) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ )) โ (((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ )))) |
37 | 36 | rspcev 3583 |
. . 3
โข ((((๐โ(๐ โ 2)) mod ๐) โ (1...(๐ โ 1)) โง (((๐ ยท ((๐โ(๐ โ 2)) mod ๐)) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ((๐โ(๐ โ 2)) mod ๐) = ๐ ))) โ โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ ))) |
38 | 29, 37 | syl 17 |
. 2
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ ))) |
39 | | oveq2 7369 |
. . . . 5
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐ )) |
40 | 39 | oveq1d 7376 |
. . . 4
โข (๐ = ๐ โ ((๐ ยท ๐) mod ๐) = ((๐ ยท ๐ ) mod ๐)) |
41 | 40 | eqeq1d 2735 |
. . 3
โข (๐ = ๐ โ (((๐ ยท ๐) mod ๐) = 1 โ ((๐ ยท ๐ ) mod ๐) = 1)) |
42 | 41 | reu8 3695 |
. 2
โข
(โ!๐ โ
(1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1 โ โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐) mod ๐) = 1 โง โ๐ โ (1...(๐ โ 1))(((๐ ยท ๐ ) mod ๐) = 1 โ ๐ = ๐ ))) |
43 | 38, 42 | sylibr 233 |
1
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ โ!๐ โ (1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1) |