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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) =/= 0 )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. p e. Prime ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) <-> ( A. p e. Prime ( p pCnt A ) <_ 1 /\ A. p e. Prime ( p pCnt B ) <_ 1 ) )
2 simpr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> p e. Prime )
3 simpl1 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. NN )
4 2 3 pccld 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
5 4 nn0red 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt A ) e. RR )
6 simpl2 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. NN )
7 2 6 pccld 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt B ) e. NN0 )
8 7 nn0red 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt B ) e. RR )
9 1red 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> 1 e. RR )
10 le2add 
 |-  ( ( ( ( p pCnt A ) e. RR /\ ( p pCnt B ) e. RR ) /\ ( 1 e. RR /\ 1 e. RR ) ) -> ( ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) -> ( ( p pCnt A ) + ( p pCnt B ) ) <_ ( 1 + 1 ) ) )
11 5 8 9 9 10 syl22anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) -> ( ( p pCnt A ) + ( p pCnt B ) ) <_ ( 1 + 1 ) ) )
12 ax-1ne0 
 |-  1 =/= 0
13 simpl3 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( A gcd B ) = 1 )
14 13 oveq2d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt ( A gcd B ) ) = ( p pCnt 1 ) )
15 3 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> A e. ZZ )
16 6 nnzd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> B e. ZZ )
17 pcgcd 
 |-  ( ( p e. Prime /\ A e. ZZ /\ B e. ZZ ) -> ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt ( A gcd B ) ) = if ( ( p pCnt A ) <_ ( p pCnt B ) , ( p pCnt A ) , ( p pCnt B ) ) )
19 pc1 
 |-  ( p e. Prime -> ( p pCnt 1 ) = 0 )
20 19 adantl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt 1 ) = 0 )
21 14 18 20 3eqtr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 1 = ( p pCnt A ) /\ 1 = ( p pCnt B ) ) -> 1 = 0 ) )
27 26 necon3ad 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( 1 =/= 0 -> -. ( 1 = ( p pCnt A ) /\ 1 = ( p pCnt B ) ) ) )
28 12 27 mpi 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> -. ( 1 = ( p pCnt A ) /\ 1 = ( p pCnt B ) ) )
29 ax-1cn 
 |-  1 e. CC
30 5 recnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt A ) e. CC )
31 subeq0 
 |-  ( ( 1 e. CC /\ ( p pCnt A ) e. CC ) -> ( ( 1 - ( p pCnt A ) ) = 0 <-> 1 = ( p pCnt A ) ) )
32 29 30 31 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 1 - ( p pCnt A ) ) = 0 <-> 1 = ( p pCnt A ) ) )
33 8 recnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt B ) e. CC )
34 subeq0 
 |-  ( ( 1 e. CC /\ ( p pCnt B ) e. CC ) -> ( ( 1 - ( p pCnt B ) ) = 0 <-> 1 = ( p pCnt B ) ) )
35 29 33 34 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 1 - ( p pCnt B ) ) = 0 <-> 1 = ( p pCnt B ) ) )
36 32 35 anbi12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 1 - ( p pCnt A ) ) = 0 /\ ( 1 - ( p pCnt B ) ) = 0 ) <-> ( 1 = ( p pCnt A ) /\ 1 = ( p pCnt B ) ) ) )
37 28 36 mtbird 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> -. ( ( 1 - ( p pCnt A ) ) = 0 /\ ( 1 - ( p pCnt B ) ) = 0 ) )
38 37 adantr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 e. RR
41 40 40 readdcli 
 |-  ( 1 + 1 ) e. RR
42 41 recni 
 |-  ( 1 + 1 ) e. CC
43 4 7 nn0addcld 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( p pCnt A ) + ( p pCnt B ) ) e. NN0 )
44 43 nn0red 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( p pCnt A ) + ( p pCnt B ) ) e. RR )
45 44 recnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( p pCnt A ) + ( p pCnt B ) ) e. CC )
46 subeq0 
 |-  ( ( ( 1 + 1 ) e. CC /\ ( ( p pCnt A ) + ( p pCnt B ) ) e. CC ) -> ( ( ( 1 + 1 ) - ( ( p pCnt A ) + ( p pCnt B ) ) ) = 0 <-> ( 1 + 1 ) = ( ( p pCnt A ) + ( p pCnt B ) ) ) )
