Step | Hyp | Ref
| Expression |
1 | | fpprbasnn 46007 |
. . . 4
โข (๐ โ ( FPPr โ๐) โ ๐ โ โ) |
2 | | fpprel 46006 |
. . . . 5
โข (๐ โ โ โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ โ
โง ((๐โ(๐ โ 1)) mod ๐) = 1))) |
3 | | 3simpa 1149 |
. . . . . 6
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ โง ((๐โ(๐ โ 1)) mod ๐) = 1) โ (๐ โ (โคโฅโ4)
โง ๐ โ
โ)) |
4 | 3 | a1i 11 |
. . . . 5
โข (๐ โ โ โ ((๐ โ
(โคโฅโ4) โง ๐ โ โ โง ((๐โ(๐ โ 1)) mod ๐) = 1) โ (๐ โ (โคโฅโ4)
โง ๐ โ
โ))) |
5 | 2, 4 | sylbid 239 |
. . . 4
โข (๐ โ โ โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ
โ))) |
6 | 1, 5 | mpcom 38 |
. . 3
โข (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ
โ)) |
7 | | fpprwppr 46017 |
. . . 4
โข (๐ โ ( FPPr โ๐) โ ((๐โ๐) mod ๐) = (๐ mod ๐)) |
8 | 1, 7 | jca 513 |
. . 3
โข (๐ โ ( FPPr โ๐) โ (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) |
9 | 6, 8 | jca 513 |
. 2
โข (๐ โ ( FPPr โ๐) โ ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) |
10 | | simprll 778 |
. . . 4
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ ๐ โ
(โคโฅโ4)) |
11 | | simprlr 779 |
. . . 4
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ ๐ โ โ) |
12 | | eluz4nn 12816 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ4) โ ๐ โ โ) |
13 | 12 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ๐ โ โ) |
14 | | nnz 12525 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โค) |
15 | 12 | nnnn0d 12478 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ4) โ ๐ โ
โ0) |
16 | | zexpcl 13988 |
. . . . . . . . . . . 12
โข ((๐ โ โค โง ๐ โ โ0)
โ (๐โ๐) โ
โค) |
17 | 14, 15, 16 | syl2anr 598 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐โ๐) โ โค) |
18 | 14 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ๐ โ โค) |
19 | | moddvds 16152 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐โ๐) โ โค โง ๐ โ โค) โ (((๐โ๐) mod ๐) = (๐ mod ๐) โ ๐ โฅ ((๐โ๐) โ ๐))) |
20 | 13, 17, 18, 19 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (((๐โ๐) mod ๐) = (๐ mod ๐) โ ๐ โฅ ((๐โ๐) โ ๐))) |
21 | | nncn 12166 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ ๐ โ
โ) |
22 | | expm1t 14002 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง ๐ โ โ) โ (๐โ๐) = ((๐โ(๐ โ 1)) ยท ๐)) |
23 | 21, 12, 22 | syl2anr 598 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐โ๐) = ((๐โ(๐ โ 1)) ยท ๐)) |
24 | 23 | oveq1d 7373 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐โ๐) โ ๐) = (((๐โ(๐ โ 1)) ยท ๐) โ ๐)) |
25 | | nnm1nn0 12459 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
26 | 12, 25 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐ โ
(โคโฅโ4) โ (๐ โ 1) โ
โ0) |
27 | | zexpcl 13988 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โค โง (๐ โ 1) โ
โ0) โ (๐โ(๐ โ 1)) โ
โค) |
28 | 14, 26, 27 | syl2anr 598 |
. . . . . . . . . . . . . . 15
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐โ(๐ โ 1)) โ
โค) |
29 | 28 | zcnd 12613 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐โ(๐ โ 1)) โ
โ) |
30 | 21 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ๐ โ โ) |
31 | 29, 30 | mulsubfacd 11621 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (((๐โ(๐ โ 1)) ยท ๐) โ ๐) = (((๐โ(๐ โ 1)) โ 1) ยท ๐)) |
32 | 24, 31 | eqtrd 2773 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐โ๐) โ ๐) = (((๐โ(๐ โ 1)) โ 1) ยท ๐)) |
33 | 32 | breq2d 5118 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โฅ ((๐โ๐) โ ๐) โ ๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท ๐))) |
34 | | 1zzd 12539 |
. . . . . . . . . . . . . 14
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ 1 โ
โค) |
35 | 28, 34 | zsubcld 12617 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐โ(๐ โ 1)) โ 1) โ
โค) |
36 | | dvdsmulgcd 16441 |
. . . . . . . . . . . . 13
โข ((((๐โ(๐ โ 1)) โ 1) โ โค โง
๐ โ โค) โ
(๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท ๐) โ ๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)))) |
37 | 35, 18, 36 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท ๐) โ ๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)))) |
38 | | eluzelz 12778 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ
(โคโฅโ4) โ ๐ โ โค) |
39 | | gcdcom 16398 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ โค โง ๐ โ โค) โ (๐ gcd ๐) = (๐ gcd ๐)) |
40 | 38, 14, 39 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ gcd ๐) = (๐ gcd ๐)) |
41 | 40 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ (๐ gcd ๐) = 1)) |
42 | 41 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ (๐ gcd ๐) = 1)) |
43 | 42 | imp 408 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (๐ gcd ๐) = 1) |
44 | 43 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) = (((๐โ(๐ โ 1)) โ 1) ยท
1)) |
45 | 35 | zcnd 12613 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐โ(๐ โ 1)) โ 1) โ
โ) |
46 | 45 | mulid1d 11177 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (((๐โ(๐ โ 1)) โ 1) ยท 1) =
((๐โ(๐ โ 1)) โ 1)) |
47 | 46 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (((๐โ(๐ โ 1)) โ 1) ยท 1) =
((๐โ(๐ โ 1)) โ 1)) |
48 | 44, 47 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) = ((๐โ(๐ โ 1)) โ 1)) |
49 | 48 | breq2d 5118 |
. . . . . . . . . . . . . . 15
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1))) |
50 | 49 | biimpd 228 |
. . . . . . . . . . . . . 14
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ gcd ๐) = 1) โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1))) |
51 | 50 | ex 414 |
. . . . . . . . . . . . 13
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐ gcd ๐) = 1 โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
52 | 51 | com23 86 |
. . . . . . . . . . . 12
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท (๐ gcd ๐)) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
53 | 37, 52 | sylbid 239 |
. . . . . . . . . . 11
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โฅ (((๐โ(๐ โ 1)) โ 1) ยท ๐) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
54 | 33, 53 | sylbid 239 |
. . . . . . . . . 10
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โฅ ((๐โ๐) โ ๐) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
55 | 20, 54 | sylbid 239 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (((๐โ๐) mod ๐) = (๐ mod ๐) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
56 | 55 | expimpd 455 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ4) โ ((๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐)) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
57 | 56 | adantr 482 |
. . . . . . 7
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ((๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐)) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)))) |
58 | 57 | imp 408 |
. . . . . 6
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ ((๐ gcd ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1))) |
59 | 58 | impcom 409 |
. . . . 5
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1)) |
60 | | eluz4eluz2 12815 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ4) โ ๐ โ
(โคโฅโ2)) |
61 | 60 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ ๐ โ
(โคโฅโ2)) |
62 | 61 | adantr 482 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ ๐ โ
(โคโฅโ2)) |
63 | 14 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐)) โ ๐ โ โค) |
64 | 26 | adantr 482 |
. . . . . . . . 9
โข ((๐ โ
(โคโฅโ4) โง ๐ โ โ) โ (๐ โ 1) โ
โ0) |
65 | 63, 64, 27 | syl2anr 598 |
. . . . . . . 8
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ (๐โ(๐ โ 1)) โ
โค) |
66 | 62, 65 | jca 513 |
. . . . . . 7
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ (๐ โ (โคโฅโ2)
โง (๐โ(๐ โ 1)) โ
โค)) |
67 | 66 | adantl 483 |
. . . . . 6
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ (๐ โ (โคโฅโ2)
โง (๐โ(๐ โ 1)) โ
โค)) |
68 | | modm1div 16153 |
. . . . . 6
โข ((๐ โ
(โคโฅโ2) โง (๐โ(๐ โ 1)) โ โค) โ (((๐โ(๐ โ 1)) mod ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1))) |
69 | 67, 68 | syl 17 |
. . . . 5
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ (((๐โ(๐ โ 1)) mod ๐) = 1 โ ๐ โฅ ((๐โ(๐ โ 1)) โ 1))) |
70 | 59, 69 | mpbird 257 |
. . . 4
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ ((๐โ(๐ โ 1)) mod ๐) = 1) |
71 | 2 | adantr 482 |
. . . . . 6
โข ((๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐)) โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ โ
โง ((๐โ(๐ โ 1)) mod ๐) = 1))) |
72 | 71 | adantl 483 |
. . . . 5
โข (((๐ โ
(โคโฅโ4) โง ๐ โ โ) โง (๐ โ โ โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ โ
โง ((๐โ(๐ โ 1)) mod ๐) = 1))) |
73 | 72 | adantl 483 |
. . . 4
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ (๐ โ ( FPPr โ๐) โ (๐ โ (โคโฅโ4)
โง ๐ โ โ
โง ((๐โ(๐ โ 1)) mod ๐) = 1))) |
74 | 10, 11, 70, 73 | mpbir3and 1343 |
. . 3
โข (((๐ gcd ๐) = 1 โง ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐)))) โ ๐ โ ( FPPr โ๐)) |
75 | 74 | ex 414 |
. 2
โข ((๐ gcd ๐) = 1 โ (((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐))) โ ๐ โ ( FPPr โ๐))) |
76 | 9, 75 | impbid2 225 |
1
โข ((๐ gcd ๐) = 1 โ (๐ โ ( FPPr โ๐) โ ((๐ โ (โคโฅโ4)
โง ๐ โ โ)
โง (๐ โ โ
โง ((๐โ๐) mod ๐) = (๐ mod ๐))))) |