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 MNM0NMN

Proof

Step Hyp Ref Expression
1 dvdszrcl MNMN
2 simpll MNM0M
3 oveq1 m=MmNM=MNM
4 3 eqeq1d m=MmNM=NMNM=N
5 4 adantl MNM0m=MmNM=NMNM=N
6 zcn NN
7 6 adantl MNN
8 7 adantr MNM0N
9 zcn MM
10 9 adantr MNM
11 10 adantr MNM0M
12 simpr MNM0M0
13 8 11 12 divcan2d MNM0MNM=N
14 2 5 13 rspcedvd MNM0mmNM=N
15 14 adantr MNM0MNmmNM=N
16 simpr MNM0MNMN
17 simpr MNN
18 17 adantr MNM0N
19 2 12 18 3jca MNM0MM0N
20 19 adantr MNM0MNMM0N
21 dvdsval2 MM0NMNNM
22 20 21 syl MNM0MNMNNM
23 16 22 mpbid MNM0MNNM
24 18 adantr MNM0MNN
25 divides NMNNMNmmNM=N
26 23 24 25 syl2anc MNM0MNNMNmmNM=N
27 15 26 mpbird MNM0MNNMN
28 27 exp31 MNM0MNNMN
29 28 com3r MNMNM0NMN
30 1 29 mpd MNM0NMN
31 30 imp MNM0NMN