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 e. NN0
5		5nn	|- 5 e. NN
6		3lt5	|- 3 < 5
7		addmodid	|- ( ( 3 e. NN0 /\ 5 e. NN /\ 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