Step | Hyp | Ref
| Expression |
1 | | mulcl 7940 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
2 | | 0cnd 7952 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โ
โ) |
3 | | simpl 109 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ
โ) |
4 | 3 | abscld 11192 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ด) โ
โ) |
5 | | simpr 110 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ
โ) |
6 | 5 | abscld 11192 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(absโ๐ต) โ
โ) |
7 | | mincl 11241 |
. . . 4
โข
(((absโ๐ด)
โ โ โง (absโ๐ต) โ โ) โ
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ โ) |
8 | 4, 6, 7 | syl2anc 411 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ โ) |
9 | 8 | recnd 7988 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ โ) |
10 | 3 | absge0d 11195 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(absโ๐ด)) |
11 | 5 | absge0d 11195 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
(absโ๐ต)) |
12 | | 0red 7960 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โ
โ) |
13 | | lemininf 11244 |
. . . . . 6
โข ((0
โ โ โง (absโ๐ด) โ โ โง (absโ๐ต) โ โ) โ (0 โค
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ (0 โค (absโ๐ด) โง 0 โค (absโ๐ต)))) |
14 | 12, 4, 6, 13 | syl3anc 1238 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ (0 โค (absโ๐ด) โง 0 โค (absโ๐ต)))) |
15 | 10, 11, 14 | mpbir2and 944 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ 0 โค
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< )) |
16 | | ap0gt0 8599 |
. . . 4
โข
((inf({(absโ๐ด), (absโ๐ต)}, โ, < ) โ โ โง 0
โค inf({(absโ๐ด),
(absโ๐ต)}, โ,
< )) โ (inf({(absโ๐ด), (absโ๐ต)}, โ, < ) # 0 โ 0 <
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ))) |
17 | 8, 15, 16 | syl2anc 411 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
(inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) # 0 โ 0 < inf({(absโ๐ด), (absโ๐ต)}, โ, < ))) |
18 | | absgt0ap 11110 |
. . . . 5
โข (๐ด โ โ โ (๐ด # 0 โ 0 <
(absโ๐ด))) |
19 | | absgt0ap 11110 |
. . . . 5
โข (๐ต โ โ โ (๐ต # 0 โ 0 <
(absโ๐ต))) |
20 | 18, 19 | bi2anan9 606 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด # 0 โง ๐ต # 0) โ (0 < (absโ๐ด) โง 0 < (absโ๐ต)))) |
21 | | ltmininf 11245 |
. . . . 5
โข ((0
โ โ โง (absโ๐ด) โ โ โง (absโ๐ต) โ โ) โ (0 <
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ (0 < (absโ๐ด) โง 0 < (absโ๐ต)))) |
22 | 12, 4, 6, 21 | syl3anc 1238 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 <
inf({(absโ๐ด),
(absโ๐ต)}, โ,
< ) โ (0 < (absโ๐ด) โง 0 < (absโ๐ต)))) |
23 | 20, 22 | bitr4d 191 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด # 0 โง ๐ต # 0) โ 0 < inf({(absโ๐ด), (absโ๐ต)}, โ, < ))) |
24 | | mulap0b 8614 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด # 0 โง ๐ต # 0) โ (๐ด ยท ๐ต) # 0)) |
25 | 17, 23, 24 | 3bitr2rd 217 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) # 0 โ inf({(absโ๐ด), (absโ๐ต)}, โ, < ) # 0)) |
26 | 1, 2, 9, 2, 25 | apcon4bid 8583 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด ยท ๐ต) = 0 โ inf({(absโ๐ด), (absโ๐ต)}, โ, < ) = 0)) |