ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-plqqs Structured version   Unicode version

Definition df-plqqs 6333
Description: Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 24-Aug-1995.)
Assertion
Ref Expression
df-plqqs  +Q  { <. <. , 
>. ,  >.  | 
Q.  Q.  <. , 
>.  ~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q  }
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-plqqs
StepHypRef Expression
1 cplq 6266 . 2  +Q
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cnq 6264 . . . . . 6  Q.
53, 4wcel 1390 . . . . 5  Q.
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5  Q.
95, 8wa 97 . . . 4  Q.  Q.
10 vw . . . . . . . . . . . . . 14  setvar
1110cv 1241 . . . . . . . . . . . . 13
12 vv . . . . . . . . . . . . . 14  setvar
1312cv 1241 . . . . . . . . . . . . 13
1411, 13cop 3370 . . . . . . . . . . . 12  <. ,  >.
15 ceq 6263 . . . . . . . . . . . 12  ~Q
1614, 15cec 6040 . . . . . . . . . . 11  <. ,  >.  ~Q
173, 16wceq 1242 . . . . . . . . . 10  <. , 
>.  ~Q
18 vu . . . . . . . . . . . . . 14  setvar
1918cv 1241 . . . . . . . . . . . . 13
20 vf . . . . . . . . . . . . . 14  setvar
2120cv 1241 . . . . . . . . . . . . 13
2219, 21cop 3370 . . . . . . . . . . . 12  <. ,  >.
2322, 15cec 6040 . . . . . . . . . . 11  <. ,  >.  ~Q
247, 23wceq 1242 . . . . . . . . . 10  <. , 
>.  ~Q
2517, 24wa 97 . . . . . . . . 9  <. ,  >.  ~Q  <. ,  >.  ~Q
26 vz . . . . . . . . . . 11  setvar
2726cv 1241 . . . . . . . . . 10
28 cplpq 6260 . . . . . . . . . . . 12  +pQ
2914, 22, 28co 5455 . . . . . . . . . . 11  <. ,  >.  +pQ  <. ,  >.
3029, 15cec 6040 . . . . . . . . . 10  <. ,  >.  +pQ 
<. ,  >.  ~Q
3127, 30wceq 1242 . . . . . . . . 9  <. ,  >.  +pQ  <. ,  >.  ~Q
3225, 31wa 97 . . . . . . . 8  <. ,  >. 
~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q
3332, 20wex 1378 . . . . . . 7  <. ,  >. 
~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q
3433, 18wex 1378 . . . . . 6  <. ,  >.  ~Q  <. ,  >.  ~Q  <. , 
>.  +pQ  <. , 
>.  ~Q
3534, 12wex 1378 . . . . 5  <. ,  >. 
~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q
3635, 10wex 1378 . . . 4  <. , 
>.  ~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q
379, 36wa 97 . . 3  Q.  Q.  <. ,  >. 
~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q
3837, 2, 6, 26coprab 5456 . 2  { <. <. ,  >. ,  >.  |  Q.  Q.  <. ,  >. 
~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q  }
391, 38wceq 1242 1  +Q  { <. <. , 
>. ,  >.  | 
Q.  Q.  <. , 
>.  ~Q  <. , 
>.  ~Q  <. ,  >.  +pQ 
<. ,  >.  ~Q  }
Colors of variables: wff set class
This definition is referenced by:  addpipqqs  6354  dmaddpq  6363
  Copyright terms: Public domain W3C validator