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 ∈ ℕ
2		1nn0	⊢ 1 ∈ ℕ0
3		1nn	⊢ 1 ∈ ℕ
4		3t1e3	⊢ ( 3 · 1 ) = 3
5	4	oveq1i	⊢ ( ( 3 · 1 ) + 1 ) = ( 3 + 1 )
6		3p1e4	⊢ ( 3 + 1 ) = 4
7	5 6	eqtri	⊢ ( ( 3 · 1 ) + 1 ) = 4
8		1lt3	⊢ 1 < 3
9	1 2 3 7 8	ndvdsi	⊢ ¬ 3 ∥ 4