Theorem 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	⊢ ( ( 𝑀 ∥ 𝑁 ∧ 𝑀 ≠ 0 ) → ( 𝑁 / 𝑀 ) ∥ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		dvdszrcl	⊢ ( 𝑀 ∥ 𝑁 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
2		simpll	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℤ )
3		oveq1	⊢ ( 𝑚 = 𝑀 → ( 𝑚 · ( 𝑁 / 𝑀 ) ) = ( 𝑀 · ( 𝑁 / 𝑀 ) ) )
4	3	eqeq1d	⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
5	4	adantl	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
6		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
7	6	adantl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
8	7	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑁 ∈ ℂ )
9		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℂ )
11	10	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℂ )
12		simpr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ≠ 0 )
13	8 11 12	divcan2d	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
14	2 5 13	rspcedvd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ∃ 𝑚 ∈ ℤ ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
15	14	adantr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ∃ 𝑚 ∈ ℤ ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
16		simpr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → 𝑀 ∥ 𝑁 )
17		simpr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
18	17	adantr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑁 ∈ ℤ )
19	2 12 18	3jca	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) )
20	19	adantr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) )
21		dvdsval2	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
22	20 21	syl	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ( 𝑀 ∥ 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )
23	16 22	mpbid	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
24	18	adantr	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → 𝑁 ∈ ℤ )
25		divides	⊢ ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑁 / 𝑀 ) ∥ 𝑁 ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
26	23 24 25	syl2anc	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ( ( 𝑁 / 𝑀 ) ∥ 𝑁 ↔ ∃ 𝑚 ∈ ℤ ( 𝑚 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
27	15 26	mpbird	⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) ∧ 𝑀 ∥ 𝑁 ) → ( 𝑁 / 𝑀 ) ∥ 𝑁 )
28	27	exp31	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≠ 0 → ( 𝑀 ∥ 𝑁 → ( 𝑁 / 𝑀 ) ∥ 𝑁 ) ) )
29	28	com3r	⊢ ( 𝑀 ∥ 𝑁 → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ≠ 0 → ( 𝑁 / 𝑀 ) ∥ 𝑁 ) ) )
30	1 29	mpd	⊢ ( 𝑀 ∥ 𝑁 → ( 𝑀 ≠ 0 → ( 𝑁 / 𝑀 ) ∥ 𝑁 ) )
31	30	imp	⊢ ( ( 𝑀 ∥ 𝑁 ∧ 𝑀 ≠ 0 ) → ( 𝑁 / 𝑀 ) ∥ 𝑁 )