47 42 45 46 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 1 + 1 ) - ( ( p pCnt A ) + ( p pCnt B ) ) ) = 0 <-> ( 1 + 1 ) = ( ( p pCnt A ) + ( p pCnt B ) ) ) )
48 47 39 bitrdi 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 1 + 1 ) - ( ( p pCnt A ) + ( p pCnt B ) ) ) = 0 <-> ( ( p pCnt A ) + ( p pCnt B ) ) = ( 1 + 1 ) ) )
49 9 recnd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> 1 e. CC )
50 49 49 30 33 addsub4d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 1 + 1 ) - ( ( p pCnt A ) + ( p pCnt B ) ) ) = ( ( 1 - ( p pCnt A ) ) + ( 1 - ( p pCnt B ) ) ) )
51 50 eqeq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 1 + 1 ) - ( ( p pCnt A ) + ( p pCnt B ) ) ) = 0 <-> ( ( 1 - ( p pCnt A ) ) + ( 1 - ( p pCnt B ) ) ) = 0 ) )
52 48 51 bitr3d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( p pCnt A ) + ( p pCnt B ) ) = ( 1 + 1 ) <-> ( ( 1 - ( p pCnt A ) ) + ( 1 - ( p pCnt B ) ) ) = 0 ) )
53 52 adantr 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 e. RR /\ ( p pCnt A ) e. RR ) -> ( 0 <_ ( 1 - ( p pCnt A ) ) <-> ( p pCnt A ) <_ 1 ) )
55 40 5 54 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( 0 <_ ( 1 - ( p pCnt A ) ) <-> ( p pCnt A ) <_ 1 ) )
56 subge0 
 |-  ( ( 1 e. RR /\ ( p pCnt B ) e. RR ) -> ( 0 <_ ( 1 - ( p pCnt B ) ) <-> ( p pCnt B ) <_ 1 ) )
57 40 8 56 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( 0 <_ ( 1 - ( p pCnt B ) ) <-> ( p pCnt B ) <_ 1 ) )
58 55 57 anbi12d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 0 <_ ( 1 - ( p pCnt A ) ) /\ 0 <_ ( 1 - ( p pCnt B ) ) ) <-> ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) ) )
59 resubcl 
 |-  ( ( 1 e. RR /\ ( p pCnt A ) e. RR ) -> ( 1 - ( p pCnt A ) ) e. RR )
60 40 5 59 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( 1 - ( p pCnt A ) ) e. RR )
61 resubcl 
 |-  ( ( 1 e. RR /\ ( p pCnt B ) e. RR ) -> ( 1 - ( p pCnt B ) ) e. RR )
62 40 8 61 sylancr 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( 1 - ( p pCnt B ) ) e. RR )
63 add20 
 |-  ( ( ( ( 1 - ( p pCnt A ) ) e. RR /\ 0 <_ ( 1 - ( p pCnt A ) ) ) /\ ( ( 1 - ( p pCnt B ) ) e. RR /\ 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 ) ) e. RR /\ ( 1 - ( p pCnt B ) ) e. RR ) /\ ( 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 ) ) e. RR /\ ( 1 - ( p pCnt B ) ) e. RR ) -> ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 bitrid 
 |-  ( ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) /\ ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) ) -> ( 1 + 1 ) =/= ( ( p pCnt A ) + ( p pCnt B ) ) )
73 72 ex 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) -> ( 1 + 1 ) =/= ( ( p pCnt A ) + ( p pCnt B ) ) ) )
74 11 73 jcad 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 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 e. NN -> A e. ZZ )
76 nnne0 
 |-  ( A e. NN -> A =/= 0 )
77 75 76 jca 
 |-  ( A e. NN -> ( A e. ZZ /\ A =/= 0 ) )
78 3 77 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( A e. ZZ /\ A =/= 0 ) )
79 nnz 
 |-  ( B e. NN -> B e. ZZ )
80 nnne0 
 |-  ( B e. NN -> B =/= 0 )
81 79 80 jca 
 |-  ( B e. NN -> ( B e. ZZ /\ B =/= 0 ) )
