Metamath Proof Explorer

Theorem isppw2

Description: Two ways to say that A is a prime power. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion isppw2 
|- ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )

Proof

Step Hyp Ref Expression
1 isppw 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E! q e. Prime q || A ) )
2 reu6 
 |-  ( E! q e. Prime q || A <-> E. p e. Prime A. q e. Prime ( q || A <-> q = p ) )
3 equid 
 |-  p = p
4 breq1 
 |-  ( q = p -> ( q || A <-> p || A ) )
5 equequ1 
 |-  ( q = p -> ( q = p <-> p = p ) )
6 4 5 bibi12d 
 |-  ( q = p -> ( ( q || A <-> q = p ) <-> ( p || A <-> p = p ) ) )
7 6 rspcva 
 |-  ( ( p e. Prime /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( p || A <-> p = p ) )
8 7 adantll 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( p || A <-> p = p ) )
9 3 8 mpbiri 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> p || A )
10 simplr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> p e. Prime )
11 simpll 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> A e. NN )
12 pcelnn 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( ( p pCnt A ) e. NN <-> p || A ) )
13 10 11 12 syl2anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( ( p pCnt A ) e. NN <-> p || A ) )
14 9 13 mpbird 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( p pCnt A ) e. NN )
15 simpr 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> q = p )
16 15 oveq1d 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( q pCnt A ) = ( p pCnt A ) )
17 simpllr 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> p e. Prime )
18 pccl 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( p pCnt A ) e. NN0 )
19 18 ancoms 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
20 19 ad2antrr 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( p pCnt A ) e. NN0 )
21 20 nn0zd 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( p pCnt A ) e. ZZ )
22 pcid 
 |-  ( ( p e. Prime /\ ( p pCnt A ) e. ZZ ) -> ( p pCnt ( p ^ ( p pCnt A ) ) ) = ( p pCnt A ) )
23 17 21 22 syl2anc 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( p pCnt ( p ^ ( p pCnt A ) ) ) = ( p pCnt A ) )
24 16 23 eqtr4d 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( q pCnt A ) = ( p pCnt ( p ^ ( p pCnt A ) ) ) )
25 15 oveq1d 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( q pCnt ( p ^ ( p pCnt A ) ) ) = ( p pCnt ( p ^ ( p pCnt A ) ) ) )
26 24 25 eqtr4d 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ q = p ) -> ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) )
27 simprr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> ( q || A <-> q = p ) )
28 27 notbid 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> ( -. q || A <-> -. q = p ) )
29 28 biimpar 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> -. q || A )
30 simplrl 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> q e. Prime )
31 simplll 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> A e. NN )
32 pceq0 
 |-  ( ( q e. Prime /\ A e. NN ) -> ( ( q pCnt A ) = 0 <-> -. q || A ) )
33 30 31 32 syl2anc 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( ( q pCnt A ) = 0 <-> -. q || A ) )
34 29 33 mpbird 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( q pCnt A ) = 0 )
35 simprl 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> q e. Prime )
36 simplr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> p e. Prime )
37 19 adantr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> ( p pCnt A ) e. NN0 )
38 prmdvdsexpr 
 |-  ( ( q e. Prime /\ p e. Prime /\ ( p pCnt A ) e. NN0 ) -> ( q || ( p ^ ( p pCnt A ) ) -> q = p ) )
39 35 36 37 38 syl3anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> ( q || ( p ^ ( p pCnt A ) ) -> q = p ) )
40 39 con3dimp 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> -. q || ( p ^ ( p pCnt A ) ) )
41 prmnn 
 |-  ( p e. Prime -> p e. NN )
42 41 adantl 
 |-  ( ( A e. NN /\ p e. Prime ) -> p e. NN )
43 42 19 nnexpcld 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( p ^ ( p pCnt A ) ) e. NN )
44 43 ad2antrr 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( p ^ ( p pCnt A ) ) e. NN )
45 pceq0 
 |-  ( ( q e. Prime /\ ( p ^ ( p pCnt A ) ) e. NN ) -> ( ( q pCnt ( p ^ ( p pCnt A ) ) ) = 0 <-> -. q || ( p ^ ( p pCnt A ) ) ) )
46 30 44 45 syl2anc 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( ( q pCnt ( p ^ ( p pCnt A ) ) ) = 0 <-> -. q || ( p ^ ( p pCnt A ) ) ) )
47 40 46 mpbird 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( q pCnt ( p ^ ( p pCnt A ) ) ) = 0 )
48 34 47 eqtr4d 
 |-  ( ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) /\ -. q = p ) -> ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) )
49 26 48 pm2.61dan 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ ( q e. Prime /\ ( q || A <-> q = p ) ) ) -> ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) )
50 49 expr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ q e. Prime ) -> ( ( q || A <-> q = p ) -> ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) ) )
51 50 ralimdva 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( A. q e. Prime ( q || A <-> q = p ) -> A. q e. Prime ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) ) )
52 51 imp 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> A. q e. Prime ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) )
53 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
54 53 ad2antrr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> A e. NN0 )
55 43 adantr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( p ^ ( p pCnt A ) ) e. NN )
56 55 nnnn0d 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( p ^ ( p pCnt A ) ) e. NN0 )
57 pc11 
 |-  ( ( A e. NN0 /\ ( p ^ ( p pCnt A ) ) e. NN0 ) -> ( A = ( p ^ ( p pCnt A ) ) <-> A. q e. Prime ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) ) )
58 54 56 57 syl2anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> ( A = ( p ^ ( p pCnt A ) ) <-> A. q e. Prime ( q pCnt A ) = ( q pCnt ( p ^ ( p pCnt A ) ) ) ) )
59 52 58 mpbird 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> A = ( p ^ ( p pCnt A ) ) )
60 oveq2 
 |-  ( k = ( p pCnt A ) -> ( p ^ k ) = ( p ^ ( p pCnt A ) ) )
61 60 rspceeqv 
 |-  ( ( ( p pCnt A ) e. NN /\ A = ( p ^ ( p pCnt A ) ) ) -> E. k e. NN A = ( p ^ k ) )
62 14 59 61 syl2anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ A. q e. Prime ( q || A <-> q = p ) ) -> E. k e. NN A = ( p ^ k ) )
63 62 ex 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( A. q e. Prime ( q || A <-> q = p ) -> E. k e. NN A = ( p ^ k ) ) )
64 prmdvdsexpb 
 |-  ( ( q e. Prime /\ p e. Prime /\ k e. NN ) -> ( q || ( p ^ k ) <-> q = p ) )
65 64 3coml 
 |-  ( ( p e. Prime /\ k e. NN /\ q e. Prime ) -> ( q || ( p ^ k ) <-> q = p ) )
66 65 3expa 
 |-  ( ( ( p e. Prime /\ k e. NN ) /\ q e. Prime ) -> ( q || ( p ^ k ) <-> q = p ) )
67 66 ralrimiva 
 |-  ( ( p e. Prime /\ k e. NN ) -> A. q e. Prime ( q || ( p ^ k ) <-> q = p ) )
68 67 adantll 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> A. q e. Prime ( q || ( p ^ k ) <-> q = p ) )
69 breq2 
 |-  ( A = ( p ^ k ) -> ( q || A <-> q || ( p ^ k ) ) )
70 69 bibi1d 
 |-  ( A = ( p ^ k ) -> ( ( q || A <-> q = p ) <-> ( q || ( p ^ k ) <-> q = p ) ) )
71 70 ralbidv 
 |-  ( A = ( p ^ k ) -> ( A. q e. Prime ( q || A <-> q = p ) <-> A. q e. Prime ( q || ( p ^ k ) <-> q = p ) ) )
72 68 71 syl5ibrcom 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( A = ( p ^ k ) -> A. q e. Prime ( q || A <-> q = p ) ) )
73 72 rexlimdva 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( E. k e. NN A = ( p ^ k ) -> A. q e. Prime ( q || A <-> q = p ) ) )
74 63 73 impbid 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( A. q e. Prime ( q || A <-> q = p ) <-> E. k e. NN A = ( p ^ k ) ) )
75 74 rexbidva 
 |-  ( A e. NN -> ( E. p e. Prime A. q e. Prime ( q || A <-> q = p ) <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )
76 2 75 syl5bb 
 |-  ( A e. NN -> ( E! q e. Prime q || A <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )
77 1 76 bitrd 
 |-  ( A e. NN -> ( ( Lam ` A ) =/= 0 <-> E. p e. Prime E. k e. NN A = ( p ^ k ) ) )