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 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
nnproddivdvdsd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
nnproddivdvdsd.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion nnproddivdvdsd ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 ↔ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 nnproddivdvdsd.1 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
2 nnproddivdvdsd.2 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
3 nnproddivdvdsd.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 3 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
5 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑁 ∈ ℂ )
6 1 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
7 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝐾 ∈ ℂ )
8 2 nncnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑀 ∈ ℂ )
10 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝐾 ∈ ℕ )
11 nnne0 ⊢ ( 𝐾 ∈ ℕ → 𝐾 ≠ 0 )
12 10 11 syl ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝐾 ≠ 0 )
13 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑀 ∈ ℕ )
14 13 nnne0d ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑀 ≠ 0 )
15 5 7 9 12 14 divdiv1d ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( ( 𝑁 / 𝐾 ) / 𝑀 ) = ( 𝑁 / ( 𝐾 · 𝑀 ) ) )
16 15 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝑁 / ( 𝐾 · 𝑀 ) ) = ( ( 𝑁 / 𝐾 ) / 𝑀 ) )
17 5 7 9 12 14 divdiv32d ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( ( 𝑁 / 𝐾 ) / 𝑀 ) = ( ( 𝑁 / 𝑀 ) / 𝐾 ) )
18 16 17 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝑁 / ( 𝐾 · 𝑀 ) ) = ( ( 𝑁 / 𝑀 ) / 𝐾 ) )
19 1 2 nnmulcld ⊢ ( 𝜑 → ( 𝐾 · 𝑀 ) ∈ ℕ )
20 19 3 nndivdvdsd ⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝐾 · 𝑀 ) ) ∈ ℕ ) )
21 20 biimpd ⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → ( 𝑁 / ( 𝐾 · 𝑀 ) ) ∈ ℕ ) )
22 21 imp ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝑁 / ( 𝐾 · 𝑀 ) ) ∈ ℕ )
23 18 22 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( ( 𝑁 / 𝑀 ) / 𝐾 ) ∈ ℕ )
24 1 nnzd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
25 2 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
26 3 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
27 24 25 26 3jca ⊢ ( 𝜑 → ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
28 muldvds2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝑀 ∥ 𝑁 ) )
29 27 28 syl ⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝑀 ∥ 𝑁 ) )
30 29 imp ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑀 ∥ 𝑁 )
31 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝑁 ∈ ℕ )
32 13 31 nndivdvdsd ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℕ ) )
33 30 32 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℕ )
34 10 33 nndivdvdsd ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) ↔ ( ( 𝑁 / 𝑀 ) / 𝐾 ) ∈ ℕ ) )
35 23 34 mpbird ⊢ ( ( 𝜑 ∧ ( 𝐾 · 𝑀 ) ∥ 𝑁 ) → 𝐾 ∥ ( 𝑁 / 𝑀 ) )
36 35 ex ⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝐾 ∥ ( 𝑁 / 𝑀 ) ) )
37 dvdszrcl ⊢ ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 ∈ ℤ ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
38 37 simprd ⊢ ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
40 dvdsmulc ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) )
41 24 40 syl3an1 ⊢ ( ( 𝜑 ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) )
42 25 41 syl3an3 ⊢ ( ( 𝜑 ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ∧ 𝜑 ) → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) )
43 42 3anidm13 ⊢ ( ( 𝜑 ∧ ( 𝑁 / 𝑀 ) ∈ ℤ ) → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) )
44 43 impancom ⊢ ( ( 𝜑 ∧ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) ) )
45 39 44 mpd ⊢ ( ( 𝜑 ∧ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) → ( 𝐾 · 𝑀 ) ∥ ( ( 𝑁 / 𝑀 ) · 𝑀 ) )
46 2 nnne0d ⊢ ( 𝜑 → 𝑀 ≠ 0 )
47 4 8 46 divcan1d ⊢ ( 𝜑 → ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) → ( ( 𝑁 / 𝑀 ) · 𝑀 ) = 𝑁 )
49 45 48 breqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) → ( 𝐾 · 𝑀 ) ∥ 𝑁 )
50 49 ex ⊢ ( 𝜑 → ( 𝐾 ∥ ( 𝑁 / 𝑀 ) → ( 𝐾 · 𝑀 ) ∥ 𝑁 ) )
51 36 50 impbid ⊢ ( 𝜑 → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 ↔ 𝐾 ∥ ( 𝑁 / 𝑀 ) ) )