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 /\ ( -u 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 e. NN0
5 3nn 
 |-  3 e. NN
6 2lt3 
 |-  2 < 3
7 addmodid 
 |-  ( ( 2 e. NN0 /\ 3 e. NN /\ 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 e. RR
11 2lt7 
 |-  2 < 7
12 10 11 ltneii 
 |-  2 =/= 7
13 2nn 
 |-  2 e. NN
14 1lt2 
 |-  1 < 2
15 eluz2b2 
 |-  ( 2 e. ( ZZ>= ` 2 ) <-> ( 2 e. NN /\ 1 < 2 ) )
16 13 14 15 mpbir2an 
 |-  2 e. ( ZZ>= ` 2 )
17 7prm 
 |-  7 e. Prime
18 dvdsprm 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 7 e. Prime ) -> ( 2 || 7 <-> 2 = 7 ) )
19 16 17 18 mp2an 
 |-  ( 2 || 7 <-> 2 = 7 )
20 12 19 nemtbir 
 |-  -. 2 || 7
21 2z 
 |-  2 e. ZZ
22 7nn 
 |-  7 e. NN
23 22 nnzi 
 |-  7 e. ZZ
24 dvdsnegb 
 |-  ( ( 2 e. ZZ /\ 7 e. ZZ ) -> ( 2 || 7 <-> 2 || -u 7 ) )
25 21 23 24 mp2an 
 |-  ( 2 || 7 <-> 2 || -u 7 )
26 20 25 mtbi 
 |-  -. 2 || -u 7
27 znegcl 
 |-  ( 7 e. ZZ -> -u 7 e. ZZ )
28 mod2eq1n2dvds 
 |-  ( -u 7 e. ZZ -> ( ( -u 7 mod 2 ) = 1 <-> -. 2 || -u 7 ) )
29 23 27 28 mp2b 
 |-  ( ( -u 7 mod 2 ) = 1 <-> -. 2 || -u 7 )
30 26 29 mpbir 
 |-  ( -u 7 mod 2 ) = 1
31 9 30 pm3.2i 
 |-  ( ( 5 mod 3 ) = 2 /\ ( -u 7 mod 2 ) = 1 )