Description: Square root of square. (Contributed by NM, 14-Jan-2006) (Revised by Mario Carneiro, 29-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | sqrtsq | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |
|
2 | resqcl | |
|
3 | sqge0 | |
|
4 | 2 3 | jca | |
5 | 4 | adantr | |
6 | sqrtsq2 | |
|
7 | 5 6 | mpancom | |
8 | 1 7 | mpbiri | |