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 )