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	⊢ ¬ 𝐴 ∥ 𝐵