Metamath Proof Explorer

Theorem ex-mod

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

Ref Expression
Assertion ex-mod ( ( 5 mod 3 ) = 2 ∧ ( - 7 mod 2 ) = 1 )

Proof

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 ∈ ℕ0
5 3nn ⊢ 3 ∈ ℕ
6 2lt3 ⊢ 2 < 3
7 addmodid ⊢ ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3 ) → ( ( 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 ∈ ℝ
11 2lt7 ⊢ 2 < 7
12 10 11 ltneii ⊢ 2 ≠ 7
13 2nn ⊢ 2 ∈ ℕ
14 1lt2 ⊢ 1 < 2
15 eluz2b2 ⊢ ( 2 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℕ ∧ 1 < 2 ) )
16 13 14 15 mpbir2an ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
17 7prm ⊢ 7 ∈ ℙ
18 dvdsprm ⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 7 ∈ ℙ ) → ( 2 ∥ 7 ↔ 2 = 7 ) )
19 16 17 18 mp2an ⊢ ( 2 ∥ 7 ↔ 2 = 7 )
20 12 19 nemtbir ⊢ ¬ 2 ∥ 7
21 2z ⊢ 2 ∈ ℤ
22 7nn ⊢ 7 ∈ ℕ
23 22 nnzi ⊢ 7 ∈ ℤ
24 dvdsnegb ⊢ ( ( 2 ∈ ℤ ∧ 7 ∈ ℤ ) → ( 2 ∥ 7 ↔ 2 ∥ - 7 ) )
25 21 23 24 mp2an ⊢ ( 2 ∥ 7 ↔ 2 ∥ - 7 )
26 20 25 mtbi ⊢ ¬ 2 ∥ - 7
27 znegcl ⊢ ( 7 ∈ ℤ → - 7 ∈ ℤ )
28 mod2eq1n2dvds ⊢ ( - 7 ∈ ℤ → ( ( - 7 mod 2 ) = 1 ↔ ¬ 2 ∥ - 7 ) )
29 23 27 28 mp2b ⊢ ( ( - 7 mod 2 ) = 1 ↔ ¬ 2 ∥ - 7 )
30 26 29 mpbir ⊢ ( - 7 mod 2 ) = 1
31 9 30 pm3.2i ⊢ ( ( 5 mod 3 ) = 2 ∧ ( - 7 mod 2 ) = 1 )