Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sqrlem1.1 | |
|
sqrlem1.2 | |
||
sqrlem5.3 | |
||
Assertion | sqrlem5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sqrlem1.1 | |
|
2 | sqrlem1.2 | |
|
3 | sqrlem5.3 | |
|
4 | 1 | ssrab3 | |
5 | 4 | sseli | |
6 | 5 | rpge0d | |
7 | 6 | rgen | |
8 | 1 2 | sqrlem3 | |
9 | pm4.24 | |
|
10 | 9 | 3anbi1i | |
11 | 3 10 | supmullem2 | |
12 | 7 8 8 11 | mp3an2i | |
13 | 1 2 | sqrlem4 | |
14 | rpre | |
|
15 | 14 | adantr | |
16 | 13 15 | syl | |
17 | 16 | recnd | |
18 | 17 | sqvald | |
19 | 2 2 | oveq12i | |
20 | 3 10 | supmul | |
21 | 7 8 8 20 | mp3an2i | |
22 | 19 21 | eqtrid | |
23 | 18 22 | eqtrd | |
24 | 12 23 | jca | |