Proof of Theorem pockthlem
Step | Hyp | Ref
| Expression |
1 | | pockthlem.7 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ ℙ) |
2 | | prmnn 12064 |
. . . . . 6
⊢ (𝑄 ∈ ℙ → 𝑄 ∈
ℕ) |
3 | 1, 2 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ ℕ) |
4 | | pockthlem.8 |
. . . . . 6
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) |
5 | 4 | nnnn0d 9188 |
. . . . 5
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈
ℕ0) |
6 | 3, 5 | nnexpcld 10631 |
. . . 4
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℕ) |
7 | 6 | nnzd 9333 |
. . 3
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ) |
8 | | pockthlem.5 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ ℙ) |
9 | | prmnn 12064 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
10 | 8, 9 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ ℕ) |
11 | | pockthlem.9 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℤ) |
12 | 10 | nnzd 9333 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℤ) |
13 | | gcddvds 11918 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) |
14 | 11, 12, 13 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑃)) |
15 | 14 | simpld 111 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝐶) |
16 | 11, 12 | gcdcld 11923 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈
ℕ0) |
17 | 16 | nn0zd 9332 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℤ) |
18 | | pockthg.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) |
19 | | pockthg.1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ ℕ) |
20 | | pockthg.2 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ ℕ) |
21 | 19, 20 | nnmulcld 8927 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) |
22 | | nnuz 9522 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
23 | 21, 22 | eleqtrdi 2263 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 · 𝐵) ∈
(ℤ≥‘1)) |
24 | | eluzp1p1 9512 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 · 𝐵) ∈ (ℤ≥‘1)
→ ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
25 | 23, 24 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 · 𝐵) + 1) ∈
(ℤ≥‘(1 + 1))) |
26 | 18, 25 | eqeltrd 2247 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(1 +
1))) |
27 | | df-2 8937 |
. . . . . . . . . . . . . 14
⊢ 2 = (1 +
1) |
28 | 27 | fveq2i 5499 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘2) = (ℤ≥‘(1 +
1)) |
29 | 26, 28 | eleqtrrdi 2264 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘2)) |
30 | | eluz2b2 9562 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘2) ↔ (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
31 | 29, 30 | sylib 121 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 1 < 𝑁)) |
32 | 31 | simpld 111 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
33 | 32 | nnzd 9333 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℤ) |
34 | 14 | simprd 113 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑃) |
35 | | pockthlem.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∥ 𝑁) |
36 | 17, 12, 33, 34, 35 | dvdstrd 11792 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 gcd 𝑃) ∥ 𝑁) |
37 | 32 | nnne0d 8923 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ≠ 0) |
38 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝐶 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
39 | 38 | necon3ai 2389 |
. . . . . . . . . 10
⊢ (𝑁 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) |
40 | 37, 39 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑁 = 0)) |
41 | | dvdslegcd 11919 |
. . . . . . . . 9
⊢ ((((𝐶 gcd 𝑃) ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝐶 = 0 ∧ 𝑁 = 0)) → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) |
42 | 17, 11, 33, 40, 41 | syl31anc 1236 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶 gcd 𝑃) ∥ 𝐶 ∧ (𝐶 gcd 𝑃) ∥ 𝑁) → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁))) |
43 | 15, 36, 42 | mp2and 431 |
. . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ (𝐶 gcd 𝑁)) |
44 | | pockthlem.10 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) |
45 | 44 | oveq1d 5868 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = (1 gcd 𝑁)) |
46 | | 1z 9238 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℤ |
47 | | eluzp1m1 9510 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝑁
∈ (ℤ≥‘(1 + 1))) → (𝑁 − 1) ∈
(ℤ≥‘1)) |
48 | 46, 26, 47 | sylancr 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈
(ℤ≥‘1)) |
49 | 48, 22 | eleqtrrdi 2264 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − 1) ∈ ℕ) |
50 | 49 | nnnn0d 9188 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − 1) ∈
ℕ0) |
51 | | zexpcl 10491 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ ℤ ∧ (𝑁 − 1) ∈
ℕ0) → (𝐶↑(𝑁 − 1)) ∈
ℤ) |
52 | 11, 50, 51 | syl2anc 409 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐶↑(𝑁 − 1)) ∈
ℤ) |
53 | | modgcd 11946 |
. . . . . . . . . 10
⊢ (((𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) |
54 | 52, 32, 53 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) gcd 𝑁) = ((𝐶↑(𝑁 − 1)) gcd 𝑁)) |
55 | | gcdcom 11928 |
. . . . . . . . . . 11
⊢ ((1
∈ ℤ ∧ 𝑁
∈ ℤ) → (1 gcd 𝑁) = (𝑁 gcd 1)) |
56 | 46, 33, 55 | sylancr 412 |
. . . . . . . . . 10
⊢ (𝜑 → (1 gcd 𝑁) = (𝑁 gcd 1)) |
57 | | gcd1 11942 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 1) = 1) |
58 | 33, 57 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 gcd 1) = 1) |
59 | 56, 58 | eqtrd 2203 |
. . . . . . . . 9
⊢ (𝜑 → (1 gcd 𝑁) = 1) |
60 | 45, 54, 59 | 3eqtr3d 2211 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1) |
61 | | rpexp 12107 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝑁 − 1) ∈ ℕ)
→ (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) |
62 | 11, 33, 49, 61 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) gcd 𝑁) = 1 ↔ (𝐶 gcd 𝑁) = 1)) |
63 | 60, 62 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑁) = 1) |
64 | 43, 63 | breqtrd 4015 |
. . . . . 6
⊢ (𝜑 → (𝐶 gcd 𝑃) ≤ 1) |
65 | 10 | nnne0d 8923 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ≠ 0) |
66 | | simpr 109 |
. . . . . . . . . 10
⊢ ((𝐶 = 0 ∧ 𝑃 = 0) → 𝑃 = 0) |
67 | 66 | necon3ai 2389 |
. . . . . . . . 9
⊢ (𝑃 ≠ 0 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) |
68 | 65, 67 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝐶 = 0 ∧ 𝑃 = 0)) |
69 | | gcdn0cl 11917 |
. . . . . . . 8
⊢ (((𝐶 ∈ ℤ ∧ 𝑃 ∈ ℤ) ∧ ¬
(𝐶 = 0 ∧ 𝑃 = 0)) → (𝐶 gcd 𝑃) ∈ ℕ) |
70 | 11, 12, 68, 69 | syl21anc 1232 |
. . . . . . 7
⊢ (𝜑 → (𝐶 gcd 𝑃) ∈ ℕ) |
71 | | nnle1eq1 8902 |
. . . . . . 7
⊢ ((𝐶 gcd 𝑃) ∈ ℕ → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) |
72 | 70, 71 | syl 14 |
. . . . . 6
⊢ (𝜑 → ((𝐶 gcd 𝑃) ≤ 1 ↔ (𝐶 gcd 𝑃) = 1)) |
73 | 64, 72 | mpbid 146 |
. . . . 5
⊢ (𝜑 → (𝐶 gcd 𝑃) = 1) |
74 | | odzcl 12197 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) |
75 | 10, 11, 73, 74 | syl3anc 1233 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℕ) |
76 | 75 | nnzd 9333 |
. . 3
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∈ ℤ) |
77 | | prmuz2 12085 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
(ℤ≥‘2)) |
78 | 8, 77 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
(ℤ≥‘2)) |
79 | 78, 28 | eleqtrdi 2263 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘(1 +
1))) |
80 | | eluzp1m1 9510 |
. . . . . 6
⊢ ((1
∈ ℤ ∧ 𝑃
∈ (ℤ≥‘(1 + 1))) → (𝑃 − 1) ∈
(ℤ≥‘1)) |
81 | 46, 79, 80 | sylancr 412 |
. . . . 5
⊢ (𝜑 → (𝑃 − 1) ∈
(ℤ≥‘1)) |
82 | 81, 22 | eleqtrrdi 2264 |
. . . 4
⊢ (𝜑 → (𝑃 − 1) ∈ ℕ) |
83 | 82 | nnzd 9333 |
. . 3
⊢ (𝜑 → (𝑃 − 1) ∈ ℤ) |
84 | 19 | nnzd 9333 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℤ) |
85 | 49 | nnzd 9333 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℤ) |
86 | | pcdvds 12268 |
. . . . . . 7
⊢ ((𝑄 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) |
87 | 1, 19, 86 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ 𝐴) |
88 | 20 | nnzd 9333 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℤ) |
89 | | dvdsmul1 11775 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐵)) |
90 | 84, 88, 89 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐵)) |
91 | 18 | oveq1d 5868 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 1) = (((𝐴 · 𝐵) + 1) − 1)) |
92 | 21 | nncnd 8892 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℂ) |
93 | | ax-1cn 7867 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
94 | | pncan 8125 |
. . . . . . . . 9
⊢ (((𝐴 · 𝐵) ∈ ℂ ∧ 1 ∈ ℂ)
→ (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) |
95 | 92, 93, 94 | sylancl 411 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 · 𝐵) + 1) − 1) = (𝐴 · 𝐵)) |
96 | 91, 95 | eqtrd 2203 |
. . . . . . 7
⊢ (𝜑 → (𝑁 − 1) = (𝐴 · 𝐵)) |
97 | 90, 96 | breqtrrd 4017 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∥ (𝑁 − 1)) |
98 | 7, 84, 85, 87, 97 | dvdstrd 11792 |
. . . . 5
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1)) |
99 | 6 | nnne0d 8923 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0) |
100 | | dvdsval2 11752 |
. . . . . 6
⊢ (((𝑄↑(𝑄 pCnt 𝐴)) ∈ ℤ ∧ (𝑄↑(𝑄 pCnt 𝐴)) ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) |
101 | 7, 99, 85, 100 | syl3anc 1233 |
. . . . 5
⊢ (𝜑 → ((𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ)) |
102 | 98, 101 | mpbid 146 |
. . . 4
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ) |
103 | | peano2zm 9250 |
. . . . . . . 8
⊢ ((𝐶↑(𝑁 − 1)) ∈ ℤ → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) |
104 | 52, 103 | syl 14 |
. . . . . . 7
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) − 1) ∈
ℤ) |
105 | | nnq 9592 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℚ) |
106 | 32, 105 | syl 14 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℚ) |
107 | 31 | simprd 113 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < 𝑁) |
108 | | q1mod 10312 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℚ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
109 | 106, 107,
108 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → (1 mod 𝑁) = 1) |
110 | 44, 109 | eqtr4d 2206 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)) |
111 | | 1zzd 9239 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
112 | | moddvds 11761 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ (𝐶↑(𝑁 − 1)) ∈ ℤ ∧ 1 ∈
ℤ) → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
113 | 32, 52, 111, 112 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝜑 → (((𝐶↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁) ↔ 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1))) |
114 | 110, 113 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∥ ((𝐶↑(𝑁 − 1)) − 1)) |
115 | 12, 33, 104, 35, 114 | dvdstrd 11792 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1)) |
116 | | odzdvds 12199 |
. . . . . . 7
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ (𝑁 − 1) ∈ ℕ0)
→ (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) |
117 | 10, 11, 73, 50, 116 | syl31anc 1236 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑(𝑁 − 1)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1))) |
118 | 115, 117 | mpbid 146 |
. . . . 5
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑁 − 1)) |
119 | 49 | nncnd 8892 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 1) ∈ ℂ) |
120 | 6 | nncnd 8892 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∈ ℂ) |
121 | 6 | nnap0d 8924 |
. . . . . 6
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) # 0) |
122 | 119, 120,
121 | divcanap1d 8708 |
. . . . 5
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) = (𝑁 − 1)) |
123 | 118, 122 | breqtrrd 4017 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴)))) |
124 | | nprmdvds1 12094 |
. . . . . 6
⊢ (𝑃 ∈ ℙ → ¬
𝑃 ∥
1) |
125 | 8, 124 | syl 14 |
. . . . 5
⊢ (𝜑 → ¬ 𝑃 ∥ 1) |
126 | 3 | nnzd 9333 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ℤ) |
127 | | iddvdsexp 11777 |
. . . . . . . . . . . . . 14
⊢ ((𝑄 ∈ ℤ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) |
128 | 126, 4, 127 | syl2anc 409 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∥ (𝑄↑(𝑄 pCnt 𝐴))) |
129 | 126, 7, 85, 128, 98 | dvdstrd 11792 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑄 ∥ (𝑁 − 1)) |
130 | 3 | nnne0d 8923 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ≠ 0) |
131 | | dvdsval2 11752 |
. . . . . . . . . . . . 13
⊢ ((𝑄 ∈ ℤ ∧ 𝑄 ≠ 0 ∧ (𝑁 − 1) ∈ ℤ) → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) |
132 | 126, 130,
85, 131 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑄 ∥ (𝑁 − 1) ↔ ((𝑁 − 1) / 𝑄) ∈ ℤ)) |
133 | 129, 132 | mpbid 146 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈ ℤ) |
134 | 50 | nn0ge0d 9191 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (𝑁 − 1)) |
135 | 49 | nnred 8891 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 − 1) ∈ ℝ) |
136 | 3 | nnred 8891 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 ∈ ℝ) |
137 | 3 | nngt0d 8922 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝑄) |
138 | | ge0div 8787 |
. . . . . . . . . . . . 13
⊢ (((𝑁 − 1) ∈ ℝ ∧
𝑄 ∈ ℝ ∧ 0
< 𝑄) → (0 ≤
(𝑁 − 1) ↔ 0 ≤
((𝑁 − 1) / 𝑄))) |
139 | 135, 136,
137, 138 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ (𝑁 − 1) ↔ 0 ≤ ((𝑁 − 1) / 𝑄))) |
140 | 134, 139 | mpbid 146 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((𝑁 − 1) / 𝑄)) |
141 | | elnn0z 9225 |
. . . . . . . . . . 11
⊢ (((𝑁 − 1) / 𝑄) ∈ ℕ0 ↔ (((𝑁 − 1) / 𝑄) ∈ ℤ ∧ 0 ≤ ((𝑁 − 1) / 𝑄))) |
142 | 133, 140,
141 | sylanbrc 415 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / 𝑄) ∈
ℕ0) |
143 | | zexpcl 10491 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ ℤ ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) |
144 | 11, 142, 143 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ) |
145 | | peano2zm 9250 |
. . . . . . . . 9
⊢ ((𝐶↑((𝑁 − 1) / 𝑄)) ∈ ℤ → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) |
146 | 144, 145 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈
ℤ) |
147 | | dvdsgcd 11967 |
. . . . . . . 8
⊢ ((𝑃 ∈ ℤ ∧ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
148 | 12, 146, 33, 147 | syl3anc 1233 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ∧ 𝑃 ∥ 𝑁) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
149 | 35, 148 | mpan2d 426 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) → 𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁))) |
150 | | odzdvds 12199 |
. . . . . . . 8
⊢ (((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) ∧ ((𝑁 − 1) / 𝑄) ∈ ℕ0) → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
151 | 10, 11, 73, 142, 150 | syl31anc 1236 |
. . . . . . 7
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
152 | 3 | nncnd 8892 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) |
153 | 3 | nnap0d 8924 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 # 0) |
154 | 4 | nnzd 9333 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℤ) |
155 | 152, 153,
154 | expm1apd 10619 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄↑((𝑄 pCnt 𝐴) − 1)) = ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄)) |
156 | 155 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) |
157 | 135, 6 | nndivred 8928 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℝ) |
158 | 157 | recnd 7948 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) ∈ ℂ) |
159 | 158, 120,
152, 153 | divassapd 8743 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · ((𝑄↑(𝑄 pCnt 𝐴)) / 𝑄))) |
160 | 122 | oveq1d 5868 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) / 𝑄) = ((𝑁 − 1) / 𝑄)) |
161 | 156, 159,
160 | 3eqtr2d 2209 |
. . . . . . . 8
⊢ (𝜑 → (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) = ((𝑁 − 1) / 𝑄)) |
162 | 161 | breq2d 4001 |
. . . . . . 7
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) ↔
((odℤ‘𝑃)‘𝐶) ∥ ((𝑁 − 1) / 𝑄))) |
163 | 151, 162 | bitr4d 190 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ ((𝐶↑((𝑁 − 1) / 𝑄)) − 1) ↔
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) |
164 | | pockthlem.11 |
. . . . . . 7
⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) |
165 | 164 | breq2d 4001 |
. . . . . 6
⊢ (𝜑 → (𝑃 ∥ (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) ↔ 𝑃 ∥ 1)) |
166 | 149, 163,
165 | 3imtr3d 201 |
. . . . 5
⊢ (𝜑 →
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))) → 𝑃 ∥ 1)) |
167 | 125, 166 | mtod 658 |
. . . 4
⊢ (𝜑 → ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1)))) |
168 | | prmpwdvds 12307 |
. . . 4
⊢
(((((𝑁 − 1) /
(𝑄↑(𝑄 pCnt 𝐴))) ∈ ℤ ∧
((odℤ‘𝑃)‘𝐶) ∈ ℤ) ∧ (𝑄 ∈ ℙ ∧ (𝑄 pCnt 𝐴) ∈ ℕ) ∧
(((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑(𝑄 pCnt 𝐴))) ∧ ¬
((odℤ‘𝑃)‘𝐶) ∥ (((𝑁 − 1) / (𝑄↑(𝑄 pCnt 𝐴))) · (𝑄↑((𝑄 pCnt 𝐴) − 1))))) → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) |
169 | 102, 76, 1, 4, 123, 167, 168 | syl222anc 1249 |
. . 3
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥
((odℤ‘𝑃)‘𝐶)) |
170 | | odzphi 12200 |
. . . . 5
⊢ ((𝑃 ∈ ℕ ∧ 𝐶 ∈ ℤ ∧ (𝐶 gcd 𝑃) = 1) →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) |
171 | 10, 11, 73, 170 | syl3anc 1233 |
. . . 4
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (ϕ‘𝑃)) |
172 | | phiprm 12177 |
. . . . 5
⊢ (𝑃 ∈ ℙ →
(ϕ‘𝑃) = (𝑃 − 1)) |
173 | 8, 172 | syl 14 |
. . . 4
⊢ (𝜑 → (ϕ‘𝑃) = (𝑃 − 1)) |
174 | 171, 173 | breqtrd 4015 |
. . 3
⊢ (𝜑 →
((odℤ‘𝑃)‘𝐶) ∥ (𝑃 − 1)) |
175 | 7, 76, 83, 169, 174 | dvdstrd 11792 |
. 2
⊢ (𝜑 → (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1)) |
176 | | pcdvdsb 12273 |
. . 3
⊢ ((𝑄 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧
(𝑄 pCnt 𝐴) ∈ ℕ0) → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
177 | 1, 83, 5, 176 | syl3anc 1233 |
. 2
⊢ (𝜑 → ((𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)) ↔ (𝑄↑(𝑄 pCnt 𝐴)) ∥ (𝑃 − 1))) |
178 | 175, 177 | mpbird 166 |
1
⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) |