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		0re	$$⊢0\in ℝ$$
2		lttri4	$$⊢\left(\mathrm{i}\in ℝ\wedge 0\in ℝ\right)\to \left(\mathrm{i}<0\vee \mathrm{i}=0\vee 0<\mathrm{i}\right)$$
3	1 2	mpan2	$$⊢\mathrm{i}\in ℝ\to \left(\mathrm{i}<0\vee \mathrm{i}=0\vee 0<\mathrm{i}\right)$$
4		reneg1lt0	$$⊢0{-}_{ℝ}1<0$$
5		1re	$$⊢1\in ℝ$$
6		rernegcl	$$⊢1\in ℝ\to 0{-}_{ℝ}1\in ℝ$$
7	5 6	ax-mp	$$⊢0{-}_{ℝ}1\in ℝ$$
8	7 1	ltnsymi	$$⊢0{-}_{ℝ}1<0\to \neg 0<0{-}_{ℝ}1$$
9	4 8	ax-mp	$$⊢\neg 0<0{-}_{ℝ}1$$
10		relt0neg1	$$⊢\mathrm{i}\in ℝ\to \left(\mathrm{i}<0\leftrightarrow 0<0{-}_{ℝ}\mathrm{i}\right)$$
11		rernegcl	$$⊢\mathrm{i}\in ℝ\to 0{-}_{ℝ}\mathrm{i}\in ℝ$$
12		mulgt0	$$⊢\left(\left(0{-}_{ℝ}\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\wedge \left(0{-}_{ℝ}\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\right)\to 0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)$$
13	12	anidms	$$⊢\left(0{-}_{ℝ}\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\to 0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)$$
14	11 13	sylan	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\to 0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)$$
15		id	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\in ℝ$$
16	11 15	remulneg2d	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)=0{-}_{ℝ}\left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}$$
17	15 15	remulcld	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\in ℝ$$
18	15 17	remulcld	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\in ℝ$$
19		ipiiie0	$$⊢\mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=0$$
20		renegadd	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}\mathrm{i}\mathrm{i}\in ℝ\right)\to \left(0{-}_{ℝ}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\leftrightarrow \mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=0\right)$$
21	19 20	mpbiri	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}\mathrm{i}\mathrm{i}\in ℝ\right)\to 0{-}_{ℝ}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
22	18 21	mpdan	$$⊢\mathrm{i}\in ℝ\to 0{-}_{ℝ}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
23	22	oveq1d	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
24		ax-icn	$$⊢\mathrm{i}\in ℂ$$
25	24 24 24	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
26	25	oveq1i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
27	24 24	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
28	27 24 24	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
29	26 28	eqtr3i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
30	29	a1i	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
31		rei4	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$
32	31	a1i	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$
33	23 30 32	3eqtrd	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=1$$
34	33	oveq2d	$$⊢\mathrm{i}\in ℝ\to 0{-}_{ℝ}\left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=0{-}_{ℝ}1$$
35	16 34	eqtrd	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)=0{-}_{ℝ}1$$
36	35	breq2d	$$⊢\mathrm{i}\in ℝ\to \left(0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)\leftrightarrow 0<0{-}_{ℝ}1\right)$$
37	36	adantr	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\to \left(0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)\leftrightarrow 0<0{-}_{ℝ}1\right)$$
38	14 37	mpbid	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\to 0<0{-}_{ℝ}1$$
39	38	ex	$$⊢\mathrm{i}\in ℝ\to \left(0<0{-}_{ℝ}\mathrm{i}\to 0<0{-}_{ℝ}1\right)$$
40	10 39	sylbid	$$⊢\mathrm{i}\in ℝ\to \left(\mathrm{i}<0\to 0<0{-}_{ℝ}1\right)$$
41	9 40	mtoi	$$⊢\mathrm{i}\in ℝ\to \neg \mathrm{i}<0$$
42		0ne1	$$⊢0\ne 1$$
43	42	neii	$$⊢\neg 0=1$$
44		oveq12	$$⊢\left(\mathrm{i}=0\wedge \mathrm{i}=0\right)\to \mathrm{i}\mathrm{i}=0\cdot 0$$
45	44	anidms	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}=0\cdot 0$$
46	45	oveq1d	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}+1=0\cdot 0+1$$
47		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
48		remul02	$$⊢0\in ℝ\to 0\cdot 0=0$$
49	1 48	ax-mp	$$⊢0\cdot 0=0$$
50	49	oveq1i	$$⊢0\cdot 0+1=0+1$$
51		readdlid	$$⊢1\in ℝ\to 0+1=1$$
52	5 51	ax-mp	$$⊢0+1=1$$
53	50 52	eqtri	$$⊢0\cdot 0+1=1$$
54	46 47 53	3eqtr3g	$$⊢\mathrm{i}=0\to 0=1$$
55	43 54	mto	$$⊢\neg \mathrm{i}=0$$
56	55	a1i	$$⊢\mathrm{i}\in ℝ\to \neg \mathrm{i}=0$$
57		mulgt0	$$⊢\left(\left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\wedge \left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\right)\to 0<\mathrm{i}\mathrm{i}$$
58	57	anidms	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\to 0<\mathrm{i}\mathrm{i}$$
59		reixi	$$⊢\mathrm{i}\mathrm{i}=0{-}_{ℝ}1$$
60	58 59	breqtrdi	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\to 0<0{-}_{ℝ}1$$
61	60	ex	$$⊢\mathrm{i}\in ℝ\to \left(0<\mathrm{i}\to 0<0{-}_{ℝ}1\right)$$
62	9 61	mtoi	$$⊢\mathrm{i}\in ℝ\to \neg 0<\mathrm{i}$$
63		3ioran	$$⊢\neg \left(\mathrm{i}<0\vee \mathrm{i}=0\vee 0<\mathrm{i}\right)\leftrightarrow \left(\neg \mathrm{i}<0\wedge \neg \mathrm{i}=0\wedge \neg 0<\mathrm{i}\right)$$
64	41 56 62 63	syl3anbrc	$$⊢\mathrm{i}\in ℝ\to \neg \left(\mathrm{i}<0\vee \mathrm{i}=0\vee 0<\mathrm{i}\right)$$
65	3 64	pm2.65i	$$⊢\neg \mathrm{i}\in ℝ$$