Theorem 8mod5e3

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

	Ref	Expression
Assertion	8mod5e3	$$⊢8\mathrm{mod}5=3$$

Proof

Step	Hyp	Ref	Expression
1		5p3e8	$$⊢5+3=8$$
2	1	eqcomi	$$⊢8=5+3$$
3	2	oveq1i	$$⊢8\mathrm{mod}5=\left(5+3\right)\mathrm{mod}5$$
4		3nn0	$$⊢3\in {\mathbb{N}}_0$$
5		5nn	$$⊢5\in \mathbb{N}$$
6		3lt5	$$⊢3<5$$
7		addmodid	$$⊢\left(3\in {\mathbb{N}}_0\wedge 5\in \mathbb{N}\wedge 3<5\right)\to \left(5+3\right)\mathrm{mod}5=3$$
8	4 5 6 7	mp3an	$$⊢\left(5+3\right)\mathrm{mod}5=3$$
9	3 8	eqtri	$$⊢8\mathrm{mod}5=3$$