Step | Hyp | Ref
| Expression |
1 | | remulcl 11141 |
. 2
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
2 | | mulcl 11140 |
. 2
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ ยท ๐ฆ) โ โ) |
3 | | simp2l 1200 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ ๐ฅ โ โ) |
4 | | simp2r 1201 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ ๐ฆ โ โ) |
5 | 3, 4 | absmuld 15345 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ(๐ฅ ยท ๐ฆ)) = ((absโ๐ฅ) ยท (absโ๐ฆ))) |
6 | 3 | abscld 15327 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ๐ฅ) โ โ) |
7 | | simp1l 1198 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ ๐ โ โ) |
8 | 4 | abscld 15327 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ๐ฆ) โ โ) |
9 | | simp1r 1199 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ ๐ โ โ) |
10 | 3 | absge0d 15335 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ 0 โค (absโ๐ฅ)) |
11 | 4 | absge0d 15335 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ 0 โค (absโ๐ฆ)) |
12 | | simp3l 1202 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ๐ฅ) โค ๐) |
13 | | simp3r 1203 |
. . . . 5
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ๐ฆ) โค ๐) |
14 | 6, 7, 8, 9, 10, 11, 12, 13 | lemul12ad 12102 |
. . . 4
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ ((absโ๐ฅ) ยท (absโ๐ฆ)) โค (๐ ยท ๐)) |
15 | 5, 14 | eqbrtrd 5128 |
. . 3
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ) โง
((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐)) โ (absโ(๐ฅ ยท ๐ฆ)) โค (๐ ยท ๐)) |
16 | 15 | 3expia 1122 |
. 2
โข (((๐ โ โ โง ๐ โ โ) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
(((absโ๐ฅ) โค ๐ โง (absโ๐ฆ) โค ๐) โ (absโ(๐ฅ ยท ๐ฆ)) โค (๐ ยท ๐))) |
17 | 1, 2, 16 | o1of2 15501 |
1
โข ((๐น โ ๐(1) โง ๐บ โ ๐(1)) โ
(๐น โf
ยท ๐บ) โ
๐(1)) |