This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ( N e. NN /\ A e. { x e. NN | x || N } ) -> ( N / A ) e. { x e. NN | x || N } )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x || N <-> A || N ) )
2 1 elrab 
 |-  ( A e. { x e. NN | x || N } <-> ( A e. NN /\ A || N ) )
3 nndivdvds 
 |-  ( ( N e. NN /\ A e. NN ) -> ( A || N <-> ( N / A ) e. NN ) )
4 3 biimpd 
 |-  ( ( N e. NN /\ A e. NN ) -> ( A || N -> ( N / A ) e. NN ) )
5 4 expcom 
 |-  ( A e. NN -> ( N e. NN -> ( A || N -> ( N / A ) e. NN ) ) )
6 5 com23 
 |-  ( A e. NN -> ( A || N -> ( N e. NN -> ( N / A ) e. NN ) ) )
7 6 imp 
 |-  ( ( A e. NN /\ A || N ) -> ( N e. NN -> ( N / A ) e. NN ) )
8 nnne0 
 |-  ( A e. NN -> A =/= 0 )
9 8 anim1ci 
 |-  ( ( A e. NN /\ A || N ) -> ( A || N /\ A =/= 0 ) )
10 divconjdvds 
 |-  ( ( A || N /\ A =/= 0 ) -> ( N / A ) || N )
11 9 10 syl 
 |-  ( ( A e. NN /\ A || N ) -> ( N / A ) || N )
12 7 11 jctird 
 |-  ( ( A e. NN /\ A || N ) -> ( N e. NN -> ( ( N / A ) e. NN /\ ( N / A ) || N ) ) )
13 2 12 sylbi 
 |-  ( A e. { x e. NN | x || N } -> ( N e. NN -> ( ( N / A ) e. NN /\ ( N / A ) || N ) ) )
14 13 impcom 
 |-  ( ( N e. NN /\ A e. { x e. NN | x || N } ) -> ( ( N / A ) e. NN /\ ( N / A ) || N ) )
15 breq1 
 |-  ( x = ( N / A ) -> ( x || N <-> ( N / A ) || N ) )
16 15 elrab 
 |-  ( ( N / A ) e. { x e. NN | x || N } <-> ( ( N / A ) e. NN /\ ( N / A ) || N ) )
17 14 16 sylibr 
 |-  ( ( N e. NN /\ A e. { x e. NN | x || N } ) -> ( N / A ) e. { x e. NN | x || N } )