Metamath Proof Explorer


Theorem sqrlem5

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

Ref Expression
Hypotheses sqrlem1.1 S=x+|x2A
sqrlem1.2 B=supS<
sqrlem5.3 T=y|aSbSy=ab
Assertion sqrlem5 A+A1TTvuTuvB2=supT<

Proof

Step Hyp Ref Expression
1 sqrlem1.1 S=x+|x2A
2 sqrlem1.2 B=supS<
3 sqrlem5.3 T=y|aSbSy=ab
4 1 ssrab3 S+
5 4 sseli vSv+
6 5 rpge0d vS0v
7 6 rgen vS0v
8 1 2 sqrlem3 A+A1SSvzSzv
9 pm4.24 vS0vvS0vvS0v
10 9 3anbi1i vS0vSSvzSzvSSvzSzvvS0vvS0vSSvzSzvSSvzSzv
11 3 10 supmullem2 vS0vSSvzSzvSSvzSzvTTvuTuv
12 7 8 8 11 mp3an2i A+A1TTvuTuv
13 1 2 sqrlem4 A+A1B+B1
14 rpre B+B
15 14 adantr B+B1B
16 13 15 syl A+A1B
17 16 recnd A+A1B
18 17 sqvald A+A1B2=BB
19 2 2 oveq12i BB=supS<supS<
20 3 10 supmul vS0vSSvzSzvSSvzSzvsupS<supS<=supT<
21 7 8 8 20 mp3an2i A+A1supS<supS<=supT<
22 19 21 eqtrid A+A1BB=supT<
23 18 22 eqtrd A+A1B2=supT<
24 12 23 jca A+A1TTvuTuvB2=supT<