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 ∈ ℕ
2		1nn0	⊢ 1 ∈ ℕ0
3		1nn	⊢ 1 ∈ ℕ
4		5cn	⊢ 5 ∈ ℂ
5	4	mulridi	⊢ ( 5 · 1 ) = 5
6	5	oveq1i	⊢ ( ( 5 · 1 ) + 1 ) = ( 5 + 1 )
7		5p1e6	⊢ ( 5 + 1 ) = 6
8	6 7	eqtri	⊢ ( ( 5 · 1 ) + 1 ) = 6
9		1lt5	⊢ 1 < 5
10	1 2 3 8 9	ndvdsi	⊢ ¬ 5 ∥ 6