Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-iplp | Unicode version |
Description: Define addition on
positive reals. From Section 11.2.1 of [HoTT], p.
(varies). We write this definition to closely resemble the definition
in HoTT although some of the conditions are redundant (for example,
implies ) and can be simplified
as
shown at genpdf 6698.
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, 26-Sep-2019.) |
Ref | Expression |
---|---|
df-iplp |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cpp 6483 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cnp 6481 | . . 3 | |
5 | vr | . . . . . . . . . 10 | |
6 | 5 | cv 1283 | . . . . . . . . 9 |
7 | 2 | cv 1283 | . . . . . . . . . 10 |
8 | c1st 5785 | . . . . . . . . . 10 | |
9 | 7, 8 | cfv 4922 | . . . . . . . . 9 |
10 | 6, 9 | wcel 1433 | . . . . . . . 8 |
11 | vs | . . . . . . . . . 10 | |
12 | 11 | cv 1283 | . . . . . . . . 9 |
13 | 3 | cv 1283 | . . . . . . . . . 10 |
14 | 13, 8 | cfv 4922 | . . . . . . . . 9 |
15 | 12, 14 | wcel 1433 | . . . . . . . 8 |
16 | vq | . . . . . . . . . 10 | |
17 | 16 | cv 1283 | . . . . . . . . 9 |
18 | cplq 6472 | . . . . . . . . . 10 | |
19 | 6, 12, 18 | co 5532 | . . . . . . . . 9 |
20 | 17, 19 | wceq 1284 | . . . . . . . 8 |
21 | 10, 15, 20 | w3a 919 | . . . . . . 7 |
22 | cnq 6470 | . . . . . . 7 | |
23 | 21, 11, 22 | wrex 2349 | . . . . . 6 |
24 | 23, 5, 22 | wrex 2349 | . . . . 5 |
25 | 24, 16, 22 | crab 2352 | . . . 4 |
26 | c2nd 5786 | . . . . . . . . . 10 | |
27 | 7, 26 | cfv 4922 | . . . . . . . . 9 |
28 | 6, 27 | wcel 1433 | . . . . . . . 8 |
29 | 13, 26 | cfv 4922 | . . . . . . . . 9 |
30 | 12, 29 | wcel 1433 | . . . . . . . 8 |
31 | 28, 30, 20 | w3a 919 | . . . . . . 7 |
32 | 31, 11, 22 | wrex 2349 | . . . . . 6 |
33 | 32, 5, 22 | wrex 2349 | . . . . 5 |
34 | 33, 16, 22 | crab 2352 | . . . 4 |
35 | 25, 34 | cop 3401 | . . 3 |
36 | 2, 3, 4, 4, 35 | cmpt2 5534 | . 2 |
37 | 1, 36 | wceq 1284 | 1 |
Colors of variables: wff set class |
This definition is referenced by: addnqprl 6719 addnqpru 6720 addclpr 6727 plpvlu 6728 dmplp 6730 addnqprlemrl 6747 addnqprlemru 6748 addassprg 6769 distrlem1prl 6772 distrlem1pru 6773 distrlem4prl 6774 distrlem4pru 6775 distrlem5prl 6776 distrlem5pru 6777 ltaddpr 6787 ltexprlemfl 6799 ltexprlemrl 6800 ltexprlemfu 6801 ltexprlemru 6802 addcanprleml 6804 addcanprlemu 6805 cauappcvgprlemladdfu 6844 cauappcvgprlemladdfl 6845 caucvgprlemladdfu 6867 |
Copyright terms: Public domain | W3C validator |