Step | Hyp | Ref
| Expression |
1 | | 0sno 27663 |
. . . 4
โข
0s โ No |
2 | 1 | a1i 11 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ 0s โ No ) |
3 | | simpll 764 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ๐ด โ No
) |
4 | | simprl 768 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ๐ต โ No
) |
5 | | simplr 766 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ 0s <s ๐ด) |
6 | | simprr 770 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ 0s <s ๐ต) |
7 | 2, 3, 2, 4, 5, 6 | sltmuld 27941 |
. 2
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ (( 0s
ยทs ๐ต)
-s ( 0s ยทs 0s )) <s
((๐ด ยทs
๐ต) -s (๐ด ยทs
0s ))) |
8 | | muls02 27945 |
. . . . 5
โข (๐ต โ
No โ ( 0s ยทs ๐ต) = 0s ) |
9 | 4, 8 | syl 17 |
. . . 4
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ( 0s
ยทs ๐ต) =
0s ) |
10 | | muls02 27945 |
. . . . . 6
โข (
0s โ No โ ( 0s
ยทs 0s ) = 0s ) |
11 | 1, 10 | ax-mp 5 |
. . . . 5
โข (
0s ยทs 0s ) =
0s |
12 | 11 | a1i 11 |
. . . 4
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ( 0s
ยทs 0s ) = 0s ) |
13 | 9, 12 | oveq12d 7419 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ (( 0s
ยทs ๐ต)
-s ( 0s ยทs 0s )) = (
0s -s 0s )) |
14 | | subsid 27881 |
. . . 4
โข (
0s โ No โ ( 0s
-s 0s ) = 0s ) |
15 | 1, 14 | ax-mp 5 |
. . 3
โข (
0s -s 0s ) = 0s |
16 | 13, 15 | eqtrdi 2780 |
. 2
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ (( 0s
ยทs ๐ต)
-s ( 0s ยทs 0s )) =
0s ) |
17 | | muls01 27916 |
. . . . 5
โข (๐ด โ
No โ (๐ด
ยทs 0s ) = 0s ) |
18 | 3, 17 | syl 17 |
. . . 4
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ (๐ด ยทs 0s ) =
0s ) |
19 | 18 | oveq2d 7417 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ((๐ด ยทs ๐ต) -s (๐ด ยทs 0s )) =
((๐ด ยทs
๐ต) -s
0s )) |
20 | | mulscl 27938 |
. . . . 5
โข ((๐ด โ
No โง ๐ต โ
No ) โ (๐ด ยทs ๐ต) โ No
) |
21 | 20 | ad2ant2r 744 |
. . . 4
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ (๐ด ยทs ๐ต) โ No
) |
22 | | subsid1 27880 |
. . . 4
โข ((๐ด ยทs ๐ต) โ
No โ ((๐ด
ยทs ๐ต)
-s 0s ) = (๐ด ยทs ๐ต)) |
23 | 21, 22 | syl 17 |
. . 3
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ((๐ด ยทs ๐ต) -s 0s ) = (๐ด ยทs ๐ต)) |
24 | 19, 23 | eqtrd 2764 |
. 2
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ ((๐ด ยทs ๐ต) -s (๐ด ยทs 0s )) =
(๐ด ยทs
๐ต)) |
25 | 7, 16, 24 | 3brtr3d 5169 |
1
โข (((๐ด โ
No โง 0s <s ๐ด) โง (๐ต โ No
โง 0s <s ๐ต)) โ 0s <s (๐ด ยทs ๐ต)) |