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		elre0re	$$⊢\mathrm{i}\in ℝ\to 0\in ℝ$$
16		id	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\in ℝ$$
17		resubdi	$$⊢\left(0{-}_{ℝ}\mathrm{i}\in ℝ\wedge 0\in ℝ\wedge \mathrm{i}\in ℝ\right)\to \left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)=\left(0{-}_{ℝ}\mathrm{i}\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}$$
18	11 15 16 17	syl3anc	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)=\left(0{-}_{ℝ}\mathrm{i}\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}$$
19		remul01	$$⊢0{-}_{ℝ}\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\cdot 0=0$$
20	11 19	syl	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\cdot 0=0$$
21	16 16	remulcld	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\in ℝ$$
22	16 21	remulcld	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\in ℝ$$
23		ipiiie0	$$⊢\mathrm{i}+\mathrm{i}\mathrm{i}\mathrm{i}=0$$
24		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)$$
25	23 24	mpbiri	$$⊢\left(\mathrm{i}\in ℝ\wedge \mathrm{i}\mathrm{i}\mathrm{i}\in ℝ\right)\to 0{-}_{ℝ}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
26	22 25	mpdan	$$⊢\mathrm{i}\in ℝ\to 0{-}_{ℝ}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
27	26	oveq1d	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
28		ax-icn	$$⊢\mathrm{i}\in ℂ$$
29	28 28 28	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}$$
30	29	oveq1i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
31	28 28	mulcli	$$⊢\mathrm{i}\mathrm{i}\in ℂ$$
32	31 28 28	mulassi	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
33	30 32	eqtr3i	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
34	33	a1i	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}$$
35		rei4	$$⊢\mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$
36	35	a1i	$$⊢\mathrm{i}\in ℝ\to \mathrm{i}\mathrm{i}\mathrm{i}\mathrm{i}=1$$
37	27 34 36	3eqtrd	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=1$$
38	20 37	oveq12d	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\cdot 0{-}_{ℝ}\left(0{-}_{ℝ}\mathrm{i}\right)\mathrm{i}=0{-}_{ℝ}1$$
39	18 38	eqtrd	$$⊢\mathrm{i}\in ℝ\to \left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)=0{-}_{ℝ}1$$
40	39	breq2d	$$⊢\mathrm{i}\in ℝ\to \left(0<\left(0{-}_{ℝ}\mathrm{i}\right)\left(0{-}_{ℝ}\mathrm{i}\right)\leftrightarrow 0<0{-}_{ℝ}1\right)$$
41	40	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)$$
42	14 41	mpbid	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<0{-}_{ℝ}\mathrm{i}\right)\to 0<0{-}_{ℝ}1$$
43	42	ex	$$⊢\mathrm{i}\in ℝ\to \left(0<0{-}_{ℝ}\mathrm{i}\to 0<0{-}_{ℝ}1\right)$$
44	10 43	sylbid	$$⊢\mathrm{i}\in ℝ\to \left(\mathrm{i}<0\to 0<0{-}_{ℝ}1\right)$$
45	9 44	mtoi	$$⊢\mathrm{i}\in ℝ\to \neg \mathrm{i}<0$$
46		0ne1	$$⊢0\ne 1$$
47	46	neii	$$⊢\neg 0=1$$
48		oveq12	$$⊢\left(\mathrm{i}=0\wedge \mathrm{i}=0\right)\to \mathrm{i}\mathrm{i}=0\cdot 0$$
49	48	anidms	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}=0\cdot 0$$
50	49	oveq1d	$$⊢\mathrm{i}=0\to \mathrm{i}\mathrm{i}+1=0\cdot 0+1$$
51		ax-i2m1	$$⊢\mathrm{i}\mathrm{i}+1=0$$
52		remul02	$$⊢0\in ℝ\to 0\cdot 0=0$$
53	1 52	ax-mp	$$⊢0\cdot 0=0$$
54	53	oveq1i	$$⊢0\cdot 0+1=0+1$$
55		readdid2	$$⊢1\in ℝ\to 0+1=1$$
56	5 55	ax-mp	$$⊢0+1=1$$
57	54 56	eqtri	$$⊢0\cdot 0+1=1$$
58	50 51 57	3eqtr3g	$$⊢\mathrm{i}=0\to 0=1$$
59	47 58	mto	$$⊢\neg \mathrm{i}=0$$
60	59	a1i	$$⊢\mathrm{i}\in ℝ\to \neg \mathrm{i}=0$$
61		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}$$
62	61	anidms	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\to 0<\mathrm{i}\mathrm{i}$$
63		reixi	$$⊢\mathrm{i}\mathrm{i}=0{-}_{ℝ}1$$
64	62 63	breqtrdi	$$⊢\left(\mathrm{i}\in ℝ\wedge 0<\mathrm{i}\right)\to 0<0{-}_{ℝ}1$$
65	64	ex	$$⊢\mathrm{i}\in ℝ\to \left(0<\mathrm{i}\to 0<0{-}_{ℝ}1\right)$$
66	9 65	mtoi	$$⊢\mathrm{i}\in ℝ\to \neg 0<\mathrm{i}$$
67		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)$$
68	45 60 66 67	syl3anbrc	$$⊢\mathrm{i}\in ℝ\to \neg \left(\mathrm{i}<0\vee \mathrm{i}=0\vee 0<\mathrm{i}\right)$$
69	3 68	pm2.65i	$$⊢\neg \mathrm{i}\in ℝ$$