Metamath Proof Explorer

Theorem sn-inelr

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

Ref Expression
Assertion sn-inelr ¬ i ∈ ℝ

Proof

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