Home Metamath Proof Explorer < Previous   Next > Related theorems Unicode version

Definition df-rq 6636
 Description: Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers df-c 6835, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation.
Assertion
Ref Expression
df-rq
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rq
StepHypRef Expression
1 crq 6578 . 2
2 vx . . . . . 6
32cv 1614 . . . . 5
4 cnq 6574 . . . . 5
53, 4wcel 1617 . . . 4
6 vy . . . . . . 7
76cv 1614 . . . . . 6
8 cmq 6577 . . . . . 6
93, 7, 8co 5020 . . . . 5
10 c1q 6575 . . . . 5
119, 10wceq 1615 . . . 4
125, 11wa 433 . . 3
1312, 2, 6copab 3597 . 2
141, 13wceq 1615 1
 Colors of variables: wff set class This definition is referenced by:  recmulpq 6665  dmrecpq 6669