dvdsprmpweqnn

Description: If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021)

		Ref	Expression
	Assertion	dvdsprmpweqnn	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n})$

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	$⊢ A \in ℤ_{\geq 2} \to A \in ℕ$
2		dvdsprmpweq	$⊢ (P \in ℙ \land A \in ℕ \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ_{0} A = P^{n})$
3	1 2	syl3an2	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ_{0} A = P^{n})$
4	3	imp	$⊢ ((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ_{0} A = P^{n}$
5		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
6	5	rexeqi	$⊢ \exists n \in ℕ_{0} A = P^{n} \leftrightarrow \exists n \in (ℕ \cup \{0\}) A = P^{n}$
7		rexun	$⊢ \exists n \in (ℕ \cup \{0\}) A = P^{n} \leftrightarrow (\exists n \in ℕ A = P^{n} \lor \exists n \in \{0\} A = P^{n})$
8	6 7	bitri	$⊢ \exists n \in ℕ_{0} A = P^{n} \leftrightarrow (\exists n \in ℕ A = P^{n} \lor \exists n \in \{0\} A = P^{n})$
9		0z	$⊢ 0 \in ℤ$
10		oveq2	$⊢ n = 0 \to P^{n} = P^{0}$
11	10	eqeq2d	$⊢ n = 0 \to (A = P^{n} \leftrightarrow A = P^{0})$
12	11	rexsng	$⊢ 0 \in ℤ \to (\exists n \in \{0\} A = P^{n} \leftrightarrow A = P^{0})$
13	9 12	ax-mp	$⊢ \exists n \in \{0\} A = P^{n} \leftrightarrow A = P^{0}$
14		prmnn	$⊢ P \in ℙ \to P \in ℕ$
15	14	nncnd	$⊢ P \in ℙ \to P \in ℂ$
16	15	exp0d	$⊢ P \in ℙ \to P^{0} = 1$
17	16	3ad2ant1	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to P^{0} = 1$
18	17	eqeq2d	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A = P^{0} \leftrightarrow A = 1)$
19		eluz2b3	$⊢ A \in ℤ_{\geq 2} \leftrightarrow (A \in ℕ \land A \neq 1)$
20		eqneqall	$⊢ A = 1 \to (A \neq 1 \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
21	20	com12	$⊢ A \neq 1 \to (A = 1 \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
22	19 21	simplbiim	$⊢ A \in ℤ_{\geq 2} \to (A = 1 \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
23	22	3ad2ant2	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A = 1 \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
24	18 23	sylbid	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A = P^{0} \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
25	24	com12	$⊢ A = P^{0} \to ((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n}))$
26	25	impd	$⊢ A = P^{0} \to (((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ A = P^{n})$
27	13 26	sylbi	$⊢ \exists n \in \{0\} A = P^{n} \to (((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ A = P^{n})$
28	27	jao1i	$⊢ (\exists n \in ℕ A = P^{n} \lor \exists n \in \{0\} A = P^{n}) \to (((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ A = P^{n})$
29	8 28	sylbi	$⊢ \exists n \in ℕ_{0} A = P^{n} \to (((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ A = P^{n})$
30	4 29	mpcom	$⊢ ((P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \land A ∥ P^{N}) \to \exists n \in ℕ A = P^{n}$
31	30	ex	$⊢ (P \in ℙ \land A \in ℤ_{\geq 2} \land N \in ℕ_{0}) \to (A ∥ P^{N} \to \exists n \in ℕ A = P^{n})$

Metamath Proof Explorer

Theorem dvdsprmpweqnn

Proof