Step |
Hyp |
Ref |
Expression |
1 |
|
aks4d1p8d3.1 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
2 |
|
aks4d1p8d3.2 |
⊢ ( 𝜑 → 𝑃 ∈ ℙ ) |
3 |
|
aks4d1p8d3.3 |
⊢ ( 𝜑 → 𝑃 ∥ 𝑁 ) |
4 |
|
pcdvds |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ) |
5 |
2 1 4
|
syl2anc |
⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ) |
6 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
7 |
2 6
|
syl |
⊢ ( 𝜑 → 𝑃 ∈ ℕ ) |
8 |
7
|
nnzd |
⊢ ( 𝜑 → 𝑃 ∈ ℤ ) |
9 |
2 1
|
pccld |
⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 ) |
10 |
8 9
|
zexpcld |
⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ ) |
11 |
8
|
zcnd |
⊢ ( 𝜑 → 𝑃 ∈ ℂ ) |
12 |
|
0red |
⊢ ( 𝜑 → 0 ∈ ℝ ) |
13 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
14 |
8
|
zred |
⊢ ( 𝜑 → 𝑃 ∈ ℝ ) |
15 |
|
0lt1 |
⊢ 0 < 1 |
16 |
15
|
a1i |
⊢ ( 𝜑 → 0 < 1 ) |
17 |
|
prmgt1 |
⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 ) |
18 |
2 17
|
syl |
⊢ ( 𝜑 → 1 < 𝑃 ) |
19 |
12 13 14 16 18
|
lttrd |
⊢ ( 𝜑 → 0 < 𝑃 ) |
20 |
12 19
|
ltned |
⊢ ( 𝜑 → 0 ≠ 𝑃 ) |
21 |
20
|
necomd |
⊢ ( 𝜑 → 𝑃 ≠ 0 ) |
22 |
9
|
nn0zd |
⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ ) |
23 |
11 21 22
|
expne0d |
⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ≠ 0 ) |
24 |
1
|
nnzd |
⊢ ( 𝜑 → 𝑁 ∈ ℤ ) |
25 |
|
dvdsval2 |
⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) ) |
26 |
10 23 24 25
|
syl3anc |
⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) ) |
27 |
5 26
|
mpbid |
⊢ ( 𝜑 → ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) |
28 |
27 10
|
gcdcomd |
⊢ ( 𝜑 → ( ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) ) |
29 |
|
pcndvds2 |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) |
30 |
2 1 29
|
syl2anc |
⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) |
31 |
|
coprm |
⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) ) |
32 |
2 27 31
|
syl2anc |
⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) ) |
33 |
30 32
|
mpbid |
⊢ ( 𝜑 → ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) |
34 |
|
pcelnn |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) ) |
35 |
2 1 34
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) ) |
36 |
3 35
|
mpbird |
⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) |
37 |
|
rpexp |
⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) ) |
38 |
8 27 36 37
|
syl3anc |
⊢ ( 𝜑 → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) ) |
39 |
33 38
|
mpbird |
⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) |
40 |
28 39
|
eqtrd |
⊢ ( 𝜑 → ( ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 1 ) |