Description: If two nonnegative integers divide each other, they must be equal. (Contributed by Mario Carneiro, 30-May-2014) (Proof shortened by AV, 7-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdseq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dvdsabseq | |
|
2 | nn0re | |
|
3 | nn0ge0 | |
|
4 | 2 3 | absidd | |
5 | 4 | adantr | |
6 | 5 | eqcomd | |
7 | 6 | adantr | |
8 | simpr | |
|
9 | nn0re | |
|
10 | nn0ge0 | |
|
11 | 9 10 | absidd | |
12 | 11 | ad2antlr | |
13 | 7 8 12 | 3eqtrd | |
14 | 1 13 | sylan2 | |