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	mp1i	$$⊢1<0\to 0{-}_{ℝ}1\in ℝ$$
8		relt0neg1	$$⊢1\in ℝ\to \left(1<0\leftrightarrow 0<0{-}_{ℝ}1\right)$$
9	2 8	ax-mp	$$⊢1<0\leftrightarrow 0<0{-}_{ℝ}1$$
10	9	biimpi	$$⊢1<0\to 0<0{-}_{ℝ}1$$
11	7 7 10 10	mulgt0d	$$⊢1<0\to 0<\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)$$
12		1red	$$⊢1\in ℝ\to 1\in ℝ$$
13	6 12	remulneg2d	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1$$
14		ax-1rid	$$⊢0{-}_{ℝ}1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
15	6 14	syl	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}1$$
16	15	oveq2d	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)\cdot 1=0{-}_{ℝ}\left(0{-}_{ℝ}1\right)$$
17		renegneg	$$⊢1\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}1\right)=1$$
18	13 16 17	3eqtrd	$$⊢1\in ℝ\to \left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
19	2 18	ax-mp	$$⊢\left(0{-}_{ℝ}1\right)\left(0{-}_{ℝ}1\right)=1$$
20	11 19	breqtrdi	$$⊢1<0\to 0<1$$
21		id	$$⊢0<1\to 0<1$$
22	20 21	jaoi	$$⊢\left(1<0\vee 0<1\right)\to 0<1$$
23	5 22	ax-mp	$$⊢0<1$$