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 
|- ( ( M || N /\ M =/= 0 ) -> ( N / M ) || N )

Proof

Step Hyp Ref Expression
1 dvdszrcl 
 |-  ( M || N -> ( M e. ZZ /\ N e. ZZ ) )
2 simpll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> M e. ZZ )
3 oveq1 
 |-  ( m = M -> ( m x. ( N / M ) ) = ( M x. ( N / M ) ) )
4 3 eqeq1d 
 |-  ( m = M -> ( ( m x. ( N / M ) ) = N <-> ( M x. ( N / M ) ) = N ) )
5 4 adantl 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ m = M ) -> ( ( m x. ( N / M ) ) = N <-> ( M x. ( N / M ) ) = N ) )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 6 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. CC )
8 7 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> N e. CC )
9 zcn 
 |-  ( M e. ZZ -> M e. CC )
10 9 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. CC )
11 10 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> M e. CC )
12 simpr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> M =/= 0 )
13 8 11 12 divcan2d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> ( M x. ( N / M ) ) = N )
14 2 5 13 rspcedvd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> E. m e. ZZ ( m x. ( N / M ) ) = N )
15 14 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> E. m e. ZZ ( m x. ( N / M ) ) = N )
16 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> M || N )
17 simpr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
18 17 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> N e. ZZ )
19 2 12 18 3jca 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) -> ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) )
20 19 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) )
21 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
22 20 21 syl 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> ( M || N <-> ( N / M ) e. ZZ ) )
23 16 22 mpbid 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> ( N / M ) e. ZZ )
24 18 adantr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> N e. ZZ )
25 divides 
 |-  ( ( ( N / M ) e. ZZ /\ N e. ZZ ) -> ( ( N / M ) || N <-> E. m e. ZZ ( m x. ( N / M ) ) = N ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> ( ( N / M ) || N <-> E. m e. ZZ ( m x. ( N / M ) ) = N ) )
27 15 26 mpbird 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ M =/= 0 ) /\ M || N ) -> ( N / M ) || N )
28 27 exp31 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M =/= 0 -> ( M || N -> ( N / M ) || N ) ) )
29 28 com3r 
 |-  ( M || N -> ( ( M e. ZZ /\ N e. ZZ ) -> ( M =/= 0 -> ( N / M ) || N ) ) )
30 1 29 mpd 
 |-  ( M || N -> ( M =/= 0 -> ( N / M ) || N ) )
31 30 imp 
 |-  ( ( M || N /\ M =/= 0 ) -> ( N / M ) || N )