Proof of Theorem sn-inelr
Step | Hyp | Ref
| Expression |
1 | | 0re 11157 |
. . 3
⊢ 0 ∈
ℝ |
2 | | lttri4 11239 |
. . 3
⊢ ((i
∈ ℝ ∧ 0 ∈ ℝ) → (i < 0 ∨ i = 0 ∨ 0 <
i)) |
3 | 1, 2 | mpan2 689 |
. 2
⊢ (i ∈
ℝ → (i < 0 ∨ i = 0 ∨ 0 < i)) |
4 | | reneg1lt0 40919 |
. . . . 5
⊢ (0
−ℝ 1) < 0 |
5 | | 1re 11155 |
. . . . . . 7
⊢ 1 ∈
ℝ |
6 | | rernegcl 40826 |
. . . . . . 7
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢ (0
−ℝ 1) ∈ ℝ |
8 | 7, 1 | ltnsymi 11274 |
. . . . 5
⊢ ((0
−ℝ 1) < 0 → ¬ 0 < (0
−ℝ 1)) |
9 | 4, 8 | ax-mp 5 |
. . . 4
⊢ ¬ 0
< (0 −ℝ 1) |
10 | | relt0neg1 40899 |
. . . . 5
⊢ (i ∈
ℝ → (i < 0 ↔ 0 < (0 −ℝ
i))) |
11 | | rernegcl 40826 |
. . . . . . . 8
⊢ (i ∈
ℝ → (0 −ℝ i) ∈ ℝ) |
12 | | mulgt0 11232 |
. . . . . . . . 9
⊢ ((((0
−ℝ i) ∈ ℝ ∧ 0 < (0
−ℝ i)) ∧ ((0 −ℝ i) ∈
ℝ ∧ 0 < (0 −ℝ i))) → 0 < ((0
−ℝ i) · (0 −ℝ
i))) |
13 | 12 | anidms 567 |
. . . . . . . 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 40869 |
. . . . . . . . . 10
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (0 −ℝ ((0
−ℝ i) · i))) |
17 | 15, 15 | remulcld 11185 |
. . . . . . . . . . . . . . 15
⊢ (i ∈
ℝ → (i · i) ∈ ℝ) |
18 | 15, 17 | remulcld 11185 |
. . . . . . . . . . . . . 14
⊢ (i ∈
ℝ → (i · (i · i)) ∈ ℝ) |
19 | | ipiiie0 40892 |
. . . . . . . . . . . . . . 15
⊢ (i + (i
· (i · i))) = 0 |
20 | | renegadd 40827 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → ((0
−ℝ i) = (i · (i · i)) ↔ (i + (i
· (i · i))) = 0)) |
21 | 19, 20 | mpbiri 257 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → (0
−ℝ i) = (i · (i · i))) |
22 | 18, 21 | mpdan 685 |
. . . . . . . . . . . . 13
⊢ (i ∈
ℝ → (0 −ℝ i) = (i · (i ·
i))) |
23 | 22 | oveq1d 7372 |
. . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) = ((i · (i
· i)) · i)) |
24 | | ax-icn 11110 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
25 | 24, 24, 24 | mulassi 11166 |
. . . . . . . . . . . . . . 15
⊢ ((i
· i) · i) = (i · (i · i)) |
26 | 25 | oveq1i 7367 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · (i · i)) ·
i) |
27 | 24, 24 | mulcli 11162 |
. . . . . . . . . . . . . . 15
⊢ (i
· i) ∈ ℂ |
28 | 27, 24, 24 | mulassi 11166 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · i) · (i ·
i)) |
29 | 26, 28 | eqtr3i 2766 |
. . . . . . . . . . . . 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 40878 |
. . . . . . . . . . . . 13
⊢ ((i
· i) · (i · i)) = 1 |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((i · i) · (i · i)) = 1) |
33 | 23, 30, 32 | 3eqtrd 2780 |
. . . . . . . . . . 11
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) =
1) |
34 | 33 | oveq2d 7373 |
. . . . . . . . . 10
⊢ (i ∈
ℝ → (0 −ℝ ((0 −ℝ i)
· i)) = (0 −ℝ 1)) |
35 | 16, 34 | eqtrd 2776 |
. . . . . . . . 9
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (0 −ℝ
1)) |
36 | 35 | breq2d 5117 |
. . . . . . . 8
⊢ (i ∈
ℝ → (0 < ((0 −ℝ i) · (0
−ℝ i)) ↔ 0 < (0 −ℝ
1))) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → (0 < ((0
−ℝ i) · (0 −ℝ i)) ↔ 0
< (0 −ℝ 1))) |
38 | 14, 37 | mpbid 231 |
. . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → 0 < (0
−ℝ 1)) |
39 | 38 | ex 413 |
. . . . 5
⊢ (i ∈
ℝ → (0 < (0 −ℝ i) → 0 < (0
−ℝ 1))) |
40 | 10, 39 | sylbid 239 |
. . . 4
⊢ (i ∈
ℝ → (i < 0 → 0 < (0 −ℝ
1))) |
41 | 9, 40 | mtoi 198 |
. . 3
⊢ (i ∈
ℝ → ¬ i < 0) |
42 | | 0ne1 12224 |
. . . . . 6
⊢ 0 ≠
1 |
43 | 42 | neii 2945 |
. . . . 5
⊢ ¬ 0
= 1 |
44 | | oveq12 7366 |
. . . . . . . 8
⊢ ((i = 0
∧ i = 0) → (i · i) = (0 · 0)) |
45 | 44 | anidms 567 |
. . . . . . 7
⊢ (i = 0
→ (i · i) = (0 · 0)) |
46 | 45 | oveq1d 7372 |
. . . . . 6
⊢ (i = 0
→ ((i · i) + 1) = ((0 · 0) + 1)) |
47 | | ax-i2m1 11119 |
. . . . . 6
⊢ ((i
· i) + 1) = 0 |
48 | | remul02 40860 |
. . . . . . . . 9
⊢ (0 ∈
ℝ → (0 · 0) = 0) |
49 | 1, 48 | ax-mp 5 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
50 | 49 | oveq1i 7367 |
. . . . . . 7
⊢ ((0
· 0) + 1) = (0 + 1) |
51 | | readdid2 40858 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (0 + 1) = 1) |
52 | 5, 51 | ax-mp 5 |
. . . . . . 7
⊢ (0 + 1) =
1 |
53 | 50, 52 | eqtri 2764 |
. . . . . 6
⊢ ((0
· 0) + 1) = 1 |
54 | 46, 47, 53 | 3eqtr3g 2799 |
. . . . 5
⊢ (i = 0
→ 0 = 1) |
55 | 43, 54 | mto 196 |
. . . 4
⊢ ¬ i
= 0 |
56 | 55 | a1i 11 |
. . 3
⊢ (i ∈
ℝ → ¬ i = 0) |
57 | | mulgt0 11232 |
. . . . . . 7
⊢ (((i
∈ ℝ ∧ 0 < i) ∧ (i ∈ ℝ ∧ 0 < i)) →
0 < (i · i)) |
58 | 57 | anidms 567 |
. . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (i · i)) |
59 | | reixi 40877 |
. . . . . 6
⊢ (i
· i) = (0 −ℝ 1) |
60 | 58, 59 | breqtrdi 5146 |
. . . . 5
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (0 −ℝ
1)) |
61 | 60 | ex 413 |
. . . 4
⊢ (i ∈
ℝ → (0 < i → 0 < (0 −ℝ
1))) |
62 | 9, 61 | mtoi 198 |
. . 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 1343 |
. 2
⊢ (i ∈
ℝ → ¬ (i < 0 ∨ i = 0 ∨ 0 < i)) |
65 | 3, 64 | pm2.65i 193 |
1
⊢ ¬ i
∈ ℝ |