Step |
Hyp |
Ref |
Expression |
1 |
|
oveq12 |
|- ( ( A = 0 /\ A = 0 ) -> ( A x. A ) = ( 0 x. 0 ) ) |
2 |
1
|
anidms |
|- ( A = 0 -> ( A x. A ) = ( 0 x. 0 ) ) |
3 |
|
0cn |
|- 0 e. CC |
4 |
3
|
mul01i |
|- ( 0 x. 0 ) = 0 |
5 |
2 4
|
eqtrdi |
|- ( A = 0 -> ( A x. A ) = 0 ) |
6 |
5
|
breq2d |
|- ( A = 0 -> ( 0 <_ ( A x. A ) <-> 0 <_ 0 ) ) |
7 |
|
0red |
|- ( ( A e. RR /\ A =/= 0 ) -> 0 e. RR ) |
8 |
|
simpl |
|- ( ( A e. RR /\ A =/= 0 ) -> A e. RR ) |
9 |
8 8
|
remulcld |
|- ( ( A e. RR /\ A =/= 0 ) -> ( A x. A ) e. RR ) |
10 |
|
msqgt0 |
|- ( ( A e. RR /\ A =/= 0 ) -> 0 < ( A x. A ) ) |
11 |
7 9 10
|
ltled |
|- ( ( A e. RR /\ A =/= 0 ) -> 0 <_ ( A x. A ) ) |
12 |
|
0re |
|- 0 e. RR |
13 |
|
leid |
|- ( 0 e. RR -> 0 <_ 0 ) |
14 |
12 13
|
mp1i |
|- ( A e. RR -> 0 <_ 0 ) |
15 |
6 11 14
|
pm2.61ne |
|- ( A e. RR -> 0 <_ ( A x. A ) ) |