# Metamath Proof Explorer

## 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 {ℕ}_{0}$
5 3nn ${⊢}3\in ℕ$
6 2lt3 ${⊢}2<3$
7 addmodid ${⊢}\left(2\in {ℕ}_{0}\wedge 3\in ℕ\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 ℕ$
14 1lt2 ${⊢}1<2$
15 eluz2b2 ${⊢}2\in {ℤ}_{\ge 2}↔\left(2\in ℕ\wedge 1<2\right)$
16 13 14 15 mpbir2an ${⊢}2\in {ℤ}_{\ge 2}$
17 7prm ${⊢}7\in ℙ$
18 dvdsprm ${⊢}\left(2\in {ℤ}_{\ge 2}\wedge 7\in ℙ\right)\to \left(2\parallel 7↔2=7\right)$
19 16 17 18 mp2an ${⊢}2\parallel 7↔2=7$
20 12 19 nemtbir ${⊢}¬2\parallel 7$
21 2z ${⊢}2\in ℤ$
22 7nn ${⊢}7\in ℕ$
23 22 nnzi ${⊢}7\in ℤ$
24 dvdsnegb ${⊢}\left(2\in ℤ\wedge 7\in ℤ\right)\to \left(2\parallel 7↔2\parallel -7\right)$
25 21 23 24 mp2an ${⊢}2\parallel 7↔2\parallel -7$
26 20 25 mtbi ${⊢}¬2\parallel -7$
27 znegcl ${⊢}7\in ℤ\to -7\in ℤ$
28 mod2eq1n2dvds ${⊢}-7\in ℤ\to \left(-7\mathrm{mod}2=1↔¬2\parallel -7\right)$
29 23 27 28 mp2b ${⊢}-7\mathrm{mod}2=1↔¬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)$