aks4d1p8d3

Description: The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024)

	Ref	Expression
Hypotheses	aks4d1p8d3.1	$⊢ φ \to N \in ℕ$
	aks4d1p8d3.2	$⊢ φ \to P \in ℙ$
	aks4d1p8d3.3	$⊢ φ \to P ∥ N$
Assertion	aks4d1p8d3	$⊢ φ \to (\frac{N}{P^{P pCnt N}}) \gcd P^{P pCnt N} = 1$

Proof

Step	Hyp	Ref	Expression
1		aks4d1p8d3.1	$⊢ φ \to N \in ℕ$
2		aks4d1p8d3.2	$⊢ φ \to P \in ℙ$
3		aks4d1p8d3.3	$⊢ φ \to P ∥ N$
4		pcdvds	$⊢ (P \in ℙ \land N \in ℕ) \to P^{P pCnt N} ∥ N$
5	2 1 4	syl2anc	$⊢ φ \to P^{P pCnt N} ∥ N$
6		prmnn	$⊢ P \in ℙ \to P \in ℕ$
7	2 6	syl	$⊢ φ \to P \in ℕ$
8	7	nnzd	$⊢ φ \to P \in ℤ$
9	2 1	pccld	$⊢ φ \to P pCnt N \in ℕ_{0}$
10	8 9	zexpcld	$⊢ φ \to P^{P pCnt N} \in ℤ$
11	8	zcnd	$⊢ φ \to P \in ℂ$
12		0red	$⊢ φ \to 0 \in ℝ$
13		1red	$⊢ φ \to 1 \in ℝ$
14	8	zred	$⊢ φ \to P \in ℝ$
15		0lt1	$⊢ 0 < 1$
16	15	a1i	$⊢ φ \to 0 < 1$
17		prmgt1	$⊢ P \in ℙ \to 1 < P$
18	2 17	syl	$⊢ φ \to 1 < P$
19	12 13 14 16 18	lttrd	$⊢ φ \to 0 < P$
20	12 19	ltned	$⊢ φ \to 0 \neq P$
21	20	necomd	$⊢ φ \to P \neq 0$
22	9	nn0zd	$⊢ φ \to P pCnt N \in ℤ$
23	11 21 22	expne0d	$⊢ φ \to P^{P pCnt N} \neq 0$
24	1	nnzd	$⊢ φ \to N \in ℤ$
25		dvdsval2	$⊢ (P^{P pCnt N} \in ℤ \land P^{P pCnt N} \neq 0 \land N \in ℤ) \to (P^{P pCnt N} ∥ N \leftrightarrow \frac{N}{P^{P pCnt N}} \in ℤ)$
26	10 23 24 25	syl3anc	$⊢ φ \to (P^{P pCnt N} ∥ N \leftrightarrow \frac{N}{P^{P pCnt N}} \in ℤ)$
27	5 26	mpbid	$⊢ φ \to \frac{N}{P^{P pCnt N}} \in ℤ$
28	27 10	gcdcomd	$⊢ φ \to (\frac{N}{P^{P pCnt N}}) \gcd P^{P pCnt N} = P^{P pCnt N} \gcd (\frac{N}{P^{P pCnt N}})$
29		pcndvds2	$⊢ (P \in ℙ \land N \in ℕ) \to \neg P ∥ (\frac{N}{P^{P pCnt N}})$
30	2 1 29	syl2anc	$⊢ φ \to \neg P ∥ (\frac{N}{P^{P pCnt N}})$
31		coprm	$⊢ (P \in ℙ \land \frac{N}{P^{P pCnt N}} \in ℤ) \to (\neg P ∥ (\frac{N}{P^{P pCnt N}}) \leftrightarrow P \gcd (\frac{N}{P^{P pCnt N}}) = 1)$
32	2 27 31	syl2anc	$⊢ φ \to (\neg P ∥ (\frac{N}{P^{P pCnt N}}) \leftrightarrow P \gcd (\frac{N}{P^{P pCnt N}}) = 1)$
33	30 32	mpbid	$⊢ φ \to P \gcd (\frac{N}{P^{P pCnt N}}) = 1$
34		pcelnn	$⊢ (P \in ℙ \land N \in ℕ) \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
35	2 1 34	syl2anc	$⊢ φ \to (P pCnt N \in ℕ \leftrightarrow P ∥ N)$
36	3 35	mpbird	$⊢ φ \to P pCnt N \in ℕ$
37		rpexp	$⊢ (P \in ℤ \land \frac{N}{P^{P pCnt N}} \in ℤ \land P pCnt N \in ℕ) \to (P^{P pCnt N} \gcd (\frac{N}{P^{P pCnt N}}) = 1 \leftrightarrow P \gcd (\frac{N}{P^{P pCnt N}}) = 1)$
38	8 27 36 37	syl3anc	$⊢ φ \to (P^{P pCnt N} \gcd (\frac{N}{P^{P pCnt N}}) = 1 \leftrightarrow P \gcd (\frac{N}{P^{P pCnt N}}) = 1)$
39	33 38	mpbird	$⊢ φ \to P^{P pCnt N} \gcd (\frac{N}{P^{P pCnt N}}) = 1$
40	28 39	eqtrd	$⊢ φ \to (\frac{N}{P^{P pCnt N}}) \gcd P^{P pCnt N} = 1$

Metamath Proof Explorer

Theorem aks4d1p8d3

Proof