Theorem 8mod5e3

Description: 8 modulo 5 is 3. (Contributed by AV, 20-Nov-2025)

	Ref	Expression
Assertion	8mod5e3	⊢ ( 8 mod 5 ) = 3

Proof

Step	Hyp	Ref	Expression
1		5p3e8	⊢ ( 5 + 3 ) = 8
2	1	eqcomi	⊢ 8 = ( 5 + 3 )
3	2	oveq1i	⊢ ( 8 mod 5 ) = ( ( 5 + 3 ) mod 5 )
4		3nn0	⊢ 3 ∈ ℕ0
5		5nn	⊢ 5 ∈ ℕ
6		3lt5	⊢ 3 < 5
7		addmodid	⊢ ( ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ ∧ 3 < 5 ) → ( ( 5 + 3 ) mod 5 ) = 3 )
8	4 5 6 7	mp3an	⊢ ( ( 5 + 3 ) mod 5 ) = 3
9	3 8	eqtri	⊢ ( 8 mod 5 ) = 3