This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝐴 ∥ ( 𝑃 ↑ 𝑁 ) → ∃ 𝑛 ∈ ℕ 𝐴 = ( 𝑃 ↑ 𝑛 ) ) )