This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝑁 / 𝑀 ) ∥ 𝑁 )