MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  absmuls Structured version   Visualization version   GIF version

Theorem absmuls 28057
Description: Surreal absolute value distributes over multiplication. (Contributed by Scott Fenton, 16-Apr-2025.)
Assertion
Ref Expression
absmuls ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)))

Proof of Theorem absmuls
StepHypRef Expression
1 mulscl 27953 . . . . . . 7 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
21adantr 480 . . . . . 6 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
3 simplll 772 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ ๐ด โˆˆ No )
4 simpllr 773 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ ๐ต โˆˆ No )
5 simplr 766 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs ๐ด)
6 simpr 484 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs ๐ต)
73, 4, 5, 6mulsge0d 27965 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs (๐ด ยทs ๐ต))
8 abssid 28054 . . . . . 6 (((๐ด ยทs ๐ต) โˆˆ No โˆง 0s โ‰คs (๐ด ยทs ๐ต)) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs ๐ต))
92, 7, 8syl2an2r 682 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs ๐ต))
10 abssid 28054 . . . . . . 7 ((๐ต โˆˆ No โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜๐ต) = ๐ต)
1110ad4ant24 751 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜๐ต) = ๐ต)
1211oveq2d 7418 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ (๐ด ยทs (abssโ€˜๐ต)) = (๐ด ยทs ๐ต))
139, 12eqtr4d 2767 . . . 4 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs (abssโ€˜๐ต)))
14 simplll 772 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ด โˆˆ No )
15 simpllr 773 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ต โˆˆ No )
1614, 15mulnegs2d 27980 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ด ยทs ( -us โ€˜๐ต)) = ( -us โ€˜(๐ด ยทs ๐ต)))
17 abssnid 28056 . . . . . . 7 ((๐ต โˆˆ No โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜๐ต) = ( -us โ€˜๐ต))
1817ad4ant24 751 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜๐ต) = ( -us โ€˜๐ต))
1918oveq2d 7418 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ด ยทs (abssโ€˜๐ต)) = (๐ด ยทs ( -us โ€˜๐ต)))
20 negs0s 27858 . . . . . . . 8 ( -us โ€˜ 0s ) = 0s
2115negscld 27868 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜๐ต) โˆˆ No )
22 simplr 766 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs ๐ด)
23 simpr 484 . . . . . . . . . . . 12 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ต โ‰คs 0s )
24 0sno 27678 . . . . . . . . . . . . . 14 0s โˆˆ No
2524a1i 11 . . . . . . . . . . . . 13 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โˆˆ No )
2615, 25slenegd 27879 . . . . . . . . . . . 12 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ต โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ต)))
2723, 26mpbid 231 . . . . . . . . . . 11 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ต))
2820, 27eqbrtrrid 5175 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs ( -us โ€˜๐ต))
2914, 21, 22, 28mulsge0d 27965 . . . . . . . . 9 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs (๐ด ยทs ( -us โ€˜๐ต)))
3029, 16breqtrd 5165 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs ( -us โ€˜(๐ด ยทs ๐ต)))
3120, 30eqbrtrid 5174 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜(๐ด ยทs ๐ต)))
322adantr 480 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
3332, 25slenegd 27879 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ ((๐ด ยทs ๐ต) โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜(๐ด ยทs ๐ต))))
3431, 33mpbird 257 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ด ยทs ๐ต) โ‰คs 0s )
35 abssnid 28056 . . . . . 6 (((๐ด ยทs ๐ต) โˆˆ No โˆง (๐ด ยทs ๐ต) โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ( -us โ€˜(๐ด ยทs ๐ต)))
362, 34, 35syl2an2r 682 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ( -us โ€˜(๐ด ยทs ๐ต)))
3716, 19, 363eqtr4rd 2775 . . . 4 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs (abssโ€˜๐ต)))
38 sletric 27616 . . . . . 6 (( 0s โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ( 0s โ‰คs ๐ต โˆจ ๐ต โ‰คs 0s ))
3924, 38mpan 687 . . . . 5 (๐ต โˆˆ No โ†’ ( 0s โ‰คs ๐ต โˆจ ๐ต โ‰คs 0s ))
4039ad2antlr 724 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ ( 0s โ‰คs ๐ต โˆจ ๐ต โ‰คs 0s ))
4113, 37, 40mpjaodan 955 . . 3 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs (abssโ€˜๐ต)))
42 abssid 28054 . . . . 5 ((๐ด โˆˆ No โˆง 0s โ‰คs ๐ด) โ†’ (abssโ€˜๐ด) = ๐ด)
4342adantlr 712 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ (abssโ€˜๐ด) = ๐ด)
4443oveq1d 7417 . . 3 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)) = (๐ด ยทs (abssโ€˜๐ต)))
4541, 44eqtr4d 2767 . 2 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง 0s โ‰คs ๐ด) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)))
46 simplll 772 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ๐ด โˆˆ No )
47 simpllr 773 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ๐ต โˆˆ No )
4846, 47mulnegs1d 27979 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (( -us โ€˜๐ด) ยทs ๐ต) = ( -us โ€˜(๐ด ยทs ๐ต)))
4910ad4ant24 751 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜๐ต) = ๐ต)
5049oveq2d 7418 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)) = (( -us โ€˜๐ด) ยทs ๐ต))
511adantr 480 . . . . . 6 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
5246negscld 27868 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ( -us โ€˜๐ด) โˆˆ No )
53 simplr 766 . . . . . . . . . . . 12 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ๐ด โ‰คs 0s )
5424a1i 11 . . . . . . . . . . . . 13 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ 0s โˆˆ No )
5546, 54slenegd 27879 . . . . . . . . . . . 12 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (๐ด โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ด)))
5653, 55mpbid 231 . . . . . . . . . . 11 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ด))
5720, 56eqbrtrrid 5175 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs ( -us โ€˜๐ด))
58 simpr 484 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs ๐ต)
5952, 47, 57, 58mulsge0d 27965 . . . . . . . . 9 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs (( -us โ€˜๐ด) ยทs ๐ต))
6059, 48breqtrd 5165 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ 0s โ‰คs ( -us โ€˜(๐ด ยทs ๐ต)))
6120, 60eqbrtrid 5174 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜(๐ด ยทs ๐ต)))
6251adantr 480 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (๐ด ยทs ๐ต) โˆˆ No )
6362, 54slenegd 27879 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ ((๐ด ยทs ๐ต) โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜(๐ด ยทs ๐ต))))
6461, 63mpbird 257 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (๐ด ยทs ๐ต) โ‰คs 0s )
6551, 64, 35syl2an2r 682 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ( -us โ€˜(๐ด ยทs ๐ต)))
6648, 50, 653eqtr4rd 2775 . . . 4 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง 0s โ‰คs ๐ต) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)))
67 simplll 772 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ด โˆˆ No )
68 simpllr 773 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ต โˆˆ No )
6967, 68mul2negsd 27981 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (( -us โ€˜๐ด) ยทs ( -us โ€˜๐ต)) = (๐ด ยทs ๐ต))
7017ad4ant24 751 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜๐ต) = ( -us โ€˜๐ต))
7170oveq2d 7418 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)) = (( -us โ€˜๐ด) ยทs ( -us โ€˜๐ต)))
7267negscld 27868 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜๐ด) โˆˆ No )
7368negscld 27868 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜๐ต) โˆˆ No )
74 simplr 766 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ด โ‰คs 0s )
7524a1i 11 . . . . . . . . . . 11 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โˆˆ No )
7667, 75slenegd 27879 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ด โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ด)))
7774, 76mpbid 231 . . . . . . . . 9 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ด))
7820, 77eqbrtrrid 5175 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs ( -us โ€˜๐ด))
79 simpr 484 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ๐ต โ‰คs 0s )
8068, 75slenegd 27879 . . . . . . . . . 10 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (๐ต โ‰คs 0s โ†” ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ต)))
8179, 80mpbid 231 . . . . . . . . 9 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ ( -us โ€˜ 0s ) โ‰คs ( -us โ€˜๐ต))
8220, 81eqbrtrrid 5175 . . . . . . . 8 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs ( -us โ€˜๐ต))
8372, 73, 78, 82mulsge0d 27965 . . . . . . 7 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs (( -us โ€˜๐ด) ยทs ( -us โ€˜๐ต)))
8483, 69breqtrd 5165 . . . . . 6 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ 0s โ‰คs (๐ด ยทs ๐ต))
8551, 84, 8syl2an2r 682 . . . . 5 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (๐ด ยทs ๐ต))
8669, 71, 853eqtr4rd 2775 . . . 4 ((((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โˆง ๐ต โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)))
8739ad2antlr 724 . . . 4 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โ†’ ( 0s โ‰คs ๐ต โˆจ ๐ต โ‰คs 0s ))
8866, 86, 87mpjaodan 955 . . 3 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)))
89 abssnid 28056 . . . . 5 ((๐ด โˆˆ No โˆง ๐ด โ‰คs 0s ) โ†’ (abssโ€˜๐ด) = ( -us โ€˜๐ด))
9089oveq1d 7417 . . . 4 ((๐ด โˆˆ No โˆง ๐ด โ‰คs 0s ) โ†’ ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)) = (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)))
9190adantlr 712 . . 3 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โ†’ ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)) = (( -us โ€˜๐ด) ยทs (abssโ€˜๐ต)))
9288, 91eqtr4d 2767 . 2 (((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โˆง ๐ด โ‰คs 0s ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)))
93 sletric 27616 . . . 4 (( 0s โˆˆ No โˆง ๐ด โˆˆ No ) โ†’ ( 0s โ‰คs ๐ด โˆจ ๐ด โ‰คs 0s ))
9424, 93mpan 687 . . 3 (๐ด โˆˆ No โ†’ ( 0s โ‰คs ๐ด โˆจ ๐ด โ‰คs 0s ))
9594adantr 480 . 2 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ ( 0s โ‰คs ๐ด โˆจ ๐ด โ‰คs 0s ))
9645, 92, 95mpjaodan 955 1 ((๐ด โˆˆ No โˆง ๐ต โˆˆ No ) โ†’ (abssโ€˜(๐ด ยทs ๐ต)) = ((abssโ€˜๐ด) ยทs (abssโ€˜๐ต)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โˆง wa 395   โˆจ wo 844   = wceq 1533   โˆˆ wcel 2098   class class class wbr 5139  โ€˜cfv 6534  (class class class)co 7402   No csur 27492   โ‰คs csle 27596   0s c0s 27674   -us cnegs 27851   ยทs cmuls 27925  absscabss 28050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-ot 4630  df-uni 4901  df-int 4942  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-1st 7969  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-1o 8462  df-2o 8463  df-nadd 8662  df-no 27495  df-slt 27496  df-bday 27497  df-sle 27597  df-sslt 27633  df-scut 27635  df-0s 27676  df-made 27693  df-old 27694  df-left 27696  df-right 27697  df-norec 27774  df-norec2 27785  df-adds 27796  df-negs 27853  df-subs 27854  df-muls 27926  df-abss 28051
This theorem is referenced by:  remulscllem2  28148
  Copyright terms: Public domain W3C validator