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

Proof

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