Step | Hyp | Ref
| Expression |
1 | | pockthlem.7 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
2 | | prmnn 16616 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
3 | 1, 2 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โ) |
4 | | pockthlem.8 |
. . . . . 6
โข (๐ โ (๐ pCnt ๐ด) โ โ) |
5 | 4 | nnnn0d 12537 |
. . . . 5
โข (๐ โ (๐ pCnt ๐ด) โ
โ0) |
6 | 3, 5 | nnexpcld 14213 |
. . . 4
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โ โ) |
7 | 6 | nnzd 12590 |
. . 3
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โ โค) |
8 | | pockthlem.5 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
9 | | prmnn 16616 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
10 | 8, 9 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ โ) |
11 | | pockthlem.9 |
. . . . 5
โข (๐ โ ๐ถ โ โค) |
12 | 10 | nnzd 12590 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โค) |
13 | | gcddvds 16449 |
. . . . . . . . . 10
โข ((๐ถ โ โค โง ๐ โ โค) โ ((๐ถ gcd ๐) โฅ ๐ถ โง (๐ถ gcd ๐) โฅ ๐)) |
14 | 11, 12, 13 | syl2anc 583 |
. . . . . . . . 9
โข (๐ โ ((๐ถ gcd ๐) โฅ ๐ถ โง (๐ถ gcd ๐) โฅ ๐)) |
15 | 14 | simpld 494 |
. . . . . . . 8
โข (๐ โ (๐ถ gcd ๐) โฅ ๐ถ) |
16 | 11, 12 | gcdcld 16454 |
. . . . . . . . . 10
โข (๐ โ (๐ถ gcd ๐) โ
โ0) |
17 | 16 | nn0zd 12589 |
. . . . . . . . 9
โข (๐ โ (๐ถ gcd ๐) โ โค) |
18 | | pockthg.4 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ = ((๐ด ยท ๐ต) + 1)) |
19 | | pockthg.1 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ด โ โ) |
20 | | pockthg.2 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ต โ โ) |
21 | 19, 20 | nnmulcld 12270 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
22 | | nnuz 12870 |
. . . . . . . . . . . . . . . 16
โข โ =
(โคโฅโ1) |
23 | 21, 22 | eleqtrdi 2842 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ด ยท ๐ต) โ
(โคโฅโ1)) |
24 | | eluzp1p1 12855 |
. . . . . . . . . . . . . . 15
โข ((๐ด ยท ๐ต) โ (โคโฅโ1)
โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ((๐ด ยท ๐ต) + 1) โ
(โคโฅโ(1 + 1))) |
26 | 18, 25 | eqeltrd 2832 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ (โคโฅโ(1 +
1))) |
27 | | df-2 12280 |
. . . . . . . . . . . . . 14
โข 2 = (1 +
1) |
28 | 27 | fveq2i 6895 |
. . . . . . . . . . . . 13
โข
(โคโฅโ2) = (โคโฅโ(1 +
1)) |
29 | 26, 28 | eleqtrrdi 2843 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ
(โคโฅโ2)) |
30 | | eluz2b2 12910 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ2) โ (๐ โ โ โง 1 < ๐)) |
31 | 29, 30 | sylib 217 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ โ โง 1 < ๐)) |
32 | 31 | simpld 494 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
33 | 32 | nnzd 12590 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
34 | 14 | simprd 495 |
. . . . . . . . 9
โข (๐ โ (๐ถ gcd ๐) โฅ ๐) |
35 | | pockthlem.6 |
. . . . . . . . 9
โข (๐ โ ๐ โฅ ๐) |
36 | 17, 12, 33, 34, 35 | dvdstrd 16243 |
. . . . . . . 8
โข (๐ โ (๐ถ gcd ๐) โฅ ๐) |
37 | 32 | nnne0d 12267 |
. . . . . . . . . 10
โข (๐ โ ๐ โ 0) |
38 | | simpr 484 |
. . . . . . . . . . 11
โข ((๐ถ = 0 โง ๐ = 0) โ ๐ = 0) |
39 | 38 | necon3ai 2964 |
. . . . . . . . . 10
โข (๐ โ 0 โ ยฌ (๐ถ = 0 โง ๐ = 0)) |
40 | 37, 39 | syl 17 |
. . . . . . . . 9
โข (๐ โ ยฌ (๐ถ = 0 โง ๐ = 0)) |
41 | | dvdslegcd 16450 |
. . . . . . . . 9
โข ((((๐ถ gcd ๐) โ โค โง ๐ถ โ โค โง ๐ โ โค) โง ยฌ (๐ถ = 0 โง ๐ = 0)) โ (((๐ถ gcd ๐) โฅ ๐ถ โง (๐ถ gcd ๐) โฅ ๐) โ (๐ถ gcd ๐) โค (๐ถ gcd ๐))) |
42 | 17, 11, 33, 40, 41 | syl31anc 1372 |
. . . . . . . 8
โข (๐ โ (((๐ถ gcd ๐) โฅ ๐ถ โง (๐ถ gcd ๐) โฅ ๐) โ (๐ถ gcd ๐) โค (๐ถ gcd ๐))) |
43 | 15, 36, 42 | mp2and 696 |
. . . . . . 7
โข (๐ โ (๐ถ gcd ๐) โค (๐ถ gcd ๐)) |
44 | | pockthlem.10 |
. . . . . . . . . 10
โข (๐ โ ((๐ถโ(๐ โ 1)) mod ๐) = 1) |
45 | 44 | oveq1d 7427 |
. . . . . . . . 9
โข (๐ โ (((๐ถโ(๐ โ 1)) mod ๐) gcd ๐) = (1 gcd ๐)) |
46 | | 1z 12597 |
. . . . . . . . . . . . . 14
โข 1 โ
โค |
47 | | eluzp1m1 12853 |
. . . . . . . . . . . . . 14
โข ((1
โ โค โง ๐
โ (โคโฅโ(1 + 1))) โ (๐ โ 1) โ
(โคโฅโ1)) |
48 | 46, 26, 47 | sylancr 586 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ 1) โ
(โคโฅโ1)) |
49 | 48, 22 | eleqtrrdi 2843 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โ 1) โ โ) |
50 | 49 | nnnn0d 12537 |
. . . . . . . . . . 11
โข (๐ โ (๐ โ 1) โ
โ0) |
51 | | zexpcl 14047 |
. . . . . . . . . . 11
โข ((๐ถ โ โค โง (๐ โ 1) โ
โ0) โ (๐ถโ(๐ โ 1)) โ
โค) |
52 | 11, 50, 51 | syl2anc 583 |
. . . . . . . . . 10
โข (๐ โ (๐ถโ(๐ โ 1)) โ
โค) |
53 | | modgcd 16479 |
. . . . . . . . . 10
โข (((๐ถโ(๐ โ 1)) โ โค โง ๐ โ โ) โ (((๐ถโ(๐ โ 1)) mod ๐) gcd ๐) = ((๐ถโ(๐ โ 1)) gcd ๐)) |
54 | 52, 32, 53 | syl2anc 583 |
. . . . . . . . 9
โข (๐ โ (((๐ถโ(๐ โ 1)) mod ๐) gcd ๐) = ((๐ถโ(๐ โ 1)) gcd ๐)) |
55 | | gcdcom 16459 |
. . . . . . . . . . 11
โข ((1
โ โค โง ๐
โ โค) โ (1 gcd ๐) = (๐ gcd 1)) |
56 | 46, 33, 55 | sylancr 586 |
. . . . . . . . . 10
โข (๐ โ (1 gcd ๐) = (๐ gcd 1)) |
57 | | gcd1 16474 |
. . . . . . . . . . 11
โข (๐ โ โค โ (๐ gcd 1) = 1) |
58 | 33, 57 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (๐ gcd 1) = 1) |
59 | 56, 58 | eqtrd 2771 |
. . . . . . . . 9
โข (๐ โ (1 gcd ๐) = 1) |
60 | 45, 54, 59 | 3eqtr3d 2779 |
. . . . . . . 8
โข (๐ โ ((๐ถโ(๐ โ 1)) gcd ๐) = 1) |
61 | | rpexp 16664 |
. . . . . . . . 9
โข ((๐ถ โ โค โง ๐ โ โค โง (๐ โ 1) โ โ)
โ (((๐ถโ(๐ โ 1)) gcd ๐) = 1 โ (๐ถ gcd ๐) = 1)) |
62 | 11, 33, 49, 61 | syl3anc 1370 |
. . . . . . . 8
โข (๐ โ (((๐ถโ(๐ โ 1)) gcd ๐) = 1 โ (๐ถ gcd ๐) = 1)) |
63 | 60, 62 | mpbid 231 |
. . . . . . 7
โข (๐ โ (๐ถ gcd ๐) = 1) |
64 | 43, 63 | breqtrd 5175 |
. . . . . 6
โข (๐ โ (๐ถ gcd ๐) โค 1) |
65 | 10 | nnne0d 12267 |
. . . . . . . . 9
โข (๐ โ ๐ โ 0) |
66 | | simpr 484 |
. . . . . . . . . 10
โข ((๐ถ = 0 โง ๐ = 0) โ ๐ = 0) |
67 | 66 | necon3ai 2964 |
. . . . . . . . 9
โข (๐ โ 0 โ ยฌ (๐ถ = 0 โง ๐ = 0)) |
68 | 65, 67 | syl 17 |
. . . . . . . 8
โข (๐ โ ยฌ (๐ถ = 0 โง ๐ = 0)) |
69 | | gcdn0cl 16448 |
. . . . . . . 8
โข (((๐ถ โ โค โง ๐ โ โค) โง ยฌ
(๐ถ = 0 โง ๐ = 0)) โ (๐ถ gcd ๐) โ โ) |
70 | 11, 12, 68, 69 | syl21anc 835 |
. . . . . . 7
โข (๐ โ (๐ถ gcd ๐) โ โ) |
71 | | nnle1eq1 12247 |
. . . . . . 7
โข ((๐ถ gcd ๐) โ โ โ ((๐ถ gcd ๐) โค 1 โ (๐ถ gcd ๐) = 1)) |
72 | 70, 71 | syl 17 |
. . . . . 6
โข (๐ โ ((๐ถ gcd ๐) โค 1 โ (๐ถ gcd ๐) = 1)) |
73 | 64, 72 | mpbid 231 |
. . . . 5
โข (๐ โ (๐ถ gcd ๐) = 1) |
74 | | odzcl 16731 |
. . . . 5
โข ((๐ โ โ โง ๐ถ โ โค โง (๐ถ gcd ๐) = 1) โ
((odโคโ๐)โ๐ถ) โ โ) |
75 | 10, 11, 73, 74 | syl3anc 1370 |
. . . 4
โข (๐ โ
((odโคโ๐)โ๐ถ) โ โ) |
76 | 75 | nnzd 12590 |
. . 3
โข (๐ โ
((odโคโ๐)โ๐ถ) โ โค) |
77 | | prmuz2 16638 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ
(โคโฅโ2)) |
78 | 8, 77 | syl 17 |
. . . . . . 7
โข (๐ โ ๐ โ
(โคโฅโ2)) |
79 | 78, 28 | eleqtrdi 2842 |
. . . . . 6
โข (๐ โ ๐ โ (โคโฅโ(1 +
1))) |
80 | | eluzp1m1 12853 |
. . . . . 6
โข ((1
โ โค โง ๐
โ (โคโฅโ(1 + 1))) โ (๐ โ 1) โ
(โคโฅโ1)) |
81 | 46, 79, 80 | sylancr 586 |
. . . . 5
โข (๐ โ (๐ โ 1) โ
(โคโฅโ1)) |
82 | 81, 22 | eleqtrrdi 2843 |
. . . 4
โข (๐ โ (๐ โ 1) โ โ) |
83 | 82 | nnzd 12590 |
. . 3
โข (๐ โ (๐ โ 1) โ โค) |
84 | 19 | nnzd 12590 |
. . . . . 6
โข (๐ โ ๐ด โ โค) |
85 | 49 | nnzd 12590 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ โค) |
86 | | pcdvds 16802 |
. . . . . . 7
โข ((๐ โ โ โง ๐ด โ โ) โ (๐โ(๐ pCnt ๐ด)) โฅ ๐ด) |
87 | 1, 19, 86 | syl2anc 583 |
. . . . . 6
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โฅ ๐ด) |
88 | 20 | nnzd 12590 |
. . . . . . . 8
โข (๐ โ ๐ต โ โค) |
89 | | dvdsmul1 16226 |
. . . . . . . 8
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ด ยท ๐ต)) |
90 | 84, 88, 89 | syl2anc 583 |
. . . . . . 7
โข (๐ โ ๐ด โฅ (๐ด ยท ๐ต)) |
91 | 18 | oveq1d 7427 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) = (((๐ด ยท ๐ต) + 1) โ 1)) |
92 | 21 | nncnd 12233 |
. . . . . . . . 9
โข (๐ โ (๐ด ยท ๐ต) โ โ) |
93 | | ax-1cn 11171 |
. . . . . . . . 9
โข 1 โ
โ |
94 | | pncan 11471 |
. . . . . . . . 9
โข (((๐ด ยท ๐ต) โ โ โง 1 โ โ)
โ (((๐ด ยท ๐ต) + 1) โ 1) = (๐ด ยท ๐ต)) |
95 | 92, 93, 94 | sylancl 585 |
. . . . . . . 8
โข (๐ โ (((๐ด ยท ๐ต) + 1) โ 1) = (๐ด ยท ๐ต)) |
96 | 91, 95 | eqtrd 2771 |
. . . . . . 7
โข (๐ โ (๐ โ 1) = (๐ด ยท ๐ต)) |
97 | 90, 96 | breqtrrd 5177 |
. . . . . 6
โข (๐ โ ๐ด โฅ (๐ โ 1)) |
98 | 7, 84, 85, 87, 97 | dvdstrd 16243 |
. . . . 5
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1)) |
99 | 6 | nnne0d 12267 |
. . . . . 6
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โ 0) |
100 | | dvdsval2 16205 |
. . . . . 6
โข (((๐โ(๐ pCnt ๐ด)) โ โค โง (๐โ(๐ pCnt ๐ด)) โ 0 โง (๐ โ 1) โ โค) โ ((๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1) โ ((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) โ โค)) |
101 | 7, 99, 85, 100 | syl3anc 1370 |
. . . . 5
โข (๐ โ ((๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1) โ ((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) โ โค)) |
102 | 98, 101 | mpbid 231 |
. . . 4
โข (๐ โ ((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) โ โค) |
103 | | peano2zm 12610 |
. . . . . . . 8
โข ((๐ถโ(๐ โ 1)) โ โค โ ((๐ถโ(๐ โ 1)) โ 1) โ
โค) |
104 | 52, 103 | syl 17 |
. . . . . . 7
โข (๐ โ ((๐ถโ(๐ โ 1)) โ 1) โ
โค) |
105 | 32 | nnred 12232 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
106 | 31 | simprd 495 |
. . . . . . . . . 10
โข (๐ โ 1 < ๐) |
107 | | 1mod 13873 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
108 | 105, 106,
107 | syl2anc 583 |
. . . . . . . . 9
โข (๐ โ (1 mod ๐) = 1) |
109 | 44, 108 | eqtr4d 2774 |
. . . . . . . 8
โข (๐ โ ((๐ถโ(๐ โ 1)) mod ๐) = (1 mod ๐)) |
110 | | 1zzd 12598 |
. . . . . . . . 9
โข (๐ โ 1 โ
โค) |
111 | | moddvds 16213 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ถโ(๐ โ 1)) โ โค โง 1 โ
โค) โ (((๐ถโ(๐ โ 1)) mod ๐) = (1 mod ๐) โ ๐ โฅ ((๐ถโ(๐ โ 1)) โ 1))) |
112 | 32, 52, 110, 111 | syl3anc 1370 |
. . . . . . . 8
โข (๐ โ (((๐ถโ(๐ โ 1)) mod ๐) = (1 mod ๐) โ ๐ โฅ ((๐ถโ(๐ โ 1)) โ 1))) |
113 | 109, 112 | mpbid 231 |
. . . . . . 7
โข (๐ โ ๐ โฅ ((๐ถโ(๐ โ 1)) โ 1)) |
114 | 12, 33, 104, 35, 113 | dvdstrd 16243 |
. . . . . 6
โข (๐ โ ๐ โฅ ((๐ถโ(๐ โ 1)) โ 1)) |
115 | | odzdvds 16733 |
. . . . . . 7
โข (((๐ โ โ โง ๐ถ โ โค โง (๐ถ gcd ๐) = 1) โง (๐ โ 1) โ โ0)
โ (๐ โฅ ((๐ถโ(๐ โ 1)) โ 1) โ
((odโคโ๐)โ๐ถ) โฅ (๐ โ 1))) |
116 | 10, 11, 73, 50, 115 | syl31anc 1372 |
. . . . . 6
โข (๐ โ (๐ โฅ ((๐ถโ(๐ โ 1)) โ 1) โ
((odโคโ๐)โ๐ถ) โฅ (๐ โ 1))) |
117 | 114, 116 | mpbid 231 |
. . . . 5
โข (๐ โ
((odโคโ๐)โ๐ถ) โฅ (๐ โ 1)) |
118 | 49 | nncnd 12233 |
. . . . . 6
โข (๐ โ (๐ โ 1) โ โ) |
119 | 6 | nncnd 12233 |
. . . . . 6
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โ โ) |
120 | 118, 119,
99 | divcan1d 11996 |
. . . . 5
โข (๐ โ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ(๐ pCnt ๐ด))) = (๐ โ 1)) |
121 | 117, 120 | breqtrrd 5177 |
. . . 4
โข (๐ โ
((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ(๐ pCnt ๐ด)))) |
122 | | nprmdvds1 16648 |
. . . . . 6
โข (๐ โ โ โ ยฌ
๐ โฅ
1) |
123 | 8, 122 | syl 17 |
. . . . 5
โข (๐ โ ยฌ ๐ โฅ 1) |
124 | 3 | nnzd 12590 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โค) |
125 | | iddvdsexp 16228 |
. . . . . . . . . . . . . 14
โข ((๐ โ โค โง (๐ pCnt ๐ด) โ โ) โ ๐ โฅ (๐โ(๐ pCnt ๐ด))) |
126 | 124, 4, 125 | syl2anc 583 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โฅ (๐โ(๐ pCnt ๐ด))) |
127 | 124, 7, 85, 126, 98 | dvdstrd 16243 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โฅ (๐ โ 1)) |
128 | 3 | nnne0d 12267 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ 0) |
129 | | dvdsval2 16205 |
. . . . . . . . . . . . 13
โข ((๐ โ โค โง ๐ โ 0 โง (๐ โ 1) โ โค) โ (๐ โฅ (๐ โ 1) โ ((๐ โ 1) / ๐) โ โค)) |
130 | 124, 128,
85, 129 | syl3anc 1370 |
. . . . . . . . . . . 12
โข (๐ โ (๐ โฅ (๐ โ 1) โ ((๐ โ 1) / ๐) โ โค)) |
131 | 127, 130 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ 1) / ๐) โ โค) |
132 | 50 | nn0ge0d 12540 |
. . . . . . . . . . . 12
โข (๐ โ 0 โค (๐ โ 1)) |
133 | 49 | nnred 12232 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ โ 1) โ โ) |
134 | 3 | nnred 12232 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ โ โ) |
135 | 3 | nngt0d 12266 |
. . . . . . . . . . . . 13
โข (๐ โ 0 < ๐) |
136 | | ge0div 12086 |
. . . . . . . . . . . . 13
โข (((๐ โ 1) โ โ โง
๐ โ โ โง 0
< ๐) โ (0 โค
(๐ โ 1) โ 0 โค
((๐ โ 1) / ๐))) |
137 | 133, 134,
135, 136 | syl3anc 1370 |
. . . . . . . . . . . 12
โข (๐ โ (0 โค (๐ โ 1) โ 0 โค ((๐ โ 1) / ๐))) |
138 | 132, 137 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ 0 โค ((๐ โ 1) / ๐)) |
139 | | elnn0z 12576 |
. . . . . . . . . . 11
โข (((๐ โ 1) / ๐) โ โ0 โ (((๐ โ 1) / ๐) โ โค โง 0 โค ((๐ โ 1) / ๐))) |
140 | 131, 138,
139 | sylanbrc 582 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ 1) / ๐) โ
โ0) |
141 | | zexpcl 14047 |
. . . . . . . . . 10
โข ((๐ถ โ โค โง ((๐ โ 1) / ๐) โ โ0) โ (๐ถโ((๐ โ 1) / ๐)) โ โค) |
142 | 11, 140, 141 | syl2anc 583 |
. . . . . . . . 9
โข (๐ โ (๐ถโ((๐ โ 1) / ๐)) โ โค) |
143 | | peano2zm 12610 |
. . . . . . . . 9
โข ((๐ถโ((๐ โ 1) / ๐)) โ โค โ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ
โค) |
144 | 142, 143 | syl 17 |
. . . . . . . 8
โข (๐ โ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ
โค) |
145 | | dvdsgcd 16491 |
. . . . . . . 8
โข ((๐ โ โค โง ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ โค โง ๐ โ โค) โ ((๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โง ๐ โฅ ๐) โ ๐ โฅ (((๐ถโ((๐ โ 1) / ๐)) โ 1) gcd ๐))) |
146 | 12, 144, 33, 145 | syl3anc 1370 |
. . . . . . 7
โข (๐ โ ((๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โง ๐ โฅ ๐) โ ๐ โฅ (((๐ถโ((๐ โ 1) / ๐)) โ 1) gcd ๐))) |
147 | 35, 146 | mpan2d 691 |
. . . . . 6
โข (๐ โ (๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ ๐ โฅ (((๐ถโ((๐ โ 1) / ๐)) โ 1) gcd ๐))) |
148 | | odzdvds 16733 |
. . . . . . . 8
โข (((๐ โ โ โง ๐ถ โ โค โง (๐ถ gcd ๐) = 1) โง ((๐ โ 1) / ๐) โ โ0) โ (๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ
((odโคโ๐)โ๐ถ) โฅ ((๐ โ 1) / ๐))) |
149 | 10, 11, 73, 140, 148 | syl31anc 1372 |
. . . . . . 7
โข (๐ โ (๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ
((odโคโ๐)โ๐ถ) โฅ ((๐ โ 1) / ๐))) |
150 | 3 | nncnd 12233 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
151 | 4 | nnzd 12590 |
. . . . . . . . . . 11
โข (๐ โ (๐ pCnt ๐ด) โ โค) |
152 | 150, 128,
151 | expm1d 14126 |
. . . . . . . . . 10
โข (๐ โ (๐โ((๐ pCnt ๐ด) โ 1)) = ((๐โ(๐ pCnt ๐ด)) / ๐)) |
153 | 152 | oveq2d 7428 |
. . . . . . . . 9
โข (๐ โ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))) = (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท ((๐โ(๐ pCnt ๐ด)) / ๐))) |
154 | 133, 6 | nndivred 12271 |
. . . . . . . . . . 11
โข (๐ โ ((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) โ โ) |
155 | 154 | recnd 11247 |
. . . . . . . . . 10
โข (๐ โ ((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) โ โ) |
156 | 155, 119,
150, 128 | divassd 12030 |
. . . . . . . . 9
โข (๐ โ ((((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ(๐ pCnt ๐ด))) / ๐) = (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท ((๐โ(๐ pCnt ๐ด)) / ๐))) |
157 | 120 | oveq1d 7427 |
. . . . . . . . 9
โข (๐ โ ((((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ(๐ pCnt ๐ด))) / ๐) = ((๐ โ 1) / ๐)) |
158 | 153, 156,
157 | 3eqtr2d 2777 |
. . . . . . . 8
โข (๐ โ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))) = ((๐ โ 1) / ๐)) |
159 | 158 | breq2d 5161 |
. . . . . . 7
โข (๐ โ
(((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))) โ
((odโคโ๐)โ๐ถ) โฅ ((๐ โ 1) / ๐))) |
160 | 149, 159 | bitr4d 281 |
. . . . . 6
โข (๐ โ (๐ โฅ ((๐ถโ((๐ โ 1) / ๐)) โ 1) โ
((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))))) |
161 | | pockthlem.11 |
. . . . . . 7
โข (๐ โ (((๐ถโ((๐ โ 1) / ๐)) โ 1) gcd ๐) = 1) |
162 | 161 | breq2d 5161 |
. . . . . 6
โข (๐ โ (๐ โฅ (((๐ถโ((๐ โ 1) / ๐)) โ 1) gcd ๐) โ ๐ โฅ 1)) |
163 | 147, 160,
162 | 3imtr3d 292 |
. . . . 5
โข (๐ โ
(((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))) โ ๐ โฅ 1)) |
164 | 123, 163 | mtod 197 |
. . . 4
โข (๐ โ ยฌ
((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1)))) |
165 | | prmpwdvds 16842 |
. . . 4
โข
(((((๐ โ 1) /
(๐โ(๐ pCnt ๐ด))) โ โค โง
((odโคโ๐)โ๐ถ) โ โค) โง (๐ โ โ โง (๐ pCnt ๐ด) โ โ) โง
(((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ(๐ pCnt ๐ด))) โง ยฌ
((odโคโ๐)โ๐ถ) โฅ (((๐ โ 1) / (๐โ(๐ pCnt ๐ด))) ยท (๐โ((๐ pCnt ๐ด) โ 1))))) โ (๐โ(๐ pCnt ๐ด)) โฅ
((odโคโ๐)โ๐ถ)) |
166 | 102, 76, 1, 4, 121, 164, 165 | syl222anc 1385 |
. . 3
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โฅ
((odโคโ๐)โ๐ถ)) |
167 | | odzphi 16734 |
. . . . 5
โข ((๐ โ โ โง ๐ถ โ โค โง (๐ถ gcd ๐) = 1) โ
((odโคโ๐)โ๐ถ) โฅ (ฯโ๐)) |
168 | 10, 11, 73, 167 | syl3anc 1370 |
. . . 4
โข (๐ โ
((odโคโ๐)โ๐ถ) โฅ (ฯโ๐)) |
169 | | phiprm 16715 |
. . . . 5
โข (๐ โ โ โ
(ฯโ๐) = (๐ โ 1)) |
170 | 8, 169 | syl 17 |
. . . 4
โข (๐ โ (ฯโ๐) = (๐ โ 1)) |
171 | 168, 170 | breqtrd 5175 |
. . 3
โข (๐ โ
((odโคโ๐)โ๐ถ) โฅ (๐ โ 1)) |
172 | 7, 76, 83, 166, 171 | dvdstrd 16243 |
. 2
โข (๐ โ (๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1)) |
173 | | pcdvdsb 16807 |
. . 3
โข ((๐ โ โ โง (๐ โ 1) โ โค โง
(๐ pCnt ๐ด) โ โ0) โ ((๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)) โ (๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1))) |
174 | 1, 83, 5, 173 | syl3anc 1370 |
. 2
โข (๐ โ ((๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1)) โ (๐โ(๐ pCnt ๐ด)) โฅ (๐ โ 1))) |
175 | 172, 174 | mpbird 256 |
1
โข (๐ โ (๐ pCnt ๐ด) โค (๐ pCnt (๐ โ 1))) |