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 ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 nnnn0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℕ0 )
2 nnnn0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
3 pc11 ⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
5 4 ad2ant2r ⊢ ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
6 eleq1 ⊢ ( ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) )
7 dfbi3 ⊢ ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ↔ ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ∨ ( ¬ ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ¬ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ) )
8 sqfpc ⊢ ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ≤ 1 )
9 8 ad4ant124 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ≤ 1 )
10 nnle1eq1 ⊢ ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ → ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ↔ ( 𝑝 pCnt 𝐴 ) = 1 ) )
11 9 10 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ → ( 𝑝 pCnt 𝐴 ) = 1 ) )
12 simprl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → 𝐵 ∈ ℕ )
13 12 adantr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℕ )
14 simplrr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( μ ‘ 𝐵 ) ≠ 0 )
15 simpr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
16 sqfpc ⊢ ( ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ≤ 1 )
17 13 14 15 16 syl3anc ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ≤ 1 )
18 nnle1eq1 ⊢ ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ → ( ( 𝑝 pCnt 𝐵 ) ≤ 1 ↔ ( 𝑝 pCnt 𝐵 ) = 1 ) )
19 17 18 syl5ibcom ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ → ( 𝑝 pCnt 𝐵 ) = 1 ) )
20 11 19 anim12d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) → ( ( 𝑝 pCnt 𝐴 ) = 1 ∧ ( 𝑝 pCnt 𝐵 ) = 1 ) ) )
21 eqtr3 ⊢ ( ( ( 𝑝 pCnt 𝐴 ) = 1 ∧ ( 𝑝 pCnt 𝐵 ) = 1 ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) )
22 20 21 syl6 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
23 id ⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℙ )
24 simpll ⊢ ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → 𝐴 ∈ ℕ )
25 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
26 23 24 25 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
27 elnn0 ⊢ ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 ↔ ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝐴 ) = 0 ) )
28 26 27 sylib ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝐴 ) = 0 ) )
29 28 ord ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ¬ ( 𝑝 pCnt 𝐴 ) ∈ ℕ → ( 𝑝 pCnt 𝐴 ) = 0 ) )
30 pccl ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( 𝑝 pCnt 𝐵 ) ∈ ℕ0 )
31 23 12 30 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ∈ ℕ0 )
32 elnn0 ⊢ ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ0 ↔ ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝐵 ) = 0 ) )
33 31 32 sylib ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ ∨ ( 𝑝 pCnt 𝐵 ) = 0 ) )
34 33 ord ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ¬ ( 𝑝 pCnt 𝐵 ) ∈ ℕ → ( 𝑝 pCnt 𝐵 ) = 0 ) )
35 29 34 anim12d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ¬ ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ¬ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) → ( ( 𝑝 pCnt 𝐴 ) = 0 ∧ ( 𝑝 pCnt 𝐵 ) = 0 ) ) )
36 eqtr3 ⊢ ( ( ( 𝑝 pCnt 𝐴 ) = 0 ∧ ( 𝑝 pCnt 𝐵 ) = 0 ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) )
37 35 36 syl6 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ¬ ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ¬ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
38 22 37 jaod ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ∨ ( ¬ ( 𝑝 pCnt 𝐴 ) ∈ ℕ ∧ ¬ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
39 7 38 syl5bi ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) → ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ) )
40 6 39 impbid2 ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ↔ ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ) )
41 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℕ ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ 𝑝 ∥ 𝐴 ) )
42 23 24 41 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ 𝑝 ∥ 𝐴 ) )
43 pcelnn ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ ↔ 𝑝 ∥ 𝐵 ) )
44 23 12 43 syl2anr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐵 ) ∈ ℕ ↔ 𝑝 ∥ 𝐵 ) )
45 42 44 bibi12d ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℕ ↔ ( 𝑝 pCnt 𝐵 ) ∈ ℕ ) ↔ ( 𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵 ) ) )
46 40 45 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ↔ ( 𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵 ) ) )
47 46 ralbidva ⊢ ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) = ( 𝑝 pCnt 𝐵 ) ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵 ) ) )
48 5 47 bitrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ ( μ ‘ 𝐴 ) ≠ 0 ) ∧ ( 𝐵 ∈ ℕ ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( 𝐴 = 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 ∥ 𝐴 ↔ 𝑝 ∥ 𝐵 ) ) )