Proof of Theorem sgn3da
| Step | Hyp | Ref
| Expression |
| 1 | | sgn3da.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 2 | | sgnval 15127 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ*
→ (sgn‘𝐴) =
if(𝐴 = 0, 0, if(𝐴 < 0, -1,
1))) |
| 3 | 1, 2 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (sgn‘𝐴) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) |
| 4 | 3 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝜑 → (0 = (sgn‘𝐴) ↔ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
| 5 | 4 | pm5.32i 574 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = (sgn‘𝐴)) ↔ (𝜑 ∧ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
| 6 | | sgn3da.1 |
. . . . . . . . 9
⊢
((sgn‘𝐴) = 0
→ (𝜓 ↔ 𝜒)) |
| 7 | 6 | eqcoms 2745 |
. . . . . . . 8
⊢ (0 =
(sgn‘𝐴) → (𝜓 ↔ 𝜒)) |
| 8 | 7 | bicomd 223 |
. . . . . . 7
⊢ (0 =
(sgn‘𝐴) → (𝜒 ↔ 𝜓)) |
| 9 | 8 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = (sgn‘𝐴)) → (𝜒 ↔ 𝜓)) |
| 10 | 5, 9 | sylbir 235 |
. . . . 5
⊢ ((𝜑 ∧ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) → (𝜒 ↔ 𝜓)) |
| 11 | 10 | expcom 413 |
. . . 4
⊢ (0 =
if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → (𝜑 → (𝜒 ↔ 𝜓))) |
| 12 | 11 | pm5.74d 273 |
. . 3
⊢ (0 =
if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → ((𝜑 → 𝜒) ↔ (𝜑 → 𝜓))) |
| 13 | 3 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝜑 → (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) ↔ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
| 14 | 13 | pm5.32i 574 |
. . . . . 6
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = (sgn‘𝐴)) ↔ (𝜑 ∧ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
| 15 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (-1 =
if(𝐴 < 0, -1, 1) →
(-1 = (sgn‘𝐴) ↔
if(𝐴 < 0, -1, 1) =
(sgn‘𝐴))) |
| 16 | 15 | imbi1d 341 |
. . . . . . . 8
⊢ (-1 =
if(𝐴 < 0, -1, 1) →
((-1 = (sgn‘𝐴) →
(((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) ↔ (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)))) |
| 17 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (1 =
if(𝐴 < 0, -1, 1) →
(1 = (sgn‘𝐴) ↔
if(𝐴 < 0, -1, 1) =
(sgn‘𝐴))) |
| 18 | 17 | imbi1d 341 |
. . . . . . . 8
⊢ (1 =
if(𝐴 < 0, -1, 1) →
((1 = (sgn‘𝐴) →
(((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) ↔ (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)))) |
| 19 | | sgn3da.6 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 0) → 𝜏) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ (𝐴 < 0 → 𝜏)) → 𝜏) |
| 21 | | simp2 1138 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ 𝜏 ∧ 𝐴 < 0) → 𝜏) |
| 22 | 21 | 3expia 1122 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ 𝜏) → (𝐴 < 0 → 𝜏)) |
| 23 | 20, 22 | impbida 801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 < 0 → 𝜏) ↔ 𝜏)) |
| 24 | | pm3.24 402 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(𝐴 < 0 ∧ ¬ 𝐴 < 0) |
| 25 | 24 | pm2.21i 119 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 < 0 ∧ ¬ 𝐴 < 0) → 𝜃) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ ¬ 𝐴 < 0)) → 𝜃) |
| 27 | 26 | expr 456 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 < 0) → (¬ 𝐴 < 0 → 𝜃)) |
| 28 | | tbtru 1548 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐴 < 0 → 𝜃) ↔ ((¬ 𝐴 < 0 → 𝜃) ↔ ⊤)) |
| 29 | 27, 28 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 0) → ((¬ 𝐴 < 0 → 𝜃) ↔ ⊤)) |
| 30 | 23, 29 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ (𝜏 ∧ ⊤))) |
| 31 | | ancom 460 |
. . . . . . . . . . . . 13
⊢ ((𝜏 ∧ ⊤) ↔ (⊤
∧ 𝜏)) |
| 32 | | truan 1551 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝜏)
↔ 𝜏) |
| 33 | 31, 32 | bitri 275 |
. . . . . . . . . . . 12
⊢ ((𝜏 ∧ ⊤) ↔ 𝜏) |
| 34 | 30, 33 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜏)) |
| 35 | 34 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜏)) |
| 36 | | sgn3da.3 |
. . . . . . . . . . . 12
⊢
((sgn‘𝐴) = -1
→ (𝜓 ↔ 𝜏)) |
| 37 | 36 | eqcoms 2745 |
. . . . . . . . . . 11
⊢ (-1 =
(sgn‘𝐴) → (𝜓 ↔ 𝜏)) |
| 38 | 37 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (𝜓 ↔ 𝜏)) |
| 39 | 35, 38 | bitr4d 282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
| 40 | 39 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (-1 = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
| 41 | 19 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 𝐴 < 0) → 𝜏) |
| 42 | 41 | 3expia 1122 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (𝐴 < 0 → 𝜏)) |
| 43 | | tbtru 1548 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 < 0 → 𝜏) ↔ ((𝐴 < 0 → 𝜏) ↔ ⊤)) |
| 44 | 42, 43 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → ((𝐴 < 0 → 𝜏) ↔ ⊤)) |
| 45 | | pm3.35 803 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝐴 < 0 ∧ (¬ 𝐴 < 0 → 𝜃)) → 𝜃) |
| 46 | 45 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ (¬ 𝐴 < 0 → 𝜃)) → 𝜃) |
| 47 | | simp2 1138 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ 𝜃 ∧ ¬ 𝐴 < 0) → 𝜃) |
| 48 | 47 | 3expia 1122 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ 𝜃) → (¬ 𝐴 < 0 → 𝜃)) |
| 49 | 46, 48 | impbida 801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → ((¬ 𝐴 < 0 → 𝜃) ↔ 𝜃)) |
| 50 | 44, 49 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ (⊤ ∧ 𝜃))) |
| 51 | | truan 1551 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝜃)
↔ 𝜃) |
| 52 | 50, 51 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜃)) |
| 53 | 52 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜃)) |
| 54 | | sgn3da.2 |
. . . . . . . . . . . 12
⊢
((sgn‘𝐴) = 1
→ (𝜓 ↔ 𝜃)) |
| 55 | 54 | eqcoms 2745 |
. . . . . . . . . . 11
⊢ (1 =
(sgn‘𝐴) → (𝜓 ↔ 𝜃)) |
| 56 | 55 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (𝜓 ↔ 𝜃)) |
| 57 | 53, 56 | bitr4d 282 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
| 58 | 57 | 3expia 1122 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (1 = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
| 59 | 16, 18, 40, 58 | ifbothda 4564 |
. . . . . . 7
⊢ (𝜑 → (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
| 60 | 59 | imp 406 |
. . . . . 6
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
| 61 | 14, 60 | sylbir 235 |
. . . . 5
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
| 62 | 61 | expcom 413 |
. . . 4
⊢ (if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → (𝜑 → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
| 63 | 62 | pm5.74d 273 |
. . 3
⊢ (if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → ((𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃))) ↔ (𝜑 → 𝜓))) |
| 64 | | sgn3da.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝜒) |
| 65 | 64 | expcom 413 |
. . . 4
⊢ (𝐴 = 0 → (𝜑 → 𝜒)) |
| 66 | 65 | adantl 481 |
. . 3
⊢
((⊤ ∧ 𝐴 =
0) → (𝜑 → 𝜒)) |
| 67 | 19 | ex 412 |
. . . . . . 7
⊢ (𝜑 → (𝐴 < 0 → 𝜏)) |
| 68 | 67 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (𝐴 < 0 → 𝜏)) |
| 69 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 𝜑) |
| 70 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
| 71 | | 0xr 11308 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
| 72 | | xrlttri2 13184 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 0 ∈ ℝ*) → (𝐴 ≠ 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
| 73 | 1, 71, 72 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
| 74 | 70, 73 | bitr3id 285 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐴 = 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
| 75 | 74 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (𝐴 < 0 ∨ 0 < 𝐴)) |
| 76 | 75 | ord 865 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (¬ 𝐴 < 0 → 0 < 𝐴)) |
| 77 | 76 | 3impia 1118 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 0 < 𝐴) |
| 78 | | sgn3da.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝜃) |
| 79 | 69, 77, 78 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 𝜃) |
| 80 | 79 | 3expia 1122 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (¬ 𝐴 < 0 → 𝜃)) |
| 81 | 68, 80 | jca 511 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃))) |
| 82 | 81 | expcom 413 |
. . . 4
⊢ (¬
𝐴 = 0 → (𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)))) |
| 83 | 82 | adantl 481 |
. . 3
⊢
((⊤ ∧ ¬ 𝐴 = 0) → (𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)))) |
| 84 | 12, 63, 66, 83 | ifbothda 4564 |
. 2
⊢ (⊤
→ (𝜑 → 𝜓)) |
| 85 | 84 | mptru 1547 |
1
⊢ (𝜑 → 𝜓) |