This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-0ne2

Description: 0ne2 without ax-mulcom . (Contributed by SN, 23-Jan-2024)

Ref Expression
Assertion sn-0ne2 ⊢ 0 ≠ 2

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 readdlid ⊢ 1 ∈ ℝ → 0 + 1 = 1
3 1 2 ax-mp ⊢ 0 + 1 = 1
4 sn-1ne2 ⊢ 1 ≠ 2
5 2re ⊢ 2 ∈ ℝ
6 1 5 lttri2i ⊢ 1 ≠ 2 ↔ 1 < 2 ∨ 2 < 1
7 4 6 mpbi ⊢ 1 < 2 ∨ 2 < 1
8 1red ⊢ 1 < 2 → 1 ∈ ℝ
9 1 5 1 ltadd2i ⊢ 1 < 2 ↔ 1 + 1 < 1 + 2
10 9 biimpi ⊢ 1 < 2 → 1 + 1 < 1 + 2
11 1p1e2 ⊢ 1 + 1 = 2
12 1p2e3 ⊢ 1 + 2 = 3
13 10 11 12 3brtr3g ⊢ 1 < 2 → 2 < 3
14 3re ⊢ 3 ∈ ℝ
15 1 5 14 lttri ⊢ 1 < 2 ∧ 2 < 3 → 1 < 3
16 13 15 mpdan ⊢ 1 < 2 → 1 < 3
17 8 16 ltned ⊢ 1 < 2 → 1 ≠ 3
18 14 a1i ⊢ 2 < 1 → 3 ∈ ℝ
19 5 1 1 ltadd2i ⊢ 2 < 1 ↔ 1 + 2 < 1 + 1
20 19 biimpi ⊢ 2 < 1 → 1 + 2 < 1 + 1
21 20 12 11 3brtr3g ⊢ 2 < 1 → 3 < 2
22 14 5 1 lttri ⊢ 3 < 2 ∧ 2 < 1 → 3 < 1
23 21 22 mpancom ⊢ 2 < 1 → 3 < 1
24 18 23 gtned ⊢ 2 < 1 → 1 ≠ 3
25 17 24 jaoi ⊢ 1 < 2 ∨ 2 < 1 → 1 ≠ 3
26 7 25 ax-mp ⊢ 1 ≠ 3
27 df-3 ⊢ 3 = 2 + 1
28 26 27 neeqtri ⊢ 1 ≠ 2 + 1
29 3 28 eqnetri ⊢ 0 + 1 ≠ 2 + 1
30 oveq1 ⊢ 0 = 2 → 0 + 1 = 2 + 1
31 30 necon3i ⊢ 0 + 1 ≠ 2 + 1 → 0 ≠ 2
32 29 31 ax-mp ⊢ 0 ≠ 2