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 φ M
zdivgd.2 φ N
zdivgd.3 φ M 0
Assertion zdivgd φ k M k = N N M

Proof

Step Hyp Ref Expression
1 zdivgd.1 φ M
2 zdivgd.2 φ N
3 zdivgd.3 φ M 0
4 zcn k k
5 4 adantl φ k k
6 1 adantr φ k M
7 3 adantr φ k M 0
8 5 6 7 divcan3d φ k M k M = k
9 oveq1 M k = N M k M = N M
10 8 9 sylan9req φ k M k = N k = N M
11 simplr φ k M k = N k
12 10 11 eqeltrrd φ k M k = N N M
13 12 rexlimdva2 φ k M k = N N M
14 2 1 3 divcan2d φ M N M = N
15 oveq2 k = N M M k = M N M
16 15 eqeq1d k = N M M k = N M N M = N
17 16 rspcev N M M N M = N k M k = N
18 17 ex N M M N M = N k M k = N
19 14 18 syl5com φ N M k M k = N
20 13 19 impbid φ k M k = N N M