Theorem recexpr

Description: The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of Gleason p. 124. (Contributed by NM, 15-May-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	recexpr	$$⊢A\in 𝑷\to \exists x\in 𝑷A{\cdot }_{𝑷}x=1_{𝑷}$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢z=w\to \left(z{<}_{𝑸}y\leftrightarrow w{<}_{𝑸}y\right)$$
2	1	anbi1d	$$⊢z=w\to \left(\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\leftrightarrow \left(w{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right)$$
3	2	exbidv	$$⊢z=w\to \left(\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\leftrightarrow \exists y\left(w{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right)$$
4	3	cbvabv	$$⊢\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}=\left\{w|\exists y\left(w{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}$$
5	4	reclem2pr	$$⊢A\in 𝑷\to \left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}\in 𝑷$$
6	4	reclem4pr	$$⊢A\in 𝑷\to A{\cdot }_{𝑷}\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}=1_{𝑷}$$
7		oveq2	$$⊢x=\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}\to A{\cdot }_{𝑷}x=A{\cdot }_{𝑷}\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}$$
8	7	eqeq1d	$$⊢x=\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}\to \left(A{\cdot }_{𝑷}x=1_{𝑷}\leftrightarrow A{\cdot }_{𝑷}\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}=1_{𝑷}\right)$$
9	8	rspcev	$$⊢\left(\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}\in 𝑷\wedge A{\cdot }_{𝑷}\left\{z|\exists y\left(z{<}_{𝑸}y\wedge \neg {*}_{𝑸}\left(y\right)\in A\right)\right\}=1_{𝑷}\right)\to \exists x\in 𝑷A{\cdot }_{𝑷}x=1_{𝑷}$$
10	5 6 9	syl2anc	$$⊢A\in 𝑷\to \exists x\in 𝑷A{\cdot }_{𝑷}x=1_{𝑷}$$