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

Metamath Proof Explorer

Theorem mumullem2

Description: Lemma for mumul . The product of two coprime squarefree numbers is squarefree. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion mumullem2 ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ( ∀ 𝑝 ∈ ℙ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) )
2 simpr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝑝 ∈ ℙ )
3 simpl1 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℕ )
4 2 3 pccld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℕ0 )
5 4 nn0red ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℝ )
6 simpl2 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℕ )
7 2 6 pccld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ∈ ℕ0 )
8 7 nn0red ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ∈ ℝ )
9 1red ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 1 ∈ ℝ )
10 le2add ⊢ ( ( ( ( 𝑝 pCnt 𝐴 ) ∈ ℝ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℝ ) ∧ ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ) )
11 5 8 9 9 10 syl22anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ) )
12 ax-1ne0 ⊢ 1 ≠ 0
13 simpl3 ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 gcd 𝐵 ) = 1 )
14 13 oveq2d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑝 pCnt 1 ) )
15 3 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐴 ∈ ℤ )
16 6 nnzd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 𝐵 ∈ ℤ )
17 pcgcd ⊢ ( ( 𝑝 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑝 pCnt ( 𝐴 gcd 𝐵 ) ) = if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) )
18 2 15 16 17 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 gcd 𝐵 ) ) = if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) )
19 pc1 ⊢ ( 𝑝 ∈ ℙ → ( 𝑝 pCnt 1 ) = 0 )
20 19 adantl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 1 ) = 0 )
21 14 18 20 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) = 0 )
22 ifid ⊢ if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , 1 , 1 ) = 1
23 ifeq12 ⊢ ( ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) → if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , 1 , 1 ) = if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) )
24 22 23 eqtr3id ⊢ ( ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) → 1 = if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) )
25 24 eqeq1d ⊢ ( ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) → ( 1 = 0 ↔ if ( ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) , ( 𝑝 pCnt 𝐴 ) , ( 𝑝 pCnt 𝐵 ) ) = 0 ) )
26 21 25 syl5ibrcom ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) → 1 = 0 ) )
27 26 necon3ad ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 1 ≠ 0 → ¬ ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) ) )
28 12 27 mpi ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ¬ ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) )
29 ax-1cn ⊢ 1 ∈ ℂ
30 5 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐴 ) ∈ ℂ )
31 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℂ ) → ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ↔ 1 = ( 𝑝 pCnt 𝐴 ) ) )
32 29 30 31 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ↔ 1 = ( 𝑝 pCnt 𝐴 ) ) )
33 8 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝐵 ) ∈ ℂ )
34 subeq0 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℂ ) → ( ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ↔ 1 = ( 𝑝 pCnt 𝐵 ) ) )
35 29 33 34 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ↔ 1 = ( 𝑝 pCnt 𝐵 ) ) )
36 32 35 anbi12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ↔ ( 1 = ( 𝑝 pCnt 𝐴 ) ∧ 1 = ( 𝑝 pCnt 𝐵 ) ) ) )
37 28 36 mtbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ¬ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) )
38 37 adantr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ¬ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) )
39 eqcom ⊢ ( ( 1 + 1 ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ↔ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) = ( 1 + 1 ) )
40 1re ⊢ 1 ∈ ℝ
41 40 40 readdcli ⊢ ( 1 + 1 ) ∈ ℝ
42 41 recni ⊢ ( 1 + 1 ) ∈ ℂ
43 4 7 nn0addcld ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℕ0 )
44 43 nn0red ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ )
45 44 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℂ )
46 subeq0 ⊢ ( ( ( 1 + 1 ) ∈ ℂ ∧ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℂ ) → ( ( ( 1 + 1 ) − ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( 1 + 1 ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) )
47 42 45 46 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 + 1 ) − ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( 1 + 1 ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) )
48 47 39 bitrdi ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 + 1 ) − ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) = ( 1 + 1 ) ) )
49 9 recnd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → 1 ∈ ℂ )
50 49 49 30 33 addsub4d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 1 + 1 ) − ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) = ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) )
51 50 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 1 + 1 ) − ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ) )
52 48 51 bitr3d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) = ( 1 + 1 ) ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ) )
53 52 adantr ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) = ( 1 + 1 ) ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ) )
54 subge0 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) )
55 40 5 54 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ↔ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) )
56 subge0 ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℝ ) → ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ↔ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) )
57 40 8 56 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ↔ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) )
58 55 57 anbi12d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) ↔ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) )
59 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt 𝐴 ) ∈ ℝ ) → ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ )
60 40 5 59 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ )
61 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( 𝑝 pCnt 𝐵 ) ∈ ℝ ) → ( 1 − ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ )
62 40 8 61 sylancr ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 1 − ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ )
63 add20 ⊢ ( ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ) ∧ ( ( 1 − ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
64 63 an4s ⊢ ( ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ ) ∧ ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
65 64 ex ⊢ ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∈ ℝ ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ ) → ( ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) ) )
66 60 62 65 syl2anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 0 ≤ ( 1 − ( 𝑝 pCnt 𝐴 ) ) ∧ 0 ≤ ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) ) )
67 58 66 sylbird ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) ) )
68 67 imp ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) + ( 1 − ( 𝑝 pCnt 𝐵 ) ) ) = 0 ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
69 53 68 bitrd ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) = ( 1 + 1 ) ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
70 39 69 bitrid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( ( 1 + 1 ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ↔ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
71 70 necon3abid ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ↔ ¬ ( ( 1 − ( 𝑝 pCnt 𝐴 ) ) = 0 ∧ ( 1 − ( 𝑝 pCnt 𝐵 ) ) = 0 ) ) )
72 38 71 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) ∧ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) → ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) )
73 72 ex ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) )
74 11 73 jcad ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ∧ ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) ) )
75 nnz ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℤ )
76 nnne0 ⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
77 75 76 jca ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) )
78 3 77 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) )
79 nnz ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℤ )
80 nnne0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ≠ 0 )
81 79 80 jca ⊢ ( 𝐵 ∈ ℕ → ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) )
82 6 81 syl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) )
83 pcmul ⊢ ( ( 𝑝 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) )
84 2 78 82 83 syl3anc ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) = ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) )
85 84 breq1d ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ↔ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ 1 ) )
86 1nn0 ⊢ 1 ∈ ℕ0
87 nn0leltp1 ⊢ ( ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℕ0 ∧ 1 ∈ ℕ0 ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ 1 ↔ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) < ( 1 + 1 ) ) )
88 43 86 87 sylancl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ 1 ↔ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) < ( 1 + 1 ) ) )
89 ltlen ⊢ ( ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ∈ ℝ ∧ ( 1 + 1 ) ∈ ℝ ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) < ( 1 + 1 ) ↔ ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ∧ ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) ) )
90 44 41 89 sylancl ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) < ( 1 + 1 ) ↔ ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ∧ ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) ) )
91 85 88 90 3bitrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ↔ ( ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ≤ ( 1 + 1 ) ∧ ( 1 + 1 ) ≠ ( ( 𝑝 pCnt 𝐴 ) + ( 𝑝 pCnt 𝐵 ) ) ) ) )
92 74 91 sylibrd ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ 𝑝 ∈ ℙ ) → ( ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ) )
93 92 ralimdva ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ∀ 𝑝 ∈ ℙ ( ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ) )
94 1 93 biimtrrid ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) → ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ) )
95 issqf ⊢ ( 𝐴 ∈ ℕ → ( ( μ ‘ 𝐴 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ) )
96 issqf ⊢ ( 𝐵 ∈ ℕ → ( ( μ ‘ 𝐵 ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) )
97 95 96 bi2anan9 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) )
98 97 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ↔ ( ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ 1 ∧ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐵 ) ≤ 1 ) ) )
99 nnmulcl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) ∈ ℕ )
100 99 3adant3 ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( 𝐴 · 𝐵 ) ∈ ℕ )
101 issqf ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℕ → ( ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ) )
102 100 101 syl ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt ( 𝐴 · 𝐵 ) ) ≤ 1 ) )
103 94 98 102 3imtr4d ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → ( ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 ) )
104 103 imp ⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝐴 gcd 𝐵 ) = 1 ) ∧ ( ( μ ‘ 𝐴 ) ≠ 0 ∧ ( μ ‘ 𝐵 ) ≠ 0 ) ) → ( μ ‘ ( 𝐴 · 𝐵 ) ) ≠ 0 )