Metamath Proof Explorer


Theorem sqrlem2

Description: Lemma for 01sqrex . (Contributed by Mario Carneiro, 10-Jul-2013)

Ref Expression
Hypotheses sqrlem1.1 S=x+|x2A
sqrlem1.2 B=supS<
Assertion sqrlem2 A+A1AS

Proof

Step Hyp Ref Expression
1 sqrlem1.1 S=x+|x2A
2 sqrlem1.2 B=supS<
3 simpl A+A1A+
4 rpre A+A
5 rpgt0 A+0<A
6 1re 1
7 lemul1 A1A0<AA1AA1A
8 6 7 mp3an2 AA0<AA1AA1A
9 4 4 5 8 syl12anc A+A1AA1A
10 9 biimpa A+A1AA1A
11 rpcn A+A
12 11 adantr A+A1A
13 sqval AA2=AA
14 13 eqcomd AAA=A2
15 12 14 syl A+A1AA=A2
16 11 mulid2d A+1A=A
17 16 adantr A+A11A=A
18 10 15 17 3brtr3d A+A1A2A
19 oveq1 x=Ax2=A2
20 19 breq1d x=Ax2AA2A
21 20 1 elrab2 ASA+A2A
22 3 18 21 sylanbrc A+A1AS