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

Definition df-plq0 6410
Description: Define addition on non-negative fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 2-Nov-2019.)
Assertion
Ref Expression
df-plq0 +Q0  { <. <. ,  >. ,  >.  | Q0 Q0  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0  }
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-plq0
StepHypRef Expression
1 cplq0 6273 . 2 +Q0
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cnq0 6271 . . . . . 6 Q0
53, 4wcel 1390 . . . . 5 Q0
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5 Q0
95, 8wa 97 . . . 4 Q0 Q0
10 vw . . . . . . . . . . . . . 14  setvar
1110cv 1241 . . . . . . . . . . . . 13
12 vv . . . . . . . . . . . . . 14  setvar
1312cv 1241 . . . . . . . . . . . . 13
1411, 13cop 3370 . . . . . . . . . . . 12  <. ,  >.
15 ceq0 6270 . . . . . . . . . . . 12 ~Q0
1614, 15cec 6040 . . . . . . . . . . 11  <. ,  >. ~Q0
173, 16wceq 1242 . . . . . . . . . 10  <. , 
>. ~Q0
18 vu . . . . . . . . . . . . . 14  setvar
1918cv 1241 . . . . . . . . . . . . 13
20 vf . . . . . . . . . . . . . 14  setvar
2120cv 1241 . . . . . . . . . . . . 13
2219, 21cop 3370 . . . . . . . . . . . 12  <. ,  >.
2322, 15cec 6040 . . . . . . . . . . 11  <. ,  >. ~Q0
247, 23wceq 1242 . . . . . . . . . 10  <. , 
>. ~Q0
2517, 24wa 97 . . . . . . . . 9  <. ,  >. ~Q0  <. ,  >. ~Q0
26 vz . . . . . . . . . . 11  setvar
2726cv 1241 . . . . . . . . . 10
28 comu 5938 . . . . . . . . . . . . . 14  .o
2911, 21, 28co 5455 . . . . . . . . . . . . 13  .o
3013, 19, 28co 5455 . . . . . . . . . . . . 13  .o
31 coa 5937 . . . . . . . . . . . . 13  +o
3229, 30, 31co 5455 . . . . . . . . . . . 12  .o  +o  .o
3313, 21, 28co 5455 . . . . . . . . . . . 12  .o
3432, 33cop 3370 . . . . . . . . . . 11  <.  .o  +o  .o  ,  .o 
>.
3534, 15cec 6040 . . . . . . . . . 10  <.  .o  +o  .o  ,  .o 
>. ~Q0
3627, 35wceq 1242 . . . . . . . . 9  <.  .o  +o  .o  ,  .o  >. ~Q0
3725, 36wa 97 . . . . . . . 8  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
3837, 20wex 1378 . . . . . . 7  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
3938, 18wex 1378 . . . . . 6  <. ,  >. ~Q0  <. ,  >. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
4039, 12wex 1378 . . . . 5  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
4140, 10wex 1378 . . . 4  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
429, 41wa 97 . . 3 Q0 Q0  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0
4342, 2, 6, 26coprab 5456 . 2  { <. <. ,  >. ,  >.  | Q0 Q0  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0  }
441, 43wceq 1242 1 +Q0  { <. <. ,  >. ,  >.  | Q0 Q0  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  +o  .o  ,  .o  >. ~Q0  }
Colors of variables: wff set class
This definition is referenced by:  dfplq0qs  6413
  Copyright terms: Public domain W3C validator