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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnnn0 | |
|
2 | nnnn0 | |
|
3 | pc11 | |
|
4 | 1 2 3 | syl2an | |
5 | 4 | ad2ant2r | |
6 | eleq1 | |
|
7 | dfbi3 | |
|
8 | sqfpc | |
|
9 | 8 | ad4ant124 | |
10 | nnle1eq1 | |
|
11 | 9 10 | syl5ibcom | |
12 | simprl | |
|
13 | 12 | adantr | |
14 | simplrr | |
|
15 | simpr | |
|
16 | sqfpc | |
|
17 | 13 14 15 16 | syl3anc | |
18 | nnle1eq1 | |
|
19 | 17 18 | syl5ibcom | |
20 | 11 19 | anim12d | |
21 | eqtr3 | |
|
22 | 20 21 | syl6 | |
23 | id | |
|
24 | simpll | |
|
25 | pccl | |
|
26 | 23 24 25 | syl2anr | |
27 | elnn0 | |
|
28 | 26 27 | sylib | |
29 | 28 | ord | |
30 | pccl | |
|
31 | 23 12 30 | syl2anr | |
32 | elnn0 | |
|
33 | 31 32 | sylib | |
34 | 33 | ord | |
35 | 29 34 | anim12d | |
36 | eqtr3 | |
|
37 | 35 36 | syl6 | |
38 | 22 37 | jaod | |
39 | 7 38 | syl5bi | |
40 | 6 39 | impbid2 | |
41 | pcelnn | |
|
42 | 23 24 41 | syl2anr | |
43 | pcelnn | |
|
44 | 23 12 43 | syl2anr | |
45 | 42 44 | bibi12d | |
46 | 40 45 | bitrd | |
47 | 46 | ralbidva | |
48 | 5 47 | bitrd | |