Metamath Proof Explorer

Theorem lt2msq1

Description: Lemma for lt2msq . (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lt2msq1 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> A e. RR )
2 1 1 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) e. RR )
3 simp2 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> B e. RR )
4 3 1 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( B x. A ) e. RR )
5 3 3 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( B x. B ) e. RR )
6 simp1 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A e. RR /\ 0 <_ A ) )
7 simp3 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> A < B )
8 1 3 7 ltled 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> A <_ B )
9 lemul1a 
 |-  ( ( ( A e. RR /\ B e. RR /\ ( A e. RR /\ 0 <_ A ) ) /\ A <_ B ) -> ( A x. A ) <_ ( B x. A ) )
10 1 3 6 8 9 syl31anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) <_ ( B x. A ) )
11 0red 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> 0 e. RR )
12 simp1r 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> 0 <_ A )
13 11 1 3 12 7 lelttrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> 0 < B )
14 ltmul2 
 |-  ( ( A e. RR /\ B e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( A < B <-> ( B x. A ) < ( B x. B ) ) )
15 1 3 3 13 14 syl112anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A < B <-> ( B x. A ) < ( B x. B ) ) )
16 7 15 mpbid 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( B x. A ) < ( B x. B ) )
17 2 4 5 10 16 lelttrd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR /\ A < B ) -> ( A x. A ) < ( B x. B ) )