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

Metamath Proof Explorer

Theorem 5ndvds6

Description: 5 does not divide 6. (Contributed by AV, 8-Sep-2025)

		Ref	Expression
	Assertion	5ndvds6	$⊢ \neg 5 ∥ 6$

Step	Hyp	Ref	Expression
1		5nn	$⊢ 5 \in ℕ$
2		1nn0	$⊢ 1 \in ℕ_{0}$
3		1nn	$⊢ 1 \in ℕ$
4		5cn	$⊢ 5 \in ℂ$
5	4	mulridi	$⊢ 5 \cdot 1 = 5$
6	5	oveq1i	$⊢ 5 \cdot 1 + 1 = 5 + 1$
7		5p1e6	$⊢ 5 + 1 = 6$
8	6 7	eqtri	$⊢ 5 \cdot 1 + 1 = 6$
9		1lt5	$⊢ 1 < 5$
10	1 2 3 8 9	ndvdsi	$⊢ \neg 5 ∥ 6$