Metamath Proof Explorer


Theorem int-sqgeq0d

Description: SquareGEQZero generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-sqgeq0d.1
|- ( ph -> A e. RR )
int-sqgeq0d.2
|- ( ph -> B e. RR )
int-sqgeq0d.3
|- ( ph -> A = B )
Assertion int-sqgeq0d
|- ( ph -> 0 <_ ( A x. B ) )

Proof

Step Hyp Ref Expression
1 int-sqgeq0d.1
 |-  ( ph -> A e. RR )
2 int-sqgeq0d.2
 |-  ( ph -> B e. RR )
3 int-sqgeq0d.3
 |-  ( ph -> A = B )
4 1 sqge0d
 |-  ( ph -> 0 <_ ( A ^ 2 ) )
5 3 oveq1d
 |-  ( ph -> ( A ^ 2 ) = ( B ^ 2 ) )
6 2 recnd
 |-  ( ph -> B e. CC )
7 6 sqvald
 |-  ( ph -> ( B ^ 2 ) = ( B x. B ) )
8 eqcom
 |-  ( A = B <-> B = A )
9 8 imbi2i
 |-  ( ( ph -> A = B ) <-> ( ph -> B = A ) )
10 3 9 mpbi
 |-  ( ph -> B = A )
11 10 oveq1d
 |-  ( ph -> ( B x. B ) = ( A x. B ) )
12 7 11 eqtrd
 |-  ( ph -> ( B ^ 2 ) = ( A x. B ) )
13 5 12 eqtrd
 |-  ( ph -> ( A ^ 2 ) = ( A x. B ) )
14 4 13 breqtrd
 |-  ( ph -> 0 <_ ( A x. B ) )