Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ โง ๐ด โ โค โง (๐ด gcd ๐) = 1)) |
2 | 1 | simp1d 1143 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
3 | 2 | phicld 16651 |
. . . . . . . . 9
โข (๐ โ (ฯโ๐) โ
โ) |
4 | 3 | nnred 12175 |
. . . . . . . 8
โข (๐ โ (ฯโ๐) โ
โ) |
5 | 4 | leidd 11728 |
. . . . . . 7
โข (๐ โ (ฯโ๐) โค (ฯโ๐)) |
6 | 3 | adantr 482 |
. . . . . . . 8
โข ((๐ โง (ฯโ๐) โค (ฯโ๐)) โ (ฯโ๐) โ
โ) |
7 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ (๐ฅ โค (ฯโ๐) โ 1 โค (ฯโ๐))) |
8 | 7 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ ((๐ โง ๐ฅ โค (ฯโ๐)) โ (๐ โง 1 โค (ฯโ๐)))) |
9 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (๐ดโ๐ฅ) = (๐ดโ1)) |
10 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ = 1 โ (seq1( ยท ,
๐น)โ๐ฅ) = (seq1( ยท , ๐น)โ1)) |
11 | 9, 10 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ ((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) = ((๐ดโ1) ยท (seq1( ยท , ๐น)โ1))) |
12 | 11 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = (((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐)) |
13 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = 1 โ (seq1( ยท ,
๐บ)โ๐ฅ) = (seq1( ยท , ๐บ)โ1)) |
14 | 13 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ ((seq1( ยท ,
๐บ)โ๐ฅ) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐)) |
15 | 12, 14 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โ (((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐))) |
16 | 10 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ฅ = 1 โ (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = (๐ gcd (seq1( ยท , ๐น)โ1))) |
17 | 16 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = 1 โ ((๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1 โ (๐ gcd (seq1( ยท , ๐น)โ1)) = 1)) |
18 | 15, 17 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = 1 โ (((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1) โ ((((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ1)) = 1))) |
19 | 8, 18 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = 1 โ (((๐ โง ๐ฅ โค (ฯโ๐)) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1)) โ ((๐ โง 1 โค (ฯโ๐)) โ ((((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ1)) = 1)))) |
20 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ง โ (๐ฅ โค (ฯโ๐) โ ๐ง โค (ฯโ๐))) |
21 | 20 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ ((๐ โง ๐ฅ โค (ฯโ๐)) โ (๐ โง ๐ง โค (ฯโ๐)))) |
22 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ง โ (๐ดโ๐ฅ) = (๐ดโ๐ง)) |
23 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ง โ (seq1( ยท , ๐น)โ๐ฅ) = (seq1( ยท , ๐น)โ๐ง)) |
24 | 22, 23 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ง โ ((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) = ((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง))) |
25 | 24 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ง โ (((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = (((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐)) |
26 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = ๐ง โ (seq1( ยท , ๐บ)โ๐ฅ) = (seq1( ยท , ๐บ)โ๐ง)) |
27 | 26 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ง โ ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐)) |
28 | 25, 27 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ง โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โ (((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐))) |
29 | 23 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ง โ (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = (๐ gcd (seq1( ยท , ๐น)โ๐ง))) |
30 | 29 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ง โ ((๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1 โ (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)) |
31 | 28, 30 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = ๐ง โ (((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1))) |
32 | 21, 31 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = ๐ง โ (((๐ โง ๐ฅ โค (ฯโ๐)) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1)) โ ((๐ โง ๐ง โค (ฯโ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)))) |
33 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง + 1) โ (๐ฅ โค (ฯโ๐) โ (๐ง + 1) โค (ฯโ๐))) |
34 | 33 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ฅ = (๐ง + 1) โ ((๐ โง ๐ฅ โค (ฯโ๐)) โ (๐ โง (๐ง + 1) โค (ฯโ๐)))) |
35 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐ง + 1) โ (๐ดโ๐ฅ) = (๐ดโ(๐ง + 1))) |
36 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐ง + 1) โ (seq1( ยท , ๐น)โ๐ฅ) = (seq1( ยท , ๐น)โ(๐ง + 1))) |
37 | 35, 36 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ง + 1) โ ((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) = ((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1)))) |
38 | 37 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ง + 1) โ (((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = (((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐)) |
39 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = (๐ง + 1) โ (seq1( ยท , ๐บ)โ๐ฅ) = (seq1( ยท , ๐บ)โ(๐ง + 1))) |
40 | 39 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ง + 1) โ ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐)) |
41 | 38, 40 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง + 1) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โ (((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐))) |
42 | 36 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐ง + 1) โ (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1)))) |
43 | 42 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ง + 1) โ ((๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1 โ (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)) |
44 | 41, 43 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = (๐ง + 1) โ (((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1))) |
45 | 34, 44 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = (๐ง + 1) โ (((๐ โง ๐ฅ โค (ฯโ๐)) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1)) โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)))) |
46 | | breq1 5113 |
. . . . . . . . . . 11
โข (๐ฅ = (ฯโ๐) โ (๐ฅ โค (ฯโ๐) โ (ฯโ๐) โค (ฯโ๐))) |
47 | 46 | anbi2d 630 |
. . . . . . . . . 10
โข (๐ฅ = (ฯโ๐) โ ((๐ โง ๐ฅ โค (ฯโ๐)) โ (๐ โง (ฯโ๐) โค (ฯโ๐)))) |
48 | | oveq2 7370 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (ฯโ๐) โ (๐ดโ๐ฅ) = (๐ดโ(ฯโ๐))) |
49 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (ฯโ๐) โ (seq1( ยท , ๐น)โ๐ฅ) = (seq1( ยท , ๐น)โ(ฯโ๐))) |
50 | 48, 49 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ฅ = (ฯโ๐) โ ((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) = ((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐)))) |
51 | 50 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = (ฯโ๐) โ (((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐)) |
52 | | fveq2 6847 |
. . . . . . . . . . . . 13
โข (๐ฅ = (ฯโ๐) โ (seq1( ยท , ๐บ)โ๐ฅ) = (seq1( ยท , ๐บ)โ(ฯโ๐))) |
53 | 52 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฅ = (ฯโ๐) โ ((seq1( ยท ,
๐บ)โ๐ฅ) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐)) |
54 | 51, 53 | eqeq12d 2753 |
. . . . . . . . . . 11
โข (๐ฅ = (ฯโ๐) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐))) |
55 | 49 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (๐ฅ = (ฯโ๐) โ (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐)))) |
56 | 55 | eqeq1d 2739 |
. . . . . . . . . . 11
โข (๐ฅ = (ฯโ๐) โ ((๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1 โ (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1)) |
57 | 54, 56 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = (ฯโ๐) โ (((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1) โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1))) |
58 | 47, 57 | imbi12d 345 |
. . . . . . . . 9
โข (๐ฅ = (ฯโ๐) โ (((๐ โง ๐ฅ โค (ฯโ๐)) โ ((((๐ดโ๐ฅ) ยท (seq1( ยท , ๐น)โ๐ฅ)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ฅ) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ฅ)) = 1)) โ ((๐ โง (ฯโ๐) โค (ฯโ๐)) โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1)))) |
59 | 1 | simp2d 1144 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โค) |
60 | | eulerth.4 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐น:๐โ1-1-ontoโ๐) |
61 | | f1of 6789 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐น:๐โ1-1-ontoโ๐ โ ๐น:๐โถ๐) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ ๐น:๐โถ๐) |
63 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . . . . 22
โข โ =
(โคโฅโ1) |
64 | 3, 63 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ (ฯโ๐) โ
(โคโฅโ1)) |
65 | | eluzfz1 13455 |
. . . . . . . . . . . . . . . . . . . . 21
โข
((ฯโ๐)
โ (โคโฅโ1) โ 1 โ
(1...(ฯโ๐))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ 1 โ
(1...(ฯโ๐))) |
67 | | eulerth.3 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ = (1...(ฯโ๐)) |
68 | 66, 67 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ 1 โ ๐) |
69 | 62, 68 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (๐นโ1) โ ๐) |
70 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ = (๐นโ1) โ (๐ฆ gcd ๐) = ((๐นโ1) gcd ๐)) |
71 | 70 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ = (๐นโ1) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ1) gcd ๐) = 1)) |
72 | | eulerth.2 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ = {๐ฆ โ (0..^๐) โฃ (๐ฆ gcd ๐) = 1} |
73 | 71, 72 | elrab2 3653 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ1) โ ๐ โ ((๐นโ1) โ (0..^๐) โง ((๐นโ1) gcd ๐) = 1)) |
74 | 69, 73 | sylib 217 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ((๐นโ1) โ (0..^๐) โง ((๐นโ1) gcd ๐) = 1)) |
75 | 74 | simpld 496 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐นโ1) โ (0..^๐)) |
76 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . 16
โข ((๐นโ1) โ (0..^๐) โ (๐นโ1) โ โค) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐นโ1) โ โค) |
78 | 59, 77 | zmulcld 12620 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด ยท (๐นโ1)) โ โค) |
79 | 78 | zred 12614 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ด ยท (๐นโ1)) โ โ) |
80 | 2 | nnrpd 12962 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ
โ+) |
81 | | modabs2 13817 |
. . . . . . . . . . . . 13
โข (((๐ด ยท (๐นโ1)) โ โ โง ๐ โ โ+)
โ (((๐ด ยท (๐นโ1)) mod ๐) mod ๐) = ((๐ด ยท (๐นโ1)) mod ๐)) |
82 | 79, 80, 81 | syl2anc 585 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด ยท (๐นโ1)) mod ๐) mod ๐) = ((๐ด ยท (๐นโ1)) mod ๐)) |
83 | | 1z 12540 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
84 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = 1 โ (๐นโ๐ฅ) = (๐นโ1)) |
85 | 84 | oveq2d 7378 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = 1 โ (๐ด ยท (๐นโ๐ฅ)) = (๐ด ยท (๐นโ1))) |
86 | 85 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = 1 โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) = ((๐ด ยท (๐นโ1)) mod ๐)) |
87 | | eulerth.5 |
. . . . . . . . . . . . . . . 16
โข ๐บ = (๐ฅ โ ๐ โฆ ((๐ด ยท (๐นโ๐ฅ)) mod ๐)) |
88 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
โข ((๐ด ยท (๐นโ1)) mod ๐) โ V |
89 | 86, 87, 88 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
โข (1 โ
๐ โ (๐บโ1) = ((๐ด ยท (๐นโ1)) mod ๐)) |
90 | 68, 89 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐บโ1) = ((๐ด ยท (๐นโ1)) mod ๐)) |
91 | 83, 90 | seq1i 13927 |
. . . . . . . . . . . . 13
โข (๐ โ (seq1( ยท , ๐บ)โ1) = ((๐ด ยท (๐นโ1)) mod ๐)) |
92 | 91 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ ((seq1( ยท , ๐บ)โ1) mod ๐) = (((๐ด ยท (๐นโ1)) mod ๐) mod ๐)) |
93 | 59 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โ) |
94 | 93 | exp1d 14053 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ดโ1) = ๐ด) |
95 | | seq1 13926 |
. . . . . . . . . . . . . . . 16
โข (1 โ
โค โ (seq1( ยท , ๐น)โ1) = (๐นโ1)) |
96 | 83, 95 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข (seq1(
ยท , ๐น)โ1) =
(๐นโ1) |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ (seq1( ยท , ๐น)โ1) = (๐นโ1)) |
98 | 94, 97 | oveq12d 7380 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) = (๐ด ยท (๐นโ1))) |
99 | 98 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((๐ด ยท (๐นโ1)) mod ๐)) |
100 | 82, 92, 99 | 3eqtr4rd 2788 |
. . . . . . . . . . 11
โข (๐ โ (((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐)) |
101 | 96 | oveq2i 7373 |
. . . . . . . . . . . 12
โข (๐ gcd (seq1( ยท , ๐น)โ1)) = (๐ gcd (๐นโ1)) |
102 | 2 | nnzd 12533 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ โค) |
103 | 102, 77 | gcdcomd 16401 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ gcd (๐นโ1)) = ((๐นโ1) gcd ๐)) |
104 | 74 | simprd 497 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐นโ1) gcd ๐) = 1) |
105 | 103, 104 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (๐ gcd (๐นโ1)) = 1) |
106 | 101, 105 | eqtrid 2789 |
. . . . . . . . . . 11
โข (๐ โ (๐ gcd (seq1( ยท , ๐น)โ1)) = 1) |
107 | 100, 106 | jca 513 |
. . . . . . . . . 10
โข (๐ โ ((((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ1)) = 1)) |
108 | 107 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง 1 โค (ฯโ๐)) โ ((((๐ดโ1) ยท (seq1( ยท , ๐น)โ1)) mod ๐) = ((seq1( ยท , ๐บ)โ1) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ1)) = 1)) |
109 | | nnre 12167 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โ โ ๐ง โ
โ) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง ๐) โ ๐ง โ โ) |
111 | 110 | lep1d 12093 |
. . . . . . . . . . . . 13
โข ((๐ง โ โ โง ๐) โ ๐ง โค (๐ง + 1)) |
112 | | peano2re 11335 |
. . . . . . . . . . . . . . 15
โข (๐ง โ โ โ (๐ง + 1) โ
โ) |
113 | 110, 112 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง ๐) โ (๐ง + 1) โ โ) |
114 | 4 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง ๐) โ (ฯโ๐) โ
โ) |
115 | | letr 11256 |
. . . . . . . . . . . . . 14
โข ((๐ง โ โ โง (๐ง + 1) โ โ โง
(ฯโ๐) โ
โ) โ ((๐ง โค
(๐ง + 1) โง (๐ง + 1) โค (ฯโ๐)) โ ๐ง โค (ฯโ๐))) |
116 | 110, 113,
114, 115 | syl3anc 1372 |
. . . . . . . . . . . . 13
โข ((๐ง โ โ โง ๐) โ ((๐ง โค (๐ง + 1) โง (๐ง + 1) โค (ฯโ๐)) โ ๐ง โค (ฯโ๐))) |
117 | 111, 116 | mpand 694 |
. . . . . . . . . . . 12
โข ((๐ง โ โ โง ๐) โ ((๐ง + 1) โค (ฯโ๐) โ ๐ง โค (ฯโ๐))) |
118 | 117 | imdistanda 573 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ (๐ โง ๐ง โค (ฯโ๐)))) |
119 | 118 | imim1d 82 |
. . . . . . . . . 10
โข (๐ง โ โ โ (((๐ โง ๐ง โค (ฯโ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)) โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)))) |
120 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ด โ โค) |
121 | | nnnn0 12427 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ โ โ ๐ง โ
โ0) |
122 | 121 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โ โ0) |
123 | | zexpcl 13989 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ด โ โค โง ๐ง โ โ0)
โ (๐ดโ๐ง) โ
โค) |
124 | 120, 122,
123 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ดโ๐ง) โ โค) |
125 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โ โ) |
126 | 125, 63 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โ
(โคโฅโ1)) |
127 | 109 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โ โ) |
128 | 127, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โ โ) |
129 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (ฯโ๐) โ โ) |
130 | 127 | lep1d 12093 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โค (๐ง + 1)) |
131 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โค (ฯโ๐)) |
132 | 127, 128,
129, 130, 131 | letrd 11319 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โค (ฯโ๐)) |
133 | | nnz 12527 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ง โ โ โ ๐ง โ
โค) |
134 | 133 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ง โ โค) |
135 | 3 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ โ (ฯโ๐) โ
โค) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (ฯโ๐) โ โค) |
137 | | eluz 12784 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((๐ง โ โค โง
(ฯโ๐) โ
โค) โ ((ฯโ๐) โ (โคโฅโ๐ง) โ ๐ง โค (ฯโ๐))) |
138 | 134, 136,
137 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((ฯโ๐) โ (โคโฅโ๐ง) โ ๐ง โค (ฯโ๐))) |
139 | 132, 138 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (ฯโ๐) โ (โคโฅโ๐ง)) |
140 | | fzss2 13488 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
((ฯโ๐)
โ (โคโฅโ๐ง) โ (1...๐ง) โ (1...(ฯโ๐))) |
141 | 139, 140 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (1...๐ง) โ (1...(ฯโ๐))) |
142 | 141, 67 | sseqtrrdi 4000 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (1...๐ง) โ ๐) |
143 | 142 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง ๐ฅ โ (1...๐ง)) โ ๐ฅ โ ๐) |
144 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ ๐) |
145 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (๐ฆ = (๐นโ๐ฅ) โ (๐ฆ gcd ๐) = ((๐นโ๐ฅ) gcd ๐)) |
146 | 145 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ฆ = (๐นโ๐ฅ) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ๐ฅ) gcd ๐) = 1)) |
147 | 146, 72 | elrab2 3653 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐นโ๐ฅ) โ ๐ โ ((๐นโ๐ฅ) โ (0..^๐) โง ((๐นโ๐ฅ) gcd ๐) = 1)) |
148 | 144, 147 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง ๐ฅ โ ๐) โ ((๐นโ๐ฅ) โ (0..^๐) โง ((๐นโ๐ฅ) gcd ๐) = 1)) |
149 | 148 | simpld 496 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ (0..^๐)) |
150 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐นโ๐ฅ) โ (0..^๐) โ (๐นโ๐ฅ) โ โค) |
151 | 149, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ โค) |
152 | 151 | adantlr 714 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง ๐ฅ โ ๐) โ (๐นโ๐ฅ) โ โค) |
153 | 143, 152 | syldan 592 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง ๐ฅ โ (1...๐ง)) โ (๐นโ๐ฅ) โ โค) |
154 | | zmulcl 12559 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โค โง ๐ฆ โ โค) โ (๐ฅ ยท ๐ฆ) โ โค) |
155 | 154 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐ฆ) โ โค) |
156 | 126, 153,
155 | seqcl 13935 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐น)โ๐ง) โ โค) |
157 | 124, 156 | zmulcld 12620 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) โ โค) |
158 | 157 | zred 12614 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) โ โ) |
159 | 72 | ssrab3 4045 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ โ (0..^๐) |
160 | 1, 72, 67, 60, 87 | eulerthlem1 16660 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ ๐บ:๐โถ๐) |
161 | 160 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง ๐ฅ โ ๐) โ (๐บโ๐ฅ) โ ๐) |
162 | 159, 161 | sselid 3947 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ฅ โ ๐) โ (๐บโ๐ฅ) โ (0..^๐)) |
163 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐บโ๐ฅ) โ (0..^๐) โ (๐บโ๐ฅ) โ โค) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฅ โ ๐) โ (๐บโ๐ฅ) โ โค) |
165 | 164 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง ๐ฅ โ ๐) โ (๐บโ๐ฅ) โ โค) |
166 | 143, 165 | syldan 592 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โง ๐ฅ โ (1...๐ง)) โ (๐บโ๐ฅ) โ โค) |
167 | 126, 166,
155 | seqcl 13935 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐บ)โ๐ง) โ โค) |
168 | 167 | zred 12614 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐บ)โ๐ง) โ โ) |
169 | 62 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐น:๐โถ๐) |
170 | | peano2nn 12172 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (๐ง โ โ โ (๐ง + 1) โ
โ) |
171 | 170 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โ โ) |
172 | 171 | nnge1d 12208 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ 1 โค (๐ง + 1)) |
173 | 171 | nnzd 12533 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โ โค) |
174 | | elfz 13437 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (((๐ง + 1) โ โค โง 1
โ โค โง (ฯโ๐) โ โค) โ ((๐ง + 1) โ
(1...(ฯโ๐))
โ (1 โค (๐ง + 1)
โง (๐ง + 1) โค
(ฯโ๐)))) |
175 | 83, 174 | mp3an2 1450 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (((๐ง + 1) โ โค โง
(ฯโ๐) โ
โค) โ ((๐ง + 1)
โ (1...(ฯโ๐)) โ (1 โค (๐ง + 1) โง (๐ง + 1) โค (ฯโ๐)))) |
176 | 173, 136,
175 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ง + 1) โ (1...(ฯโ๐)) โ (1 โค (๐ง + 1) โง (๐ง + 1) โค (ฯโ๐)))) |
177 | 172, 131,
176 | mpbir2and 712 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โ (1...(ฯโ๐))) |
178 | 177, 67 | eleqtrrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ง + 1) โ ๐) |
179 | 169, 178 | ffvelcdmd 7041 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐นโ(๐ง + 1)) โ ๐) |
180 | | oveq1 7369 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฆ = (๐นโ(๐ง + 1)) โ (๐ฆ gcd ๐) = ((๐นโ(๐ง + 1)) gcd ๐)) |
181 | 180 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ = (๐นโ(๐ง + 1)) โ ((๐ฆ gcd ๐) = 1 โ ((๐นโ(๐ง + 1)) gcd ๐) = 1)) |
182 | 181, 72 | elrab2 3653 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐นโ(๐ง + 1)) โ ๐ โ ((๐นโ(๐ง + 1)) โ (0..^๐) โง ((๐นโ(๐ง + 1)) gcd ๐) = 1)) |
183 | 179, 182 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐นโ(๐ง + 1)) โ (0..^๐) โง ((๐นโ(๐ง + 1)) gcd ๐) = 1)) |
184 | 183 | simpld 496 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐นโ(๐ง + 1)) โ (0..^๐)) |
185 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ(๐ง + 1)) โ (0..^๐) โ (๐นโ(๐ง + 1)) โ โค) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐นโ(๐ง + 1)) โ โค) |
187 | 120, 186 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ด ยท (๐นโ(๐ง + 1))) โ โค) |
188 | 80 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ โ
โ+) |
189 | | modmul1 13836 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ดโ๐ง) ยท (seq1( ยท ,
๐น)โ๐ง)) โ โ โง (seq1( ยท ,
๐บ)โ๐ง) โ โ) โง ((๐ด ยท (๐นโ(๐ง + 1))) โ โค โง ๐ โ โ+)
โง (((๐ดโ๐ง) ยท (seq1( ยท ,
๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐)) |
190 | 189 | 3expia 1122 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ดโ๐ง) ยท (seq1( ยท ,
๐น)โ๐ง)) โ โ โง (seq1( ยท ,
๐บ)โ๐ง) โ โ) โง ((๐ด ยท (๐นโ(๐ง + 1))) โ โค โง ๐ โ โ+))
โ ((((๐ดโ๐ง) ยท (seq1( ยท ,
๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐))) |
191 | 158, 168,
187, 188, 190 | syl22anc 838 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐))) |
192 | 124 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ดโ๐ง) โ โ) |
193 | 156 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐น)โ๐ง) โ โ) |
194 | 93 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ด โ โ) |
195 | 186 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐นโ(๐ง + 1)) โ โ) |
196 | 192, 193,
194, 195 | mul4d 11374 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) = (((๐ดโ๐ง) ยท ๐ด) ยท ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1))))) |
197 | 194, 122 | expp1d 14059 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ดโ(๐ง + 1)) = ((๐ดโ๐ง) ยท ๐ด)) |
198 | | seqp1 13928 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ
(โคโฅโ1) โ (seq1( ยท , ๐น)โ(๐ง + 1)) = ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) |
199 | 126, 198 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐น)โ(๐ง + 1)) = ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) |
200 | 197, 199 | oveq12d 7380 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) = (((๐ดโ๐ง) ยท ๐ด) ยท ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1))))) |
201 | 196, 200 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) = ((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1)))) |
202 | 201 | oveq1d 7377 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐)) |
203 | 187 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ด ยท (๐นโ(๐ง + 1))) โ โ) |
204 | 203, 188 | modcld 13787 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) โ โ) |
205 | | modabs2 13817 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด ยท (๐นโ(๐ง + 1))) โ โ โง ๐ โ โ+)
โ (((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) mod ๐) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) |
206 | 203, 188,
205 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) mod ๐) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) |
207 | | modmul1 13836 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ด ยท
(๐นโ(๐ง + 1))) mod ๐) โ โ โง (๐ด ยท (๐นโ(๐ง + 1))) โ โ) โง ((seq1(
ยท , ๐บ)โ๐ง) โ โค โง ๐ โ โ+)
โง (((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) mod ๐) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) โ ((((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐) = (((๐ด ยท (๐นโ(๐ง + 1))) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐)) |
208 | 204, 203,
167, 188, 206, 207 | syl221anc 1382 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐) = (((๐ด ยท (๐นโ(๐ง + 1))) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐)) |
209 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (๐ฅ = (๐ง + 1) โ (๐นโ๐ฅ) = (๐นโ(๐ง + 1))) |
210 | 209 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ฅ = (๐ง + 1) โ (๐ด ยท (๐นโ๐ฅ)) = (๐ด ยท (๐นโ(๐ง + 1)))) |
211 | 210 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ฅ = (๐ง + 1) โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) |
212 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) โ V |
213 | 211, 87, 212 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ง + 1) โ ๐ โ (๐บโ(๐ง + 1)) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) |
214 | 178, 213 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐บโ(๐ง + 1)) = ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐)) |
215 | 214 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((seq1( ยท , ๐บ)โ๐ง) ยท (๐บโ(๐ง + 1))) = ((seq1( ยท , ๐บ)โ๐ง) ยท ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐))) |
216 | | seqp1 13928 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง โ
(โคโฅโ1) โ (seq1( ยท , ๐บ)โ(๐ง + 1)) = ((seq1( ยท , ๐บ)โ๐ง) ยท (๐บโ(๐ง + 1)))) |
217 | 126, 216 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐บ)โ(๐ง + 1)) = ((seq1( ยท , ๐บ)โ๐ง) ยท (๐บโ(๐ง + 1)))) |
218 | 204 | recnd 11190 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) โ โ) |
219 | 167 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐บ)โ๐ง) โ โ) |
220 | 218, 219 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) ยท (seq1( ยท , ๐บ)โ๐ง)) = ((seq1( ยท , ๐บ)โ๐ง) ยท ((๐ด ยท (๐นโ(๐ง + 1))) mod ๐))) |
221 | 215, 217,
220 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (seq1( ยท , ๐บ)โ(๐ง + 1)) = (((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) ยท (seq1( ยท , ๐บ)โ๐ง))) |
222 | 221 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) = ((((๐ด ยท (๐นโ(๐ง + 1))) mod ๐) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐)) |
223 | 187 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ด ยท (๐นโ(๐ง + 1))) โ โ) |
224 | 219, 223 | mulcomd 11183 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) = ((๐ด ยท (๐นโ(๐ง + 1))) ยท (seq1( ยท , ๐บ)โ๐ง))) |
225 | 224 | oveq1d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((๐ด ยท (๐นโ(๐ง + 1))) ยท (seq1( ยท , ๐บ)โ๐ง)) mod ๐)) |
226 | 208, 222,
225 | 3eqtr4rd 2788 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐)) |
227 | 202, 226 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) = (((seq1( ยท , ๐บ)โ๐ง) ยท (๐ด ยท (๐นโ(๐ง + 1)))) mod ๐) โ (((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐))) |
228 | 191, 227 | sylibd 238 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โ (((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐))) |
229 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ๐ โ โค) |
230 | 229, 186 | gcdcomd 16401 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ gcd (๐นโ(๐ง + 1))) = ((๐นโ(๐ง + 1)) gcd ๐)) |
231 | 183 | simprd 497 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐นโ(๐ง + 1)) gcd ๐) = 1) |
232 | 230, 231 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ gcd (๐นโ(๐ง + 1))) = 1) |
233 | | rpmul 16542 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง (seq1(
ยท , ๐น)โ๐ง) โ โค โง (๐นโ(๐ง + 1)) โ โค) โ (((๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1 โง (๐ gcd (๐นโ(๐ง + 1))) = 1) โ (๐ gcd ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) = 1)) |
234 | 229, 156,
186, 233 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1 โง (๐ gcd (๐นโ(๐ง + 1))) = 1) โ (๐ gcd ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) = 1)) |
235 | 232, 234 | mpan2d 693 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1 โ (๐ gcd ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) = 1)) |
236 | 199 | oveq2d 7378 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = (๐ gcd ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1))))) |
237 | 236 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1 โ (๐ gcd ((seq1( ยท , ๐น)โ๐ง) ยท (๐นโ(๐ง + 1)))) = 1)) |
238 | 235, 237 | sylibrd 259 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ ((๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1 โ (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)) |
239 | 228, 238 | anim12d 610 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ง โ โ โง (๐ง + 1) โค (ฯโ๐))) โ (((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1))) |
240 | 239 | an12s 648 |
. . . . . . . . . . . 12
โข ((๐ง โ โ โง (๐ โง (๐ง + 1) โค (ฯโ๐))) โ (((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1))) |
241 | 240 | ex 414 |
. . . . . . . . . . 11
โข (๐ง โ โ โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ (((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)))) |
242 | 241 | a2d 29 |
. . . . . . . . . 10
โข (๐ง โ โ โ (((๐ โง (๐ง + 1) โค (ฯโ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)) โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)))) |
243 | 119, 242 | syld 47 |
. . . . . . . . 9
โข (๐ง โ โ โ (((๐ โง ๐ง โค (ฯโ๐)) โ ((((๐ดโ๐ง) ยท (seq1( ยท , ๐น)โ๐ง)) mod ๐) = ((seq1( ยท , ๐บ)โ๐ง) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ๐ง)) = 1)) โ ((๐ โง (๐ง + 1) โค (ฯโ๐)) โ ((((๐ดโ(๐ง + 1)) ยท (seq1( ยท , ๐น)โ(๐ง + 1))) mod ๐) = ((seq1( ยท , ๐บ)โ(๐ง + 1)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(๐ง + 1))) = 1)))) |
244 | 19, 32, 45, 58, 108, 243 | nnind 12178 |
. . . . . . . 8
โข
((ฯโ๐)
โ โ โ ((๐
โง (ฯโ๐) โค
(ฯโ๐)) โ
((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1))) |
245 | 6, 244 | mpcom 38 |
. . . . . . 7
โข ((๐ โง (ฯโ๐) โค (ฯโ๐)) โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1)) |
246 | 5, 245 | mpdan 686 |
. . . . . 6
โข (๐ โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1)) |
247 | 246 | simpld 496 |
. . . . 5
โข (๐ โ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐)) |
248 | 3 | nnnn0d 12480 |
. . . . . . . 8
โข (๐ โ (ฯโ๐) โ
โ0) |
249 | | zexpcl 13989 |
. . . . . . . 8
โข ((๐ด โ โค โง
(ฯโ๐) โ
โ0) โ (๐ดโ(ฯโ๐)) โ โค) |
250 | 59, 248, 249 | syl2anc 585 |
. . . . . . 7
โข (๐ โ (๐ดโ(ฯโ๐)) โ โค) |
251 | 67 | eleq2i 2830 |
. . . . . . . . 9
โข (๐ฅ โ ๐ โ ๐ฅ โ (1...(ฯโ๐))) |
252 | 251, 151 | sylan2br 596 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...(ฯโ๐))) โ (๐นโ๐ฅ) โ โค) |
253 | 154 | adantl 483 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (๐ฅ ยท ๐ฆ) โ โค) |
254 | 64, 252, 253 | seqcl 13935 |
. . . . . . 7
โข (๐ โ (seq1( ยท , ๐น)โ(ฯโ๐)) โ
โค) |
255 | 250, 254 | zmulcld 12620 |
. . . . . 6
โข (๐ โ ((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ
โค) |
256 | | mulcl 11142 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โ) |
257 | 256 | adantl 483 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยท ๐ฆ) โ โ) |
258 | | mulcom 11144 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)) |
259 | 258 | adantl 483 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ ยท ๐ฆ) = (๐ฆ ยท ๐ฅ)) |
260 | | mulass 11146 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) |
261 | 260 | adantl 483 |
. . . . . . . 8
โข ((๐ โง (๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ)) โ ((๐ฅ ยท ๐ฆ) ยท ๐ง) = (๐ฅ ยท (๐ฆ ยท ๐ง))) |
262 | | ssidd 3972 |
. . . . . . . 8
โข (๐ โ โ โ
โ) |
263 | | f1ocnv 6801 |
. . . . . . . . . . 11
โข (๐น:๐โ1-1-ontoโ๐ โ โก๐น:๐โ1-1-ontoโ๐) |
264 | 60, 263 | syl 17 |
. . . . . . . . . 10
โข (๐ โ โก๐น:๐โ1-1-ontoโ๐) |
265 | 2 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โ) |
266 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ด โ โค) |
267 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ฆ โ ๐) โ (๐นโ๐ฆ) โ ๐) |
268 | 267 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) โ ๐) |
269 | 159, 268 | sselid 3947 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) โ (0..^๐)) |
270 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ๐ฆ) โ (0..^๐) โ (๐นโ๐ฆ) โ โค) |
271 | 269, 270 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) โ โค) |
272 | 266, 271 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ด ยท (๐นโ๐ฆ)) โ โค) |
273 | 62 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ง โ ๐) โ (๐นโ๐ง) โ ๐) |
274 | 273 | adantrl 715 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) โ ๐) |
275 | 159, 274 | sselid 3947 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) โ (0..^๐)) |
276 | | elfzoelz 13579 |
. . . . . . . . . . . . . . . . . 18
โข ((๐นโ๐ง) โ (0..^๐) โ (๐นโ๐ง) โ โค) |
277 | 275, 276 | syl 17 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) โ โค) |
278 | 266, 277 | zmulcld 12620 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ด ยท (๐นโ๐ง)) โ โค) |
279 | | moddvds 16154 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง (๐ด ยท (๐นโ๐ฆ)) โ โค โง (๐ด ยท (๐นโ๐ง)) โ โค) โ (((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ง)) mod ๐) โ ๐ โฅ ((๐ด ยท (๐นโ๐ฆ)) โ (๐ด ยท (๐นโ๐ง))))) |
280 | 265, 272,
278, 279 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ง)) mod ๐) โ ๐ โฅ ((๐ด ยท (๐นโ๐ฆ)) โ (๐ด ยท (๐นโ๐ง))))) |
281 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ = ๐ฆ โ (๐นโ๐ฅ) = (๐นโ๐ฆ)) |
282 | 281 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ๐ฆ โ (๐ด ยท (๐นโ๐ฅ)) = (๐ด ยท (๐นโ๐ฆ))) |
283 | 282 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ๐ฆ โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) = ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) |
284 | | ovex 7395 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด ยท (๐นโ๐ฆ)) mod ๐) โ V |
285 | 283, 87, 284 | fvmpt 6953 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ โ ๐ โ (๐บโ๐ฆ) = ((๐ด ยท (๐นโ๐ฆ)) mod ๐)) |
286 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ = ๐ง โ (๐นโ๐ฅ) = (๐นโ๐ง)) |
287 | 286 | oveq2d 7378 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ๐ง โ (๐ด ยท (๐นโ๐ฅ)) = (๐ด ยท (๐นโ๐ง))) |
288 | 287 | oveq1d 7377 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ๐ง โ ((๐ด ยท (๐นโ๐ฅ)) mod ๐) = ((๐ด ยท (๐นโ๐ง)) mod ๐)) |
289 | | ovex 7395 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด ยท (๐นโ๐ง)) mod ๐) โ V |
290 | 288, 87, 289 | fvmpt 6953 |
. . . . . . . . . . . . . . . . 17
โข (๐ง โ ๐ โ (๐บโ๐ง) = ((๐ด ยท (๐นโ๐ง)) mod ๐)) |
291 | 285, 290 | eqeqan12d 2751 |
. . . . . . . . . . . . . . . 16
โข ((๐ฆ โ ๐ โง ๐ง โ ๐) โ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ง)) mod ๐))) |
292 | 291 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ((๐ด ยท (๐นโ๐ฆ)) mod ๐) = ((๐ด ยท (๐นโ๐ง)) mod ๐))) |
293 | 93 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ด โ โ) |
294 | 271 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) โ โ) |
295 | 277 | zcnd 12615 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) โ โ) |
296 | 293, 294,
295 | subdid 11618 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) = ((๐ด ยท (๐นโ๐ฆ)) โ (๐ด ยท (๐นโ๐ง)))) |
297 | 296 | breq2d 5122 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) โ ๐ โฅ ((๐ด ยท (๐นโ๐ฆ)) โ (๐ด ยท (๐นโ๐ง))))) |
298 | 280, 292,
297 | 3bitr4d 311 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))))) |
299 | 102, 59 | gcdcomd 16401 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ gcd ๐ด) = (๐ด gcd ๐)) |
300 | 1 | simp3d 1145 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐ด gcd ๐) = 1) |
301 | 299, 300 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ gcd ๐ด) = 1) |
302 | 301 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ gcd ๐ด) = 1) |
303 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ โค) |
304 | 271, 277 | zsubcld 12619 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) โ (๐นโ๐ง)) โ โค) |
305 | | coprmdvds 16536 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ โค โง ๐ด โ โค โง ((๐นโ๐ฆ) โ (๐นโ๐ง)) โ โค) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ ((๐นโ๐ฆ) โ (๐นโ๐ง)))) |
306 | 303, 266,
304, 305 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) โง (๐ gcd ๐ด) = 1) โ ๐ โฅ ((๐นโ๐ฆ) โ (๐นโ๐ง)))) |
307 | 271 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) โ โ) |
308 | 80 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ๐ โ
โ+) |
309 | | elfzole1 13587 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐นโ๐ฆ) โ (0..^๐) โ 0 โค (๐นโ๐ฆ)) |
310 | 269, 309 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค (๐นโ๐ฆ)) |
311 | | elfzolt2 13588 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐นโ๐ฆ) โ (0..^๐) โ (๐นโ๐ฆ) < ๐) |
312 | 269, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ฆ) < ๐) |
313 | | modid 13808 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐นโ๐ฆ) โ โ โง ๐ โ โ+) โง (0 โค
(๐นโ๐ฆ) โง (๐นโ๐ฆ) < ๐)) โ ((๐นโ๐ฆ) mod ๐) = (๐นโ๐ฆ)) |
314 | 307, 308,
310, 312, 313 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) mod ๐) = (๐นโ๐ฆ)) |
315 | 277 | zred 12614 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) โ โ) |
316 | | elfzole1 13587 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐นโ๐ง) โ (0..^๐) โ 0 โค (๐นโ๐ง)) |
317 | 275, 316 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ 0 โค (๐นโ๐ง)) |
318 | | elfzolt2 13588 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐นโ๐ง) โ (0..^๐) โ (๐นโ๐ง) < ๐) |
319 | 275, 318 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐นโ๐ง) < ๐) |
320 | | modid 13808 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐นโ๐ง) โ โ โง ๐ โ โ+) โง (0 โค
(๐นโ๐ง) โง (๐นโ๐ง) < ๐)) โ ((๐นโ๐ง) mod ๐) = (๐นโ๐ง)) |
321 | 315, 308,
317, 319, 320 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ง) mod ๐) = (๐นโ๐ง)) |
322 | 314, 321 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฆ) mod ๐) = ((๐นโ๐ง) mod ๐) โ (๐นโ๐ฆ) = (๐นโ๐ง))) |
323 | | moddvds 16154 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ โ โง (๐นโ๐ฆ) โ โค โง (๐นโ๐ง) โ โค) โ (((๐นโ๐ฆ) mod ๐) = ((๐นโ๐ง) mod ๐) โ ๐ โฅ ((๐นโ๐ฆ) โ (๐นโ๐ง)))) |
324 | 265, 271,
277, 323 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (((๐นโ๐ฆ) mod ๐) = ((๐นโ๐ง) mod ๐) โ ๐ โฅ ((๐นโ๐ฆ) โ (๐นโ๐ง)))) |
325 | | f1of1 6788 |
. . . . . . . . . . . . . . . . . . 19
โข (๐น:๐โ1-1-ontoโ๐ โ ๐น:๐โ1-1โ๐) |
326 | 60, 325 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐น:๐โ1-1โ๐) |
327 | | f1fveq 7214 |
. . . . . . . . . . . . . . . . . 18
โข ((๐น:๐โ1-1โ๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
328 | 326, 327 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐นโ๐ฆ) = (๐นโ๐ง) โ ๐ฆ = ๐ง)) |
329 | 322, 324,
328 | 3bitr3d 309 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ โฅ ((๐นโ๐ฆ) โ (๐นโ๐ง)) โ ๐ฆ = ๐ง)) |
330 | 306, 329 | sylibd 238 |
. . . . . . . . . . . . . . 15
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) โง (๐ gcd ๐ด) = 1) โ ๐ฆ = ๐ง)) |
331 | 302, 330 | mpan2d 693 |
. . . . . . . . . . . . . 14
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ (๐ โฅ (๐ด ยท ((๐นโ๐ฆ) โ (๐นโ๐ง))) โ ๐ฆ = ๐ง)) |
332 | 298, 331 | sylbid 239 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฆ โ ๐ โง ๐ง โ ๐)) โ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ๐ฆ = ๐ง)) |
333 | 332 | ralrimivva 3198 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ๐ฆ = ๐ง)) |
334 | | dff13 7207 |
. . . . . . . . . . . 12
โข (๐บ:๐โ1-1โ๐ โ (๐บ:๐โถ๐ โง โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐บโ๐ฆ) = (๐บโ๐ง) โ ๐ฆ = ๐ง))) |
335 | 160, 333,
334 | sylanbrc 584 |
. . . . . . . . . . 11
โข (๐ โ ๐บ:๐โ1-1โ๐) |
336 | 67 | ovexi 7396 |
. . . . . . . . . . . . . 14
โข ๐ โ V |
337 | 336 | f1oen 8920 |
. . . . . . . . . . . . 13
โข (๐น:๐โ1-1-ontoโ๐ โ ๐ โ ๐) |
338 | 60, 337 | syl 17 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ ๐) |
339 | | fzofi 13886 |
. . . . . . . . . . . . 13
โข
(0..^๐) โ
Fin |
340 | | ssfi 9124 |
. . . . . . . . . . . . 13
โข
(((0..^๐) โ Fin
โง ๐ โ (0..^๐)) โ ๐ โ Fin) |
341 | 339, 159,
340 | mp2an 691 |
. . . . . . . . . . . 12
โข ๐ โ Fin |
342 | | f1finf1o 9222 |
. . . . . . . . . . . 12
โข ((๐ โ ๐ โง ๐ โ Fin) โ (๐บ:๐โ1-1โ๐ โ ๐บ:๐โ1-1-ontoโ๐)) |
343 | 338, 341,
342 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ (๐บ:๐โ1-1โ๐ โ ๐บ:๐โ1-1-ontoโ๐)) |
344 | 335, 343 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ ๐บ:๐โ1-1-ontoโ๐) |
345 | | f1oco 6812 |
. . . . . . . . . 10
โข ((โก๐น:๐โ1-1-ontoโ๐ โง ๐บ:๐โ1-1-ontoโ๐) โ (โก๐น โ ๐บ):๐โ1-1-ontoโ๐) |
346 | 264, 344,
345 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (โก๐น โ ๐บ):๐โ1-1-ontoโ๐) |
347 | | f1oeq23 6780 |
. . . . . . . . . 10
โข ((๐ = (1...(ฯโ๐)) โง ๐ = (1...(ฯโ๐))) โ ((โก๐น โ ๐บ):๐โ1-1-ontoโ๐ โ (โก๐น โ ๐บ):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐)))) |
348 | 67, 67, 347 | mp2an 691 |
. . . . . . . . 9
โข ((โก๐น โ ๐บ):๐โ1-1-ontoโ๐ โ (โก๐น โ ๐บ):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |
349 | 346, 348 | sylib 217 |
. . . . . . . 8
โข (๐ โ (โก๐น โ ๐บ):(1...(ฯโ๐))โ1-1-ontoโ(1...(ฯโ๐))) |
350 | 252 | zcnd 12615 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ (1...(ฯโ๐))) โ (๐นโ๐ฅ) โ โ) |
351 | 67 | eleq2i 2830 |
. . . . . . . . 9
โข (๐ค โ ๐ โ ๐ค โ (1...(ฯโ๐))) |
352 | | fvco3 6945 |
. . . . . . . . . . . 12
โข ((๐บ:๐โถ๐ โง ๐ค โ ๐) โ ((โก๐น โ ๐บ)โ๐ค) = (โก๐นโ(๐บโ๐ค))) |
353 | 160, 352 | sylan 581 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ((โก๐น โ ๐บ)โ๐ค) = (โก๐นโ(๐บโ๐ค))) |
354 | 353 | fveq2d 6851 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ (๐นโ((โก๐น โ ๐บ)โ๐ค)) = (๐นโ(โก๐นโ(๐บโ๐ค)))) |
355 | 60 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ ๐น:๐โ1-1-ontoโ๐) |
356 | 160 | ffvelcdmda 7040 |
. . . . . . . . . . 11
โข ((๐ โง ๐ค โ ๐) โ (๐บโ๐ค) โ ๐) |
357 | | f1ocnvfv2 7228 |
. . . . . . . . . . 11
โข ((๐น:๐โ1-1-ontoโ๐ โง (๐บโ๐ค) โ ๐) โ (๐นโ(โก๐นโ(๐บโ๐ค))) = (๐บโ๐ค)) |
358 | 355, 356,
357 | syl2anc 585 |
. . . . . . . . . 10
โข ((๐ โง ๐ค โ ๐) โ (๐นโ(โก๐นโ(๐บโ๐ค))) = (๐บโ๐ค)) |
359 | 354, 358 | eqtr2d 2778 |
. . . . . . . . 9
โข ((๐ โง ๐ค โ ๐) โ (๐บโ๐ค) = (๐นโ((โก๐น โ ๐บ)โ๐ค))) |
360 | 351, 359 | sylan2br 596 |
. . . . . . . 8
โข ((๐ โง ๐ค โ (1...(ฯโ๐))) โ (๐บโ๐ค) = (๐นโ((โก๐น โ ๐บ)โ๐ค))) |
361 | 257, 259,
261, 64, 262, 349, 350, 360 | seqf1o 13956 |
. . . . . . 7
โข (๐ โ (seq1( ยท , ๐บ)โ(ฯโ๐)) = (seq1( ยท , ๐น)โ(ฯโ๐))) |
362 | 361, 254 | eqeltrd 2838 |
. . . . . 6
โข (๐ โ (seq1( ยท , ๐บ)โ(ฯโ๐)) โ
โค) |
363 | | moddvds 16154 |
. . . . . 6
โข ((๐ โ โ โง ((๐ดโ(ฯโ๐)) ยท (seq1( ยท ,
๐น)โ(ฯโ๐))) โ โค โง (seq1( ยท ,
๐บ)โ(ฯโ๐)) โ โค) โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท ,
๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โ ๐ โฅ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (seq1( ยท ,
๐บ)โ(ฯโ๐))))) |
364 | 2, 255, 362, 363 | syl3anc 1372 |
. . . . 5
โข (๐ โ ((((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) mod ๐) = ((seq1( ยท , ๐บ)โ(ฯโ๐)) mod ๐) โ ๐ โฅ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (seq1( ยท ,
๐บ)โ(ฯโ๐))))) |
365 | 247, 364 | mpbid 231 |
. . . 4
โข (๐ โ ๐ โฅ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (seq1( ยท ,
๐บ)โ(ฯโ๐)))) |
366 | 254 | zcnd 12615 |
. . . . . . . 8
โข (๐ โ (seq1( ยท , ๐น)โ(ฯโ๐)) โ
โ) |
367 | 366 | mulid2d 11180 |
. . . . . . 7
โข (๐ โ (1 ยท (seq1(
ยท , ๐น)โ(ฯโ๐))) = (seq1( ยท , ๐น)โ(ฯโ๐))) |
368 | 361, 367 | eqtr4d 2780 |
. . . . . 6
โข (๐ โ (seq1( ยท , ๐บ)โ(ฯโ๐)) = (1 ยท (seq1( ยท
, ๐น)โ(ฯโ๐)))) |
369 | 368 | oveq2d 7378 |
. . . . 5
โข (๐ โ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (seq1( ยท ,
๐บ)โ(ฯโ๐))) = (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (1 ยท (seq1(
ยท , ๐น)โ(ฯโ๐))))) |
370 | 250 | zcnd 12615 |
. . . . . 6
โข (๐ โ (๐ดโ(ฯโ๐)) โ โ) |
371 | | ax-1cn 11116 |
. . . . . . 7
โข 1 โ
โ |
372 | | subdir 11596 |
. . . . . . 7
โข (((๐ดโ(ฯโ๐)) โ โ โง 1 โ
โ โง (seq1( ยท , ๐น)โ(ฯโ๐)) โ โ) โ (((๐ดโ(ฯโ๐)) โ 1) ยท (seq1(
ยท , ๐น)โ(ฯโ๐))) = (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (1 ยท (seq1(
ยท , ๐น)โ(ฯโ๐))))) |
373 | 371, 372 | mp3an2 1450 |
. . . . . 6
โข (((๐ดโ(ฯโ๐)) โ โ โง (seq1(
ยท , ๐น)โ(ฯโ๐)) โ โ) โ (((๐ดโ(ฯโ๐)) โ 1) ยท (seq1(
ยท , ๐น)โ(ฯโ๐))) = (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (1 ยท (seq1(
ยท , ๐น)โ(ฯโ๐))))) |
374 | 370, 366,
373 | syl2anc 585 |
. . . . 5
โข (๐ โ (((๐ดโ(ฯโ๐)) โ 1) ยท (seq1( ยท ,
๐น)โ(ฯโ๐))) = (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (1 ยท (seq1(
ยท , ๐น)โ(ฯโ๐))))) |
375 | | zsubcl 12552 |
. . . . . . . 8
โข (((๐ดโ(ฯโ๐)) โ โค โง 1 โ
โค) โ ((๐ดโ(ฯโ๐)) โ 1) โ
โค) |
376 | 250, 83, 375 | sylancl 587 |
. . . . . . 7
โข (๐ โ ((๐ดโ(ฯโ๐)) โ 1) โ
โค) |
377 | 376 | zcnd 12615 |
. . . . . 6
โข (๐ โ ((๐ดโ(ฯโ๐)) โ 1) โ
โ) |
378 | 377, 366 | mulcomd 11183 |
. . . . 5
โข (๐ โ (((๐ดโ(ฯโ๐)) โ 1) ยท (seq1( ยท ,
๐น)โ(ฯโ๐))) = ((seq1( ยท , ๐น)โ(ฯโ๐)) ยท ((๐ดโ(ฯโ๐)) โ 1))) |
379 | 369, 374,
378 | 3eqtr2d 2783 |
. . . 4
โข (๐ โ (((๐ดโ(ฯโ๐)) ยท (seq1( ยท , ๐น)โ(ฯโ๐))) โ (seq1( ยท ,
๐บ)โ(ฯโ๐))) = ((seq1( ยท , ๐น)โ(ฯโ๐)) ยท ((๐ดโ(ฯโ๐)) โ 1))) |
380 | 365, 379 | breqtrd 5136 |
. . 3
โข (๐ โ ๐ โฅ ((seq1( ยท , ๐น)โ(ฯโ๐)) ยท ((๐ดโ(ฯโ๐)) โ 1))) |
381 | 246 | simprd 497 |
. . 3
โข (๐ โ (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1) |
382 | | coprmdvds 16536 |
. . . 4
โข ((๐ โ โค โง (seq1(
ยท , ๐น)โ(ฯโ๐)) โ โค โง ((๐ดโ(ฯโ๐)) โ 1) โ โค) โ ((๐ โฅ ((seq1( ยท ,
๐น)โ(ฯโ๐)) ยท ((๐ดโ(ฯโ๐)) โ 1)) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1) โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1))) |
383 | 102, 254,
376, 382 | syl3anc 1372 |
. . 3
โข (๐ โ ((๐ โฅ ((seq1( ยท , ๐น)โ(ฯโ๐)) ยท ((๐ดโ(ฯโ๐)) โ 1)) โง (๐ gcd (seq1( ยท , ๐น)โ(ฯโ๐))) = 1) โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1))) |
384 | 380, 381,
383 | mp2and 698 |
. 2
โข (๐ โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1)) |
385 | | moddvds 16154 |
. . . 4
โข ((๐ โ โ โง (๐ดโ(ฯโ๐)) โ โค โง 1 โ
โค) โ (((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐) โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1))) |
386 | 83, 385 | mp3an3 1451 |
. . 3
โข ((๐ โ โ โง (๐ดโ(ฯโ๐)) โ โค) โ
(((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐) โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1))) |
387 | 2, 250, 386 | syl2anc 585 |
. 2
โข (๐ โ (((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐) โ ๐ โฅ ((๐ดโ(ฯโ๐)) โ 1))) |
388 | 384, 387 | mpbird 257 |
1
โข (๐ โ ((๐ดโ(ฯโ๐)) mod ๐) = (1 mod ๐)) |