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

Metamath Proof Explorer

Theorem ndvdsi

Description: A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses ndvdsi.1 ⊢ 𝐴 ∈ ℕ
ndvdsi.2 ⊢ 𝑄 ∈ ℕ0
ndvdsi.3 ⊢ 𝑅 ∈ ℕ
ndvdsi.4 ⊢ ( ( 𝐴 · 𝑄 ) + 𝑅 ) = 𝐵
ndvdsi.5 ⊢ 𝑅 < 𝐴
Assertion ndvdsi ¬ 𝐴 ∥ 𝐵

Proof

Step Hyp Ref Expression
1 ndvdsi.1 ⊢ 𝐴 ∈ ℕ
2 ndvdsi.2 ⊢ 𝑄 ∈ ℕ0
3 ndvdsi.3 ⊢ 𝑅 ∈ ℕ
4 ndvdsi.4 ⊢ ( ( 𝐴 · 𝑄 ) + 𝑅 ) = 𝐵
5 ndvdsi.5 ⊢ 𝑅 < 𝐴
6 1 nnzi ⊢ 𝐴 ∈ ℤ
7 2 nn0zi ⊢ 𝑄 ∈ ℤ
8 dvdsmul1 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝑄 ) )
9 6 7 8 mp2an ⊢ 𝐴 ∥ ( 𝐴 · 𝑄 )
10 zmulcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑄 ∈ ℤ ) → ( 𝐴 · 𝑄 ) ∈ ℤ )
11 6 7 10 mp2an ⊢ ( 𝐴 · 𝑄 ) ∈ ℤ
12 3 5 pm3.2i ⊢ ( 𝑅 ∈ ℕ ∧ 𝑅 < 𝐴 )
13 ndvdsadd ⊢ ( ( ( 𝐴 · 𝑄 ) ∈ ℤ ∧ 𝐴 ∈ ℕ ∧ ( 𝑅 ∈ ℕ ∧ 𝑅 < 𝐴 ) ) → ( 𝐴 ∥ ( 𝐴 · 𝑄 ) → ¬ 𝐴 ∥ ( ( 𝐴 · 𝑄 ) + 𝑅 ) ) )
14 11 1 12 13 mp3an ⊢ ( 𝐴 ∥ ( 𝐴 · 𝑄 ) → ¬ 𝐴 ∥ ( ( 𝐴 · 𝑄 ) + 𝑅 ) )
15 9 14 ax-mp ⊢ ¬ 𝐴 ∥ ( ( 𝐴 · 𝑄 ) + 𝑅 )
16 4 breq2i ⊢ ( 𝐴 ∥ ( ( 𝐴 · 𝑄 ) + 𝑅 ) ↔ 𝐴 ∥ 𝐵 )
17 15 16 mtbi ⊢ ¬ 𝐴 ∥ 𝐵