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 ⊢01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03

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→01≠12
14 6 12 13 mp2 ⊢01≠12
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→01≠20
21 16 19 20 mp2 ⊢01≠20
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→01≠03
31 24 29 30 mp2 ⊢01≠03
32 14 21 31 3pm3.2i ⊢01≠12∧01≠20∧01≠03
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→12≠20
36 33 34 35 mp2 ⊢12≠20
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→12≠03
40 37 38 39 mp2 ⊢12≠03
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→20≠03
48 41 46 47 mp2 ⊢20≠03
49 36 40 48 3pm3.2i ⊢12≠20∧12≠03∧20≠03
50 32 49 pm3.2i ⊢01≠12∧01≠20∧01≠03∧12≠20∧12≠03∧20≠03