Theorem 5ndvds3

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

	Ref	Expression
Assertion	5ndvds3	$$⊢\neg 5\parallel 3$$

Proof

Step	Hyp	Ref	Expression
1		5nn	$$⊢5\in \mathbb{N}$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3		3nn	$$⊢3\in \mathbb{N}$$
4		5cn	$$⊢5\in ℂ$$
5	4	mul01i	$$⊢5\cdot 0=0$$
6	5	oveq1i	$$⊢5\cdot 0+3=0+3$$
7		3cn	$$⊢3\in ℂ$$
8	7	addlidi	$$⊢0+3=3$$
9	6 8	eqtri	$$⊢5\cdot 0+3=3$$
10		3lt5	$$⊢3<5$$
11	1 2 3 9 10	ndvdsi	$$⊢\neg 5\parallel 3$$