Theorem 5ndvds3

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

	Ref	Expression
Assertion	5ndvds3	⊢ ¬ 5 ∥ 3

Proof

Step	Hyp	Ref	Expression
1		5nn	⊢ 5 ∈ ℕ
2		0nn0	⊢ 0 ∈ ℕ0
3		3nn	⊢ 3 ∈ ℕ
4		5cn	⊢ 5 ∈ ℂ
5	4	mul01i	⊢ ( 5 · 0 ) = 0
6	5	oveq1i	⊢ ( ( 5 · 0 ) + 3 ) = ( 0 + 3 )
7		3cn	⊢ 3 ∈ ℂ
8	7	addlidi	⊢ ( 0 + 3 ) = 3
9	6 8	eqtri	⊢ ( ( 5 · 0 ) + 3 ) = 3
10		3lt5	⊢ 3 < 5
11	1 2 3 9 10	ndvdsi	⊢ ¬ 5 ∥ 3