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 ⊢ A ∈ ℕ ∧ B ∈ ℕ ∧ A gcd B = 1 ∧ μ ⁡ A ≠ 0 ∧ μ ⁡ B ≠ 0 → μ ⁡ A ⁢ B ≠ 0

Proof

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