Proof of Theorem absmuls
| Step | Hyp | Ref
| Expression |
| 1 | | mulscl 28160 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 ·s 𝐵) ∈ No
) |
| 2 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → (𝐴 ·s 𝐵) ∈ No
) |
| 3 | | simplll 775 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → 𝐴 ∈ No
) |
| 4 | | simpllr 776 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → 𝐵 ∈ No
) |
| 5 | | simplr 769 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → 0s ≤s
𝐴) |
| 6 | | simpr 484 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → 0s ≤s
𝐵) |
| 7 | 3, 4, 5, 6 | mulsge0d 28172 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → 0s ≤s
(𝐴 ·s
𝐵)) |
| 8 | | abssid 28265 |
. . . . . 6
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ 0s ≤s (𝐴 ·s 𝐵)) → (abss‘(𝐴 ·s 𝐵)) = (𝐴 ·s 𝐵)) |
| 9 | 2, 7, 8 | syl2an2r 685 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) →
(abss‘(𝐴
·s 𝐵)) =
(𝐴 ·s
𝐵)) |
| 10 | | abssid 28265 |
. . . . . . 7
⊢ ((𝐵 ∈
No ∧ 0s ≤s 𝐵) → (abss‘𝐵) = 𝐵) |
| 11 | 10 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) →
(abss‘𝐵) =
𝐵) |
| 12 | 11 | oveq2d 7447 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) → (𝐴 ·s
(abss‘𝐵))
= (𝐴 ·s
𝐵)) |
| 13 | 9, 12 | eqtr4d 2780 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 0s ≤s 𝐵) →
(abss‘(𝐴
·s 𝐵)) =
(𝐴 ·s
(abss‘𝐵))) |
| 14 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 𝐴 ∈
No ) |
| 15 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 𝐵 ∈
No ) |
| 16 | 14, 15 | mulnegs2d 28187 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (𝐴 ·s (
-us ‘𝐵)) =
( -us ‘(𝐴
·s 𝐵))) |
| 17 | | abssnid 28267 |
. . . . . . 7
⊢ ((𝐵 ∈
No ∧ 𝐵 ≤s
0s ) → (abss‘𝐵) = ( -us ‘𝐵)) |
| 18 | 17 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) →
(abss‘𝐵) =
( -us ‘𝐵)) |
| 19 | 18 | oveq2d 7447 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (𝐴 ·s
(abss‘𝐵))
= (𝐴 ·s (
-us ‘𝐵))) |
| 20 | | negs0s 28058 |
. . . . . . . 8
⊢ (
-us ‘ 0s ) = 0s |
| 21 | 15 | negscld 28069 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (
-us ‘𝐵)
∈ No ) |
| 22 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 0s
≤s 𝐴) |
| 23 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 𝐵 ≤s 0s
) |
| 24 | | 0sno 27871 |
. . . . . . . . . . . . . 14
⊢
0s ∈ No |
| 25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 0s
∈ No ) |
| 26 | 15, 25 | slenegd 28080 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (𝐵 ≤s 0s ↔ (
-us ‘ 0s ) ≤s ( -us ‘𝐵))) |
| 27 | 23, 26 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (
-us ‘ 0s ) ≤s ( -us ‘𝐵)) |
| 28 | 20, 27 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 0s
≤s ( -us ‘𝐵)) |
| 29 | 14, 21, 22, 28 | mulsge0d 28172 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 0s
≤s (𝐴
·s ( -us ‘𝐵))) |
| 30 | 29, 16 | breqtrd 5169 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → 0s
≤s ( -us ‘(𝐴 ·s 𝐵))) |
| 31 | 20, 30 | eqbrtrid 5178 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (
-us ‘ 0s ) ≤s ( -us ‘(𝐴 ·s 𝐵))) |
| 32 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (𝐴 ·s 𝐵) ∈
No ) |
| 33 | 32, 25 | slenegd 28080 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → ((𝐴 ·s 𝐵) ≤s 0s ↔ (
-us ‘ 0s ) ≤s ( -us ‘(𝐴 ·s 𝐵)))) |
| 34 | 31, 33 | mpbird 257 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) → (𝐴 ·s 𝐵) ≤s 0s
) |
| 35 | | abssnid 28267 |
. . . . . 6
⊢ (((𝐴 ·s 𝐵) ∈
No ∧ (𝐴
·s 𝐵)
≤s 0s ) → (abss‘(𝐴 ·s 𝐵)) = ( -us ‘(𝐴 ·s 𝐵))) |
| 36 | 2, 34, 35 | syl2an2r 685 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
( -us ‘(𝐴
·s 𝐵))) |
| 37 | 16, 19, 36 | 3eqtr4rd 2788 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) ∧ 𝐵 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
(𝐴 ·s
(abss‘𝐵))) |
| 38 | | sletric 27809 |
. . . . . 6
⊢ ((
0s ∈ No ∧ 𝐵 ∈ No )
→ ( 0s ≤s 𝐵 ∨ 𝐵 ≤s 0s )) |
| 39 | 24, 38 | mpan 690 |
. . . . 5
⊢ (𝐵 ∈
No → ( 0s ≤s 𝐵 ∨ 𝐵 ≤s 0s )) |
| 40 | 39 | ad2antlr 727 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → ( 0s ≤s 𝐵 ∨ 𝐵 ≤s 0s )) |
| 41 | 13, 37, 40 | mpjaodan 961 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → (abss‘(𝐴 ·s 𝐵)) = (𝐴 ·s
(abss‘𝐵))) |
| 42 | | abssid 28265 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴) |
| 43 | 42 | adantlr 715 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → (abss‘𝐴) = 𝐴) |
| 44 | 43 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → ((abss‘𝐴) ·s
(abss‘𝐵))
= (𝐴 ·s
(abss‘𝐵))) |
| 45 | 41, 44 | eqtr4d 2780 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 0s ≤s 𝐴) → (abss‘(𝐴 ·s 𝐵)) =
((abss‘𝐴)
·s (abss‘𝐵))) |
| 46 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → 𝐴 ∈
No ) |
| 47 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → 𝐵 ∈
No ) |
| 48 | 46, 47 | mulnegs1d 28186 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → ((
-us ‘𝐴)
·s 𝐵) = (
-us ‘(𝐴
·s 𝐵))) |
| 49 | 10 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
(abss‘𝐵) =
𝐵) |
| 50 | 49 | oveq2d 7447 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → ((
-us ‘𝐴)
·s (abss‘𝐵)) = (( -us ‘𝐴) ·s 𝐵)) |
| 51 | 1 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) → (𝐴 ·s 𝐵) ∈
No ) |
| 52 | 46 | negscld 28069 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (
-us ‘𝐴)
∈ No ) |
| 53 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → 𝐴 ≤s 0s
) |
| 54 | 24 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
0s ∈ No ) |
| 55 | 46, 54 | slenegd 28080 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (𝐴 ≤s 0s ↔ (
-us ‘ 0s ) ≤s ( -us ‘𝐴))) |
| 56 | 53, 55 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (
-us ‘ 0s ) ≤s ( -us ‘𝐴)) |
| 57 | 20, 56 | eqbrtrrid 5179 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
0s ≤s ( -us ‘𝐴)) |
| 58 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
0s ≤s 𝐵) |
| 59 | 52, 47, 57, 58 | mulsge0d 28172 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
0s ≤s (( -us ‘𝐴) ·s 𝐵)) |
| 60 | 59, 48 | breqtrd 5169 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
0s ≤s ( -us ‘(𝐴 ·s 𝐵))) |
| 61 | 20, 60 | eqbrtrid 5178 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (
-us ‘ 0s ) ≤s ( -us ‘(𝐴 ·s 𝐵))) |
| 62 | 51 | adantr 480 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (𝐴 ·s 𝐵) ∈
No ) |
| 63 | 62, 54 | slenegd 28080 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → ((𝐴 ·s 𝐵) ≤s 0s ↔ (
-us ‘ 0s ) ≤s ( -us ‘(𝐴 ·s 𝐵)))) |
| 64 | 61, 63 | mpbird 257 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) → (𝐴 ·s 𝐵) ≤s 0s
) |
| 65 | 51, 64, 35 | syl2an2r 685 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
(abss‘(𝐴
·s 𝐵)) =
( -us ‘(𝐴
·s 𝐵))) |
| 66 | 48, 50, 65 | 3eqtr4rd 2788 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 0s
≤s 𝐵) →
(abss‘(𝐴
·s 𝐵)) =
(( -us ‘𝐴)
·s (abss‘𝐵))) |
| 67 | | simplll 775 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
𝐴 ∈ No ) |
| 68 | | simpllr 776 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
𝐵 ∈ No ) |
| 69 | 67, 68 | mul2negsd 28188 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → ((
-us ‘𝐴)
·s ( -us ‘𝐵)) = (𝐴 ·s 𝐵)) |
| 70 | 17 | ad4ant24 754 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
(abss‘𝐵) =
( -us ‘𝐵)) |
| 71 | 70 | oveq2d 7447 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → ((
-us ‘𝐴)
·s (abss‘𝐵)) = (( -us ‘𝐴) ·s (
-us ‘𝐵))) |
| 72 | 67 | negscld 28069 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → (
-us ‘𝐴)
∈ No ) |
| 73 | 68 | negscld 28069 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → (
-us ‘𝐵)
∈ No ) |
| 74 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
𝐴 ≤s 0s
) |
| 75 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
0s ∈ No ) |
| 76 | 67, 75 | slenegd 28080 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
(𝐴 ≤s 0s
↔ ( -us ‘ 0s ) ≤s ( -us
‘𝐴))) |
| 77 | 74, 76 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → (
-us ‘ 0s ) ≤s ( -us ‘𝐴)) |
| 78 | 20, 77 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
0s ≤s ( -us ‘𝐴)) |
| 79 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
𝐵 ≤s 0s
) |
| 80 | 68, 75 | slenegd 28080 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
(𝐵 ≤s 0s
↔ ( -us ‘ 0s ) ≤s ( -us
‘𝐵))) |
| 81 | 79, 80 | mpbid 232 |
. . . . . . . . 9
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) → (
-us ‘ 0s ) ≤s ( -us ‘𝐵)) |
| 82 | 20, 81 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
0s ≤s ( -us ‘𝐵)) |
| 83 | 72, 73, 78, 82 | mulsge0d 28172 |
. . . . . . 7
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
0s ≤s (( -us ‘𝐴) ·s ( -us
‘𝐵))) |
| 84 | 83, 69 | breqtrd 5169 |
. . . . . 6
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
0s ≤s (𝐴
·s 𝐵)) |
| 85 | 51, 84, 8 | syl2an2r 685 |
. . . . 5
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
(𝐴 ·s
𝐵)) |
| 86 | 69, 71, 85 | 3eqtr4rd 2788 |
. . . 4
⊢ ((((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) ∧ 𝐵 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
(( -us ‘𝐴)
·s (abss‘𝐵))) |
| 87 | 39 | ad2antlr 727 |
. . . 4
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) → (
0s ≤s 𝐵 ∨
𝐵 ≤s 0s
)) |
| 88 | 66, 86, 87 | mpjaodan 961 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
(( -us ‘𝐴)
·s (abss‘𝐵))) |
| 89 | | abssnid 28267 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐴 ≤s
0s ) → (abss‘𝐴) = ( -us ‘𝐴)) |
| 90 | 89 | oveq1d 7446 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐴 ≤s
0s ) → ((abss‘𝐴) ·s
(abss‘𝐵))
= (( -us ‘𝐴) ·s
(abss‘𝐵))) |
| 91 | 90 | adantlr 715 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) →
((abss‘𝐴)
·s (abss‘𝐵)) = (( -us ‘𝐴) ·s
(abss‘𝐵))) |
| 92 | 88, 91 | eqtr4d 2780 |
. 2
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝐴 ≤s 0s ) →
(abss‘(𝐴
·s 𝐵)) =
((abss‘𝐴)
·s (abss‘𝐵))) |
| 93 | | sletric 27809 |
. . . 4
⊢ ((
0s ∈ No ∧ 𝐴 ∈ No )
→ ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s )) |
| 94 | 24, 93 | mpan 690 |
. . 3
⊢ (𝐴 ∈
No → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s )) |
| 95 | 94 | adantr 480 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( 0s ≤s 𝐴 ∨ 𝐴 ≤s 0s )) |
| 96 | 45, 92, 95 | mpjaodan 961 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (abss‘(𝐴 ·s 𝐵)) =
((abss‘𝐴)
·s (abss‘𝐵))) |