Theorem sn-0lt1

Description: 0lt1 without ax-mulcom . (Contributed by SN, 13-Feb-2024)

	Ref	Expression
Assertion	sn-0lt1	$$⊢0<1$$

Proof

Step	Hyp	Ref	Expression
1		ax-1ne0	$$⊢1\ne 0$$
2		1re	$$⊢1\in ℝ$$
3		0re	$$⊢0\in ℝ$$
4	2 3	lttri2i	$$⊢1\ne 0\leftrightarrow \left(1<0\vee 0<1\right)$$
5	1 4	mpbi	$$⊢\left(1<0\vee 0<1\right)$$
6		rernegcl	$$⊢1\in ℝ\to 0{-}_{ℝ}1\in ℝ$$
7	2 6	ax-mp	$$⊢0{-}_{ℝ}1\in ℝ$$
8	7	a1i	$$⊢1<0\to 0{-}_{ℝ}1\in ℝ$$
9		relt0neg1	$$⊢1\in ℝ\to \left(1<0\leftrightarrow 0<0{-}_{ℝ}1\right)$$
10	2 9	ax-mp	$$⊢1<0\leftrightarrow 0<0{-}_{ℝ}1$$
11	10	biimpi	$$⊢1<0\to 0<0{-}_{ℝ}1$$
12	8 8 11 11	mulgt0d	$$⊢1<0\to 0<\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)$$
13		resubdi	$$⊢\left(0{-}_{ℝ}1\in ℝ\wedge 0\in ℝ\wedge 1\in ℝ\right)\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
14	7 3 2 13	mp3an	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
15		remul01	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 0=0$$
16	7 15	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\cdot 0=0$$
17		ax-1rid	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
18	7 17	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
19	16 18	oveq12i	$$⊢\left(0{-}_{ℝ}1\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)$$
20		renegneg	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
21	2 20	ax-mp	$$⊢0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
22	14 19 21	3eqtri	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
23	12 22	breqtrdi	$$⊢1<0\to 0<1$$
24		id	$$⊢0<1\to 0<1$$
25	23 24	jaoi	$$⊢\left(1<0\vee 0<1\right)\to 0<1$$
26	5 25	ax-mp	$$⊢0<1$$