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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdszrcl | |
|
2 | simpll | |
|
3 | oveq1 | |
|
4 | 3 | eqeq1d | |
5 | 4 | adantl | |
6 | zcn | |
|
7 | 6 | adantl | |
8 | 7 | adantr | |
9 | zcn | |
|
10 | 9 | adantr | |
11 | 10 | adantr | |
12 | simpr | |
|
13 | 8 11 12 | divcan2d | |
14 | 2 5 13 | rspcedvd | |
15 | 14 | adantr | |
16 | simpr | |
|
17 | simpr | |
|
18 | 17 | adantr | |
19 | 2 12 18 | 3jca | |
20 | 19 | adantr | |
21 | dvdsval2 | |
|
22 | 20 21 | syl | |
23 | 16 22 | mpbid | |
24 | 18 | adantr | |
25 | divides | |
|
26 | 23 24 25 | syl2anc | |
27 | 15 26 | mpbird | |
28 | 27 | exp31 | |
29 | 28 | com3r | |
30 | 1 29 | mpd | |
31 | 30 | imp | |