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

Definition df-mq0 6411
Description: Define multiplication 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-mq0 ·Q0  { <. <. , 
>. ,  >.  | Q0 Q0  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  ,  .o  >. ~Q0  }
Distinct variable group:   ,,,,,,

Detailed syntax breakdown of Definition df-mq0
StepHypRef Expression
1 cmq0 6274 . 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 . . . . . . . . . . . . 13  .o
2911, 19, 28co 5455 . . . . . . . . . . . 12  .o
3013, 21, 28co 5455 . . . . . . . . . . . 12  .o
3129, 30cop 3370 . . . . . . . . . . 11  <.  .o  ,  .o  >.
3231, 15cec 6040 . . . . . . . . . 10  <.  .o  ,  .o  >. ~Q0
3327, 32wceq 1242 . . . . . . . . 9  <.  .o  ,  .o  >. ~Q0
3425, 33wa 97 . . . . . . . 8  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  ,  .o  >. ~Q0
3534, 20wex 1378 . . . . . . 7  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  ,  .o  >. ~Q0
3635, 18wex 1378 . . . . . 6  <. ,  >. ~Q0  <. ,  >. ~Q0  <.  .o  ,  .o  >. ~Q0
3736, 12wex 1378 . . . . 5  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  ,  .o  >. ~Q0
3837, 10wex 1378 . . . 4  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  ,  .o  >. ~Q0
399, 38wa 97 . . 3 Q0 Q0  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  ,  .o  >. ~Q0
4039, 2, 6, 26coprab 5456 . 2  { <. <. ,  >. ,  >.  | Q0 Q0  <. , 
>. ~Q0  <. ,  >. ~Q0  <.  .o  ,  .o  >. ~Q0  }
411, 40wceq 1242 1 ·Q0  { <. <. , 
>. ,  >.  | Q0 Q0  <. ,  >. ~Q0  <. , 
>. ~Q0  <.  .o  ,  .o  >. ~Q0  }
Colors of variables: wff set class
This definition is referenced by:  dfmq0qs  6412
  Copyright terms: Public domain W3C validator