Proof of Theorem sgn3da
Step | Hyp | Ref
| Expression |
1 | | sgn3da.0 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
2 | | sgnval 14675 |
. . . . . . . . 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 2749 |
. . . . . . 7
⊢ (𝜑 → (0 = (sgn‘𝐴) ↔ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
5 | 4 | pm5.32i 578 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = (sgn‘𝐴)) ↔ (𝜑 ∧ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
6 | | sgn3da.1 |
. . . . . . . . 9
⊢
((sgn‘𝐴) = 0
→ (𝜓 ↔ 𝜒)) |
7 | 6 | eqcoms 2746 |
. . . . . . . 8
⊢ (0 =
(sgn‘𝐴) → (𝜓 ↔ 𝜒)) |
8 | 7 | bicomd 226 |
. . . . . . 7
⊢ (0 =
(sgn‘𝐴) → (𝜒 ↔ 𝜓)) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 0 = (sgn‘𝐴)) → (𝜒 ↔ 𝜓)) |
10 | 5, 9 | sylbir 238 |
. . . . 5
⊢ ((𝜑 ∧ 0 = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) → (𝜒 ↔ 𝜓)) |
11 | 10 | expcom 417 |
. . . 4
⊢ (0 =
if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → (𝜑 → (𝜒 ↔ 𝜓))) |
12 | 11 | pm5.74d 276 |
. . 3
⊢ (0 =
if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → ((𝜑 → 𝜒) ↔ (𝜑 → 𝜓))) |
13 | 3 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝜑 → (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) ↔ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
14 | 13 | pm5.32i 578 |
. . . . . 6
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = (sgn‘𝐴)) ↔ (𝜑 ∧ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)))) |
15 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (-1 =
if(𝐴 < 0, -1, 1) →
(-1 = (sgn‘𝐴) ↔
if(𝐴 < 0, -1, 1) =
(sgn‘𝐴))) |
16 | 15 | imbi1d 345 |
. . . . . . . 8
⊢ (-1 =
if(𝐴 < 0, -1, 1) →
((-1 = (sgn‘𝐴) →
(((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) ↔ (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)))) |
17 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (1 =
if(𝐴 < 0, -1, 1) →
(1 = (sgn‘𝐴) ↔
if(𝐴 < 0, -1, 1) =
(sgn‘𝐴))) |
18 | 17 | imbi1d 345 |
. . . . . . . 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 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ (𝐴 < 0 → 𝜏)) → 𝜏) |
21 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ 𝜏 ∧ 𝐴 < 0) → 𝜏) |
22 | 21 | 3expia 1123 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 < 0) ∧ 𝜏) → (𝐴 < 0 → 𝜏)) |
23 | 20, 22 | impbida 801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 0) → ((𝐴 < 0 → 𝜏) ↔ 𝜏)) |
24 | | pm3.24 406 |
. . . . . . . . . . . . . . . . 17
⊢ ¬
(𝐴 < 0 ∧ ¬ 𝐴 < 0) |
25 | 24 | pm2.21i 119 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 < 0 ∧ ¬ 𝐴 < 0) → 𝜃) |
26 | 25 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐴 < 0 ∧ ¬ 𝐴 < 0)) → 𝜃) |
27 | 26 | expr 460 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 < 0) → (¬ 𝐴 < 0 → 𝜃)) |
28 | | tbtru 1551 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐴 < 0 → 𝜃) ↔ ((¬ 𝐴 < 0 → 𝜃) ↔ ⊤)) |
29 | 27, 28 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 0) → ((¬ 𝐴 < 0 → 𝜃) ↔ ⊤)) |
30 | 23, 29 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ (𝜏 ∧ ⊤))) |
31 | | ancom 464 |
. . . . . . . . . . . . 13
⊢ ((𝜏 ∧ ⊤) ↔ (⊤
∧ 𝜏)) |
32 | | truan 1554 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝜏)
↔ 𝜏) |
33 | 31, 32 | bitri 278 |
. . . . . . . . . . . 12
⊢ ((𝜏 ∧ ⊤) ↔ 𝜏) |
34 | 30, 33 | bitrdi 290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜏)) |
35 | 34 | 3adant3 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜏)) |
36 | | sgn3da.3 |
. . . . . . . . . . . 12
⊢
((sgn‘𝐴) = -1
→ (𝜓 ↔ 𝜏)) |
37 | 36 | eqcoms 2746 |
. . . . . . . . . . 11
⊢ (-1 =
(sgn‘𝐴) → (𝜓 ↔ 𝜏)) |
38 | 37 | 3ad2ant3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (𝜓 ↔ 𝜏)) |
39 | 35, 38 | bitr4d 285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 0 ∧ -1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
40 | 39 | 3expia 1123 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 0) → (-1 = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
41 | 19 | 3adant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 𝐴 < 0) → 𝜏) |
42 | 41 | 3expia 1123 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (𝐴 < 0 → 𝜏)) |
43 | | tbtru 1551 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 < 0 → 𝜏) ↔ ((𝐴 < 0 → 𝜏) ↔ ⊤)) |
44 | 42, 43 | sylib 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → ((𝐴 < 0 → 𝜏) ↔ ⊤)) |
45 | | pm3.35 803 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝐴 < 0 ∧ (¬ 𝐴 < 0 → 𝜃)) → 𝜃) |
46 | 45 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ (¬ 𝐴 < 0 → 𝜃)) → 𝜃) |
47 | | simp2 1139 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ 𝜃 ∧ ¬ 𝐴 < 0) → 𝜃) |
48 | 47 | 3expia 1123 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝐴 < 0) ∧ 𝜃) → (¬ 𝐴 < 0 → 𝜃)) |
49 | 46, 48 | impbida 801 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → ((¬ 𝐴 < 0 → 𝜃) ↔ 𝜃)) |
50 | 44, 49 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ (⊤ ∧ 𝜃))) |
51 | | truan 1554 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝜃)
↔ 𝜃) |
52 | 50, 51 | bitrdi 290 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜃)) |
53 | 52 | 3adant3 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜃)) |
54 | | sgn3da.2 |
. . . . . . . . . . . 12
⊢
((sgn‘𝐴) = 1
→ (𝜓 ↔ 𝜃)) |
55 | 54 | eqcoms 2746 |
. . . . . . . . . . 11
⊢ (1 =
(sgn‘𝐴) → (𝜓 ↔ 𝜃)) |
56 | 55 | 3ad2ant3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (𝜓 ↔ 𝜃)) |
57 | 53, 56 | bitr4d 285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 < 0 ∧ 1 = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
58 | 57 | 3expia 1123 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 < 0) → (1 = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
59 | 16, 18, 40, 58 | ifbothda 4491 |
. . . . . . 7
⊢ (𝜑 → (if(𝐴 < 0, -1, 1) = (sgn‘𝐴) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
60 | 59 | imp 410 |
. . . . . 6
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = (sgn‘𝐴)) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
61 | 14, 60 | sylbir 238 |
. . . . 5
⊢ ((𝜑 ∧ if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1))) → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓)) |
62 | 61 | expcom 417 |
. . . 4
⊢ (if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → (𝜑 → (((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)) ↔ 𝜓))) |
63 | 62 | pm5.74d 276 |
. . 3
⊢ (if(𝐴 < 0, -1, 1) = if(𝐴 = 0, 0, if(𝐴 < 0, -1, 1)) → ((𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃))) ↔ (𝜑 → 𝜓))) |
64 | | sgn3da.4 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 = 0) → 𝜒) |
65 | 64 | expcom 417 |
. . . 4
⊢ (𝐴 = 0 → (𝜑 → 𝜒)) |
66 | 65 | adantl 485 |
. . 3
⊢
((⊤ ∧ 𝐴 =
0) → (𝜑 → 𝜒)) |
67 | 19 | ex 416 |
. . . . . . 7
⊢ (𝜑 → (𝐴 < 0 → 𝜏)) |
68 | 67 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (𝐴 < 0 → 𝜏)) |
69 | | simp1 1138 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 𝜑) |
70 | | df-ne 2942 |
. . . . . . . . . . . 12
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
71 | | 0xr 10904 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
72 | | xrlttri2 12756 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ*
∧ 0 ∈ ℝ*) → (𝐴 ≠ 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
73 | 1, 71, 72 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ≠ 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
74 | 70, 73 | bitr3id 288 |
. . . . . . . . . . 11
⊢ (𝜑 → (¬ 𝐴 = 0 ↔ (𝐴 < 0 ∨ 0 < 𝐴))) |
75 | 74 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (𝐴 < 0 ∨ 0 < 𝐴)) |
76 | 75 | ord 864 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (¬ 𝐴 < 0 → 0 < 𝐴)) |
77 | 76 | 3impia 1119 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 0 < 𝐴) |
78 | | sgn3da.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ 0 < 𝐴) → 𝜃) |
79 | 69, 77, 78 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 = 0 ∧ ¬ 𝐴 < 0) → 𝜃) |
80 | 79 | 3expia 1123 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → (¬ 𝐴 < 0 → 𝜃)) |
81 | 68, 80 | jca 515 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐴 = 0) → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃))) |
82 | 81 | expcom 417 |
. . . 4
⊢ (¬
𝐴 = 0 → (𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)))) |
83 | 82 | adantl 485 |
. . 3
⊢
((⊤ ∧ ¬ 𝐴 = 0) → (𝜑 → ((𝐴 < 0 → 𝜏) ∧ (¬ 𝐴 < 0 → 𝜃)))) |
84 | 12, 63, 66, 83 | ifbothda 4491 |
. 2
⊢ (⊤
→ (𝜑 → 𝜓)) |
85 | 84 | mptru 1550 |
1
⊢ (𝜑 → 𝜓) |