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	$⊢ φ \to K \in ℕ$
	nnproddivdvdsd.2	$⊢ φ \to M \in ℕ$
	nnproddivdvdsd.3	$⊢ φ \to N \in ℕ$
Assertion	nnproddivdvdsd	$⊢ φ \to (K \cdot M ∥ N \leftrightarrow K ∥ (\frac{N}{M}))$

Proof

Step	Hyp	Ref	Expression
1		nnproddivdvdsd.1	$⊢ φ \to K \in ℕ$
2		nnproddivdvdsd.2	$⊢ φ \to M \in ℕ$
3		nnproddivdvdsd.3	$⊢ φ \to N \in ℕ$
4	3	nncnd	$⊢ φ \to N \in ℂ$
5	4	adantr	$⊢ (φ \land K \cdot M ∥ N) \to N \in ℂ$
6	1	nncnd	$⊢ φ \to K \in ℂ$
7	6	adantr	$⊢ (φ \land K \cdot M ∥ N) \to K \in ℂ$
8	2	nncnd	$⊢ φ \to M \in ℂ$
9	8	adantr	$⊢ (φ \land K \cdot M ∥ N) \to M \in ℂ$
10	1	adantr	$⊢ (φ \land K \cdot M ∥ N) \to K \in ℕ$
11		nnne0	$⊢ K \in ℕ \to K \neq 0$
12	10 11	syl	$⊢ (φ \land K \cdot M ∥ N) \to K \neq 0$
13	2	adantr	$⊢ (φ \land K \cdot M ∥ N) \to M \in ℕ$
14	13	nnne0d	$⊢ (φ \land K \cdot M ∥ N) \to M \neq 0$
15	5 7 9 12 14	divdiv1d	$⊢ (φ \land K \cdot M ∥ N) \to \frac{\frac{N}{K}}{M} = \frac{N}{K \cdot M}$
16	15	eqcomd	$⊢ (φ \land K \cdot M ∥ N) \to \frac{N}{K \cdot M} = \frac{\frac{N}{K}}{M}$
17	5 7 9 12 14	divdiv32d	$⊢ (φ \land K \cdot M ∥ N) \to \frac{\frac{N}{K}}{M} = \frac{\frac{N}{M}}{K}$
18	16 17	eqtrd	$⊢ (φ \land K \cdot M ∥ N) \to \frac{N}{K \cdot M} = \frac{\frac{N}{M}}{K}$
19	1 2	nnmulcld	$⊢ φ \to K \cdot M \in ℕ$
20	19 3	nndivdvdsd	$⊢ φ \to (K \cdot M ∥ N \leftrightarrow \frac{N}{K \cdot M} \in ℕ)$
21	20	biimpd	$⊢ φ \to (K \cdot M ∥ N \to \frac{N}{K \cdot M} \in ℕ)$
22	21	imp	$⊢ (φ \land K \cdot M ∥ N) \to \frac{N}{K \cdot M} \in ℕ$
23	18 22	eqeltrrd	$⊢ (φ \land K \cdot M ∥ N) \to \frac{\frac{N}{M}}{K} \in ℕ$
24	1	nnzd	$⊢ φ \to K \in ℤ$
25	2	nnzd	$⊢ φ \to M \in ℤ$
26	3	nnzd	$⊢ φ \to N \in ℤ$
27	24 25 26	3jca	$⊢ φ \to (K \in ℤ \land M \in ℤ \land N \in ℤ)$
28		muldvds2	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \cdot M ∥ N \to M ∥ N)$
29	27 28	syl	$⊢ φ \to (K \cdot M ∥ N \to M ∥ N)$
30	29	imp	$⊢ (φ \land K \cdot M ∥ N) \to M ∥ N$
31	3	adantr	$⊢ (φ \land K \cdot M ∥ N) \to N \in ℕ$
32	13 31	nndivdvdsd	$⊢ (φ \land K \cdot M ∥ N) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℕ)$
33	30 32	mpbid	$⊢ (φ \land K \cdot M ∥ N) \to \frac{N}{M} \in ℕ$
34	10 33	nndivdvdsd	$⊢ (φ \land K \cdot M ∥ N) \to (K ∥ (\frac{N}{M}) \leftrightarrow \frac{\frac{N}{M}}{K} \in ℕ)$
35	23 34	mpbird	$⊢ (φ \land K \cdot M ∥ N) \to K ∥ (\frac{N}{M})$
36	35	ex	$⊢ φ \to (K \cdot M ∥ N \to K ∥ (\frac{N}{M}))$
37		dvdszrcl	$⊢ K ∥ (\frac{N}{M}) \to (K \in ℤ \land \frac{N}{M} \in ℤ)$
38	37	simprd	$⊢ K ∥ (\frac{N}{M}) \to \frac{N}{M} \in ℤ$
39	38	adantl	$⊢ (φ \land K ∥ (\frac{N}{M})) \to \frac{N}{M} \in ℤ$
40		dvdsmulc	$⊢ (K \in ℤ \land \frac{N}{M} \in ℤ \land M \in ℤ) \to (K ∥ (\frac{N}{M}) \to K \cdot M ∥ (\frac{N}{M}) \cdot M)$
41	24 40	syl3an1	$⊢ (φ \land \frac{N}{M} \in ℤ \land M \in ℤ) \to (K ∥ (\frac{N}{M}) \to K \cdot M ∥ (\frac{N}{M}) \cdot M)$
42	25 41	syl3an3	$⊢ (φ \land \frac{N}{M} \in ℤ \land φ) \to (K ∥ (\frac{N}{M}) \to K \cdot M ∥ (\frac{N}{M}) \cdot M)$
43	42	3anidm13	$⊢ (φ \land \frac{N}{M} \in ℤ) \to (K ∥ (\frac{N}{M}) \to K \cdot M ∥ (\frac{N}{M}) \cdot M)$
44	43	impancom	$⊢ (φ \land K ∥ (\frac{N}{M})) \to (\frac{N}{M} \in ℤ \to K \cdot M ∥ (\frac{N}{M}) \cdot M)$
45	39 44	mpd	$⊢ (φ \land K ∥ (\frac{N}{M})) \to K \cdot M ∥ (\frac{N}{M}) \cdot M$
46	2	nnne0d	$⊢ φ \to M \neq 0$
47	4 8 46	divcan1d	$⊢ φ \to (\frac{N}{M}) \cdot M = N$
48	47	adantr	$⊢ (φ \land K ∥ (\frac{N}{M})) \to (\frac{N}{M}) \cdot M = N$
49	45 48	breqtrd	$⊢ (φ \land K ∥ (\frac{N}{M})) \to K \cdot M ∥ N$
50	49	ex	$⊢ φ \to (K ∥ (\frac{N}{M}) \to K \cdot M ∥ N)$
51	36 50	impbid	$⊢ φ \to (K \cdot M ∥ N \leftrightarrow K ∥ (\frac{N}{M}))$

Metamath Proof Explorer

Theorem nnproddivdvdsd

Proof