Theorem 3ndvds4

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

	Ref	Expression
Assertion	3ndvds4	|- -. 3 || 4

Proof

Step	Hyp	Ref	Expression
1		3nn	|- 3 e. NN
2		1nn0	|- 1 e. NN0
3		1nn	|- 1 e. NN
4		3t1e3	|- ( 3 x. 1 ) = 3
5	4	oveq1i	|- ( ( 3 x. 1 ) + 1 ) = ( 3 + 1 )
6		3p1e4	|- ( 3 + 1 ) = 4
7	5 6	eqtri	|- ( ( 3 x. 1 ) + 1 ) = 4
8		1lt3	|- 1 < 3
9	1 2 3 7 8	ndvdsi	|- -. 3 || 4