Description: The complement of a divisor of N is also a divisor of N . (Contributed by Mario Carneiro, 2-Jul-2015) (Proof shortened by AV, 9-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dvdsdivcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | breq1 | |
|
2 | 1 | elrab | |
3 | nndivdvds | |
|
4 | 3 | biimpd | |
5 | 4 | expcom | |
6 | 5 | com23 | |
7 | 6 | imp | |
8 | nnne0 | |
|
9 | 8 | anim1ci | |
10 | divconjdvds | |
|
11 | 9 10 | syl | |
12 | 7 11 | jctird | |
13 | 2 12 | sylbi | |
14 | 13 | impcom | |
15 | breq1 | |
|
16 | 15 | elrab | |
17 | 14 16 | sylibr | |