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 ∈ ℕ ∧ A ∈ x ∈ ℕ | x ∥ N → N A ∈ x ∈ ℕ | x ∥ N

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = A → x ∥ N ↔ A ∥ N
2 1 elrab ⊢ A ∈ x ∈ ℕ | x ∥ N ↔ A ∈ ℕ ∧ A ∥ N
3 nndivdvds ⊢ N ∈ ℕ ∧ A ∈ ℕ → A ∥ N ↔ N A ∈ ℕ
4 3 biimpd ⊢ N ∈ ℕ ∧ A ∈ ℕ → A ∥ N → N A ∈ ℕ
5 4 expcom ⊢ A ∈ ℕ → N ∈ ℕ → A ∥ N → N A ∈ ℕ
6 5 com23 ⊢ A ∈ ℕ → A ∥ N → N ∈ ℕ → N A ∈ ℕ
7 6 imp ⊢ A ∈ ℕ ∧ A ∥ N → N ∈ ℕ → N A ∈ ℕ
8 nnne0 ⊢ A ∈ ℕ → A ≠ 0
9 8 anim1ci ⊢ A ∈ ℕ ∧ A ∥ N → A ∥ N ∧ A ≠ 0
10 divconjdvds ⊢ A ∥ N ∧ A ≠ 0 → N A ∥ N
11 9 10 syl ⊢ A ∈ ℕ ∧ A ∥ N → N A ∥ N
12 7 11 jctird ⊢ A ∈ ℕ ∧ A ∥ N → N ∈ ℕ → N A ∈ ℕ ∧ N A ∥ N
13 2 12 sylbi ⊢ A ∈ x ∈ ℕ | x ∥ N → N ∈ ℕ → N A ∈ ℕ ∧ N A ∥ N
14 13 impcom ⊢ N ∈ ℕ ∧ A ∈ x ∈ ℕ | x ∥ N → N A ∈ ℕ ∧ N A ∥ N
15 breq1 ⊢ x = N A → x ∥ N ↔ N A ∥ N
16 15 elrab ⊢ N A ∈ x ∈ ℕ | x ∥ N ↔ N A ∈ ℕ ∧ N A ∥ N
17 14 16 sylibr ⊢ N ∈ ℕ ∧ A ∈ x ∈ ℕ | x ∥ N → N A ∈ x ∈ ℕ | x ∥ N