Metamath Proof Explorer


Theorem zdivgd

Description: Two ways to express " N is an integer multiple of M ". Originally a subproof of zdiv . (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses zdivgd.1 ( 𝜑𝑀 ∈ ℂ )
zdivgd.2 ( 𝜑𝑁 ∈ ℂ )
zdivgd.3 ( 𝜑𝑀 ≠ 0 )
Assertion zdivgd ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 zdivgd.1 ( 𝜑𝑀 ∈ ℂ )
2 zdivgd.2 ( 𝜑𝑁 ∈ ℂ )
3 zdivgd.3 ( 𝜑𝑀 ≠ 0 )
4 zcn ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
5 4 adantl ( ( 𝜑𝑘 ∈ ℤ ) → 𝑘 ∈ ℂ )
6 1 adantr ( ( 𝜑𝑘 ∈ ℤ ) → 𝑀 ∈ ℂ )
7 3 adantr ( ( 𝜑𝑘 ∈ ℤ ) → 𝑀 ≠ 0 )
8 5 6 7 divcan3d ( ( 𝜑𝑘 ∈ ℤ ) → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = 𝑘 )
9 oveq1 ( ( 𝑀 · 𝑘 ) = 𝑁 → ( ( 𝑀 · 𝑘 ) / 𝑀 ) = ( 𝑁 / 𝑀 ) )
10 8 9 sylan9req ( ( ( 𝜑𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 = ( 𝑁 / 𝑀 ) )
11 simplr ( ( ( 𝜑𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → 𝑘 ∈ ℤ )
12 10 11 eqeltrrd ( ( ( 𝜑𝑘 ∈ ℤ ) ∧ ( 𝑀 · 𝑘 ) = 𝑁 ) → ( 𝑁 / 𝑀 ) ∈ ℤ )
13 12 rexlimdva2 ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 → ( 𝑁 / 𝑀 ) ∈ ℤ ) )
14 2 1 3 divcan2d ( 𝜑 → ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 )
15 oveq2 ( 𝑘 = ( 𝑁 / 𝑀 ) → ( 𝑀 · 𝑘 ) = ( 𝑀 · ( 𝑁 / 𝑀 ) ) )
16 15 eqeq1d ( 𝑘 = ( 𝑁 / 𝑀 ) → ( ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) )
17 16 rspcev ( ( ( 𝑁 / 𝑀 ) ∈ ℤ ∧ ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 ) → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 )
18 17 ex ( ( 𝑁 / 𝑀 ) ∈ ℤ → ( ( 𝑀 · ( 𝑁 / 𝑀 ) ) = 𝑁 → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
19 14 18 syl5com ( 𝜑 → ( ( 𝑁 / 𝑀 ) ∈ ℤ → ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ) )
20 13 19 impbid ( 𝜑 → ( ∃ 𝑘 ∈ ℤ ( 𝑀 · 𝑘 ) = 𝑁 ↔ ( 𝑁 / 𝑀 ) ∈ ℤ ) )