Theorem ex-mod

Description: Example for df-mod . (Contributed by AV, 3-Sep-2021)

	Ref	Expression
Assertion	ex-mod	$$⊢\left(5\mathrm{mod}3=2\wedge -7\mathrm{mod}2=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		3p2e5	$$⊢3+2=5$$
2	1	eqcomi	$$⊢5=3+2$$
3	2	oveq1i	$$⊢5\mathrm{mod}3=\left(3+2\right)\mathrm{mod}3$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		3nn	$$⊢3\in \mathbb{N}$$
6		2lt3	$$⊢2<3$$
7		addmodid	$$⊢\left(2\in {\mathbb{N}}_0\wedge 3\in \mathbb{N}\wedge 2<3\right)\to \left(3+2\right)\mathrm{mod}3=2$$
8	4 5 6 7	mp3an	$$⊢\left(3+2\right)\mathrm{mod}3=2$$
9	3 8	eqtri	$$⊢5\mathrm{mod}3=2$$
10		2re	$$⊢2\in ℝ$$
11		2lt7	$$⊢2<7$$
12	10 11	ltneii	$$⊢2\ne 7$$
13		2nn	$$⊢2\in \mathbb{N}$$
14		1lt2	$$⊢1<2$$
15		eluz2b2	$$⊢2\in {\mathbb{Z}}_{\ge 2}\leftrightarrow \left(2\in \mathbb{N}\wedge 1<2\right)$$
16	13 14 15	mpbir2an	$$⊢2\in {\mathbb{Z}}_{\ge 2}$$
17		7prm	$$⊢7\in \mathbb{P}$$
18		dvdsprm	$$⊢\left(2\in {\mathbb{Z}}_{\ge 2}\wedge 7\in \mathbb{P}\right)\to \left(2\parallel 7\leftrightarrow 2=7\right)$$
19	16 17 18	mp2an	$$⊢2\parallel 7\leftrightarrow 2=7$$
20	12 19	nemtbir	$$⊢\neg 2\parallel 7$$
21		2z	$$⊢2\in \mathbb{Z}$$
22		7nn	$$⊢7\in \mathbb{N}$$
23	22	nnzi	$$⊢7\in \mathbb{Z}$$
24		dvdsnegb	$$⊢\left(2\in \mathbb{Z}\wedge 7\in \mathbb{Z}\right)\to \left(2\parallel 7\leftrightarrow 2\parallel -7\right)$$
25	21 23 24	mp2an	$$⊢2\parallel 7\leftrightarrow 2\parallel -7$$
26	20 25	mtbi	$$⊢\neg 2\parallel -7$$
27		znegcl	$$⊢7\in \mathbb{Z}\to -7\in \mathbb{Z}$$
28		mod2eq1n2dvds	$$⊢-7\in \mathbb{Z}\to \left(-7\mathrm{mod}2=1\leftrightarrow \neg 2\parallel -7\right)$$
29	23 27 28	mp2b	$$⊢-7\mathrm{mod}2=1\leftrightarrow \neg 2\parallel -7$$
30	26 29	mpbir	$$⊢-7\mathrm{mod}2=1$$
31	9 30	pm3.2i	$$⊢\left(5\mathrm{mod}3=2\wedge -7\mathrm{mod}2=1\right)$$