Metamath Proof Explorer


Theorem mulle0b

Description: A condition for multiplication to be nonpositive. (Contributed by Scott Fenton, 25-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 remulcl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ๐ด ยท ๐ต ) โˆˆ โ„ )
2 1 le0neg1d โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( ๐ด ยท ๐ต ) โ‰ค 0 โ†” 0 โ‰ค - ( ๐ด ยท ๐ต ) ) )
3 le0neg2 โŠข ( ๐ต โˆˆ โ„ โ†’ ( 0 โ‰ค ๐ต โ†” - ๐ต โ‰ค 0 ) )
4 3 anbi2d โŠข ( ๐ต โˆˆ โ„ โ†’ ( ( ๐ด โ‰ค 0 โˆง 0 โ‰ค ๐ต ) โ†” ( ๐ด โ‰ค 0 โˆง - ๐ต โ‰ค 0 ) ) )
5 le0neg1 โŠข ( ๐ต โˆˆ โ„ โ†’ ( ๐ต โ‰ค 0 โ†” 0 โ‰ค - ๐ต ) )
6 5 anbi2d โŠข ( ๐ต โˆˆ โ„ โ†’ ( ( 0 โ‰ค ๐ด โˆง ๐ต โ‰ค 0 ) โ†” ( 0 โ‰ค ๐ด โˆง 0 โ‰ค - ๐ต ) ) )
7 4 6 orbi12d โŠข ( ๐ต โˆˆ โ„ โ†’ ( ( ( ๐ด โ‰ค 0 โˆง 0 โ‰ค ๐ต ) โˆจ ( 0 โ‰ค ๐ด โˆง ๐ต โ‰ค 0 ) ) โ†” ( ( ๐ด โ‰ค 0 โˆง - ๐ต โ‰ค 0 ) โˆจ ( 0 โ‰ค ๐ด โˆง 0 โ‰ค - ๐ต ) ) ) )
8 7 adantl โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( ( ๐ด โ‰ค 0 โˆง 0 โ‰ค ๐ต ) โˆจ ( 0 โ‰ค ๐ด โˆง ๐ต โ‰ค 0 ) ) โ†” ( ( ๐ด โ‰ค 0 โˆง - ๐ต โ‰ค 0 ) โˆจ ( 0 โ‰ค ๐ด โˆง 0 โ‰ค - ๐ต ) ) ) )
9 renegcl โŠข ( ๐ต โˆˆ โ„ โ†’ - ๐ต โˆˆ โ„ )
10 mulge0b โŠข ( ( ๐ด โˆˆ โ„ โˆง - ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค ( ๐ด ยท - ๐ต ) โ†” ( ( ๐ด โ‰ค 0 โˆง - ๐ต โ‰ค 0 ) โˆจ ( 0 โ‰ค ๐ด โˆง 0 โ‰ค - ๐ต ) ) ) )
11 9 10 sylan2 โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค ( ๐ด ยท - ๐ต ) โ†” ( ( ๐ด โ‰ค 0 โˆง - ๐ต โ‰ค 0 ) โˆจ ( 0 โ‰ค ๐ด โˆง 0 โ‰ค - ๐ต ) ) ) )
12 recn โŠข ( ๐ด โˆˆ โ„ โ†’ ๐ด โˆˆ โ„‚ )
13 recn โŠข ( ๐ต โˆˆ โ„ โ†’ ๐ต โˆˆ โ„‚ )
14 mulneg2 โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( ๐ด ยท - ๐ต ) = - ( ๐ด ยท ๐ต ) )
15 14 breq2d โŠข ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( 0 โ‰ค ( ๐ด ยท - ๐ต ) โ†” 0 โ‰ค - ( ๐ด ยท ๐ต ) ) )
16 12 13 15 syl2an โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค ( ๐ด ยท - ๐ต ) โ†” 0 โ‰ค - ( ๐ด ยท ๐ต ) ) )
17 8 11 16 3bitr2rd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( 0 โ‰ค - ( ๐ด ยท ๐ต ) โ†” ( ( ๐ด โ‰ค 0 โˆง 0 โ‰ค ๐ต ) โˆจ ( 0 โ‰ค ๐ด โˆง ๐ต โ‰ค 0 ) ) ) )
18 2 17 bitrd โŠข ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ ) โ†’ ( ( ๐ด ยท ๐ต ) โ‰ค 0 โ†” ( ( ๐ด โ‰ค 0 โˆง 0 โ‰ค ๐ต ) โˆจ ( 0 โ‰ค ๐ด โˆง ๐ต โ‰ค 0 ) ) ) )