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μA0BμB0A=BppApB

Proof

Step Hyp Ref Expression
1 nnnn0 AA0
2 nnnn0 BB0
3 pc11 A0B0A=BpppCntA=ppCntB
4 1 2 3 syl2an ABA=BpppCntA=ppCntB
5 4 ad2ant2r AμA0BμB0A=BpppCntA=ppCntB
6 eleq1 ppCntA=ppCntBppCntAppCntB
7 dfbi3 ppCntAppCntBppCntAppCntB¬ppCntA¬ppCntB
8 sqfpc AμA0pppCntA1
9 8 ad4ant124 AμA0BμB0pppCntA1
10 nnle1eq1 ppCntAppCntA1ppCntA=1
11 9 10 syl5ibcom AμA0BμB0pppCntAppCntA=1
12 simprl AμA0BμB0B
13 12 adantr AμA0BμB0pB
14 simplrr AμA0BμB0pμB0
15 simpr AμA0BμB0pp
16 sqfpc BμB0pppCntB1
17 13 14 15 16 syl3anc AμA0BμB0pppCntB1
18 nnle1eq1 ppCntBppCntB1ppCntB=1
19 17 18 syl5ibcom AμA0BμB0pppCntBppCntB=1
20 11 19 anim12d AμA0BμB0pppCntAppCntBppCntA=1ppCntB=1
21 eqtr3 ppCntA=1ppCntB=1ppCntA=ppCntB
22 20 21 syl6 AμA0BμB0pppCntAppCntBppCntA=ppCntB
23 id pp
24 simpll AμA0BμB0A
25 pccl pAppCntA0
26 23 24 25 syl2anr AμA0BμB0pppCntA0
27 elnn0 ppCntA0ppCntAppCntA=0
28 26 27 sylib AμA0BμB0pppCntAppCntA=0
29 28 ord AμA0BμB0p¬ppCntAppCntA=0
30 pccl pBppCntB0
31 23 12 30 syl2anr AμA0BμB0pppCntB0
32 elnn0 ppCntB0ppCntBppCntB=0
33 31 32 sylib AμA0BμB0pppCntBppCntB=0
34 33 ord AμA0BμB0p¬ppCntBppCntB=0
35 29 34 anim12d AμA0BμB0p¬ppCntA¬ppCntBppCntA=0ppCntB=0
36 eqtr3 ppCntA=0ppCntB=0ppCntA=ppCntB
37 35 36 syl6 AμA0BμB0p¬ppCntA¬ppCntBppCntA=ppCntB
38 22 37 jaod AμA0BμB0pppCntAppCntB¬ppCntA¬ppCntBppCntA=ppCntB
39 7 38 syl5bi AμA0BμB0pppCntAppCntBppCntA=ppCntB
40 6 39 impbid2 AμA0BμB0pppCntA=ppCntBppCntAppCntB
41 pcelnn pAppCntApA
42 23 24 41 syl2anr AμA0BμB0pppCntApA
43 pcelnn pBppCntBpB
44 23 12 43 syl2anr AμA0BμB0pppCntBpB
45 42 44 bibi12d AμA0BμB0pppCntAppCntBpApB
46 40 45 bitrd AμA0BμB0pppCntA=ppCntBpApB
47 46 ralbidva AμA0BμB0pppCntA=ppCntBppApB
48 5 47 bitrd AμA0BμB0A=BppApB