Step | Hyp | Ref
| Expression |
1 | | reumodprminv 12255 |
. . . 4
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ โ!๐ โ (1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1) |
2 | | reurex 2691 |
. . . 4
โข
(โ!๐ โ
(1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1 โ โ๐ โ (1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1) |
3 | | prmz 12113 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โค) |
4 | 3 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โค) |
5 | 4 | adantl 277 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โค) |
6 | | elfzelz 10027 |
. . . . . . . . . . 11
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โค) |
7 | 6 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โ ๐ โ โค) |
8 | | elfzoelz 10149 |
. . . . . . . . . . 11
โข (๐ผ โ (1..^๐) โ ๐ผ โ โค) |
9 | 8 | 3ad2ant3 1020 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ผ โ โค) |
10 | | zmulcl 9308 |
. . . . . . . . . 10
โข ((๐ โ โค โง ๐ผ โ โค) โ (๐ ยท ๐ผ) โ โค) |
11 | 7, 9, 10 | syl2an 289 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐ผ) โ โค) |
12 | 5, 11 | zsubcld 9382 |
. . . . . . . 8
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ โ (๐ ยท ๐ผ)) โ โค) |
13 | | prmnn 12112 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
14 | 13 | 3ad2ant1 1018 |
. . . . . . . . 9
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โ) |
15 | 14 | adantl 277 |
. . . . . . . 8
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
16 | | zmodfzo 10349 |
. . . . . . . 8
โข (((๐ โ (๐ ยท ๐ผ)) โ โค โง ๐ โ โ) โ ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (0..^๐)) |
17 | 12, 15, 16 | syl2anc 411 |
. . . . . . 7
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (0..^๐)) |
18 | 9 | adantl 277 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ โ โค) |
19 | | zq 9628 |
. . . . . . . . . 10
โข (๐ผ โ โค โ ๐ผ โ
โ) |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ โ โ) |
21 | | zq 9628 |
. . . . . . . . . 10
โข ((๐ โ (๐ ยท ๐ผ)) โ โค โ (๐ โ (๐ ยท ๐ผ)) โ โ) |
22 | 12, 21 | syl 14 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ โ (๐ ยท ๐ผ)) โ โ) |
23 | | elfzoelz 10149 |
. . . . . . . . . . 11
โข (๐ โ (1..^๐) โ ๐ โ โค) |
24 | 23 | 3ad2ant2 1019 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โค) |
25 | 24 | adantl 277 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โค) |
26 | | zq 9628 |
. . . . . . . . . 10
โข (๐ โ โค โ ๐ โ
โ) |
27 | 5, 26 | syl 14 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
28 | 15 | nngt0d 8965 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ 0 < ๐) |
29 | | modqaddmulmod 10393 |
. . . . . . . . 9
โข (((๐ผ โ โ โง (๐ โ (๐ ยท ๐ผ)) โ โ โง ๐ โ โค) โง (๐ โ โ โง 0 < ๐)) โ ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐) = ((๐ผ + ((๐ โ (๐ ยท ๐ผ)) ยท ๐)) mod ๐)) |
30 | 20, 22, 25, 27, 28, 29 | syl32anc 1246 |
. . . . . . . 8
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐) = ((๐ผ + ((๐ โ (๐ ยท ๐ผ)) ยท ๐)) mod ๐)) |
31 | 13 | nncnd 8935 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
32 | 31 | 3ad2ant1 1018 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โ) |
33 | 32 | adantl 277 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
34 | 6 | zcnd 9378 |
. . . . . . . . . . . . 13
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
35 | 34 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โ ๐ โ โ) |
36 | 8 | zcnd 9378 |
. . . . . . . . . . . . 13
โข (๐ผ โ (1..^๐) โ ๐ผ โ โ) |
37 | 36 | 3ad2ant3 1020 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ผ โ โ) |
38 | | mulcl 7940 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ผ โ โ) โ (๐ ยท ๐ผ) โ โ) |
39 | 35, 37, 38 | syl2an 289 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐ผ) โ โ) |
40 | 23 | zcnd 9378 |
. . . . . . . . . . . . 13
โข (๐ โ (1..^๐) โ ๐ โ โ) |
41 | 40 | 3ad2ant2 1019 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โ) |
42 | 41 | adantl 277 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
43 | 33, 39, 42 | subdird 8374 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ โ (๐ ยท ๐ผ)) ยท ๐) = ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐))) |
44 | 43 | oveq2d 5893 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ผ + ((๐ โ (๐ ยท ๐ผ)) ยท ๐)) = (๐ผ + ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)))) |
45 | 44 | oveq1d 5892 |
. . . . . . . 8
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + ((๐ โ (๐ ยท ๐ผ)) ยท ๐)) mod ๐) = ((๐ผ + ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐))) mod ๐)) |
46 | | mulcom 7942 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = (๐ ยท ๐)) |
47 | 31, 40, 46 | syl2an 289 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ (๐ ยท ๐) = (๐ ยท ๐)) |
48 | 47 | oveq1d 5892 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((๐ ยท ๐) mod ๐) = ((๐ ยท ๐) mod ๐)) |
49 | 23 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โค) |
50 | 3 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โค) |
51 | 50, 26 | syl 14 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ๐ โ โ) |
52 | 13 | nngt0d 8965 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ โ โ 0 <
๐) |
53 | 52 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ 0 < ๐) |
54 | | mulqmod0 10332 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โค โง ๐ โ โ โง 0 <
๐) โ ((๐ ยท ๐) mod ๐) = 0) |
55 | 49, 51, 53, 54 | syl3anc 1238 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((๐ ยท ๐) mod ๐) = 0) |
56 | 48, 55 | eqtrd 2210 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((๐ ยท ๐) mod ๐) = 0) |
57 | 56 | 3adant3 1017 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ((๐ ยท ๐) mod ๐) = 0) |
58 | 57 | adantl 277 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐) mod ๐) = 0) |
59 | 35 | adantr 276 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
60 | 37 | adantl 277 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ โ โ) |
61 | 59, 60, 42 | mul32d 8112 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐ผ) ยท ๐) = ((๐ ยท ๐) ยท ๐ผ)) |
62 | 61 | oveq1d 5892 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐) = (((๐ ยท ๐) ยท ๐ผ) mod ๐)) |
63 | | elfznn 10056 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1...(๐ โ 1)) โ ๐ โ โ) |
64 | 63 | adantr 276 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โ ๐ โ โ) |
65 | 64 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
66 | | elfzo1 10192 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (1..^๐) โ (๐ โ โ โง ๐ โ โ โง ๐ < ๐)) |
67 | 66 | simp1bi 1012 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ (1..^๐) โ ๐ โ โ) |
68 | 67 | 3ad2ant2 1019 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ โ โ) |
69 | 68 | adantl 277 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ โ โ) |
70 | 65, 69 | nnmulcld 8970 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐) โ โ) |
71 | | nnq 9635 |
. . . . . . . . . . . . . . . . 17
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ โ) |
72 | 70, 71 | syl 14 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐) โ โ) |
73 | | modqmulmod 10391 |
. . . . . . . . . . . . . . . 16
โข ((((๐ ยท ๐) โ โ โง ๐ผ โ โค) โง (๐ โ โ โง 0 < ๐)) โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐) = (((๐ ยท ๐) ยท ๐ผ) mod ๐)) |
74 | 72, 18, 27, 28, 73 | syl22anc 1239 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐) = (((๐ ยท ๐) ยท ๐ผ) mod ๐)) |
75 | 62, 74 | eqtr4d 2213 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐) = ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐)) |
76 | 58, 75 | oveq12d 5895 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐) mod ๐) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐)) = (0 โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐))) |
77 | 76 | oveq1d 5892 |
. . . . . . . . . . . 12
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((((๐ ยท ๐) mod ๐) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐)) mod ๐) = ((0 โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐)) mod ๐)) |
78 | 15, 69 | nnmulcld 8970 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐) โ โ) |
79 | | nnq 9635 |
. . . . . . . . . . . . . 14
โข ((๐ ยท ๐) โ โ โ (๐ ยท ๐) โ โ) |
80 | 78, 79 | syl 14 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐) โ โ) |
81 | | elfzo1 10192 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ (1..^๐) โ (๐ผ โ โ โง ๐ โ โ โง ๐ผ < ๐)) |
82 | 81 | simp1bi 1012 |
. . . . . . . . . . . . . . . . . 18
โข (๐ผ โ (1..^๐) โ ๐ผ โ โ) |
83 | 82 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ผ โ โ) |
84 | 83 | adantl 277 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ โ โ) |
85 | 65, 84 | nnmulcld 8970 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐ผ) โ โ) |
86 | 85, 69 | nnmulcld 8970 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐ผ) ยท ๐) โ โ) |
87 | | nnq 9635 |
. . . . . . . . . . . . . 14
โข (((๐ ยท ๐ผ) ยท ๐) โ โ โ ((๐ ยท ๐ผ) ยท ๐) โ โ) |
88 | 86, 87 | syl 14 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐ผ) ยท ๐) โ โ) |
89 | | modqsubmodmod 10385 |
. . . . . . . . . . . . 13
โข ((((๐ ยท ๐) โ โ โง ((๐ ยท ๐ผ) ยท ๐) โ โ) โง (๐ โ โ โง 0 < ๐)) โ ((((๐ ยท ๐) mod ๐) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐)) mod ๐) = (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) |
90 | 80, 88, 27, 28, 89 | syl22anc 1239 |
. . . . . . . . . . . 12
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((((๐ ยท ๐) mod ๐) โ (((๐ ยท ๐ผ) ยท ๐) mod ๐)) mod ๐) = (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) |
91 | | mulcom 7942 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) = (๐ ยท ๐)) |
92 | 41, 34, 91 | syl2anr 290 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ (1...(๐ โ 1)) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ ยท ๐) = (๐ ยท ๐)) |
93 | 92 | oveq1d 5892 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ (1...(๐ โ 1)) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐) mod ๐) = ((๐ ยท ๐) mod ๐)) |
94 | 93 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ (1...(๐ โ 1)) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐) mod ๐) = 1 โ ((๐ ยท ๐) mod ๐) = 1)) |
95 | 94 | biimpd 144 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ (1...(๐ โ 1)) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐) mod ๐) = 1 โ ((๐ ยท ๐) mod ๐) = 1)) |
96 | 95 | impancom 260 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โ ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ((๐ ยท ๐) mod ๐) = 1)) |
97 | 96 | imp 124 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐) mod ๐) = 1) |
98 | 97 | oveq1d 5892 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐) mod ๐) ยท ๐ผ) = (1 ยท ๐ผ)) |
99 | 98 | oveq1d 5892 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐) = ((1 ยท ๐ผ) mod ๐)) |
100 | 99 | oveq2d 5893 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (0 โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐)) = (0 โ ((1 ยท ๐ผ) mod ๐))) |
101 | 100 | oveq1d 5892 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((0 โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐)) mod ๐) = ((0 โ ((1 ยท ๐ผ) mod ๐)) mod ๐)) |
102 | 60 | mulid2d 7978 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (1 ยท ๐ผ) = ๐ผ) |
103 | 102 | oveq1d 5892 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((1 ยท ๐ผ) mod ๐) = (๐ผ mod ๐)) |
104 | 84 | nnnn0d 9231 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ โ
โ0) |
105 | 104 | nn0ge0d 9234 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ 0 โค ๐ผ) |
106 | | elfzolt2 10158 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ผ โ (1..^๐) โ ๐ผ < ๐) |
107 | 106 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ๐ผ < ๐) |
108 | 107 | adantl 277 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ๐ผ < ๐) |
109 | | modqid 10351 |
. . . . . . . . . . . . . . . . 17
โข (((๐ผ โ โ โง ๐ โ โ) โง (0 โค
๐ผ โง ๐ผ < ๐)) โ (๐ผ mod ๐) = ๐ผ) |
110 | 20, 27, 105, 108, 109 | syl22anc 1239 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ผ mod ๐) = ๐ผ) |
111 | 103, 110 | eqtrd 2210 |
. . . . . . . . . . . . . . 15
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((1 ยท ๐ผ) mod ๐) = ๐ผ) |
112 | 111 | oveq2d 5893 |
. . . . . . . . . . . . . 14
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (0 โ ((1 ยท ๐ผ) mod ๐)) = (0 โ ๐ผ)) |
113 | 112 | oveq1d 5892 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((0 โ ((1 ยท ๐ผ) mod ๐)) mod ๐) = ((0 โ ๐ผ) mod ๐)) |
114 | 101, 113 | eqtrd 2210 |
. . . . . . . . . . . 12
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((0 โ ((((๐ ยท ๐) mod ๐) ยท ๐ผ) mod ๐)) mod ๐) = ((0 โ ๐ผ) mod ๐)) |
115 | 77, 90, 114 | 3eqtr3d 2218 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐) = ((0 โ ๐ผ) mod ๐)) |
116 | 115 | oveq2d 5893 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ผ + (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) = (๐ผ + ((0 โ ๐ผ) mod ๐))) |
117 | 116 | oveq1d 5892 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) mod ๐) = ((๐ผ + ((0 โ ๐ผ) mod ๐)) mod ๐)) |
118 | | qsubcl 9640 |
. . . . . . . . . . 11
โข (((๐ ยท ๐) โ โ โง ((๐ ยท ๐ผ) ยท ๐) โ โ) โ ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) โ โ) |
119 | 80, 88, 118 | syl2anc 411 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) โ โ) |
120 | | modqadd2mod 10376 |
. . . . . . . . . 10
โข
(((((๐ ยท
๐) โ ((๐ ยท ๐ผ) ยท ๐)) โ โ โง ๐ผ โ โ) โง (๐ โ โ โง 0 < ๐)) โ ((๐ผ + (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) mod ๐) = ((๐ผ + ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐))) mod ๐)) |
121 | 119, 20, 27, 28, 120 | syl22anc 1239 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + (((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐)) mod ๐)) mod ๐) = ((๐ผ + ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐))) mod ๐)) |
122 | | 0zd 9267 |
. . . . . . . . . . . . 13
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ 0 โ
โค) |
123 | 122, 18 | zsubcld 9382 |
. . . . . . . . . . . 12
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (0 โ ๐ผ) โ โค) |
124 | | zq 9628 |
. . . . . . . . . . . 12
โข ((0
โ ๐ผ) โ โค
โ (0 โ ๐ผ) โ
โ) |
125 | 123, 124 | syl 14 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (0 โ ๐ผ) โ โ) |
126 | | modqadd2mod 10376 |
. . . . . . . . . . 11
โข ((((0
โ ๐ผ) โ โ
โง ๐ผ โ โ)
โง (๐ โ โ
โง 0 < ๐)) โ
((๐ผ + ((0 โ ๐ผ) mod ๐)) mod ๐) = ((๐ผ + (0 โ ๐ผ)) mod ๐)) |
127 | 125, 20, 27, 28, 126 | syl22anc 1239 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + ((0 โ ๐ผ) mod ๐)) mod ๐) = ((๐ผ + (0 โ ๐ผ)) mod ๐)) |
128 | | 0cnd 7952 |
. . . . . . . . . . . . . 14
โข (๐ผ โ (1..^๐) โ 0 โ โ) |
129 | 36, 128 | pncan3d 8273 |
. . . . . . . . . . . . 13
โข (๐ผ โ (1..^๐) โ (๐ผ + (0 โ ๐ผ)) = 0) |
130 | 129 | 3ad2ant3 1020 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ (๐ผ + (0 โ ๐ผ)) = 0) |
131 | 130 | adantl 277 |
. . . . . . . . . . 11
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (๐ผ + (0 โ ๐ผ)) = 0) |
132 | 131 | oveq1d 5892 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + (0 โ ๐ผ)) mod ๐) = (0 mod ๐)) |
133 | 3, 26 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
134 | | q0mod 10357 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 0 <
๐) โ (0 mod ๐) = 0) |
135 | 133, 52, 134 | syl2anc 411 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (0 mod
๐) = 0) |
136 | 135 | 3ad2ant1 1018 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ (0 mod ๐) = 0) |
137 | 136 | adantl 277 |
. . . . . . . . . 10
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ (0 mod ๐) = 0) |
138 | 127, 132,
137 | 3eqtrd 2214 |
. . . . . . . . 9
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + ((0 โ ๐ผ) mod ๐)) mod ๐) = 0) |
139 | 117, 121,
138 | 3eqtr3d 2218 |
. . . . . . . 8
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + ((๐ ยท ๐) โ ((๐ ยท ๐ผ) ยท ๐))) mod ๐) = 0) |
140 | 30, 45, 139 | 3eqtrd 2214 |
. . . . . . 7
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐) = 0) |
141 | | oveq1 5884 |
. . . . . . . . . . 11
โข (๐ = ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (๐ ยท ๐) = (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) |
142 | 141 | oveq2d 5893 |
. . . . . . . . . 10
โข (๐ = ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (๐ผ + (๐ ยท ๐)) = (๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐))) |
143 | 142 | oveq1d 5892 |
. . . . . . . . 9
โข (๐ = ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ ((๐ผ + (๐ ยท ๐)) mod ๐) = ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐)) |
144 | 143 | eqeq1d 2186 |
. . . . . . . 8
โข (๐ = ((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (((๐ผ + (๐ ยท ๐)) mod ๐) = 0 โ ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐) = 0)) |
145 | 144 | rspcev 2843 |
. . . . . . 7
โข ((((๐ โ (๐ ยท ๐ผ)) mod ๐) โ (0..^๐) โง ((๐ผ + (((๐ โ (๐ ยท ๐ผ)) mod ๐) ยท ๐)) mod ๐) = 0) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
146 | 17, 140, 145 | syl2anc 411 |
. . . . . 6
โข (((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โง (๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐))) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |
147 | 146 | ex 115 |
. . . . 5
โข ((๐ โ (1...(๐ โ 1)) โง ((๐ ยท ๐) mod ๐) = 1) โ ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
148 | 147 | rexlimiva 2589 |
. . . 4
โข
(โ๐ โ
(1...(๐ โ 1))((๐ ยท ๐) mod ๐) = 1 โ ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
149 | 1, 2, 148 | 3syl 17 |
. . 3
โข ((๐ โ โ โง ๐ โ (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
150 | 149 | 3adant3 1017 |
. 2
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0)) |
151 | 150 | pm2.43i 49 |
1
โข ((๐ โ โ โง ๐ โ (1..^๐) โง ๐ผ โ (1..^๐)) โ โ๐ โ (0..^๐)((๐ผ + (๐ ยท ๐)) mod ๐) = 0) |