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 } )