Metamath Proof Explorer


Theorem 3ndvds4

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

Ref Expression
Assertion 3ndvds4 ¬34

Proof

Step Hyp Ref Expression
1 3nn 3
2 1nn0 10
3 1nn 1
4 3t1e3 31=3
5 4 oveq1i 31+1=3+1
6 3p1e4 3+1=4
7 5 6 eqtri 31+1=4
8 1lt3 1<3
9 1 2 3 7 8 ndvdsi ¬34