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	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 ( 𝑥 +Q 𝑥 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		distrnq	⊢ ( 𝐴 ·Q ( ( *Q ‘ ( 1Q +Q 1Q ) ) +Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·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 ∈ Q
4		addclnq	⊢ ( ( 1Q ∈ Q ∧ 1Q ∈ Q ) → ( 1Q +Q 1Q ) ∈ Q )
5	3 3 4	mp2an	⊢ ( 1Q +Q 1Q ) ∈ Q
6		recidnq	⊢ ( ( 1Q +Q 1Q ) ∈ 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 ) ∈ Q → ( *Q ‘ ( 1Q +Q 1Q ) ) ∈ Q )
17		addclnq	⊢ ( ( ( *Q ‘ ( 1Q +Q 1Q ) ) ∈ Q ∧ ( *Q ‘ ( 1Q +Q 1Q ) ) ∈ Q ) → ( ( *Q ‘ ( 1Q +Q 1Q ) ) +Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ∈ Q )
18	16 16 17	syl2anc	⊢ ( ( 1Q +Q 1Q ) ∈ Q → ( ( *Q ‘ ( 1Q +Q 1Q ) ) +Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ∈ Q )
19		mulidnq	⊢ ( ( ( *Q ‘ ( 1Q +Q 1Q ) ) +Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ∈ 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	⊢ ( 𝐴 ·Q ( ( *Q ‘ ( 1Q +Q 1Q ) ) +Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = ( 𝐴 ·Q 1Q )
24	1 23	eqtr3i	⊢ ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = ( 𝐴 ·Q 1Q )
25		mulidnq	⊢ ( 𝐴 ∈ Q → ( 𝐴 ·Q 1Q ) = 𝐴 )
26	24 25	eqtrid	⊢ ( 𝐴 ∈ Q → ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = 𝐴 )
27		ovex	⊢ ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ∈ V
28		oveq12	⊢ ( ( 𝑥 = ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ∧ 𝑥 = ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) → ( 𝑥 +Q 𝑥 ) = ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) )
29	28	anidms	⊢ ( 𝑥 = ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) → ( 𝑥 +Q 𝑥 ) = ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) )
30	29	eqeq1d	⊢ ( 𝑥 = ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) → ( ( 𝑥 +Q 𝑥 ) = 𝐴 ↔ ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = 𝐴 ) )
31	27 30	spcev	⊢ ( ( ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) +Q ( 𝐴 ·Q ( *Q ‘ ( 1Q +Q 1Q ) ) ) ) = 𝐴 → ∃ 𝑥 ( 𝑥 +Q 𝑥 ) = 𝐴 )
32	26 31	syl	⊢ ( 𝐴 ∈ Q → ∃ 𝑥 ( 𝑥 +Q 𝑥 ) = 𝐴 )