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 7316.
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 7101 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cnp 7099 | . . 3 | |
5 | vr | . . . . . . . . . 10 | |
6 | 5 | cv 1330 | . . . . . . . . 9 |
7 | 2 | cv 1330 | . . . . . . . . . 10 |
8 | c1st 6036 | . . . . . . . . . 10 | |
9 | 7, 8 | cfv 5123 | . . . . . . . . 9 |
10 | 6, 9 | wcel 1480 | . . . . . . . 8 |
11 | vs | . . . . . . . . . 10 | |
12 | 11 | cv 1330 | . . . . . . . . 9 |
13 | 3 | cv 1330 | . . . . . . . . . 10 |
14 | 13, 8 | cfv 5123 | . . . . . . . . 9 |
15 | 12, 14 | wcel 1480 | . . . . . . . 8 |
16 | vq | . . . . . . . . . 10 | |
17 | 16 | cv 1330 | . . . . . . . . 9 |
18 | cplq 7090 | . . . . . . . . . 10 | |
19 | 6, 12, 18 | co 5774 | . . . . . . . . 9 |
20 | 17, 19 | wceq 1331 | . . . . . . . 8 |
21 | 10, 15, 20 | w3a 962 | . . . . . . 7 |
22 | cnq 7088 | . . . . . . 7 | |
23 | 21, 11, 22 | wrex 2417 | . . . . . 6 |
24 | 23, 5, 22 | wrex 2417 | . . . . 5 |
25 | 24, 16, 22 | crab 2420 | . . . 4 |
26 | c2nd 6037 | . . . . . . . . . 10 | |
27 | 7, 26 | cfv 5123 | . . . . . . . . 9 |
28 | 6, 27 | wcel 1480 | . . . . . . . 8 |
29 | 13, 26 | cfv 5123 | . . . . . . . . 9 |
30 | 12, 29 | wcel 1480 | . . . . . . . 8 |
31 | 28, 30, 20 | w3a 962 | . . . . . . 7 |
32 | 31, 11, 22 | wrex 2417 | . . . . . 6 |
33 | 32, 5, 22 | wrex 2417 | . . . . 5 |
34 | 33, 16, 22 | crab 2420 | . . . 4 |
35 | 25, 34 | cop 3530 | . . 3 |
36 | 2, 3, 4, 4, 35 | cmpo 5776 | . 2 |
37 | 1, 36 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: addnqprl 7337 addnqpru 7338 addclpr 7345 plpvlu 7346 dmplp 7348 addnqprlemrl 7365 addnqprlemru 7366 addassprg 7387 distrlem1prl 7390 distrlem1pru 7391 distrlem4prl 7392 distrlem4pru 7393 distrlem5prl 7394 distrlem5pru 7395 ltaddpr 7405 ltexprlemfl 7417 ltexprlemrl 7418 ltexprlemfu 7419 ltexprlemru 7420 addcanprleml 7422 addcanprlemu 7423 cauappcvgprlemladdfu 7462 cauappcvgprlemladdfl 7463 caucvgprlemladdfu 7485 |
Copyright terms: Public domain | W3C validator |