Metamath Proof Explorer


Theorem sqrmo

Description: Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion sqrmo A * x x 2 = A 0 x i x +

Proof

Step Hyp Ref Expression
1 simplr1 x x 2 = A 0 x i x + y y 2 = A 0 y i y + x 2 = A
2 simprr1 x x 2 = A 0 x i x + y y 2 = A 0 y i y + y 2 = A
3 1 2 eqtr4d x x 2 = A 0 x i x + y y 2 = A 0 y i y + x 2 = y 2
4 sqeqor x y x 2 = y 2 x = y x = y
5 4 ad2ant2r x x 2 = A 0 x i x + y y 2 = A 0 y i y + x 2 = y 2 x = y x = y
6 3 5 mpbid x x 2 = A 0 x i x + y y 2 = A 0 y i y + x = y x = y
7 6 ord x x 2 = A 0 x i x + y y 2 = A 0 y i y + ¬ x = y x = y
8 3simpc x 2 = A 0 x i x + 0 x i x +
9 fveq2 x = y x = y
10 9 breq2d x = y 0 x 0 y
11 oveq2 x = y i x = i y
12 neleq1 i x = i y i x + i y +
13 11 12 syl x = y i x + i y +
14 10 13 anbi12d x = y 0 x i x + 0 y i y +
15 8 14 syl5ibcom x 2 = A 0 x i x + x = y 0 y i y +
16 15 ad2antlr x x 2 = A 0 x i x + y y 2 = A 0 y i y + x = y 0 y i y +
17 7 16 syld x x 2 = A 0 x i x + y y 2 = A 0 y i y + ¬ x = y 0 y i y +
18 negeq y = 0 y = 0
19 neg0 0 = 0
20 18 19 syl6eq y = 0 y = 0
21 20 eqeq2d y = 0 x = y x = 0
22 eqeq2 y = 0 x = y x = 0
23 21 22 bitr4d y = 0 x = y x = y
24 23 biimpcd x = y y = 0 x = y
25 24 necon3bd x = y ¬ x = y y 0
26 7 25 syli x x 2 = A 0 x i x + y y 2 = A 0 y i y + ¬ x = y y 0
27 3simpc y 2 = A 0 y i y + 0 y i y +
28 cnpart y y 0 0 y i y + ¬ 0 y i y +
29 27 28 syl5ib y y 0 y 2 = A 0 y i y + ¬ 0 y i y +
30 29 impancom y y 2 = A 0 y i y + y 0 ¬ 0 y i y +
31 30 adantl x x 2 = A 0 x i x + y y 2 = A 0 y i y + y 0 ¬ 0 y i y +
32 26 31 syld x x 2 = A 0 x i x + y y 2 = A 0 y i y + ¬ x = y ¬ 0 y i y +
33 17 32 pm2.65d x x 2 = A 0 x i x + y y 2 = A 0 y i y + ¬ ¬ x = y
34 33 notnotrd x x 2 = A 0 x i x + y y 2 = A 0 y i y + x = y
35 34 an4s x y x 2 = A 0 x i x + y 2 = A 0 y i y + x = y
36 35 ex x y x 2 = A 0 x i x + y 2 = A 0 y i y + x = y
37 36 a1i A x y x 2 = A 0 x i x + y 2 = A 0 y i y + x = y
38 37 ralrimivv A x y x 2 = A 0 x i x + y 2 = A 0 y i y + x = y
39 oveq1 x = y x 2 = y 2
40 39 eqeq1d x = y x 2 = A y 2 = A
41 fveq2 x = y x = y
42 41 breq2d x = y 0 x 0 y
43 oveq2 x = y i x = i y
44 neleq1 i x = i y i x + i y +
45 43 44 syl x = y i x + i y +
46 40 42 45 3anbi123d x = y x 2 = A 0 x i x + y 2 = A 0 y i y +
47 46 rmo4 * x x 2 = A 0 x i x + x y x 2 = A 0 x i x + y 2 = A 0 y i y + x = y
48 38 47 sylibr A * x x 2 = A 0 x i x +