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 ) )