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 6606.
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 6391 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cnp 6389 | . . 3 | |
5 | vr | . . . . . . . . . 10 | |
6 | 5 | cv 1242 | . . . . . . . . 9 |
7 | 2 | cv 1242 | . . . . . . . . . 10 |
8 | c1st 5765 | . . . . . . . . . 10 | |
9 | 7, 8 | cfv 4902 | . . . . . . . . 9 |
10 | 6, 9 | wcel 1393 | . . . . . . . 8 |
11 | vs | . . . . . . . . . 10 | |
12 | 11 | cv 1242 | . . . . . . . . 9 |
13 | 3 | cv 1242 | . . . . . . . . . 10 |
14 | 13, 8 | cfv 4902 | . . . . . . . . 9 |
15 | 12, 14 | wcel 1393 | . . . . . . . 8 |
16 | vq | . . . . . . . . . 10 | |
17 | 16 | cv 1242 | . . . . . . . . 9 |
18 | cplq 6380 | . . . . . . . . . 10 | |
19 | 6, 12, 18 | co 5512 | . . . . . . . . 9 |
20 | 17, 19 | wceq 1243 | . . . . . . . 8 |
21 | 10, 15, 20 | w3a 885 | . . . . . . 7 |
22 | cnq 6378 | . . . . . . 7 | |
23 | 21, 11, 22 | wrex 2307 | . . . . . 6 |
24 | 23, 5, 22 | wrex 2307 | . . . . 5 |
25 | 24, 16, 22 | crab 2310 | . . . 4 |
26 | c2nd 5766 | . . . . . . . . . 10 | |
27 | 7, 26 | cfv 4902 | . . . . . . . . 9 |
28 | 6, 27 | wcel 1393 | . . . . . . . 8 |
29 | 13, 26 | cfv 4902 | . . . . . . . . 9 |
30 | 12, 29 | wcel 1393 | . . . . . . . 8 |
31 | 28, 30, 20 | w3a 885 | . . . . . . 7 |
32 | 31, 11, 22 | wrex 2307 | . . . . . 6 |
33 | 32, 5, 22 | wrex 2307 | . . . . 5 |
34 | 33, 16, 22 | crab 2310 | . . . 4 |
35 | 25, 34 | cop 3378 | . . 3 |
36 | 2, 3, 4, 4, 35 | cmpt2 5514 | . 2 |
37 | 1, 36 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: addnqprl 6627 addnqpru 6628 addclpr 6635 plpvlu 6636 dmplp 6638 addnqprlemrl 6655 addnqprlemru 6656 addassprg 6677 distrlem1prl 6680 distrlem1pru 6681 distrlem4prl 6682 distrlem4pru 6683 distrlem5prl 6684 distrlem5pru 6685 ltaddpr 6695 ltexprlemfl 6707 ltexprlemrl 6708 ltexprlemfu 6709 ltexprlemru 6710 addcanprleml 6712 addcanprlemu 6713 cauappcvgprlemladdfu 6752 cauappcvgprlemladdfl 6753 caucvgprlemladdfu 6775 |
Copyright terms: Public domain | W3C validator |