Metamath Proof Explorer

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 (z <_{𝑸} y \leftrightarrow w <_{𝑸} y)$
2	1	anbi1d	$⊢ z = w \to ((z <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow (w <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
3	2	exbidv	$⊢ z = w \to (\exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A) \leftrightarrow \exists y (w <_{𝑸} y \land \neg _{𝑸} (y) \in A))$
4	3	cbvabv	$⊢ \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} = \{w \| \exists y (w <_{𝑸} y \land \neg _{𝑸} (y) \in A)\}$
5	4	reclem2pr	$⊢ A \in 𝑷 \to \{z \| \exists y (z <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\} \in 𝑷$
6	4	reclem4pr	$⊢ A \in 𝑷 \to A \cdot_{𝑷} \{z \| \exists y (z <_{𝑸} y \land \neg *_{𝑸} (y) \in A)\} = 1_{𝑷}$
7		oveq2	$⊢ x = \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} \to A \cdot_{𝑷} x = A \cdot_{𝑷} \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\}$
8	7	eqeq1d	$⊢ x = \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} \to (A \cdot_{𝑷} x = 1_{𝑷} \leftrightarrow A \cdot_{𝑷} \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} = 1_{𝑷})$
9	8	rspcev	$⊢ (\{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} \in 𝑷 \land A \cdot_{𝑷} \{z \| \exists y (z <_{𝑸} y \land \neg _{𝑸} (y) \in A)\} = 1_{𝑷}) \to \exists x \in 𝑷 A \cdot_{𝑷} x = 1_{𝑷}$
10	5 6 9	syl2anc	$⊢ A \in 𝑷 \to \exists x \in 𝑷 A \cdot_{𝑷} x = 1_{𝑷}$