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\in 𝑸\to \exists xx{+}_{𝑸}x=A$$

Proof

Step	Hyp	Ref	Expression
1		distrnq	$$⊢A{\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
2		distrnq	$$⊢\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
3		1nq	$$⊢1_{𝑸}\in 𝑸$$
4		addclnq	$$⊢\left(1_{𝑸}\in 𝑸\wedge 1_{𝑸}\in 𝑸\right)\to 1_{𝑸}{+}_{𝑸}{1}_{𝑸}\in 𝑸$$
5	3 3 4	mp2an	$$⊢1_{𝑸}{+}_{𝑸}{1}_{𝑸}\in 𝑸$$
6		recidnq	$$⊢1_{𝑸}{+}_{𝑸}{1}_{𝑸}\in 𝑸\to \left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=1_{𝑸}$$
7	5 6	ax-mp	$$⊢\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=1_{𝑸}$$
8	7 7	oveq12i	$$⊢\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=1_{𝑸}{+}_{𝑸}{1}_{𝑸}$$
9	2 8	eqtri	$$⊢\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=1_{𝑸}{+}_{𝑸}{1}_{𝑸}$$
10	9	oveq1i	$$⊢\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
11	7	oveq2i	$$⊢\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}{1}_{𝑸}$$
12		mulassnq	$$⊢\left(\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
13		mulcomnq	$$⊢\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
14	13	oveq1i	$$⊢\left(\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
15	12 14	eqtr3i	$$⊢\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
16		recclnq	$$⊢1_{𝑸}{+}_{𝑸}{1}_{𝑸}\in 𝑸\to {*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸$$
17		addclnq	$$⊢\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸\wedge {*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸\right)\to {*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸$$
18	16 16 17	syl2anc	$$⊢1_{𝑸}{+}_{𝑸}{1}_{𝑸}\in 𝑸\to {*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸$$
19		mulidnq	$$⊢{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in 𝑸\to \left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}{1}_{𝑸}={*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
20	5 18 19	mp2b	$$⊢\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){\cdot }_{𝑸}{1}_{𝑸}={*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
21	11 15 20	3eqtr3i	$$⊢\left(\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\right){\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)={*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)$$
22	10 21 7	3eqtr3i	$$⊢{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)=1_{𝑸}$$
23	22	oveq2i	$$⊢A{\cdot }_{𝑸}\left({*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right){+}_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=A{\cdot }_{𝑸}{1}_{𝑸}$$
24	1 23	eqtr3i	$$⊢\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=A{\cdot }_{𝑸}{1}_{𝑸}$$
25		mulidnq	$$⊢A\in 𝑸\to A{\cdot }_{𝑸}{1}_{𝑸}=A$$
26	24 25	eqtrid	$$⊢A\in 𝑸\to \left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=A$$
27		ovex	$$⊢A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\in \mathrm{V}$$
28		oveq12	$$⊢\left(x=A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\wedge x=A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)\to x{+}_{𝑸}x=\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
29	28	anidms	$$⊢x=A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\to x{+}_{𝑸}x=\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)$$
30	29	eqeq1d	$$⊢x=A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\to \left(x{+}_{𝑸}x=A\leftrightarrow \left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=A\right)$$
31	27 30	spcev	$$⊢\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right){+}_{𝑸}\left(A{\cdot }_{𝑸}{*}_{𝑸}\left(1_{𝑸}{+}_{𝑸}{1}_{𝑸}\right)\right)=A\to \exists xx{+}_{𝑸}x=A$$
32	26 31	syl	$$⊢A\in 𝑸\to \exists xx{+}_{𝑸}x=A$$