Metamath Proof Explorer

Theorem sn-mullt0d

Description: The product of two negative numbers is positive. (Contributed by SN, 1-Dec-2025)

Ref Expression
Hypotheses sn-mullt0d.a 
|- ( ph -> A e. RR )
sn-mullt0d.b 
|- ( ph -> B e. RR )
sn-mullt0d.1 
|- ( ph -> A < 0 )
sn-mullt0d.2 
|- ( ph -> B < 0 )
Assertion sn-mullt0d 
|- ( ph -> 0 < ( A x. B ) )

Proof

Step Hyp Ref Expression
1 sn-mullt0d.a 
 |-  ( ph -> A e. RR )
2 sn-mullt0d.b 
 |-  ( ph -> B e. RR )
3 sn-mullt0d.1 
 |-  ( ph -> A < 0 )
4 sn-mullt0d.2 
 |-  ( ph -> B < 0 )
5 3 lt0ne0d 
 |-  ( ph -> A =/= 0 )
6 4 lt0ne0d 
 |-  ( ph -> B =/= 0 )
7 5 6 jca 
 |-  ( ph -> ( A =/= 0 /\ B =/= 0 ) )
8 neanior 
 |-  ( ( A =/= 0 /\ B =/= 0 ) <-> -. ( A = 0 \/ B = 0 ) )
9 7 8 sylib 
 |-  ( ph -> -. ( A = 0 \/ B = 0 ) )
10 1 2 sn-remul0ord 
 |-  ( ph -> ( ( A x. B ) = 0 <-> ( A = 0 \/ B = 0 ) ) )
11 9 10 mtbird 
 |-  ( ph -> -. ( A x. B ) = 0 )
12 11 neqcomd 
 |-  ( ph -> -. 0 = ( A x. B ) )
13 0red 
 |-  ( ph -> 0 e. RR )
14 2 13 4 ltnsymd 
 |-  ( ph -> -. 0 < B )
15 1 2 3 mullt0b1d 
 |-  ( ph -> ( 0 < B <-> ( A x. B ) < 0 ) )
16 14 15 mtbid 
 |-  ( ph -> -. ( A x. B ) < 0 )
17 ioran 
 |-  ( -. ( 0 = ( A x. B ) \/ ( A x. B ) < 0 ) <-> ( -. 0 = ( A x. B ) /\ -. ( A x. B ) < 0 ) )
18 12 16 17 sylanbrc 
 |-  ( ph -> -. ( 0 = ( A x. B ) \/ ( A x. B ) < 0 ) )
19 1 2 remulcld 
 |-  ( ph -> ( A x. B ) e. RR )
20 13 19 lttrid 
 |-  ( ph -> ( 0 < ( A x. B ) <-> -. ( 0 = ( A x. B ) \/ ( A x. B ) < 0 ) ) )
21 18 20 mpbird 
 |-  ( ph -> 0 < ( A x. B ) )