Metamath Proof Explorer


Theorem msqge0

Description: A square is nonnegative. (Contributed by NM, 23-May-2007) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion msqge0 A 0 A A

Proof

Step Hyp Ref Expression
1 oveq12 A = 0 A = 0 A A = 0 0
2 1 anidms A = 0 A A = 0 0
3 0cn 0
4 3 mul01i 0 0 = 0
5 2 4 eqtrdi A = 0 A A = 0
6 5 breq2d A = 0 0 A A 0 0
7 0red A A 0 0
8 simpl A A 0 A
9 8 8 remulcld A A 0 A A
10 msqgt0 A A 0 0 < A A
11 7 9 10 ltled A A 0 0 A A
12 0re 0
13 leid 0 0 0
14 12 13 mp1i A 0 0
15 6 11 14 pm2.61ne A 0 A A