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