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	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝐴 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )

Proof

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	⊢ ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )
9	8	anim1ci	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐴 ∥ 𝑁 ) → ( 𝐴 ∥ 𝑁 ∧ 𝐴 ≠ 0 ) )
10		divconjdvds	⊢ ( ( 𝐴 ∥ 𝑁 ∧ 𝐴 ≠ 0 ) → ( 𝑁 / 𝐴 ) ∥ 𝑁 )
11	9 10	syl	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐴 ∥ 𝑁 ) → ( 𝑁 / 𝐴 ) ∥ 𝑁 )
12	7 11	jctird	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐴 ∥ 𝑁 ) → ( 𝑁 ∈ ℕ → ( ( 𝑁 / 𝐴 ) ∈ ℕ ∧ ( 𝑁 / 𝐴 ) ∥ 𝑁 ) ) )
13	2 12	sylbi	⊢ ( 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } → ( 𝑁 ∈ ℕ → ( ( 𝑁 / 𝐴 ) ∈ ℕ ∧ ( 𝑁 / 𝐴 ) ∥ 𝑁 ) ) )
14	13	impcom	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( ( 𝑁 / 𝐴 ) ∈ ℕ ∧ ( 𝑁 / 𝐴 ) ∥ 𝑁 ) )
15		breq1	⊢ ( 𝑥 = ( 𝑁 / 𝐴 ) → ( 𝑥 ∥ 𝑁 ↔ ( 𝑁 / 𝐴 ) ∥ 𝑁 ) )
16	15	elrab	⊢ ( ( 𝑁 / 𝐴 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ↔ ( ( 𝑁 / 𝐴 ) ∈ ℕ ∧ ( 𝑁 / 𝐴 ) ∥ 𝑁 ) )
17	14 16	sylibr	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝐴 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )