This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 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 )