Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqrlem1.1 | |
|
sqrlem1.2 | |
||
Assertion | sqrlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqrlem1.1 | |
|
2 | sqrlem1.2 | |
|
3 | simpl | |
|
4 | rpre | |
|
5 | rpgt0 | |
|
6 | 1re | |
|
7 | lemul1 | |
|
8 | 6 7 | mp3an2 | |
9 | 4 4 5 8 | syl12anc | |
10 | 9 | biimpa | |
11 | rpcn | |
|
12 | 11 | adantr | |
13 | sqval | |
|
14 | 13 | eqcomd | |
15 | 12 14 | syl | |
16 | 11 | mulid2d | |
17 | 16 | adantr | |
18 | 10 15 17 | 3brtr3d | |
19 | oveq1 | |
|
20 | 19 | breq1d | |
21 | 20 1 | elrab2 | |
22 | 3 18 21 | sylanbrc | |