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 ( 𝐴 ∈ 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 syl5eq ⊢ ( 𝐴 ∈ 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 𝑥 ) = 𝐴 )