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