Metamath Proof Explorer

Theorem usgrexmpldifpr

Description: Lemma for usgrexmpledg : all "edges" are different. (Contributed by Alexander van der Vekens, 15-Aug-2017)

Ref Expression
Assertion usgrexmpldifpr ⊢ 0 1 ≠ 1 2 ∧ 0 1 ≠ 2 0 ∧ 0 1 ≠ 0 3 ∧ 1 2 ≠ 2 0 ∧ 1 2 ≠ 0 3 ∧ 2 0 ≠ 0 3

Proof

Step Hyp Ref Expression
1 0z ⊢ 0 ∈ ℤ
2 1z ⊢ 1 ∈ ℤ
3 1 2 pm3.2i ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ
4 2z ⊢ 2 ∈ ℤ
5 2 4 pm3.2i ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ
6 3 5 pm3.2i ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ
7 ax-1ne0 ⊢ 1 ≠ 0
8 7 necomi ⊢ 0 ≠ 1
9 2ne0 ⊢ 2 ≠ 0
10 9 necomi ⊢ 0 ≠ 2
11 8 10 pm3.2i ⊢ 0 ≠ 1 ∧ 0 ≠ 2
12 11 orci ⊢ 0 ≠ 1 ∧ 0 ≠ 2 ∨ 1 ≠ 1 ∧ 1 ≠ 2
13 prneimg ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ → 0 ≠ 1 ∧ 0 ≠ 2 ∨ 1 ≠ 1 ∧ 1 ≠ 2 → 0 1 ≠ 1 2
14 6 12 13 mp2 ⊢ 0 1 ≠ 1 2
15 4 1 pm3.2i ⊢ 2 ∈ ℤ ∧ 0 ∈ ℤ
16 3 15 pm3.2i ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ
17 1ne2 ⊢ 1 ≠ 2
18 17 7 pm3.2i ⊢ 1 ≠ 2 ∧ 1 ≠ 0
19 18 olci ⊢ 0 ≠ 2 ∧ 0 ≠ 0 ∨ 1 ≠ 2 ∧ 1 ≠ 0
20 prneimg ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ → 0 ≠ 2 ∧ 0 ≠ 0 ∨ 1 ≠ 2 ∧ 1 ≠ 0 → 0 1 ≠ 2 0
21 16 19 20 mp2 ⊢ 0 1 ≠ 2 0
22 3nn ⊢ 3 ∈ ℕ
23 1 22 pm3.2i ⊢ 0 ∈ ℤ ∧ 3 ∈ ℕ
24 3 23 pm3.2i ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ
25 1re ⊢ 1 ∈ ℝ
26 1lt3 ⊢ 1 < 3
27 25 26 ltneii ⊢ 1 ≠ 3
28 7 27 pm3.2i ⊢ 1 ≠ 0 ∧ 1 ≠ 3
29 28 olci ⊢ 0 ≠ 0 ∧ 0 ≠ 3 ∨ 1 ≠ 0 ∧ 1 ≠ 3
30 prneimg ⊢ 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ → 0 ≠ 0 ∧ 0 ≠ 3 ∨ 1 ≠ 0 ∧ 1 ≠ 3 → 0 1 ≠ 0 3
31 24 29 30 mp2 ⊢ 0 1 ≠ 0 3
32 14 21 31 3pm3.2i ⊢ 0 1 ≠ 1 2 ∧ 0 1 ≠ 2 0 ∧ 0 1 ≠ 0 3
33 5 15 pm3.2i ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ
34 18 orci ⊢ 1 ≠ 2 ∧ 1 ≠ 0 ∨ 2 ≠ 2 ∧ 2 ≠ 0
35 prneimg ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ → 1 ≠ 2 ∧ 1 ≠ 0 ∨ 2 ≠ 2 ∧ 2 ≠ 0 → 1 2 ≠ 2 0
36 33 34 35 mp2 ⊢ 1 2 ≠ 2 0
37 5 23 pm3.2i ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ
38 28 orci ⊢ 1 ≠ 0 ∧ 1 ≠ 3 ∨ 2 ≠ 0 ∧ 2 ≠ 3
39 prneimg ⊢ 1 ∈ ℤ ∧ 2 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ → 1 ≠ 0 ∧ 1 ≠ 3 ∨ 2 ≠ 0 ∧ 2 ≠ 3 → 1 2 ≠ 0 3
40 37 38 39 mp2 ⊢ 1 2 ≠ 0 3
41 15 23 pm3.2i ⊢ 2 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ
42 2re ⊢ 2 ∈ ℝ
43 2lt3 ⊢ 2 < 3
44 42 43 ltneii ⊢ 2 ≠ 3
45 9 44 pm3.2i ⊢ 2 ≠ 0 ∧ 2 ≠ 3
46 45 orci ⊢ 2 ≠ 0 ∧ 2 ≠ 3 ∨ 0 ≠ 0 ∧ 0 ≠ 3
47 prneimg ⊢ 2 ∈ ℤ ∧ 0 ∈ ℤ ∧ 0 ∈ ℤ ∧ 3 ∈ ℕ → 2 ≠ 0 ∧ 2 ≠ 3 ∨ 0 ≠ 0 ∧ 0 ≠ 3 → 2 0 ≠ 0 3
48 41 46 47 mp2 ⊢ 2 0 ≠ 0 3
49 36 40 48 3pm3.2i ⊢ 1 2 ≠ 2 0 ∧ 1 2 ≠ 0 3 ∧ 2 0 ≠ 0 3
50 32 49 pm3.2i ⊢ 0 1 ≠ 1 2 ∧ 0 1 ≠ 2 0 ∧ 0 1 ≠ 0 3 ∧ 1 2 ≠ 2 0 ∧ 1 2 ≠ 0 3 ∧ 2 0 ≠ 0 3