Proof of Theorem sn-inelr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0re 11263 | . . 3
⊢ 0 ∈
ℝ | 
| 2 |  | lttri4 11345 | . . 3
⊢ ((i
∈ ℝ ∧ 0 ∈ ℝ) → (i < 0 ∨ i = 0 ∨ 0 <
i)) | 
| 3 | 1, 2 | mpan2 691 | . 2
⊢ (i ∈
ℝ → (i < 0 ∨ i = 0 ∨ 0 < i)) | 
| 4 |  | reneg1lt0 42496 | . . . . 5
⊢ (0
−ℝ 1) < 0 | 
| 5 |  | 1re 11261 | . . . . . . 7
⊢ 1 ∈
ℝ | 
| 6 |  | rernegcl 42401 | . . . . . . 7
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) | 
| 7 | 5, 6 | ax-mp 5 | . . . . . 6
⊢ (0
−ℝ 1) ∈ ℝ | 
| 8 | 7, 1 | ltnsymi 11380 | . . . . 5
⊢ ((0
−ℝ 1) < 0 → ¬ 0 < (0
−ℝ 1)) | 
| 9 | 4, 8 | ax-mp 5 | . . . 4
⊢  ¬ 0
< (0 −ℝ 1) | 
| 10 |  | relt0neg1 42474 | . . . . 5
⊢ (i ∈
ℝ → (i < 0 ↔ 0 < (0 −ℝ
i))) | 
| 11 |  | rernegcl 42401 | . . . . . . . 8
⊢ (i ∈
ℝ → (0 −ℝ i) ∈ ℝ) | 
| 12 |  | mulgt0 11338 | . . . . . . . . 9
⊢ ((((0
−ℝ i) ∈ ℝ ∧ 0 < (0
−ℝ i)) ∧ ((0 −ℝ i) ∈
ℝ ∧ 0 < (0 −ℝ i))) → 0 < ((0
−ℝ i) · (0 −ℝ
i))) | 
| 13 | 12 | anidms 566 | . . . . . . . 8
⊢ (((0
−ℝ i) ∈ ℝ ∧ 0 < (0
−ℝ i)) → 0 < ((0 −ℝ i)
· (0 −ℝ i))) | 
| 14 | 11, 13 | sylan 580 | . . . . . . 7
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → 0 < ((0
−ℝ i) · (0 −ℝ
i))) | 
| 15 |  | id 22 | . . . . . . . . . . 11
⊢ (i ∈
ℝ → i ∈ ℝ) | 
| 16 | 11, 15 | remulneg2d 42444 | . . . . . . . . . 10
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (0 −ℝ ((0
−ℝ i) · i))) | 
| 17 | 15, 15 | remulcld 11291 | . . . . . . . . . . . . . . 15
⊢ (i ∈
ℝ → (i · i) ∈ ℝ) | 
| 18 | 15, 17 | remulcld 11291 | . . . . . . . . . . . . . 14
⊢ (i ∈
ℝ → (i · (i · i)) ∈ ℝ) | 
| 19 |  | ipiiie0 42467 | . . . . . . . . . . . . . . 15
⊢ (i + (i
· (i · i))) = 0 | 
| 20 |  | renegadd 42402 | . . . . . . . . . . . . . . 15
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → ((0
−ℝ i) = (i · (i · i)) ↔ (i + (i
· (i · i))) = 0)) | 
| 21 | 19, 20 | mpbiri 258 | . . . . . . . . . . . . . 14
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → (0
−ℝ i) = (i · (i · i))) | 
| 22 | 18, 21 | mpdan 687 | . . . . . . . . . . . . 13
⊢ (i ∈
ℝ → (0 −ℝ i) = (i · (i ·
i))) | 
| 23 | 22 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) = ((i · (i
· i)) · i)) | 
| 24 |  | ax-icn 11214 | . . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ | 
| 25 | 24, 24, 24 | mulassi 11272 | . . . . . . . . . . . . . . 15
⊢ ((i
· i) · i) = (i · (i · i)) | 
| 26 | 25 | oveq1i 7441 | . . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · (i · i)) ·
i) | 
| 27 | 24, 24 | mulcli 11268 | . . . . . . . . . . . . . . 15
⊢ (i
· i) ∈ ℂ | 
| 28 | 27, 24, 24 | mulassi 11272 | . . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · i) · (i ·
i)) | 
| 29 | 26, 28 | eqtr3i 2767 | . . . . . . . . . . . . 13
⊢ ((i
· (i · i)) · i) = ((i · i) · (i ·
i)) | 
| 30 | 29 | a1i 11 | . . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((i · (i · i)) · i) = ((i · i)
· (i · i))) | 
| 31 |  | rei4 42453 | . . . . . . . . . . . . 13
⊢ ((i
· i) · (i · i)) = 1 | 
| 32 | 31 | a1i 11 | . . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((i · i) · (i · i)) = 1) | 
| 33 | 23, 30, 32 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) =
1) | 
| 34 | 33 | oveq2d 7447 | . . . . . . . . . 10
⊢ (i ∈
ℝ → (0 −ℝ ((0 −ℝ i)
· i)) = (0 −ℝ 1)) | 
| 35 | 16, 34 | eqtrd 2777 | . . . . . . . . 9
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (0 −ℝ
1)) | 
| 36 | 35 | breq2d 5155 | . . . . . . . 8
⊢ (i ∈
ℝ → (0 < ((0 −ℝ i) · (0
−ℝ i)) ↔ 0 < (0 −ℝ
1))) | 
| 37 | 36 | adantr 480 | . . . . . . 7
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → (0 < ((0
−ℝ i) · (0 −ℝ i)) ↔ 0
< (0 −ℝ 1))) | 
| 38 | 14, 37 | mpbid 232 | . . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → 0 < (0
−ℝ 1)) | 
| 39 | 38 | ex 412 | . . . . 5
⊢ (i ∈
ℝ → (0 < (0 −ℝ i) → 0 < (0
−ℝ 1))) | 
| 40 | 10, 39 | sylbid 240 | . . . 4
⊢ (i ∈
ℝ → (i < 0 → 0 < (0 −ℝ
1))) | 
| 41 | 9, 40 | mtoi 199 | . . 3
⊢ (i ∈
ℝ → ¬ i < 0) | 
| 42 |  | 0ne1 12337 | . . . . . 6
⊢ 0 ≠
1 | 
| 43 | 42 | neii 2942 | . . . . 5
⊢  ¬ 0
= 1 | 
| 44 |  | oveq12 7440 | . . . . . . . 8
⊢ ((i = 0
∧ i = 0) → (i · i) = (0 · 0)) | 
| 45 | 44 | anidms 566 | . . . . . . 7
⊢ (i = 0
→ (i · i) = (0 · 0)) | 
| 46 | 45 | oveq1d 7446 | . . . . . 6
⊢ (i = 0
→ ((i · i) + 1) = ((0 · 0) + 1)) | 
| 47 |  | ax-i2m1 11223 | . . . . . 6
⊢ ((i
· i) + 1) = 0 | 
| 48 |  | remul02 42435 | . . . . . . . . 9
⊢ (0 ∈
ℝ → (0 · 0) = 0) | 
| 49 | 1, 48 | ax-mp 5 | . . . . . . . 8
⊢ (0
· 0) = 0 | 
| 50 | 49 | oveq1i 7441 | . . . . . . 7
⊢ ((0
· 0) + 1) = (0 + 1) | 
| 51 |  | readdlid 42433 | . . . . . . . 8
⊢ (1 ∈
ℝ → (0 + 1) = 1) | 
| 52 | 5, 51 | ax-mp 5 | . . . . . . 7
⊢ (0 + 1) =
1 | 
| 53 | 50, 52 | eqtri 2765 | . . . . . 6
⊢ ((0
· 0) + 1) = 1 | 
| 54 | 46, 47, 53 | 3eqtr3g 2800 | . . . . 5
⊢ (i = 0
→ 0 = 1) | 
| 55 | 43, 54 | mto 197 | . . . 4
⊢  ¬ i
= 0 | 
| 56 | 55 | a1i 11 | . . 3
⊢ (i ∈
ℝ → ¬ i = 0) | 
| 57 |  | mulgt0 11338 | . . . . . . 7
⊢ (((i
∈ ℝ ∧ 0 < i) ∧ (i ∈ ℝ ∧ 0 < i)) →
0 < (i · i)) | 
| 58 | 57 | anidms 566 | . . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (i · i)) | 
| 59 |  | reixi 42452 | . . . . . 6
⊢ (i
· i) = (0 −ℝ 1) | 
| 60 | 58, 59 | breqtrdi 5184 | . . . . 5
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (0 −ℝ
1)) | 
| 61 | 60 | ex 412 | . . . 4
⊢ (i ∈
ℝ → (0 < i → 0 < (0 −ℝ
1))) | 
| 62 | 9, 61 | mtoi 199 | . . 3
⊢ (i ∈
ℝ → ¬ 0 < i) | 
| 63 |  | 3ioran 1106 | . . 3
⊢ (¬ (i
< 0 ∨ i = 0 ∨ 0 < i) ↔ (¬ i < 0 ∧ ¬ i = 0 ∧
¬ 0 < i)) | 
| 64 | 41, 56, 62, 63 | syl3anbrc 1344 | . 2
⊢ (i ∈
ℝ → ¬ (i < 0 ∨ i = 0 ∨ 0 < i)) | 
| 65 | 3, 64 | pm2.65i 194 | 1
⊢  ¬ i
∈ ℝ |