Proof of Theorem sgnneg
| Step | Hyp | Ref
| Expression |
| 1 | | recn 11245 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 2 | 1 | negeq0d 11612 |
. . . 4
⊢ (𝐴 ∈ ℝ → (𝐴 = 0 ↔ -𝐴 = 0)) |
| 3 | 2 | bicomd 223 |
. . 3
⊢ (𝐴 ∈ ℝ → (-𝐴 = 0 ↔ 𝐴 = 0)) |
| 4 | | eqidd 2738 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ -𝐴 = 0) → 0 =
0) |
| 5 | 3 | necon3bbid 2978 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (¬
-𝐴 = 0 ↔ 𝐴 ≠ 0)) |
| 6 | 5 | biimpa 476 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ ¬
-𝐴 = 0) → 𝐴 ≠ 0) |
| 7 | | lt0neg2 11770 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ -𝐴 < 0)) |
| 8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 < 𝐴 ↔ -𝐴 < 0)) |
| 9 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
| 10 | | 0red 11264 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → 0 ∈
ℝ) |
| 11 | 9, 10 | lttri2d 11400 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝐴 ≠ 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
| 12 | 11 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 < 0 ∨ 0 < 𝐴)) |
| 13 | | ltnsym2 11360 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℝ) → ¬ (𝐴
< 0 ∧ 0 < 𝐴)) |
| 14 | 10, 13 | mpdan 687 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → ¬
(𝐴 < 0 ∧ 0 <
𝐴)) |
| 15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ¬ (𝐴 < 0 ∧ 0 < 𝐴)) |
| 16 | 12, 15 | jca 511 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ((𝐴 < 0 ∨ 0 < 𝐴) ∧ ¬ (𝐴 < 0 ∧ 0 < 𝐴))) |
| 17 | | pm5.17 1014 |
. . . . . . . . 9
⊢ (((𝐴 < 0 ∨ 0 < 𝐴) ∧ ¬ (𝐴 < 0 ∧ 0 < 𝐴)) ↔ (𝐴 < 0 ↔ ¬ 0 < 𝐴)) |
| 18 | 16, 17 | sylib 218 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴 < 0 ↔ ¬ 0 <
𝐴)) |
| 19 | 18 | con2bid 354 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (0 < 𝐴 ↔ ¬ 𝐴 < 0)) |
| 20 | 8, 19 | bitr3d 281 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (-𝐴 < 0 ↔ ¬ 𝐴 < 0)) |
| 21 | 20 | ifbid 4549 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → if(-𝐴 < 0, -1, 1) = if(¬ 𝐴 < 0, -1,
1)) |
| 22 | | ifnot 4578 |
. . . . 5
⊢ if(¬
𝐴 < 0, -1, 1) = if(𝐴 < 0, 1, -1) |
| 23 | 21, 22 | eqtrdi 2793 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → if(-𝐴 < 0, -1, 1) = if(𝐴 < 0, 1,
-1)) |
| 24 | 6, 23 | syldan 591 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ ¬
-𝐴 = 0) → if(-𝐴 < 0, -1, 1) = if(𝐴 < 0, 1,
-1)) |
| 25 | 3, 4, 24 | ifbieq12d2 4560 |
. 2
⊢ (𝐴 ∈ ℝ → if(-𝐴 = 0, 0, if(-𝐴 < 0, -1, 1)) = if(𝐴 = 0, 0, if(𝐴 < 0, 1, -1))) |
| 26 | | renegcl 11572 |
. . 3
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
| 27 | | rexr 11307 |
. . 3
⊢ (-𝐴 ∈ ℝ → -𝐴 ∈
ℝ*) |
| 28 | | sgnval 15127 |
. . 3
⊢ (-𝐴 ∈ ℝ*
→ (sgn‘-𝐴) =
if(-𝐴 = 0, 0, if(-𝐴 < 0, -1,
1))) |
| 29 | 26, 27, 28 | 3syl 18 |
. 2
⊢ (𝐴 ∈ ℝ →
(sgn‘-𝐴) = if(-𝐴 = 0, 0, if(-𝐴 < 0, -1, 1))) |
| 30 | | df-neg 11495 |
. . . 4
⊢
-(sgn‘𝐴) = (0
− (sgn‘𝐴)) |
| 31 | 30 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℝ →
-(sgn‘𝐴) = (0 −
(sgn‘𝐴))) |
| 32 | | rexr 11307 |
. . . . 5
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ*) |
| 33 | | sgnval 15127 |
. . . . 5
⊢ (𝐴 ∈ ℝ*
→ (sgn‘𝐴) =
if(𝐴 = 0, 0, if(𝐴 < 0, -1,
1))) |
| 34 | 32, 33 | syl 17 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) |
| 35 | 34 | oveq2d 7447 |
. . 3
⊢ (𝐴 ∈ ℝ → (0
− (sgn‘𝐴)) = (0
− if(𝐴 = 0, 0,
if(𝐴 < 0, -1,
1)))) |
| 36 | | ovif2 7532 |
. . . . 5
⊢ (0
− if(𝐴 = 0, 0,
if(𝐴 < 0, -1, 1))) =
if(𝐴 = 0, (0 − 0), (0
− if(𝐴 < 0, -1,
1))) |
| 37 | | biid 261 |
. . . . . 6
⊢ (𝐴 = 0 ↔ 𝐴 = 0) |
| 38 | | 0m0e0 12386 |
. . . . . 6
⊢ (0
− 0) = 0 |
| 39 | | ovif2 7532 |
. . . . . . 7
⊢ (0
− if(𝐴 < 0, -1,
1)) = if(𝐴 < 0, (0
− -1), (0 − 1)) |
| 40 | | biid 261 |
. . . . . . . 8
⊢ (𝐴 < 0 ↔ 𝐴 < 0) |
| 41 | | 0cn 11253 |
. . . . . . . . . 10
⊢ 0 ∈
ℂ |
| 42 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 43 | 41, 42 | subnegi 11588 |
. . . . . . . . 9
⊢ (0
− -1) = (0 + 1) |
| 44 | | 0p1e1 12388 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
| 45 | 43, 44 | eqtr2i 2766 |
. . . . . . . 8
⊢ 1 = (0
− -1) |
| 46 | | df-neg 11495 |
. . . . . . . 8
⊢ -1 = (0
− 1) |
| 47 | 40, 45, 46 | ifbieq12i 4553 |
. . . . . . 7
⊢ if(𝐴 < 0, 1, -1) = if(𝐴 < 0, (0 − -1), (0
− 1)) |
| 48 | 39, 47 | eqtr4i 2768 |
. . . . . 6
⊢ (0
− if(𝐴 < 0, -1,
1)) = if(𝐴 < 0, 1,
-1) |
| 49 | 37, 38, 48 | ifbieq12i 4553 |
. . . . 5
⊢ if(𝐴 = 0, (0 − 0), (0 −
if(𝐴 < 0, -1, 1))) =
if(𝐴 = 0, 0, if(𝐴 < 0, 1,
-1)) |
| 50 | 36, 49 | eqtri 2765 |
. . . 4
⊢ (0
− if(𝐴 = 0, 0,
if(𝐴 < 0, -1, 1))) =
if(𝐴 = 0, 0, if(𝐴 < 0, 1,
-1)) |
| 51 | 50 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℝ → (0
− if(𝐴 = 0, 0,
if(𝐴 < 0, -1, 1))) =
if(𝐴 = 0, 0, if(𝐴 < 0, 1,
-1))) |
| 52 | 31, 35, 51 | 3eqtrd 2781 |
. 2
⊢ (𝐴 ∈ ℝ →
-(sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, 1, -1))) |
| 53 | 25, 29, 52 | 3eqtr4d 2787 |
1
⊢ (𝐴 ∈ ℝ →
(sgn‘-𝐴) =
-(sgn‘𝐴)) |