Metamath Proof Explorer

Theorem halfnq

Description: One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of Gleason p. 120. (Contributed by NM, 16-Mar-1996) (Revised by Mario Carneiro, 10-May-2013) (New usage is discouraged.)

Ref Expression
Assertion halfnq 
|- ( A e. Q. -> E. x ( x +Q x ) = A )

Proof

Step Hyp Ref Expression
1 distrnq 
 |-  ( A .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) )
2 distrnq 
 |-  ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) )
3 1nq 
 |-  1Q e. Q.
4 addclnq 
 |-  ( ( 1Q e. Q. /\ 1Q e. Q. ) -> ( 1Q +Q 1Q ) e. Q. )
5 3 3 4 mp2an 
 |-  ( 1Q +Q 1Q ) e. Q.
6 recidnq 
 |-  ( ( 1Q +Q 1Q ) e. Q. -> ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q )
7 5 6 ax-mp 
 |-  ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q
8 7 7 oveq12i 
 |-  ( ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( 1Q +Q 1Q )
9 2 8 eqtri 
 |-  ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( 1Q +Q 1Q )
10 9 oveq1i 
 |-  ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) )
11 7 oveq2i 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q )
12 mulassnq 
 |-  ( ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) )
13 mulcomnq 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) = ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) )
14 13 oveq1i 
 |-  ( ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) )
15 12 14 eqtr3i 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) )
16 recclnq 
 |-  ( ( 1Q +Q 1Q ) e. Q. -> ( *Q ` ( 1Q +Q 1Q ) ) e. Q. )
17 addclnq 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) e. Q. /\ ( *Q ` ( 1Q +Q 1Q ) ) e. Q. ) -> ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. )
18 16 16 17 syl2anc 
 |-  ( ( 1Q +Q 1Q ) e. Q. -> ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. )
19 mulidnq 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. -> ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) )
20 5 18 19 mp2b 
 |-  ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) )
21 11 15 20 3eqtr3i 
 |-  ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) )
22 10 21 7 3eqtr3i 
 |-  ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q
23 22 oveq2i 
 |-  ( A .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( A .Q 1Q )
24 1 23 eqtr3i 
 |-  ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( A .Q 1Q )
25 mulidnq 
 |-  ( A e. Q. -> ( A .Q 1Q ) = A )
26 24 25 syl5eq 
 |-  ( A e. Q. -> ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A )
27 ovex 
 |-  ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. _V
28 oveq12 
 |-  ( ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) /\ x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) -> ( x +Q x ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) )
29 28 anidms 
 |-  ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) -> ( x +Q x ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) )
30 29 eqeq1d 
 |-  ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) -> ( ( x +Q x ) = A <-> ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A ) )
31 27 30 spcev 
 |-  ( ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A -> E. x ( x +Q x ) = A )
32 26 31 syl 
 |-  ( A e. Q. -> E. x ( x +Q x ) = A )