Metamath Proof Explorer


Theorem mulge0

Description: The product of two nonnegative numbers is nonnegative. (Contributed by NM, 8-Oct-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion mulge0 ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) )

Proof

Step Hyp Ref Expression
1 0red โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ 0 โˆˆ โ„ )
2 simpl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐ด โˆˆ โ„ )
3 1 2 leloed โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค ๐ด โ†” ( 0 < ๐ด โˆจ 0 = ๐ด ) ) )
4 simpr โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„ )
5 1 4 leloed โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค ๐ต โ†” ( 0 < ๐ต โˆจ 0 = ๐ต ) ) )
6 3 5 anbi12d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) โ†” ( ( 0 < ๐ด โˆจ 0 = ๐ด ) โˆง ( 0 < ๐ต โˆจ 0 = ๐ต ) ) ) )
7 0red โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ 0 โˆˆ โ„ )
8 simpll โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ ๐ด โˆˆ โ„ )
9 simplr โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ ๐ต โˆˆ โ„ )
10 8 9 remulcld โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„ )
11 mulgt0 โŠข ( ( ( ๐ด โˆˆ โ„ โˆง 0 < ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 < ๐ต ) ) โ†’ 0 < ( ๐ด ยท ๐ต ) )
12 11 an4s โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ 0 < ( ๐ด ยท ๐ต ) )
13 7 10 12 ltled โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 < ๐ด โˆง 0 < ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) )
14 13 ex โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 < ๐ด โˆง 0 < ๐ต ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
15 0re โŠข 0 โˆˆ โ„
16 leid โŠข ( 0 โˆˆ โ„ โ†’ 0 โ‰ค 0 )
17 15 16 ax-mp โŠข 0 โ‰ค 0
18 4 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐ต โˆˆ โ„‚ )
19 18 mul02d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 ยท ๐ต ) = 0 )
20 17 19 breqtrrid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ 0 โ‰ค ( 0 ยท ๐ต ) )
21 oveq1 โŠข ( 0 = ๐ด โ†’ ( 0 ยท ๐ต ) = ( ๐ด ยท ๐ต ) )
22 21 breq2d โŠข ( 0 = ๐ด โ†’ ( 0 โ‰ค ( 0 ยท ๐ต ) โ†” 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
23 20 22 syl5ibcom โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 = ๐ด โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
24 23 adantrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 = ๐ด โˆง 0 < ๐ต ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
25 2 recnd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ๐ด โˆˆ โ„‚ )
26 25 mul01d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ๐ด ยท 0 ) = 0 )
27 17 26 breqtrrid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ 0 โ‰ค ( ๐ด ยท 0 ) )
28 oveq2 โŠข ( 0 = ๐ต โ†’ ( ๐ด ยท 0 ) = ( ๐ด ยท ๐ต ) )
29 28 breq2d โŠข ( 0 = ๐ต โ†’ ( 0 โ‰ค ( ๐ด ยท 0 ) โ†” 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
30 27 29 syl5ibcom โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 = ๐ต โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
31 30 adantld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 < ๐ด โˆง 0 = ๐ต ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
32 30 adantld โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 = ๐ด โˆง 0 = ๐ต ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
33 14 24 31 32 ccased โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( ( 0 < ๐ด โˆจ 0 = ๐ด ) โˆง ( 0 < ๐ต โˆจ 0 = ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
34 6 33 sylbid โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) ) )
35 34 imp โŠข ( ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โˆง ( 0 โ‰ค ๐ด โˆง 0 โ‰ค ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) )
36 35 an4s โŠข ( ( ( ๐ด โˆˆ โ„ โˆง 0 โ‰ค ๐ด ) โˆง ( ๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต ) ) โ†’ 0 โ‰ค ( ๐ด ยท ๐ต ) )