Metamath Proof Explorer

Theorem nnproddivdvdsd

Description: A product of natural numbers divides a natural number if and only if a factor divides the quotient, a deduction version. (Contributed by metakunt, 12-May-2024)

Ref Expression
Hypotheses nnproddivdvdsd.1 
|- ( ph -> K e. NN )
nnproddivdvdsd.2 
|- ( ph -> M e. NN )
nnproddivdvdsd.3 
|- ( ph -> N e. NN )
Assertion nnproddivdvdsd 
|- ( ph -> ( ( K x. M ) || N <-> K || ( N / M ) ) )

Proof

Step Hyp Ref Expression
1 nnproddivdvdsd.1 
 |-  ( ph -> K e. NN )
2 nnproddivdvdsd.2 
 |-  ( ph -> M e. NN )
3 nnproddivdvdsd.3 
 |-  ( ph -> N e. NN )
4 3 nncnd 
 |-  ( ph -> N e. CC )
5 4 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> N e. CC )
6 1 nncnd 
 |-  ( ph -> K e. CC )
7 6 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> K e. CC )
8 2 nncnd 
 |-  ( ph -> M e. CC )
9 8 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> M e. CC )
10 1 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> K e. NN )
11 nnne0 
 |-  ( K e. NN -> K =/= 0 )
12 10 11 syl 
 |-  ( ( ph /\ ( K x. M ) || N ) -> K =/= 0 )
13 2 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> M e. NN )
14 13 nnne0d 
 |-  ( ( ph /\ ( K x. M ) || N ) -> M =/= 0 )
15 5 7 9 12 14 divdiv1d 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( ( N / K ) / M ) = ( N / ( K x. M ) ) )
16 15 eqcomd 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( N / ( K x. M ) ) = ( ( N / K ) / M ) )
17 5 7 9 12 14 divdiv32d 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( ( N / K ) / M ) = ( ( N / M ) / K ) )
18 16 17 eqtrd 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( N / ( K x. M ) ) = ( ( N / M ) / K ) )
19 1 2 nnmulcld 
 |-  ( ph -> ( K x. M ) e. NN )
20 19 3 nndivdvdsd 
 |-  ( ph -> ( ( K x. M ) || N <-> ( N / ( K x. M ) ) e. NN ) )
21 20 biimpd 
 |-  ( ph -> ( ( K x. M ) || N -> ( N / ( K x. M ) ) e. NN ) )
22 21 imp 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( N / ( K x. M ) ) e. NN )
23 18 22 eqeltrrd 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( ( N / M ) / K ) e. NN )
24 1 nnzd 
 |-  ( ph -> K e. ZZ )
25 2 nnzd 
 |-  ( ph -> M e. ZZ )
26 3 nnzd 
 |-  ( ph -> N e. ZZ )
27 24 25 26 3jca 
 |-  ( ph -> ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) )
28 muldvds2 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) || N -> M || N ) )
29 27 28 syl 
 |-  ( ph -> ( ( K x. M ) || N -> M || N ) )
30 29 imp 
 |-  ( ( ph /\ ( K x. M ) || N ) -> M || N )
31 3 adantr 
 |-  ( ( ph /\ ( K x. M ) || N ) -> N e. NN )
32 13 31 nndivdvdsd 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( M || N <-> ( N / M ) e. NN ) )
33 30 32 mpbid 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( N / M ) e. NN )
34 10 33 nndivdvdsd 
 |-  ( ( ph /\ ( K x. M ) || N ) -> ( K || ( N / M ) <-> ( ( N / M ) / K ) e. NN ) )
35 23 34 mpbird 
 |-  ( ( ph /\ ( K x. M ) || N ) -> K || ( N / M ) )
36 35 ex 
 |-  ( ph -> ( ( K x. M ) || N -> K || ( N / M ) ) )
37 dvdszrcl 
 |-  ( K || ( N / M ) -> ( K e. ZZ /\ ( N / M ) e. ZZ ) )
38 37 simprd 
 |-  ( K || ( N / M ) -> ( N / M ) e. ZZ )
39 38 adantl 
 |-  ( ( ph /\ K || ( N / M ) ) -> ( N / M ) e. ZZ )
40 dvdsmulc 
 |-  ( ( K e. ZZ /\ ( N / M ) e. ZZ /\ M e. ZZ ) -> ( K || ( N / M ) -> ( K x. M ) || ( ( N / M ) x. M ) ) )
41 24 40 syl3an1 
 |-  ( ( ph /\ ( N / M ) e. ZZ /\ M e. ZZ ) -> ( K || ( N / M ) -> ( K x. M ) || ( ( N / M ) x. M ) ) )
42 25 41 syl3an3 
 |-  ( ( ph /\ ( N / M ) e. ZZ /\ ph ) -> ( K || ( N / M ) -> ( K x. M ) || ( ( N / M ) x. M ) ) )
43 42 3anidm13 
 |-  ( ( ph /\ ( N / M ) e. ZZ ) -> ( K || ( N / M ) -> ( K x. M ) || ( ( N / M ) x. M ) ) )
44 43 impancom 
 |-  ( ( ph /\ K || ( N / M ) ) -> ( ( N / M ) e. ZZ -> ( K x. M ) || ( ( N / M ) x. M ) ) )
45 39 44 mpd 
 |-  ( ( ph /\ K || ( N / M ) ) -> ( K x. M ) || ( ( N / M ) x. M ) )
46 2 nnne0d 
 |-  ( ph -> M =/= 0 )
47 4 8 46 divcan1d 
 |-  ( ph -> ( ( N / M ) x. M ) = N )
48 47 adantr 
 |-  ( ( ph /\ K || ( N / M ) ) -> ( ( N / M ) x. M ) = N )
49 45 48 breqtrd 
 |-  ( ( ph /\ K || ( N / M ) ) -> ( K x. M ) || N )
50 49 ex 
 |-  ( ph -> ( K || ( N / M ) -> ( K x. M ) || N ) )
51 36 50 impbid 
 |-  ( ph -> ( ( K x. M ) || N <-> K || ( N / M ) ) )