Theorem sn-inelr

Description: inelr without ax-mulcom . (Contributed by SN, 1-Jun-2024)

	Ref	Expression
Assertion	sn-inelr	$$⊢\neg \mathrm{i}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		reneg1lt0	$$⊢0{-}_{ℝ}1<0$$
2		1re	$$⊢1\in ℝ$$
3		rernegcl	$$⊢1\in ℝ\to 0{-}_{ℝ}1\in ℝ$$
4	2 3	ax-mp	$$⊢0{-}_{ℝ}1\in ℝ$$
5		0re	$$⊢0\in ℝ$$
6	4 5	ltnsymi	$$⊢0{-}_{ℝ}1<0\to \neg 0<0{-}_{ℝ}1$$
7	1 6	ax-mp	$$⊢\neg 0<0{-}_{ℝ}1$$
8		reixi	$$⊢\mathrm{i}\mathrm{i}=0{-}_{ℝ}1$$
9	8	breq2i	$$⊢0<\mathrm{i}\mathrm{i}\leftrightarrow 0<0{-}_{ℝ}1$$
10	7 9	mtbir	$$⊢\neg 0<\mathrm{i}\mathrm{i}$$
11		id	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\in ℝ$$
12		0ne1	$$⊢0\ne 1$$
13	12	a1i	$$⊢\mathrm{i}\in ℝ\to 0\ne 1$$
14		id	$$⊢\mathrm{i}=0\to \mathrm{i}=0$$
15	14 14	oveq12d	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}=0\cdot 0$$
16	15	oveq1d	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}+1=0\cdot 0+1$$
17		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
18		remul02	$$⊢0\in ℝ\to 0\cdot 0=0$$
19	5 18	ax-mp	$$⊢0\cdot 0=0$$
20	19	oveq1i	$$⊢0\cdot 0+1=0+1$$
21		readdlid	$$⊢1\in ℝ\to 0+1=1$$
22	2 21	ax-mp	$$⊢0+1=1$$
23	20 22	eqtri	$$⊢0\cdot 0+1=1$$
24	16 17 23	3eqtr3g	$$⊢\mathrm{i}=0\to 0=1$$
25	24	adantl	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}=0\right)\to 0=1$$
26	13 25	mteqand	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\ne 0$$
27	11 26	sn-msqgt0d	$$⊢\mathrm{i}\in ℝ\to 0<\mathrm{i}\mathrm{i}$$
28	10 27	mto	$$⊢\neg \mathrm{i}\in ℝ$$