Metamath Proof Explorer

Theorem sn-inelr

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

Ref Expression
Assertion sn-inelr 
|- -. _i e. RR

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 lttri4 
 |-  ( ( _i e. RR /\ 0 e. RR ) -> ( _i < 0 \/ _i = 0 \/ 0 < _i ) )
3 1 2 mpan2 
 |-  ( _i e. RR -> ( _i < 0 \/ _i = 0 \/ 0 < _i ) )
4 reneg1lt0 
 |-  ( 0 -R 1 ) < 0
5 1re 
 |-  1 e. RR
6 rernegcl 
 |-  ( 1 e. RR -> ( 0 -R 1 ) e. RR )
7 5 6 ax-mp 
 |-  ( 0 -R 1 ) e. RR
8 7 1 ltnsymi 
 |-  ( ( 0 -R 1 ) < 0 -> -. 0 < ( 0 -R 1 ) )
9 4 8 ax-mp 
 |-  -. 0 < ( 0 -R 1 )
10 relt0neg1 
 |-  ( _i e. RR -> ( _i < 0 <-> 0 < ( 0 -R _i ) ) )
11 rernegcl 
 |-  ( _i e. RR -> ( 0 -R _i ) e. RR )
12 mulgt0 
 |-  ( ( ( ( 0 -R _i ) e. RR /\ 0 < ( 0 -R _i ) ) /\ ( ( 0 -R _i ) e. RR /\ 0 < ( 0 -R _i ) ) ) -> 0 < ( ( 0 -R _i ) x. ( 0 -R _i ) ) )
13 12 anidms 
 |-  ( ( ( 0 -R _i ) e. RR /\ 0 < ( 0 -R _i ) ) -> 0 < ( ( 0 -R _i ) x. ( 0 -R _i ) ) )
14 11 13 sylan 
 |-  ( ( _i e. RR /\ 0 < ( 0 -R _i ) ) -> 0 < ( ( 0 -R _i ) x. ( 0 -R _i ) ) )
15 elre0re 
 |-  ( _i e. RR -> 0 e. RR )
16 id 
 |-  ( _i e. RR -> _i e. RR )
17 resubdi 
 |-  ( ( ( 0 -R _i ) e. RR /\ 0 e. RR /\ _i e. RR ) -> ( ( 0 -R _i ) x. ( 0 -R _i ) ) = ( ( ( 0 -R _i ) x. 0 ) -R ( ( 0 -R _i ) x. _i ) ) )
18 11 15 16 17 syl3anc 
 |-  ( _i e. RR -> ( ( 0 -R _i ) x. ( 0 -R _i ) ) = ( ( ( 0 -R _i ) x. 0 ) -R ( ( 0 -R _i ) x. _i ) ) )
19 remul01 
 |-  ( ( 0 -R _i ) e. RR -> ( ( 0 -R _i ) x. 0 ) = 0 )
20 11 19 syl 
 |-  ( _i e. RR -> ( ( 0 -R _i ) x. 0 ) = 0 )
21 16 16 remulcld 
 |-  ( _i e. RR -> ( _i x. _i ) e. RR )
22 16 21 remulcld 
 |-  ( _i e. RR -> ( _i x. ( _i x. _i ) ) e. RR )
23 ipiiie0 
 |-  ( _i + ( _i x. ( _i x. _i ) ) ) = 0
24 renegadd 
 |-  ( ( _i e. RR /\ ( _i x. ( _i x. _i ) ) e. RR ) -> ( ( 0 -R _i ) = ( _i x. ( _i x. _i ) ) <-> ( _i + ( _i x. ( _i x. _i ) ) ) = 0 ) )
25 23 24 mpbiri 
 |-  ( ( _i e. RR /\ ( _i x. ( _i x. _i ) ) e. RR ) -> ( 0 -R _i ) = ( _i x. ( _i x. _i ) ) )
26 22 25 mpdan 
 |-  ( _i e. RR -> ( 0 -R _i ) = ( _i x. ( _i x. _i ) ) )
27 26 oveq1d 
 |-  ( _i e. RR -> ( ( 0 -R _i ) x. _i ) = ( ( _i x. ( _i x. _i ) ) x. _i ) )
28 ax-icn 
 |-  _i e. CC
29 28 28 28 mulassi 
 |-  ( ( _i x. _i ) x. _i ) = ( _i x. ( _i x. _i ) )
30 29 oveq1i 
 |-  ( ( ( _i x. _i ) x. _i ) x. _i ) = ( ( _i x. ( _i x. _i ) ) x. _i )
31 28 28 mulcli 
 |-  ( _i x. _i ) e. CC
32 31 28 28 mulassi 
 |-  ( ( ( _i x. _i ) x. _i ) x. _i ) = ( ( _i x. _i ) x. ( _i x. _i ) )
