Step | Hyp | Ref
| Expression |
1 | | pockthi.d |
. 2
โข ๐ท โ โ |
2 | | pockthi.p |
. . . . . 6
โข ๐ โ โ |
3 | | prmnn 16557 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โ) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
โข ๐ โ โ |
5 | | pockthi.e |
. . . . . 6
โข ๐ธ โ โ |
6 | 5 | nnnn0i 12428 |
. . . . 5
โข ๐ธ โ
โ0 |
7 | | nnexpcl 13987 |
. . . . 5
โข ((๐ โ โ โง ๐ธ โ โ0)
โ (๐โ๐ธ) โ
โ) |
8 | 4, 6, 7 | mp2an 691 |
. . . 4
โข (๐โ๐ธ) โ โ |
9 | 8 | a1i 11 |
. . 3
โข (๐ท โ โ โ (๐โ๐ธ) โ โ) |
10 | | id 22 |
. . 3
โข (๐ท โ โ โ ๐ท โ
โ) |
11 | | pockthi.gt |
. . . 4
โข ๐ท < (๐โ๐ธ) |
12 | 11 | a1i 11 |
. . 3
โข (๐ท โ โ โ ๐ท < (๐โ๐ธ)) |
13 | | pockthi.n |
. . . . 5
โข ๐ = (๐ + 1) |
14 | | pockthi.fac |
. . . . . . 7
โข ๐ = (๐ท ยท (๐โ๐ธ)) |
15 | 1 | nncni 12170 |
. . . . . . . 8
โข ๐ท โ โ |
16 | 8 | nncni 12170 |
. . . . . . . 8
โข (๐โ๐ธ) โ โ |
17 | 15, 16 | mulcomi 11170 |
. . . . . . 7
โข (๐ท ยท (๐โ๐ธ)) = ((๐โ๐ธ) ยท ๐ท) |
18 | 14, 17 | eqtri 2765 |
. . . . . 6
โข ๐ = ((๐โ๐ธ) ยท ๐ท) |
19 | 18 | oveq1i 7372 |
. . . . 5
โข (๐ + 1) = (((๐โ๐ธ) ยท ๐ท) + 1) |
20 | 13, 19 | eqtri 2765 |
. . . 4
โข ๐ = (((๐โ๐ธ) ยท ๐ท) + 1) |
21 | 20 | a1i 11 |
. . 3
โข (๐ท โ โ โ ๐ = (((๐โ๐ธ) ยท ๐ท) + 1)) |
22 | | prmdvdsexpb 16599 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ โ โ โง ๐ธ โ โ) โ (๐ฅ โฅ (๐โ๐ธ) โ ๐ฅ = ๐)) |
23 | 2, 5, 22 | mp3an23 1454 |
. . . . . 6
โข (๐ฅ โ โ โ (๐ฅ โฅ (๐โ๐ธ) โ ๐ฅ = ๐)) |
24 | | pockthi.m |
. . . . . . . . . . . . 13
โข ๐ = (๐บ ยท ๐) |
25 | | pockthi.g |
. . . . . . . . . . . . . 14
โข ๐บ โ โ |
26 | 25, 4 | nnmulcli 12185 |
. . . . . . . . . . . . 13
โข (๐บ ยท ๐) โ โ |
27 | 24, 26 | eqeltri 2834 |
. . . . . . . . . . . 12
โข ๐ โ โ |
28 | 27 | nncni 12170 |
. . . . . . . . . . 11
โข ๐ โ โ |
29 | | ax-1cn 11116 |
. . . . . . . . . . 11
โข 1 โ
โ |
30 | 28, 29, 13 | mvrraddi 11425 |
. . . . . . . . . 10
โข (๐ โ 1) = ๐ |
31 | 30 | oveq2i 7373 |
. . . . . . . . 9
โข (๐ดโ(๐ โ 1)) = (๐ดโ๐) |
32 | 31 | oveq1i 7372 |
. . . . . . . 8
โข ((๐ดโ(๐ โ 1)) mod ๐) = ((๐ดโ๐) mod ๐) |
33 | | pockthi.mod |
. . . . . . . . 9
โข ((๐ดโ๐) mod ๐) = (1 mod ๐) |
34 | | peano2nn 12172 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ (๐ + 1) โ
โ) |
35 | 27, 34 | ax-mp 5 |
. . . . . . . . . . . 12
โข (๐ + 1) โ
โ |
36 | 13, 35 | eqeltri 2834 |
. . . . . . . . . . 11
โข ๐ โ โ |
37 | 36 | nnrei 12169 |
. . . . . . . . . 10
โข ๐ โ โ |
38 | 27 | nngt0i 12199 |
. . . . . . . . . . . 12
โข 0 <
๐ |
39 | 27 | nnrei 12169 |
. . . . . . . . . . . . 13
โข ๐ โ โ |
40 | | 1re 11162 |
. . . . . . . . . . . . 13
โข 1 โ
โ |
41 | | ltaddpos2 11653 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง 1 โ
โ) โ (0 < ๐
โ 1 < (๐ +
1))) |
42 | 39, 40, 41 | mp2an 691 |
. . . . . . . . . . . 12
โข (0 <
๐ โ 1 < (๐ + 1)) |
43 | 38, 42 | mpbi 229 |
. . . . . . . . . . 11
โข 1 <
(๐ + 1) |
44 | 43, 13 | breqtrri 5137 |
. . . . . . . . . 10
โข 1 <
๐ |
45 | | 1mod 13815 |
. . . . . . . . . 10
โข ((๐ โ โ โง 1 <
๐) โ (1 mod ๐) = 1) |
46 | 37, 44, 45 | mp2an 691 |
. . . . . . . . 9
โข (1 mod
๐) = 1 |
47 | 33, 46 | eqtri 2765 |
. . . . . . . 8
โข ((๐ดโ๐) mod ๐) = 1 |
48 | 32, 47 | eqtri 2765 |
. . . . . . 7
โข ((๐ดโ(๐ โ 1)) mod ๐) = 1 |
49 | | oveq2 7370 |
. . . . . . . . . . . 12
โข (๐ฅ = ๐ โ ((๐ โ 1) / ๐ฅ) = ((๐ โ 1) / ๐)) |
50 | 25 | nncni 12170 |
. . . . . . . . . . . . . . 15
โข ๐บ โ โ |
51 | 4 | nncni 12170 |
. . . . . . . . . . . . . . 15
โข ๐ โ โ |
52 | 50, 51 | mulcomi 11170 |
. . . . . . . . . . . . . 14
โข (๐บ ยท ๐) = (๐ ยท ๐บ) |
53 | 30, 24, 52 | 3eqtrri 2770 |
. . . . . . . . . . . . 13
โข (๐ ยท ๐บ) = (๐ โ 1) |
54 | 36 | nncni 12170 |
. . . . . . . . . . . . . . 15
โข ๐ โ โ |
55 | 54, 29 | subcli 11484 |
. . . . . . . . . . . . . 14
โข (๐ โ 1) โ
โ |
56 | 4 | nnne0i 12200 |
. . . . . . . . . . . . . 14
โข ๐ โ 0 |
57 | 55, 51, 50, 56 | divmuli 11916 |
. . . . . . . . . . . . 13
โข (((๐ โ 1) / ๐) = ๐บ โ (๐ ยท ๐บ) = (๐ โ 1)) |
58 | 53, 57 | mpbir 230 |
. . . . . . . . . . . 12
โข ((๐ โ 1) / ๐) = ๐บ |
59 | 49, 58 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (๐ฅ = ๐ โ ((๐ โ 1) / ๐ฅ) = ๐บ) |
60 | 59 | oveq2d 7378 |
. . . . . . . . . 10
โข (๐ฅ = ๐ โ (๐ดโ((๐ โ 1) / ๐ฅ)) = (๐ดโ๐บ)) |
61 | 60 | oveq1d 7377 |
. . . . . . . . 9
โข (๐ฅ = ๐ โ ((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) = ((๐ดโ๐บ) โ 1)) |
62 | 61 | oveq1d 7377 |
. . . . . . . 8
โข (๐ฅ = ๐ โ (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = (((๐ดโ๐บ) โ 1) gcd ๐)) |
63 | | pockthi.gcd |
. . . . . . . 8
โข (((๐ดโ๐บ) โ 1) gcd ๐) = 1 |
64 | 62, 63 | eqtrdi 2793 |
. . . . . . 7
โข (๐ฅ = ๐ โ (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1) |
65 | | pockthi.a |
. . . . . . . . 9
โข ๐ด โ โ |
66 | 65 | nnzi 12534 |
. . . . . . . 8
โข ๐ด โ โค |
67 | | oveq1 7369 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ด โ (๐ฆโ(๐ โ 1)) = (๐ดโ(๐ โ 1))) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ด โ ((๐ฆโ(๐ โ 1)) mod ๐) = ((๐ดโ(๐ โ 1)) mod ๐)) |
69 | 68 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ฆ = ๐ด โ (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โ ((๐ดโ(๐ โ 1)) mod ๐) = 1)) |
70 | | oveq1 7369 |
. . . . . . . . . . . . 13
โข (๐ฆ = ๐ด โ (๐ฆโ((๐ โ 1) / ๐ฅ)) = (๐ดโ((๐ โ 1) / ๐ฅ))) |
71 | 70 | oveq1d 7377 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ด โ ((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) = ((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1)) |
72 | 71 | oveq1d 7377 |
. . . . . . . . . . 11
โข (๐ฆ = ๐ด โ (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐)) |
73 | 72 | eqeq1d 2739 |
. . . . . . . . . 10
โข (๐ฆ = ๐ด โ ((((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1 โ (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) |
74 | 69, 73 | anbi12d 632 |
. . . . . . . . 9
โข (๐ฆ = ๐ด โ ((((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1) โ (((๐ดโ(๐ โ 1)) mod ๐) = 1 โง (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1))) |
75 | 74 | rspcev 3584 |
. . . . . . . 8
โข ((๐ด โ โค โง (((๐ดโ(๐ โ 1)) mod ๐) = 1 โง (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) |
76 | 66, 75 | mpan 689 |
. . . . . . 7
โข ((((๐ดโ(๐ โ 1)) mod ๐) = 1 โง (((๐ดโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1) โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) |
77 | 48, 64, 76 | sylancr 588 |
. . . . . 6
โข (๐ฅ = ๐ โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) |
78 | 23, 77 | syl6bi 253 |
. . . . 5
โข (๐ฅ โ โ โ (๐ฅ โฅ (๐โ๐ธ) โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1))) |
79 | 78 | rgen 3067 |
. . . 4
โข
โ๐ฅ โ
โ (๐ฅ โฅ (๐โ๐ธ) โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1)) |
80 | 79 | a1i 11 |
. . 3
โข (๐ท โ โ โ
โ๐ฅ โ โ
(๐ฅ โฅ (๐โ๐ธ) โ โ๐ฆ โ โค (((๐ฆโ(๐ โ 1)) mod ๐) = 1 โง (((๐ฆโ((๐ โ 1) / ๐ฅ)) โ 1) gcd ๐) = 1))) |
81 | 9, 10, 12, 21, 80 | pockthg 16785 |
. 2
โข (๐ท โ โ โ ๐ โ
โ) |
82 | 1, 81 | ax-mp 5 |
1
โข ๐ โ โ |