| 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 ) |