Proof of Theorem pockthlem
Step | Hyp | Ref
| Expression |
1 | | pockthlem.7 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℙ) |
2 | | pockthg.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℕ) |
3 | | pcdvds 15939 |
. . . . . . 7
⊢ ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) |
4 | 1, 2, 3 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) |
5 | 2 | nnzd 11809 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℤ) |
6 | | pockthg.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℕ) |
7 | 6 | nnzd 11809 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) |
8 | | dvdsmul1 15380 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵)) |
9 | 5, 7, 8 | syl2anc 581 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐵)) |
10 | | pockthg.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) |
11 | 10 | oveq1d 6920 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1)) |
12 | 2, 6 | nnmulcld 11404 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
13 | 12 | nncnd 11368 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
14 | | ax-1cn 10310 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
15 | | pncan 10607 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) |
16 | 13, 14, 15 | sylancl 582 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) |
17 | 11, 16 | eqtrd 2861 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵)) |
18 | 9, 17 | breqtrrd 4901 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∥ (𝑁 − 1)) |
19 | | prmnn 15760 |
. . . . . . . . . 10
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
20 | 1, 19 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℕ) |
21 | | pockthlem.8 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) |
22 | 21 | nnnn0d 11678 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈
ℕ0) |
23 | 20, 22 | nnexpcld 13326 |
. . . . . . . 8
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ) |
24 | 23 | nnzd 11809 |
. . . . . . 7
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ) |
25 | | 1z 11735 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
26 | | nnuz 12005 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
27 | 12, 26 | syl6eleq 2916 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 · 𝐵) ∈
(ℤ≥‘1)) |
28 | | eluzp1p1 11994 |
. . . . . . . . . . . 12
⊢ ((𝐴 · 𝐵) ∈ (ℤ≥‘1)
→ ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
30 | 10, 29 | eqeltrd 2906 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(1 +
1))) |
31 | | eluzp1m1 11992 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘1)) |
32 | 25, 30, 31 | sylancr 583 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘1)) |
33 | 32, 26 | syl6eleqr 2917 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
34 | 33 | nnzd 11809 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
35 | | dvdstr 15395 |
. . . . . . 7
⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))) |
36 | 24, 5, 34, 35 | syl3anc 1496 |
. . . . . 6
⊢ (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴 ∧ 𝐴 ∥ (𝑁 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1))) |
37 | 4, 18, 36 | mp2and 692 |
. . . . 5
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) |
38 | 23 | nnne0d 11401 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0) |
39 | | dvdsval2 15360 |
. . . . . 6
⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) |
40 | 24, 38, 34, 39 | syl3anc 1496 |
. . . . 5
⊢ (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) |
41 | 37, 40 | mpbid 224 |
. . . 4
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ) |
42 | | pockthlem.5 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) |
43 | | prmnn 15760 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℕ) |
45 | | pockthlem.9 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℤ) |
46 | 44 | nnzd 11809 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℤ) |
47 | | gcddvds 15598 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) |
48 | 45, 46, 47 | syl2anc 581 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) |
49 | 48 | simpld 490 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶) |
50 | 48 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃) |
51 | | pockthlem.6 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
52 | 45, 46 | gcdcld 15603 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈
ℕ0) |
53 | 52 | nn0zd 11808 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ) |
54 | | df-2 11414 |
. . . . . . . . . . . . . . . 16
⊢ 2 = (1 +
1) |
55 | 54 | fveq2i 6436 |
. . . . . . . . . . . . . . 15
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
56 | 30, 55 | syl6eleqr 2917 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
57 | | eluz2b2 12044 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
58 | 56, 57 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
59 | 58 | simpld 490 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℕ) |
60 | 59 | nnzd 11809 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℤ) |
61 | | dvdstr 15395 |
. . . . . . . . . . 11
⊢ (((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐶 gcd 𝑃) ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁)) |
62 | 53, 46, 60, 61 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝑃 ∧ 𝑃 ∥ 𝑁) → (𝐶 gcd 𝑃) ∥ 𝑁)) |
63 | 50, 51, 62 | mp2and 692 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁) |
64 | 59 | nnne0d 11401 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) |
65 | | simpr 479 |
. . . . . . . . . . . 12
⊢ ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
66 | 65 | necon3ai 3024 |
. . . . . . . . . . 11
⊢ (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) |
68 | | dvdslegcd 15599 |
. . . . . . . . . 10
⊢ ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) |
69 | 53, 45, 60, 67, 68 | syl31anc 1498 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) |
70 | 49, 63, 69 | mp2and 692 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)) |
71 | | pockthlem.10 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) |
72 | 71 | oveq1d 6920 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁)) |
73 | 33 | nnnn0d 11678 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
74 | | zexpcl 13169 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈
ℕ0) → (𝐶↑(𝑁 − 1)) ∈
ℤ) |
75 | 45, 73, 74 | syl2anc 581 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℤ) |
76 | | modgcd 15626 |
. . . . . . . . . . 11
⊢ (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) |
77 | 75, 59, 76 | syl2anc 581 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) |
78 | | gcdcom 15608 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1)) |
79 | 25, 60, 78 | sylancr 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1)) |
80 | | gcd1 15622 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1) |
81 | 60, 80 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 gcd 1) = 1) |
82 | 79, 81 | eqtrd 2861 |
. . . . . . . . . 10
⊢ (𝜑 → (1 gcd 𝑁) = 1) |
83 | 72, 77, 82 | 3eqtr3d 2869 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1) |
84 | | rpexp 15803 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ)
→ (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) |
85 | 45, 60, 33, 84 | syl3anc 1496 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) |
86 | 83, 85 | mpbid 224 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑁) = 1) |
87 | 70, 86 | breqtrd 4899 |
. . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ 1) |
88 | 44 | nnne0d 11401 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ≠ 0) |
89 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0) |
90 | 89 | necon3ai 3024 |
. . . . . . . . . 10
⊢ (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) |
91 | 88, 90 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) |
92 | | gcdn0cl 15597 |
. . . . . . . . 9
⊢ (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬
(𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ) |
93 | 45, 46, 91, 92 | syl21anc 873 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ) |
94 | | nnle1eq1 11382 |
. . . . . . . 8
⊢ ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) |
95 | 93, 94 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) |
96 | 87, 95 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → (𝐶 gcd 𝑃) = 1) |
97 | | odzcl 15869 |
. . . . . 6
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) |
98 | 44, 45, 96, 97 | syl3anc 1496 |
. . . . 5
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) |
99 | 98 | nnzd 11809 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℤ) |
100 | 59 | nnred 11367 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
101 | 58 | simprd 491 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑁) |
102 | | 1mod 12997 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
103 | 100, 101,
102 | syl2anc 581 |
. . . . . . . . 9
⊢ (𝜑 → (1 mod 𝑁) = 1) |
104 | 71, 103 | eqtr4d 2864 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)) |
105 | | 1zzd 11736 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
106 | | moddvds 15368 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
107 | 59, 75, 105, 106 | syl3anc 1496 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
108 | 104, 107 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) |
109 | | peano2zm 11748 |
. . . . . . . . 9
⊢ ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) |
110 | 75, 109 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) |
111 | | dvdstr 15395 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ((𝐶↑(𝑁 − 1)) − 1) ∈ ℤ)
→ ((𝑃 ∥ 𝑁 ∧ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
112 | 46, 60, 110, 111 | syl3anc 1496 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∥ 𝑁 ∧ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
113 | 51, 108, 112 | mp2and 692 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)) |
114 | | odzdvds 15871 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0)
→ (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) |
115 | 44, 45, 96, 73, 114 | syl31anc 1498 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) |
116 | 113, 115 | mpbid 224 |
. . . . 5
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)) |
117 | 33 | nncnd 11368 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
118 | 23 | nncnd 11368 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ) |
119 | 117, 118,
38 | divcan1d 11128 |
. . . . 5
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1)) |
120 | 116, 119 | breqtrrd 4901 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴)))) |
121 | | nprmdvds1 15789 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) |
122 | 42, 121 | syl 17 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ 1) |
123 | 20 | nnzd 11809 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ ℤ) |
124 | | iddvdsexp 15382 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) |
125 | 123, 21, 124 | syl2anc 581 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) |
126 | | dvdstr 15395 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1))) |
127 | 123, 24, 34, 126 | syl3anc 1496 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴)) ∧ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) → 𝑄 ∥ (𝑁 − 1))) |
128 | 125, 37, 127 | mp2and 692 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∥ (𝑁 − 1)) |
129 | 20 | nnne0d 11401 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ≠ 0) |
130 | | dvdsval2 15360 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) |
131 | 123, 129,
34, 130 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) |
132 | 128, 131 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ) |
133 | 73 | nn0ge0d 11681 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁 − 1)) |
134 | 33 | nnred 11367 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
135 | 20 | nnred 11367 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ℝ) |
136 | 20 | nngt0d 11400 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑄) |
137 | | ge0div 11220 |
. . . . . . . . . . . . 13
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ 0
< 𝑄) → (0 ≤
(𝑁 − 1) ↔ 0 ≤
((𝑁 − 1) / 𝑄))) |
138 | 134, 135,
136, 137 | syl3anc 1496 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄))) |
139 | 133, 138 | mpbid 224 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄)) |
140 | | elnn0z 11717 |
. . . . . . . . . . 11
⊢ (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄))) |
141 | 132, 139,
140 | sylanbrc 580 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈
ℕ0) |
142 | | zexpcl 13169 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) |
143 | 45, 141, 142 | syl2anc 581 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) |
144 | | peano2zm 11748 |
. . . . . . . . 9
⊢ ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) |
145 | 143, 144 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) |
146 | | dvdsgcd 15634 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
147 | 46, 145, 60, 146 | syl3anc 1496 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
148 | 51, 147 | mpan2d 687 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
149 | | odzdvds 15871 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
150 | 44, 45, 96, 141, 149 | syl31anc 1498 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
151 | 20 | nncnd 11368 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) |
152 | 21 | nnzd 11809 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ) |
153 | 151, 129,
152 | expm1d 13312 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)) |
154 | 153 | oveq2d 6921 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) |
155 | 134, 23 | nndivred 11405 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ) |
156 | 155 | recnd 10385 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ) |
157 | 156, 118,
151, 129 | divassd 11162 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) |
158 | 119 | oveq1d 6920 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄)) |
159 | 154, 157,
158 | 3eqtr2d 2867 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄)) |
160 | 159 | breq2d 4885 |
. . . . . . 7
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
161 | 150, 160 | bitr4d 274 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) |
162 | | pockthlem.11 |
. . . . . . 7
⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) |
163 | 162 | breq2d 4885 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1)) |
164 | 148, 161,
163 | 3imtr3d 285 |
. . . . 5
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1)) |
165 | 122, 164 | mtod 190 |
. . . 4
⊢ (𝜑 → ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))) |
166 | | prmpwdvds 15979 |
. . . 4
⊢
(((((𝑁 − 1) /
(𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧
((odℤ‘𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) |
167 | 41, 99, 1, 21, 120, 165, 166 | syl222anc 1511 |
. . 3
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) |
168 | | odzphi 15872 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) |
169 | 44, 45, 96, 168 | syl3anc 1496 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) |
170 | | phiprm 15853 |
. . . . 5
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
171 | 42, 170 | syl 17 |
. . . 4
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
172 | 169, 171 | breqtrd 4899 |
. . 3
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1)) |
173 | | prmuz2 15780 |
. . . . . . . . 9
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
174 | 42, 173 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
175 | 174, 55 | syl6eleq 2916 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(1 +
1))) |
176 | | eluzp1m1 11992 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ 𝑃
∈ (ℤ≥‘(1 + 1))) → (𝑃 − 1) ∈
(ℤ≥‘1)) |
177 | 25, 175, 176 | sylancr 583 |
. . . . . 6
⊢ (𝜑 → (𝑃 − 1) ∈
(ℤ≥‘1)) |
178 | 177, 26 | syl6eleqr 2917 |
. . . . 5
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
179 | 178 | nnzd 11809 |
. . . 4
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
180 | | dvdstr 15395 |
. . . 4
⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧
((odℤ‘𝑃)‘𝐶) ∈ ℤ ∧ (𝑃 − 1) ∈ ℤ) → (((𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶) ∧ ((odℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
181 | 24, 99, 179, 180 | syl3anc 1496 |
. . 3
⊢ (𝜑 → (((𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶) ∧ ((odℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1)) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
182 | 167, 172,
181 | mp2and 692 |
. 2
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)) |
183 | | pcdvdsb 15944 |
. . 3
⊢ ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧
(𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
184 | 1, 179, 22, 183 | syl3anc 1496 |
. 2
⊢ (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
185 | 182, 184 | mpbird 249 |
1
⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |