divconjdvds

Description: If a nonzero integer M divides another integer N , the other integer N divided by the nonzero integer M (i.e. thedivisor conjugate of N to M ) divides the other integer N . Theorem 1.1(k) in ApostolNT p. 14. (Contributed by AV, 7-Aug-2021)

		Ref	Expression
	Assertion	divconjdvds	$⊢ (M ∥ N \land M \neq 0) \to (\frac{N}{M}) ∥ N$

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	$⊢ M ∥ N \to (M \in ℤ \land N \in ℤ)$
2		simpll	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \in ℤ$
3		oveq1	$⊢ m = M \to m (\frac{N}{M}) = M (\frac{N}{M})$
4	3	eqeq1d	$⊢ m = M \to (m (\frac{N}{M}) = N \leftrightarrow M (\frac{N}{M}) = N)$
5	4	adantl	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land m = M) \to (m (\frac{N}{M}) = N \leftrightarrow M (\frac{N}{M}) = N)$
6		zcn	$⊢ N \in ℤ \to N \in ℂ$
7	6	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℂ$
8	7	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \in ℂ$
9		zcn	$⊢ M \in ℤ \to M \in ℂ$
10	9	adantr	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℂ$
11	10	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \in ℂ$
12		simpr	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to M \neq 0$
13	8 11 12	divcan2d	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to M (\frac{N}{M}) = N$
14	2 5 13	rspcedvd	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to \exists m \in ℤ m (\frac{N}{M}) = N$
15	14	adantr	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to \exists m \in ℤ m (\frac{N}{M}) = N$
16		simpr	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to M ∥ N$
17		simpr	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℤ$
18	17	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to N \in ℤ$
19	2 12 18	3jca	$⊢ ((M \in ℤ \land N \in ℤ) \land M \neq 0) \to (M \in ℤ \land M \neq 0 \land N \in ℤ)$
20	19	adantr	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to (M \in ℤ \land M \neq 0 \land N \in ℤ)$
21		dvdsval2	$⊢ (M \in ℤ \land M \neq 0 \land N \in ℤ) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$
22	20 21	syl	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to (M ∥ N \leftrightarrow \frac{N}{M} \in ℤ)$
23	16 22	mpbid	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to \frac{N}{M} \in ℤ$
24	18	adantr	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to N \in ℤ$
25		divides	$⊢ (\frac{N}{M} \in ℤ \land N \in ℤ) \to ((\frac{N}{M}) ∥ N \leftrightarrow \exists m \in ℤ m (\frac{N}{M}) = N)$
26	23 24 25	syl2anc	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to ((\frac{N}{M}) ∥ N \leftrightarrow \exists m \in ℤ m (\frac{N}{M}) = N)$
27	15 26	mpbird	$⊢ (((M \in ℤ \land N \in ℤ) \land M \neq 0) \land M ∥ N) \to (\frac{N}{M}) ∥ N$
28	27	exp31	$⊢ (M \in ℤ \land N \in ℤ) \to (M \neq 0 \to (M ∥ N \to (\frac{N}{M}) ∥ N))$
29	28	com3r	$⊢ M ∥ N \to ((M \in ℤ \land N \in ℤ) \to (M \neq 0 \to (\frac{N}{M}) ∥ N))$
30	1 29	mpd	$⊢ M ∥ N \to (M \neq 0 \to (\frac{N}{M}) ∥ N)$
31	30	imp	$⊢ (M ∥ N \land M \neq 0) \to (\frac{N}{M}) ∥ N$

Metamath Proof Explorer

Theorem divconjdvds

Proof