Theorem 5ndvds6

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

	Ref	Expression
Assertion	5ndvds6	|- -. 5 || 6

Proof

Step	Hyp	Ref	Expression
1		5nn	|- 5 e. NN
2		1nn0	|- 1 e. NN0
3		1nn	|- 1 e. NN
4		5cn	|- 5 e. CC
5	4	mulridi	|- ( 5 x. 1 ) = 5
6	5	oveq1i	|- ( ( 5 x. 1 ) + 1 ) = ( 5 + 1 )
7		5p1e6	|- ( 5 + 1 ) = 6
8	6 7	eqtri	|- ( ( 5 x. 1 ) + 1 ) = 6
9		1lt5	|- 1 < 5
10	1 2 3 8 9	ndvdsi	|- -. 5 || 6