Theorem 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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eluz2nn	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → 𝐴 ∈ ℕ )
2		dvdsprmpweq	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
3	1 2	syl3an2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
4	3	imp	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) )
5		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
6	5	rexeqi	⊢ ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ ∃ 𝑛 ∈ ( ℕ ∪ { 0 } ) 𝐴 = ( 𝑃 ↑ 𝑛 ) )
7		rexun	⊢ ( ∃ 𝑛 ∈ ( ℕ ∪ { 0 } ) 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ ( ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ∨ ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
8	6 7	bitri	⊢ ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ ( ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ∨ ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
9		0z	⊢ 0 ∈ ℤ
10		oveq2	⊢ ( 𝑛 = 0 → ( 𝑃 ↑ 𝑛 ) = ( 𝑃 ↑ 0 ) )
11	10	eqeq2d	⊢ ( 𝑛 = 0 → ( 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ 0 ) ) )
12	11	rexsng	⊢ ( 0 ∈ ℤ → ( ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ 0 ) ) )
13	9 12	ax-mp	⊢ ( ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) ↔ 𝐴 = ( 𝑃 ↑ 0 ) )
14		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
15	14	nncnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
16	15	exp0d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 0 ) = 1 )
17	16	3ad2ant1	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝑃 ↑ 0 ) = 1 )
18	17	eqeq2d	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 = ( 𝑃 ↑ 0 ) ↔ 𝐴 = 1 ) )
19		eluz2b3	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝐴 ∈ ℕ ∧ 𝐴 ≠ 1 ) )
20		eqneqall	⊢ ( 𝐴 = 1 → ( 𝐴 ≠ 1 → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
21	20	com12	⊢ ( 𝐴 ≠ 1 → ( 𝐴 = 1 → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
22	19 21	simplbiim	⊢ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐴 = 1 → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
23	22	3ad2ant2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 = 1 → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
24	18 23	sylbid	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 = ( 𝑃 ↑ 0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
25	24	com12	⊢ ( 𝐴 = ( 𝑃 ↑ 0 ) → ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) ) )
26	25	impd	⊢ ( 𝐴 = ( 𝑃 ↑ 0 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
27	13 26	sylbi	⊢ ( ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
28	27	jao1i	⊢ ( ( ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ∨ ∃ 𝑛 ∈ { 0 } 𝐴 = ( 𝑃 ↑ 𝑛 ) ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
29	8 28	sylbi	⊢ ( ∃ 𝑛 ∈ ℕ0 𝐴 = ( 𝑃 ↑ 𝑛 ) → ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )
30	4 29	mpcom	⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) )
31	30	ex	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )