Proof of Theorem sn-inelr
Step | Hyp | Ref
| Expression |
1 | | 0re 10666 |
. . 3
⊢ 0 ∈
ℝ |
2 | | lttri4 10748 |
. . 3
⊢ ((i
∈ ℝ ∧ 0 ∈ ℝ) → (i < 0 ∨ i = 0 ∨ 0 <
i)) |
3 | 1, 2 | mpan2 691 |
. 2
⊢ (i ∈
ℝ → (i < 0 ∨ i = 0 ∨ 0 < i)) |
4 | | reneg1lt0 39916 |
. . . . 5
⊢ (0
−ℝ 1) < 0 |
5 | | 1re 10664 |
. . . . . . 7
⊢ 1 ∈
ℝ |
6 | | rernegcl 39836 |
. . . . . . 7
⊢ (1 ∈
ℝ → (0 −ℝ 1) ∈ ℝ) |
7 | 5, 6 | ax-mp 5 |
. . . . . 6
⊢ (0
−ℝ 1) ∈ ℝ |
8 | 7, 1 | ltnsymi 10782 |
. . . . 5
⊢ ((0
−ℝ 1) < 0 → ¬ 0 < (0
−ℝ 1)) |
9 | 4, 8 | ax-mp 5 |
. . . 4
⊢ ¬ 0
< (0 −ℝ 1) |
10 | | relt0neg1 39907 |
. . . . 5
⊢ (i ∈
ℝ → (i < 0 ↔ 0 < (0 −ℝ
i))) |
11 | | rernegcl 39836 |
. . . . . . . 8
⊢ (i ∈
ℝ → (0 −ℝ i) ∈ ℝ) |
12 | | mulgt0 10741 |
. . . . . . . . 9
⊢ ((((0
−ℝ i) ∈ ℝ ∧ 0 < (0
−ℝ i)) ∧ ((0 −ℝ i) ∈
ℝ ∧ 0 < (0 −ℝ i))) → 0 < ((0
−ℝ i) · (0 −ℝ
i))) |
13 | 12 | anidms 571 |
. . . . . . . 8
⊢ (((0
−ℝ i) ∈ ℝ ∧ 0 < (0
−ℝ i)) → 0 < ((0 −ℝ i)
· (0 −ℝ i))) |
14 | 11, 13 | sylan 584 |
. . . . . . 7
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → 0 < ((0
−ℝ i) · (0 −ℝ
i))) |
15 | | elre0re 39778 |
. . . . . . . . . . 11
⊢ (i ∈
ℝ → 0 ∈ ℝ) |
16 | | id 22 |
. . . . . . . . . . 11
⊢ (i ∈
ℝ → i ∈ ℝ) |
17 | | resubdi 39861 |
. . . . . . . . . . 11
⊢ (((0
−ℝ i) ∈ ℝ ∧ 0 ∈ ℝ ∧ i
∈ ℝ) → ((0 −ℝ i) · (0
−ℝ i)) = (((0 −ℝ i) · 0)
−ℝ ((0 −ℝ i) ·
i))) |
18 | 11, 15, 16, 17 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (((0 −ℝ i) · 0)
−ℝ ((0 −ℝ i) ·
i))) |
19 | | remul01 39872 |
. . . . . . . . . . . 12
⊢ ((0
−ℝ i) ∈ ℝ → ((0
−ℝ i) · 0) = 0) |
20 | 11, 19 | syl 17 |
. . . . . . . . . . 11
⊢ (i ∈
ℝ → ((0 −ℝ i) · 0) =
0) |
21 | 16, 16 | remulcld 10694 |
. . . . . . . . . . . . . . 15
⊢ (i ∈
ℝ → (i · i) ∈ ℝ) |
22 | 16, 21 | remulcld 10694 |
. . . . . . . . . . . . . 14
⊢ (i ∈
ℝ → (i · (i · i)) ∈ ℝ) |
23 | | ipiiie0 39901 |
. . . . . . . . . . . . . . 15
⊢ (i + (i
· (i · i))) = 0 |
24 | | renegadd 39837 |
. . . . . . . . . . . . . . 15
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → ((0
−ℝ i) = (i · (i · i)) ↔ (i + (i
· (i · i))) = 0)) |
25 | 23, 24 | mpbiri 261 |
. . . . . . . . . . . . . 14
⊢ ((i
∈ ℝ ∧ (i · (i · i)) ∈ ℝ) → (0
−ℝ i) = (i · (i · i))) |
26 | 22, 25 | mpdan 687 |
. . . . . . . . . . . . 13
⊢ (i ∈
ℝ → (0 −ℝ i) = (i · (i ·
i))) |
27 | 26 | oveq1d 7158 |
. . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) = ((i · (i
· i)) · i)) |
28 | | ax-icn 10619 |
. . . . . . . . . . . . . . . 16
⊢ i ∈
ℂ |
29 | 28, 28, 28 | mulassi 10675 |
. . . . . . . . . . . . . . 15
⊢ ((i
· i) · i) = (i · (i · i)) |
30 | 29 | oveq1i 7153 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · (i · i)) ·
i) |
31 | 28, 28 | mulcli 10671 |
. . . . . . . . . . . . . . 15
⊢ (i
· i) ∈ ℂ |
32 | 31, 28, 28 | mulassi 10675 |
. . . . . . . . . . . . . 14
⊢ (((i
· i) · i) · i) = ((i · i) · (i ·
i)) |
33 | 30, 32 | eqtr3i 2784 |
. . . . . . . . . . . . 13
⊢ ((i
· (i · i)) · i) = ((i · i) · (i ·
i)) |
34 | 33 | a1i 11 |
. . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((i · (i · i)) · i) = ((i · i)
· (i · i))) |
35 | | rei4 39887 |
. . . . . . . . . . . . 13
⊢ ((i
· i) · (i · i)) = 1 |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (i ∈
ℝ → ((i · i) · (i · i)) = 1) |
37 | 27, 34, 36 | 3eqtrd 2798 |
. . . . . . . . . . 11
⊢ (i ∈
ℝ → ((0 −ℝ i) · i) =
1) |
38 | 20, 37 | oveq12d 7161 |
. . . . . . . . . 10
⊢ (i ∈
ℝ → (((0 −ℝ i) · 0)
−ℝ ((0 −ℝ i) · i)) = (0
−ℝ 1)) |
39 | 18, 38 | eqtrd 2794 |
. . . . . . . . 9
⊢ (i ∈
ℝ → ((0 −ℝ i) · (0
−ℝ i)) = (0 −ℝ
1)) |
40 | 39 | breq2d 5037 |
. . . . . . . 8
⊢ (i ∈
ℝ → (0 < ((0 −ℝ i) · (0
−ℝ i)) ↔ 0 < (0 −ℝ
1))) |
41 | 40 | adantr 485 |
. . . . . . 7
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → (0 < ((0
−ℝ i) · (0 −ℝ i)) ↔ 0
< (0 −ℝ 1))) |
42 | 14, 41 | mpbid 235 |
. . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < (0 −ℝ i)) → 0 < (0
−ℝ 1)) |
43 | 42 | ex 417 |
. . . . 5
⊢ (i ∈
ℝ → (0 < (0 −ℝ i) → 0 < (0
−ℝ 1))) |
44 | 10, 43 | sylbid 243 |
. . . 4
⊢ (i ∈
ℝ → (i < 0 → 0 < (0 −ℝ
1))) |
45 | 9, 44 | mtoi 202 |
. . 3
⊢ (i ∈
ℝ → ¬ i < 0) |
46 | | 0ne1 11730 |
. . . . . 6
⊢ 0 ≠
1 |
47 | 46 | neii 2951 |
. . . . 5
⊢ ¬ 0
= 1 |
48 | | oveq12 7152 |
. . . . . . . 8
⊢ ((i = 0
∧ i = 0) → (i · i) = (0 · 0)) |
49 | 48 | anidms 571 |
. . . . . . 7
⊢ (i = 0
→ (i · i) = (0 · 0)) |
50 | 49 | oveq1d 7158 |
. . . . . 6
⊢ (i = 0
→ ((i · i) + 1) = ((0 · 0) + 1)) |
51 | | ax-i2m1 10628 |
. . . . . 6
⊢ ((i
· i) + 1) = 0 |
52 | | remul02 39870 |
. . . . . . . . 9
⊢ (0 ∈
ℝ → (0 · 0) = 0) |
53 | 1, 52 | ax-mp 5 |
. . . . . . . 8
⊢ (0
· 0) = 0 |
54 | 53 | oveq1i 7153 |
. . . . . . 7
⊢ ((0
· 0) + 1) = (0 + 1) |
55 | | readdid2 39868 |
. . . . . . . 8
⊢ (1 ∈
ℝ → (0 + 1) = 1) |
56 | 5, 55 | ax-mp 5 |
. . . . . . 7
⊢ (0 + 1) =
1 |
57 | 54, 56 | eqtri 2782 |
. . . . . 6
⊢ ((0
· 0) + 1) = 1 |
58 | 50, 51, 57 | 3eqtr3g 2817 |
. . . . 5
⊢ (i = 0
→ 0 = 1) |
59 | 47, 58 | mto 200 |
. . . 4
⊢ ¬ i
= 0 |
60 | 59 | a1i 11 |
. . 3
⊢ (i ∈
ℝ → ¬ i = 0) |
61 | | mulgt0 10741 |
. . . . . . 7
⊢ (((i
∈ ℝ ∧ 0 < i) ∧ (i ∈ ℝ ∧ 0 < i)) →
0 < (i · i)) |
62 | 61 | anidms 571 |
. . . . . 6
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (i · i)) |
63 | | reixi 39886 |
. . . . . 6
⊢ (i
· i) = (0 −ℝ 1) |
64 | 62, 63 | breqtrdi 5066 |
. . . . 5
⊢ ((i
∈ ℝ ∧ 0 < i) → 0 < (0 −ℝ
1)) |
65 | 64 | ex 417 |
. . . 4
⊢ (i ∈
ℝ → (0 < i → 0 < (0 −ℝ
1))) |
66 | 9, 65 | mtoi 202 |
. . 3
⊢ (i ∈
ℝ → ¬ 0 < i) |
67 | | 3ioran 1104 |
. . 3
⊢ (¬ (i
< 0 ∨ i = 0 ∨ 0 < i) ↔ (¬ i < 0 ∧ ¬ i = 0 ∧
¬ 0 < i)) |
68 | 45, 60, 66, 67 | syl3anbrc 1341 |
. 2
⊢ (i ∈
ℝ → ¬ (i < 0 ∨ i = 0 ∨ 0 < i)) |
69 | 3, 68 | pm2.65i 197 |
1
⊢ ¬ i
∈ ℝ |