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 
|- ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( A e. ( ZZ>= ` 2 ) -> A e. NN )
2 dvdsprmpweq 
 |-  ( ( P e. Prime /\ A e. NN /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )
3 1 2 syl3an2 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN0 A = ( P ^ n ) ) )
4 3 imp 
 |-  ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN0 A = ( P ^ n ) )
5 df-n0 
 |-  NN0 = ( NN u. { 0 } )
6 5 rexeqi 
 |-  ( E. n e. NN0 A = ( P ^ n ) <-> E. n e. ( NN u. { 0 } ) A = ( P ^ n ) )
7 rexun 
 |-  ( E. n e. ( NN u. { 0 } ) A = ( P ^ n ) <-> ( E. n e. NN A = ( P ^ n ) \/ E. n e. { 0 } A = ( P ^ n ) ) )
8 6 7 bitri 
 |-  ( E. n e. NN0 A = ( P ^ n ) <-> ( E. n e. NN A = ( P ^ n ) \/ E. n e. { 0 } A = ( P ^ n ) ) )
9 0z 
 |-  0 e. ZZ
10 oveq2 
 |-  ( n = 0 -> ( P ^ n ) = ( P ^ 0 ) )
11 10 eqeq2d 
 |-  ( n = 0 -> ( A = ( P ^ n ) <-> A = ( P ^ 0 ) ) )
12 11 rexsng 
 |-  ( 0 e. ZZ -> ( E. n e. { 0 } A = ( P ^ n ) <-> A = ( P ^ 0 ) ) )
13 9 12 ax-mp 
 |-  ( E. n e. { 0 } A = ( P ^ n ) <-> A = ( P ^ 0 ) )
14 prmnn 
 |-  ( P e. Prime -> P e. NN )
15 14 nncnd 
 |-  ( P e. Prime -> P e. CC )
16 15 exp0d 
 |-  ( P e. Prime -> ( P ^ 0 ) = 1 )
17 16 3ad2ant1 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( P ^ 0 ) = 1 )
18 17 eqeq2d 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A = ( P ^ 0 ) <-> A = 1 ) )
19 eluz2b3 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( A e. NN /\ A =/= 1 ) )
20 eqneqall 
 |-  ( A = 1 -> ( A =/= 1 -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
21 20 com12 
 |-  ( A =/= 1 -> ( A = 1 -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
22 19 21 simplbiim 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( A = 1 -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
23 22 3ad2ant2 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A = 1 -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
24 18 23 sylbid 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A = ( P ^ 0 ) -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
25 24 com12 
 |-  ( A = ( P ^ 0 ) -> ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) ) )
26 25 impd 
 |-  ( A = ( P ^ 0 ) -> ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN A = ( P ^ n ) ) )
27 13 26 sylbi 
 |-  ( E. n e. { 0 } A = ( P ^ n ) -> ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN A = ( P ^ n ) ) )
28 27 jao1i 
 |-  ( ( E. n e. NN A = ( P ^ n ) \/ E. n e. { 0 } A = ( P ^ n ) ) -> ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN A = ( P ^ n ) ) )
29 8 28 sylbi 
 |-  ( E. n e. NN0 A = ( P ^ n ) -> ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN A = ( P ^ n ) ) )
30 4 29 mpcom 
 |-  ( ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) /\ A || ( P ^ N ) ) -> E. n e. NN A = ( P ^ n ) )
31 30 ex 
 |-  ( ( P e. Prime /\ A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A || ( P ^ N ) -> E. n e. NN A = ( P ^ n ) ) )