ex-mod

		Ref	Expression
	Assertion	ex-mod	$⊢ (5 \mod 3 = 2 \land -7 \mod 2 = 1)$

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

Metamath Proof Explorer