| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > df-nq0 | Unicode version | ||
| Description: Define class of nonnegative 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.) |
| Ref | Expression |
|---|---|
| df-nq0 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnq0 7354 |
. 2
| |
| 2 | com 4626 |
. . . 4
| |
| 3 | cnpi 7339 |
. . . 4
| |
| 4 | 2, 3 | cxp 4661 |
. . 3
|
| 5 | ceq0 7353 |
. . 3
| |
| 6 | 4, 5 | cqs 6591 |
. 2
|
| 7 | 1, 6 | wceq 1364 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: dfmq0qs 7496 dfplq0qs 7497 nq0ex 7507 nqnq0 7508 nq0nn 7509 addclnq0 7518 mulclnq0 7519 distrnq0 7526 mulcomnq0 7527 addassnq0 7529 prarloclemcalc 7569 |
| Copyright terms: Public domain | W3C validator |