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	⊢ ( 𝐴 ∈ P → ∃ 𝑥 ∈ P ( 𝐴 ·P 𝑥 ) = 1P )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑧 = 𝑤 → ( 𝑧 <Q 𝑦 ↔ 𝑤 <Q 𝑦 ) )
2	1	anbi1d	⊢ ( 𝑧 = 𝑤 → ( ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ↔ ( 𝑤 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ) )
3	2	exbidv	⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ↔ ∃ 𝑦 ( 𝑤 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) ) )
4	3	cbvabv	⊢ { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } = { 𝑤 ∣ ∃ 𝑦 ( 𝑤 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) }
5	4	reclem2pr	⊢ ( 𝐴 ∈ P → { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ∈ P )
6	4	reclem4pr	⊢ ( 𝐴 ∈ P → ( 𝐴 ·P { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ) = 1P )
7		oveq2	⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } → ( 𝐴 ·P 𝑥 ) = ( 𝐴 ·P { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ) )
8	7	eqeq1d	⊢ ( 𝑥 = { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } → ( ( 𝐴 ·P 𝑥 ) = 1P ↔ ( 𝐴 ·P { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ) = 1P ) )
9	8	rspcev	⊢ ( ( { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ∈ P ∧ ( 𝐴 ·P { 𝑧 ∣ ∃ 𝑦 ( 𝑧 <Q 𝑦 ∧ ¬ ( *Q ‘ 𝑦 ) ∈ 𝐴 ) } ) = 1P ) → ∃ 𝑥 ∈ P ( 𝐴 ·P 𝑥 ) = 1P )
10	5 6 9	syl2anc	⊢ ( 𝐴 ∈ P → ∃ 𝑥 ∈ P ( 𝐴 ·P 𝑥 ) = 1P )