82 6 81 syl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( B e. ZZ /\ B =/= 0 ) )
83 pcmul 
 |-  ( ( p e. Prime /\ ( A e. ZZ /\ A =/= 0 ) /\ ( B e. ZZ /\ B =/= 0 ) ) -> ( p pCnt ( A x. B ) ) = ( ( p pCnt A ) + ( p pCnt B ) ) )
84 2 78 82 83 syl3anc 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( p pCnt ( A x. B ) ) = ( ( p pCnt A ) + ( p pCnt B ) ) )
85 84 breq1d 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( p pCnt ( A x. B ) ) <_ 1 <-> ( ( p pCnt A ) + ( p pCnt B ) ) <_ 1 ) )
86 1nn0 
 |-  1 e. NN0
87 nn0leltp1 
 |-  ( ( ( ( p pCnt A ) + ( p pCnt B ) ) e. NN0 /\ 1 e. NN0 ) -> ( ( ( p pCnt A ) + ( p pCnt B ) ) <_ 1 <-> ( ( p pCnt A ) + ( p pCnt B ) ) < ( 1 + 1 ) ) )
88 43 86 87 sylancl 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( p pCnt A ) + ( p pCnt B ) ) <_ 1 <-> ( ( p pCnt A ) + ( p pCnt B ) ) < ( 1 + 1 ) ) )
89 ltlen 
 |-  ( ( ( ( p pCnt A ) + ( p pCnt B ) ) e. RR /\ ( 1 + 1 ) e. RR ) -> ( ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( 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 e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( p pCnt ( A x. B ) ) <_ 1 <-> ( ( ( p pCnt A ) + ( p pCnt B ) ) <_ ( 1 + 1 ) /\ ( 1 + 1 ) =/= ( ( p pCnt A ) + ( p pCnt B ) ) ) ) )
92 74 91 sylibrd 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ p e. Prime ) -> ( ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) -> ( p pCnt ( A x. B ) ) <_ 1 ) )
93 92 ralimdva 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( A. p e. Prime ( ( p pCnt A ) <_ 1 /\ ( p pCnt B ) <_ 1 ) -> A. p e. Prime ( p pCnt ( A x. B ) ) <_ 1 ) )
94 1 93 biimtrrid 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( ( A. p e. Prime ( p pCnt A ) <_ 1 /\ A. p e. Prime ( p pCnt B ) <_ 1 ) -> A. p e. Prime ( p pCnt ( A x. B ) ) <_ 1 ) )
95 issqf 
 |-  ( A e. NN -> ( ( mmu ` A ) =/= 0 <-> A. p e. Prime ( p pCnt A ) <_ 1 ) )
96 issqf 
 |-  ( B e. NN -> ( ( mmu ` B ) =/= 0 <-> A. p e. Prime ( p pCnt B ) <_ 1 ) )
97 95 96 bi2anan9 
 |-  ( ( A e. NN /\ B e. NN ) -> ( ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) <-> ( A. p e. Prime ( p pCnt A ) <_ 1 /\ A. p e. Prime ( p pCnt B ) <_ 1 ) ) )
98 97 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) <-> ( A. p e. Prime ( p pCnt A ) <_ 1 /\ A. p e. Prime ( p pCnt B ) <_ 1 ) ) )
99 nnmulcl 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A x. B ) e. NN )
100 99 3adant3 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( A x. B ) e. NN )
101 issqf 
 |-  ( ( A x. B ) e. NN -> ( ( mmu ` ( A x. B ) ) =/= 0 <-> A. p e. Prime ( p pCnt ( A x. B ) ) <_ 1 ) )
102 100 101 syl 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( ( mmu ` ( A x. B ) ) =/= 0 <-> A. p e. Prime ( p pCnt ( A x. B ) ) <_ 1 ) )
103 94 98 102 3imtr4d 
 |-  ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) -> ( ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) -> ( mmu ` ( A x. B ) ) =/= 0 ) )
104 103 imp 
 |-  ( ( ( A e. NN /\ B e. NN /\ ( A gcd B ) = 1 ) /\ ( ( mmu ` A ) =/= 0 /\ ( mmu ` B ) =/= 0 ) ) -> ( mmu ` ( A x. B ) ) =/= 0 )