Proof of Theorem absslt
Step | Hyp | Ref
| Expression |
1 | | negscl 27922 |
. . . . . . 7
⊢ (𝐴 ∈
No → ( -us ‘𝐴) ∈ No
) |
2 | 1 | ad2antrr 725 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → ( -us ‘𝐴) ∈
No ) |
3 | | absscl 28108 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ No → (abss‘(
-us ‘𝐴))
∈ No ) |
4 | 1, 3 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈
No → (abss‘( -us ‘𝐴)) ∈
No ) |
5 | 4 | ad2antrr 725 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → (abss‘(
-us ‘𝐴))
∈ No ) |
6 | | simplr 768 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → 𝐵 ∈ No
) |
7 | | sleabs 28116 |
. . . . . . . 8
⊢ ((
-us ‘𝐴)
∈ No → ( -us ‘𝐴) ≤s (abss‘(
-us ‘𝐴))) |
8 | 1, 7 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈
No → ( -us ‘𝐴) ≤s (abss‘(
-us ‘𝐴))) |
9 | 8 | ad2antrr 725 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → ( -us ‘𝐴) ≤s (abss‘(
-us ‘𝐴))) |
10 | | abssneg 28115 |
. . . . . . . . 9
⊢ (𝐴 ∈
No → (abss‘( -us ‘𝐴)) =
(abss‘𝐴)) |
11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (abss‘(
-us ‘𝐴)) =
(abss‘𝐴)) |
12 | 11 | breq1d 5152 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((abss‘(
-us ‘𝐴))
<s 𝐵 ↔
(abss‘𝐴)
<s 𝐵)) |
13 | 12 | biimpar 477 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → (abss‘(
-us ‘𝐴))
<s 𝐵) |
14 | 2, 5, 6, 9, 13 | slelttrd 27668 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → ( -us ‘𝐴) <s 𝐵) |
15 | | simpll 766 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → 𝐴 ∈ No
) |
16 | | absscl 28108 |
. . . . . . 7
⊢ (𝐴 ∈
No → (abss‘𝐴) ∈ No
) |
17 | 16 | ad2antrr 725 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → (abss‘𝐴) ∈
No ) |
18 | | sleabs 28116 |
. . . . . . 7
⊢ (𝐴 ∈
No → 𝐴 ≤s
(abss‘𝐴)) |
19 | 18 | ad2antrr 725 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → 𝐴 ≤s (abss‘𝐴)) |
20 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → (abss‘𝐴) <s 𝐵) |
21 | 15, 17, 6, 19, 20 | slelttrd 27668 |
. . . . 5
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → 𝐴 <s 𝐵) |
22 | 14, 21 | jca 511 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (abss‘𝐴) <s 𝐵) → (( -us ‘𝐴) <s 𝐵 ∧ 𝐴 <s 𝐵)) |
23 | 22 | ex 412 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((abss‘𝐴) <s 𝐵 → (( -us ‘𝐴) <s 𝐵 ∧ 𝐴 <s 𝐵))) |
24 | | abssor 28114 |
. . . . 5
⊢ (𝐴 ∈
No → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us
‘𝐴))) |
25 | 24 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us
‘𝐴))) |
26 | | breq1 5145 |
. . . . . . 7
⊢
((abss‘𝐴) = 𝐴 → ((abss‘𝐴) <s 𝐵 ↔ 𝐴 <s 𝐵)) |
27 | 26 | biimprd 247 |
. . . . . 6
⊢
((abss‘𝐴) = 𝐴 → (𝐴 <s 𝐵 → (abss‘𝐴) <s 𝐵)) |
28 | | breq1 5145 |
. . . . . . 7
⊢
((abss‘𝐴) = ( -us ‘𝐴) →
((abss‘𝐴)
<s 𝐵 ↔ (
-us ‘𝐴)
<s 𝐵)) |
29 | 28 | biimprd 247 |
. . . . . 6
⊢
((abss‘𝐴) = ( -us ‘𝐴) → (( -us
‘𝐴) <s 𝐵 →
(abss‘𝐴)
<s 𝐵)) |
30 | 27, 29 | jaoa 954 |
. . . . 5
⊢
(((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us
‘𝐴)) → ((𝐴 <s 𝐵 ∧ ( -us ‘𝐴) <s 𝐵) → (abss‘𝐴) <s 𝐵)) |
31 | 30 | ancomsd 465 |
. . . 4
⊢
(((abss‘𝐴) = 𝐴 ∨ (abss‘𝐴) = ( -us
‘𝐴)) → (((
-us ‘𝐴)
<s 𝐵 ∧ 𝐴 <s 𝐵) → (abss‘𝐴) <s 𝐵)) |
32 | 25, 31 | syl 17 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( -us ‘𝐴) <s 𝐵 ∧ 𝐴 <s 𝐵) → (abss‘𝐴) <s 𝐵)) |
33 | 23, 32 | impbid 211 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐴) <s 𝐵 ∧ 𝐴 <s 𝐵))) |
34 | 1 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( -us ‘𝐴) ∈
No ) |
35 | | simpr 484 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐵 ∈ No
) |
36 | 34, 35 | sltnegd 27933 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( -us ‘𝐴) <s 𝐵 ↔ ( -us ‘𝐵) <s ( -us
‘( -us ‘𝐴)))) |
37 | | negnegs 27930 |
. . . . . 6
⊢ (𝐴 ∈
No → ( -us ‘( -us ‘𝐴)) = 𝐴) |
38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( -us ‘(
-us ‘𝐴)) =
𝐴) |
39 | 38 | breq2d 5154 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( -us ‘𝐵) <s ( -us
‘( -us ‘𝐴)) ↔ ( -us ‘𝐵) <s 𝐴)) |
40 | 36, 39 | bitrd 279 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( -us ‘𝐴) <s 𝐵 ↔ ( -us ‘𝐵) <s 𝐴)) |
41 | 40 | anbi1d 629 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( -us ‘𝐴) <s 𝐵 ∧ 𝐴 <s 𝐵) ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵))) |
42 | 33, 41 | bitrd 279 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((abss‘𝐴) <s 𝐵 ↔ (( -us ‘𝐵) <s 𝐴 ∧ 𝐴 <s 𝐵))) |