Step |
Hyp |
Ref |
Expression |
1 |
|
halfnq |
|- ( A e. Q. -> E. x ( x +Q x ) = A ) |
2 |
|
eleq1a |
|- ( A e. Q. -> ( ( x +Q x ) = A -> ( x +Q x ) e. Q. ) ) |
3 |
|
addnqf |
|- +Q : ( Q. X. Q. ) --> Q. |
4 |
3
|
fdmi |
|- dom +Q = ( Q. X. Q. ) |
5 |
|
0nnq |
|- -. (/) e. Q. |
6 |
4 5
|
ndmovrcl |
|- ( ( x +Q x ) e. Q. -> ( x e. Q. /\ x e. Q. ) ) |
7 |
|
ltaddnq |
|- ( ( x e. Q. /\ x e. Q. ) -> x |
8 |
6 7
|
syl |
|- ( ( x +Q x ) e. Q. -> x |
9 |
2 8
|
syl6 |
|- ( A e. Q. -> ( ( x +Q x ) = A -> x |
10 |
|
breq2 |
|- ( ( x +Q x ) = A -> ( x x |
11 |
9 10
|
mpbidi |
|- ( A e. Q. -> ( ( x +Q x ) = A -> x |
12 |
11
|
eximdv |
|- ( A e. Q. -> ( E. x ( x +Q x ) = A -> E. x x |
13 |
1 12
|
mpd |
|- ( A e. Q. -> E. x x |