Metamath Proof Explorer


Theorem dvdsdivcl

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 NAx|xNNAx|xN

Proof

Step Hyp Ref Expression
1 breq1 x=AxNAN
2 1 elrab Ax|xNAAN
3 nndivdvds NAANNA
4 3 biimpd NAANNA
5 4 expcom ANANNA
6 5 com23 AANNNA
7 6 imp AANNNA
8 nnne0 AA0
9 8 anim1ci AANANA0
10 divconjdvds ANA0NAN
11 9 10 syl AANNAN
12 7 11 jctird AANNNANAN
13 2 12 sylbi Ax|xNNNANAN
14 13 impcom NAx|xNNANAN
15 breq1 x=NAxNNAN
16 15 elrab NAx|xNNANAN
17 14 16 sylibr NAx|xNNAx|xN