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

Metamath Proof Explorer

Definition df-1nq

Description: Define positive fraction 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-2.2 of Gleason p. 117. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion df-1nq 1Q = ⟨ 1o , 1o ⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1q ⊢ 1Q
1 c1o ⊢ 1o
2 1 1 cop ⊢ ⟨ 1o , 1o ⟩
3 0 2 wceq ⊢ 1Q = ⟨ 1o , 1o ⟩