Theorem 3ndvds4

Description: 3 does not divide 4. (Contributed by AV, 18-Aug-2021)

	Ref	Expression
Assertion	3ndvds4	$$⊢\neg 3\parallel 4$$

Proof

Step	Hyp	Ref	Expression
1		3nn	$$⊢3\in \mathbb{N}$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		1nn	$$⊢1\in \mathbb{N}$$
4		3t1e3	$$⊢3\cdot 1=3$$
5	4	oveq1i	$$⊢3\cdot 1+1=3+1$$
6		3p1e4	$$⊢3+1=4$$
7	5 6	eqtri	$$⊢3\cdot 1+1=4$$
8		1lt3	$$⊢1<3$$
9	1 2 3 7 8	ndvdsi	$$⊢\neg 3\parallel 4$$