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		readdid2	⊢ ( 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