33 30 32 eqtr3i 
 |-  ( ( _i x. ( _i x. _i ) ) x. _i ) = ( ( _i x. _i ) x. ( _i x. _i ) )
34 33 a1i 
 |-  ( _i e. RR -> ( ( _i x. ( _i x. _i ) ) x. _i ) = ( ( _i x. _i ) x. ( _i x. _i ) ) )
35 rei4 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = 1
36 35 a1i 
 |-  ( _i e. RR -> ( ( _i x. _i ) x. ( _i x. _i ) ) = 1 )
37 27 34 36 3eqtrd 
 |-  ( _i e. RR -> ( ( 0 -R _i ) x. _i ) = 1 )
38 20 37 oveq12d 
 |-  ( _i e. RR -> ( ( ( 0 -R _i ) x. 0 ) -R ( ( 0 -R _i ) x. _i ) ) = ( 0 -R 1 ) )
39 18 38 eqtrd 
 |-  ( _i e. RR -> ( ( 0 -R _i ) x. ( 0 -R _i ) ) = ( 0 -R 1 ) )
40 39 breq2d 
 |-  ( _i e. RR -> ( 0 < ( ( 0 -R _i ) x. ( 0 -R _i ) ) <-> 0 < ( 0 -R 1 ) ) )
41 40 adantr 
 |-  ( ( _i e. RR /\ 0 < ( 0 -R _i ) ) -> ( 0 < ( ( 0 -R _i ) x. ( 0 -R _i ) ) <-> 0 < ( 0 -R 1 ) ) )
42 14 41 mpbid 
 |-  ( ( _i e. RR /\ 0 < ( 0 -R _i ) ) -> 0 < ( 0 -R 1 ) )
43 42 ex 
 |-  ( _i e. RR -> ( 0 < ( 0 -R _i ) -> 0 < ( 0 -R 1 ) ) )
44 10 43 sylbid 
 |-  ( _i e. RR -> ( _i < 0 -> 0 < ( 0 -R 1 ) ) )
45 9 44 mtoi 
 |-  ( _i e. RR -> -. _i < 0 )
46 0ne1 
 |-  0 =/= 1
47 46 neii 
 |-  -. 0 = 1
48 oveq12 
 |-  ( ( _i = 0 /\ _i = 0 ) -> ( _i x. _i ) = ( 0 x. 0 ) )
49 48 anidms 
 |-  ( _i = 0 -> ( _i x. _i ) = ( 0 x. 0 ) )
50 49 oveq1d 
 |-  ( _i = 0 -> ( ( _i x. _i ) + 1 ) = ( ( 0 x. 0 ) + 1 ) )
51 ax-i2m1 
 |-  ( ( _i x. _i ) + 1 ) = 0
52 remul02 
 |-  ( 0 e. RR -> ( 0 x. 0 ) = 0 )
53 1 52 ax-mp 
 |-  ( 0 x. 0 ) = 0
54 53 oveq1i 
 |-  ( ( 0 x. 0 ) + 1 ) = ( 0 + 1 )
55 readdid2 
 |-  ( 1 e. RR -> ( 0 + 1 ) = 1 )
56 5 55 ax-mp 
 |-  ( 0 + 1 ) = 1
57 54 56 eqtri 
 |-  ( ( 0 x. 0 ) + 1 ) = 1
58 50 51 57 3eqtr3g 
 |-  ( _i = 0 -> 0 = 1 )
59 47 58 mto 
 |-  -. _i = 0
60 59 a1i 
 |-  ( _i e. RR -> -. _i = 0 )
61 mulgt0 
 |-  ( ( ( _i e. RR /\ 0 < _i ) /\ ( _i e. RR /\ 0 < _i ) ) -> 0 < ( _i x. _i ) )
62 61 anidms 
 |-  ( ( _i e. RR /\ 0 < _i ) -> 0 < ( _i x. _i ) )
63 reixi 
 |-  ( _i x. _i ) = ( 0 -R 1 )
64 62 63 breqtrdi 
 |-  ( ( _i e. RR /\ 0 < _i ) -> 0 < ( 0 -R 1 ) )
65 64 ex 
 |-  ( _i e. RR -> ( 0 < _i -> 0 < ( 0 -R 1 ) ) )
66 9 65 mtoi 
 |-  ( _i e. RR -> -. 0 < _i )
67 3ioran 
 |-  ( -. ( _i < 0 \/ _i = 0 \/ 0 < _i ) <-> ( -. _i < 0 /\ -. _i = 0 /\ -. 0 < _i ) )
68 45 60 66 67 syl3anbrc 
 |-  ( _i e. RR -> -. ( _i < 0 \/ _i = 0 \/ 0 < _i ) )
69 3 68 pm2.65i 
 |-  -. _i e. RR