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 syl5bi
 |-  ( ( ( ( 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 ) ) )