This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulgt1

Description: The product of two numbers greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005) (Proof shortened by SN, 29-Jun-2025)

Ref Expression
Assertion mulgt1 
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < ( A x. B ) )

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 e. RR )
2 simpll 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> A e. RR )
3 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4 3 adantr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> ( A x. B ) e. RR )
5 simprl 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < A )
6 simprr 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < B )
7 0red 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 0 e. RR )
8 0lt1 
 |-  0 < 1
9 8 a1i 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 0 < 1 )
10 7 1 2 9 5 lttrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 0 < A )
11 ltmulgt11 
 |-  ( ( A e. RR /\ B e. RR /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
12 11 3expa 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ 0 < A ) -> ( 1 < B <-> A < ( A x. B ) ) )
13 10 12 syldan 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> ( 1 < B <-> A < ( A x. B ) ) )
14 6 13 mpbid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> A < ( A x. B ) )
15 1 2 4 5 14 lttrd 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 1 < A /\ 1 < B ) ) -> 1 < ( A x. B ) )