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

Metamath Proof Explorer

Theorem sqf11

Description: A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015)

Ref Expression
Assertion sqf11 
|- ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> ( A = B <-> A. p e. Prime ( p || A <-> p || B ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 
 |-  ( A e. NN -> A e. NN0 )
2 nnnn0 
 |-  ( B e. NN -> B e. NN0 )
3 pc11 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )
5 4 ad2ant2r 
 |-  ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> ( A = B <-> A. p e. Prime ( p pCnt A ) = ( p pCnt B ) ) )
6 eleq1 
 |-  ( ( p pCnt A ) = ( p pCnt B ) -> ( ( p pCnt A ) e. NN <-> ( p pCnt B ) e. NN ) )
7 dfbi3 
 |-  ( ( ( p pCnt A ) e. NN <-> ( p pCnt B ) e. NN ) <-> ( ( ( p pCnt A ) e. NN /\ ( p pCnt B ) e. NN ) \/ ( -. ( p pCnt A ) e. NN /\ -. ( p pCnt B ) e. NN ) ) )
8 sqfpc 
 |-  ( ( A e. NN /\ ( mmu ` A ) =/= 0 /\ p e. Prime ) -> ( p pCnt A ) <_ 1 )
9 8 ad4ant124 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p pCnt A ) <_ 1 )
10 nnle1eq1 
 |-  ( ( p pCnt A ) e. NN -> ( ( p pCnt A ) <_ 1 <-> ( p pCnt A ) = 1 ) )
11 9 10 syl5ibcom 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt A ) e. NN -> ( p pCnt A ) = 1 ) )
12 simprl 
 |-  ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> B e. NN )
13 12 adantr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> B e. NN )
14 simplrr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( mmu ` B ) =/= 0 )
15 simpr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> p e. Prime )
16 sqfpc 
 |-  ( ( B e. NN /\ ( mmu ` B ) =/= 0 /\ p e. Prime ) -> ( p pCnt B ) <_ 1 )
17 13 14 15 16 syl3anc 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p pCnt B ) <_ 1 )
18 nnle1eq1 
 |-  ( ( p pCnt B ) e. NN -> ( ( p pCnt B ) <_ 1 <-> ( p pCnt B ) = 1 ) )
19 17 18 syl5ibcom 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt B ) e. NN -> ( p pCnt B ) = 1 ) )
20 11 19 anim12d 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( ( p pCnt A ) e. NN /\ ( p pCnt B ) e. NN ) -> ( ( p pCnt A ) = 1 /\ ( p pCnt B ) = 1 ) ) )
21 eqtr3 
 |-  ( ( ( p pCnt A ) = 1 /\ ( p pCnt B ) = 1 ) -> ( p pCnt A ) = ( p pCnt B ) )
22 20 21 syl6 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( ( p pCnt A ) e. NN /\ ( p pCnt B ) e. NN ) -> ( p pCnt A ) = ( p pCnt B ) ) )
23 id 
 |-  ( p e. Prime -> p e. Prime )
24 simpll 
 |-  ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> A e. NN )
25 pccl 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( p pCnt A ) e. NN0 )
26 23 24 25 syl2anr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
27 elnn0 
 |-  ( ( p pCnt A ) e. NN0 <-> ( ( p pCnt A ) e. NN \/ ( p pCnt A ) = 0 ) )
28 26 27 sylib 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt A ) e. NN \/ ( p pCnt A ) = 0 ) )
29 28 ord 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( -. ( p pCnt A ) e. NN -> ( p pCnt A ) = 0 ) )
30 pccl 
 |-  ( ( p e. Prime /\ B e. NN ) -> ( p pCnt B ) e. NN0 )
31 23 12 30 syl2anr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( p pCnt B ) e. NN0 )
32 elnn0 
 |-  ( ( p pCnt B ) e. NN0 <-> ( ( p pCnt B ) e. NN \/ ( p pCnt B ) = 0 ) )
33 31 32 sylib 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt B ) e. NN \/ ( p pCnt B ) = 0 ) )
34 33 ord 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( -. ( p pCnt B ) e. NN -> ( p pCnt B ) = 0 ) )
35 29 34 anim12d 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( -. ( p pCnt A ) e. NN /\ -. ( p pCnt B ) e. NN ) -> ( ( p pCnt A ) = 0 /\ ( p pCnt B ) = 0 ) ) )
36 eqtr3 
 |-  ( ( ( p pCnt A ) = 0 /\ ( p pCnt B ) = 0 ) -> ( p pCnt A ) = ( p pCnt B ) )
37 35 36 syl6 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( -. ( p pCnt A ) e. NN /\ -. ( p pCnt B ) e. NN ) -> ( p pCnt A ) = ( p pCnt B ) ) )
38 22 37 jaod 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( ( ( p pCnt A ) e. NN /\ ( p pCnt B ) e. NN ) \/ ( -. ( p pCnt A ) e. NN /\ -. ( p pCnt B ) e. NN ) ) -> ( p pCnt A ) = ( p pCnt B ) ) )
39 7 38 biimtrid 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( ( p pCnt A ) e. NN <-> ( p pCnt B ) e. NN ) -> ( p pCnt A ) = ( p pCnt B ) ) )
40 6 39 impbid2 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt A ) = ( p pCnt B ) <-> ( ( p pCnt A ) e. NN <-> ( p pCnt B ) e. NN ) ) )
41 pcelnn 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( ( p pCnt A ) e. NN <-> p || A ) )
42 23 24 41 syl2anr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt A ) e. NN <-> p || A ) )
43 pcelnn 
 |-  ( ( p e. Prime /\ B e. NN ) -> ( ( p pCnt B ) e. NN <-> p || B ) )
44 23 12 43 syl2anr 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt B ) e. NN <-> p || B ) )
45 42 44 bibi12d 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( ( p pCnt A ) e. NN <-> ( p pCnt B ) e. NN ) <-> ( p || A <-> p || B ) ) )
46 40 45 bitrd 
 |-  ( ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) /\ p e. Prime ) -> ( ( p pCnt A ) = ( p pCnt B ) <-> ( p || A <-> p || B ) ) )
47 46 ralbidva 
 |-  ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> ( A. p e. Prime ( p pCnt A ) = ( p pCnt B ) <-> A. p e. Prime ( p || A <-> p || B ) ) )
48 5 47 bitrd 
 |-  ( ( ( A e. NN /\ ( mmu ` A ) =/= 0 ) /\ ( B e. NN /\ ( mmu ` B ) =/= 0 ) ) -> ( A = B <-> A. p e. Prime ( p || A <-> p || B ) ) )