Metamath Proof Explorer

Theorem pc11

Description: The prime count function, viewed as a function from NN to ( NN ^m Prime ) , is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pc11 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( A = B -> ( p pCnt A ) = ( p pCnt B ) )
2 1 ralrimivw 
 |-  ( A = B -> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) )
3 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
4 nn0z 
 |-  ( B e. NN0 -> B e. ZZ )
5 zq 
 |-  ( A e. ZZ -> A e. QQ )
6 pcxcl 
 |-  ( ( p e. Prime /\ A e. QQ ) -> ( p pCnt A ) e. RR* )
7 5 6 sylan2 
 |-  ( ( p e. Prime /\ A e. ZZ ) -> ( p pCnt A ) e. RR* )
8 zq 
 |-  ( B e. ZZ -> B e. QQ )
9 pcxcl 
 |-  ( ( p e. Prime /\ B e. QQ ) -> ( p pCnt B ) e. RR* )
10 8 9 sylan2 
 |-  ( ( p e. Prime /\ B e. ZZ ) -> ( p pCnt B ) e. RR* )
11 7 10 anim12dan 
 |-  ( ( p e. Prime /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( p pCnt A ) e. RR* /\ ( p pCnt B ) e. RR* ) )
12 xrletri3 
 |-  ( ( ( p pCnt A ) e. RR* /\ ( p pCnt B ) e. RR* ) -> ( ( p pCnt A ) = ( p pCnt B ) <-> ( ( p pCnt A ) <_ ( p pCnt B ) /\ ( p pCnt B ) <_ ( p pCnt A ) ) ) )
13 11 12 syl 
 |-  ( ( p e. Prime /\ ( A e. ZZ /\ B e. ZZ ) ) -> ( ( p pCnt A ) = ( p pCnt B ) <-> ( ( p pCnt A ) <_ ( p pCnt B ) /\ ( p pCnt B ) <_ ( p pCnt A ) ) ) )
14 13 ancoms 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ p e. Prime ) -> ( ( p pCnt A ) = ( p pCnt B ) <-> ( ( p pCnt A ) <_ ( p pCnt B ) /\ ( p pCnt B ) <_ ( p pCnt A ) ) ) )
15 14 ralbidva 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) <-> A. p e. Prime ( ( p pCnt A ) <_ ( p pCnt B ) /\ ( p pCnt B ) <_ ( p pCnt A ) ) ) )
16 r19.26 
 |-  ( A. p e. Prime ( ( p pCnt A ) <_ ( p pCnt B ) /\ ( p pCnt B ) <_ ( p pCnt A ) ) <-> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) /\ A. p e. Prime ( p pCnt B ) <_ ( p pCnt A ) ) )
17 15 16 bitrdi 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) <-> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) /\ A. p e. Prime ( p pCnt B ) <_ ( p pCnt A ) ) ) )
18 pc2dvds 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A || B <-> A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) ) )
19 pc2dvds 
 |-  ( ( B e. ZZ /\ A e. ZZ ) -> ( B || A <-> A. p e. Prime ( p pCnt B ) <_ ( p pCnt A ) ) )
20 19 ancoms 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( B || A <-> A. p e. Prime ( p pCnt B ) <_ ( p pCnt A ) ) )
21 18 20 anbi12d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A || B /\ B || A ) <-> ( A. p e. Prime ( p pCnt A ) <_ ( p pCnt B ) /\ A. p e. Prime ( p pCnt B ) <_ ( p pCnt A ) ) ) )
22 17 21 bitr4d 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) <-> ( A || B /\ B || A ) ) )
23 3 4 22 syl2an 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) <-> ( A || B /\ B || A ) ) )
24 dvdseq 
 |-  ( ( ( A e. NN0 /\ B e. NN0 ) /\ ( A || B /\ B || A ) ) -> A = B )
25 24 ex 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A || B /\ B || A ) -> A = B ) )
26 23 25 sylbid 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) -> A = B ) )
27 2 26 impbid2 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )