Metamath Proof Explorer


Theorem resqreu

Description: Existence and uniqueness for the real square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqreu A0A∃!xx2=A0xix+

Proof

Step Hyp Ref Expression
1 resqrex A0Ax0xx2=A
2 recn xx
3 2 adantr x0xx2=Ax
4 simprr x0xx2=Ax2=A
5 rere xx=x
6 5 breq2d x0x0x
7 6 biimpar x0x0x
8 7 adantrr x0xx2=A0x
9 rennim xix+
10 9 adantr x0xx2=Aix+
11 4 8 10 3jca x0xx2=Ax2=A0xix+
12 3 11 jca x0xx2=Axx2=A0xix+
13 12 reximi2 x0xx2=Axx2=A0xix+
14 1 13 syl A0Axx2=A0xix+
15 recn AA
16 15 adantr A0AA
17 sqrmo A*xx2=A0xix+
18 16 17 syl A0A*xx2=A0xix+
19 reu5 ∃!xx2=A0xix+xx2=A0xix+*xx2=A0xix+
20 14 18 19 sylanbrc A0A∃!xx2=A0xix+