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 id ⊢ ( i ∈ ℝ → i ∈ ℝ )
16 11 15 remulneg2d ⊢ ( i ∈ ℝ → ( ( 0 −ℝ i ) · ( 0 −ℝ i ) ) = ( 0 −ℝ ( ( 0 −ℝ i ) · i ) ) )
17 15 15 remulcld ⊢ ( i ∈ ℝ → ( i · i ) ∈ ℝ )
18 15 17 remulcld ⊢ ( i ∈ ℝ → ( i · ( i · i ) ) ∈ ℝ )
19 ipiiie0 ⊢ ( i + ( i · ( i · i ) ) ) = 0
20 renegadd ⊢ ( ( i ∈ ℝ ∧ ( i · ( i · i ) ) ∈ ℝ ) → ( ( 0 −ℝ i ) = ( i · ( i · i ) ) ↔ ( i + ( i · ( i · i ) ) ) = 0 ) )
21 19 20 mpbiri ⊢ ( ( i ∈ ℝ ∧ ( i · ( i · i ) ) ∈ ℝ ) → ( 0 −ℝ i ) = ( i · ( i · i ) ) )
22 18 21 mpdan ⊢ ( i ∈ ℝ → ( 0 −ℝ i ) = ( i · ( i · i ) ) )
23 22 oveq1d ⊢ ( i ∈ ℝ → ( ( 0 −ℝ i ) · i ) = ( ( i · ( i · i ) ) · i ) )
24 ax-icn ⊢ i ∈ ℂ
25 24 24 24 mulassi ⊢ ( ( i · i ) · i ) = ( i · ( i · i ) )
26 25 oveq1i ⊢ ( ( ( i · i ) · i ) · i ) = ( ( i · ( i · i ) ) · i )
27 24 24 mulcli ⊢ ( i · i ) ∈ ℂ
28 27 24 24 mulassi ⊢ ( ( ( i · i ) · i ) · i ) = ( ( i · i ) · ( i · i ) )
29 26 28 eqtr3i ⊢ ( ( i · ( i · i ) ) · i ) = ( ( i · i ) · ( i · i ) )
30 29 a1i ⊢ ( i ∈ ℝ → ( ( i · ( i · i ) ) · i ) = ( ( i · i ) · ( i · i ) ) )
31 rei4 ⊢ ( ( i · i ) · ( i · i ) ) = 1
32 31 a1i ⊢ ( i ∈ ℝ → ( ( i · i ) · ( i · i ) ) = 1 )
33 23 30 32 3eqtrd ⊢ ( i ∈ ℝ → ( ( 0 −ℝ i ) · i ) = 1 )
34 33 oveq2d ⊢ ( i ∈ ℝ → ( 0 −ℝ ( ( 0 −ℝ i ) · i ) ) = ( 0 −ℝ 1 ) )
35 16 34 eqtrd ⊢ ( i ∈ ℝ → ( ( 0 −ℝ i ) · ( 0 −ℝ i ) ) = ( 0 −ℝ 1 ) )
36 35 breq2d ⊢ ( i ∈ ℝ → ( 0 < ( ( 0 −ℝ i ) · ( 0 −ℝ i ) ) ↔ 0 < ( 0 −ℝ 1 ) ) )
37 36 adantr ⊢ ( ( i ∈ ℝ ∧ 0 < ( 0 −ℝ i ) ) → ( 0 < ( ( 0 −ℝ i ) · ( 0 −ℝ i ) ) ↔ 0 < ( 0 −ℝ 1 ) ) )
38 14 37 mpbid ⊢ ( ( i ∈ ℝ ∧ 0 < ( 0 −ℝ i ) ) → 0 < ( 0 −ℝ 1 ) )
39 38 ex ⊢ ( i ∈ ℝ → ( 0 < ( 0 −ℝ i ) → 0 < ( 0 −ℝ 1 ) ) )
40 10 39 sylbid ⊢ ( i ∈ ℝ → ( i < 0 → 0 < ( 0 −ℝ 1 ) ) )
41 9 40 mtoi ⊢ ( i ∈ ℝ → ¬ i < 0 )
42 0ne1 ⊢ 0 ≠ 1
43 42 neii ⊢ ¬ 0 = 1
44 oveq12 ⊢ ( ( i = 0 ∧ i = 0 ) → ( i · i ) = ( 0 · 0 ) )
45 44 anidms ⊢ ( i = 0 → ( i · i ) = ( 0 · 0 ) )
46 45 oveq1d ⊢ ( i = 0 → ( ( i · i ) + 1 ) = ( ( 0 · 0 ) + 1 ) )
47 ax-i2m1 ⊢ ( ( i · i ) + 1 ) = 0
48 remul02 ⊢ ( 0 ∈ ℝ → ( 0 · 0 ) = 0 )
49 1 48 ax-mp ⊢ ( 0 · 0 ) = 0
50 49 oveq1i ⊢ ( ( 0 · 0 ) + 1 ) = ( 0 + 1 )
51 readdlid ⊢ ( 1 ∈ ℝ → ( 0 + 1 ) = 1 )
52 5 51 ax-mp ⊢ ( 0 + 1 ) = 1
53 50 52 eqtri ⊢ ( ( 0 · 0 ) + 1 ) = 1
54 46 47 53 3eqtr3g ⊢ ( i = 0 → 0 = 1 )
55 43 54 mto ⊢ ¬ i = 0
56 55 a1i ⊢ ( i ∈ ℝ → ¬ i = 0 )
57 mulgt0 ⊢ ( ( ( i ∈ ℝ ∧ 0 < i ) ∧ ( i ∈ ℝ ∧ 0 < i ) ) → 0 < ( i · i ) )
58 57 anidms ⊢ ( ( i ∈ ℝ ∧ 0 < i ) → 0 < ( i · i ) )
59 reixi ⊢ ( i · i ) = ( 0 −ℝ 1 )
60 58 59 breqtrdi ⊢ ( ( i ∈ ℝ ∧ 0 < i ) → 0 < ( 0 −ℝ 1 ) )
61 60 ex ⊢ ( i ∈ ℝ → ( 0 < i → 0 < ( 0 −ℝ 1 ) ) )
62 9 61 mtoi ⊢ ( i ∈ ℝ → ¬ 0 < i )
63 3ioran ⊢ ( ¬ ( i < 0 ∨ i = 0 ∨ 0 < i ) ↔ ( ¬ i < 0 ∧ ¬ i = 0 ∧ ¬ 0 < i ) )
64 41 56 62 63 syl3anbrc ⊢ ( i ∈ ℝ → ¬ ( i < 0 ∨ i = 0 ∨ 0 < i ) )
65 3 64 pm2.65i ⊢ ¬ i ∈ ℝ