Theorem 5ndvds6

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

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

Proof

Step	Hyp	Ref	Expression
1		5nn	$$⊢5\in \mathbb{N}$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		1nn	$$⊢1\in \mathbb{N}$$
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\parallel 6$$