Metamath Proof Explorer


Definition df-1r

Description: Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.2 of Gleason p. 126. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-1r 1𝑹=1𝑷+𝑷1𝑷1𝑷~𝑹

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1r class1𝑹
1 c1p class1𝑷
2 cpp class+𝑷
3 1 1 2 co class1𝑷+𝑷1𝑷
4 3 1 cop class1𝑷+𝑷1𝑷1𝑷
5 cer class~𝑹
6 4 5 cec class1𝑷+𝑷1𝑷1𝑷~𝑹
7 0 6 wceq wff1𝑹=1𝑷+𝑷1𝑷1𝑷~𝑹