Theorem sn-0ne2

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

	Ref	Expression
Assertion	sn-0ne2	$$⊢0\ne 2$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2		readdid2	$$⊢1\in ℝ\to 0+1=1$$
3	1 2	ax-mp	$$⊢0+1=1$$
4		sn-1ne2	$$⊢1\ne 2$$
5		2re	$$⊢2\in ℝ$$
6	1 5	lttri2i	$$⊢1\ne 2\leftrightarrow \left(1<2\vee 2<1\right)$$
7	4 6	mpbi	$$⊢\left(1<2\vee 2<1\right)$$
8		1red	$$⊢1<2\to 1\in ℝ$$
9	1 5 1	ltadd2i	$$⊢1<2\leftrightarrow 1+1<1+2$$
10	9	biimpi	$$⊢1<2\to 1+1<1+2$$
11		1p1e2	$$⊢1+1=2$$
12		1p2e3	$$⊢1+2=3$$
13	10 11 12	3brtr3g	$$⊢1<2\to 2<3$$
14		3re	$$⊢3\in ℝ$$
15	1 5 14	lttri	$$⊢\left(1<2\wedge 2<3\right)\to 1<3$$
16	13 15	mpdan	$$⊢1<2\to 1<3$$
17	8 16	ltned	$$⊢1<2\to 1\ne 3$$
18	14	a1i	$$⊢2<1\to 3\in ℝ$$
19	5 1 1	ltadd2i	$$⊢2<1\leftrightarrow 1+2<1+1$$
20	19	biimpi	$$⊢2<1\to 1+2<1+1$$
21	20 12 11	3brtr3g	$$⊢2<1\to 3<2$$
22	14 5 1	lttri	$$⊢\left(3<2\wedge 2<1\right)\to 3<1$$
23	21 22	mpancom	$$⊢2<1\to 3<1$$
24	18 23	gtned	$$⊢2<1\to 1\ne 3$$
25	17 24	jaoi	$$⊢\left(1<2\vee 2<1\right)\to 1\ne 3$$
26	7 25	ax-mp	$$⊢1\ne 3$$
27		df-3	$$⊢3=2+1$$
28	26 27	neeqtri	$$⊢1\ne 2+1$$
29	3 28	eqnetri	$$⊢0+1\ne 2+1$$
30		oveq1	$$⊢0=2\to 0+1=2+1$$
31	30	necon3i	$$⊢0+1\ne 2+1\to 0\ne 2$$
32	29 31	ax-mp	$$⊢0\ne 2$$