![]() |
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,
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() 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 7002 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cnp 7000 |
. . 3
![]() ![]() | |
5 | vr |
. . . . . . . . . 10
![]() ![]() | |
6 | 5 | cv 1298 |
. . . . . . . . 9
![]() ![]() |
7 | 2 | cv 1298 |
. . . . . . . . . 10
![]() ![]() |
8 | c1st 5967 |
. . . . . . . . . 10
![]() ![]() | |
9 | 7, 8 | cfv 5059 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wcel 1448 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vs |
. . . . . . . . . 10
![]() ![]() | |
12 | 11 | cv 1298 |
. . . . . . . . 9
![]() ![]() |
13 | 3 | cv 1298 |
. . . . . . . . . 10
![]() ![]() |
14 | 13, 8 | cfv 5059 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 12, 14 | wcel 1448 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | vq |
. . . . . . . . . 10
![]() ![]() | |
17 | 16 | cv 1298 |
. . . . . . . . 9
![]() ![]() |
18 | cplq 6991 |
. . . . . . . . . 10
![]() ![]() | |
19 | 6, 12, 18 | co 5706 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | wceq 1299 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 10, 15, 20 | w3a 930 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cnq 6989 |
. . . . . . 7
![]() ![]() | |
23 | 21, 11, 22 | wrex 2376 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 5, 22 | wrex 2376 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24, 16, 22 | crab 2379 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | c2nd 5968 |
. . . . . . . . . 10
![]() ![]() | |
27 | 7, 26 | cfv 5059 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
28 | 6, 27 | wcel 1448 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 13, 26 | cfv 5059 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
30 | 12, 29 | wcel 1448 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 28, 30, 20 | w3a 930 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 31, 11, 22 | wrex 2376 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 5, 22 | wrex 2376 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 33, 16, 22 | crab 2379 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 25, 34 | cop 3477 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 2, 3, 4, 4, 35 | cmpo 5708 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 1, 36 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: addnqprl 7238 addnqpru 7239 addclpr 7246 plpvlu 7247 dmplp 7249 addnqprlemrl 7266 addnqprlemru 7267 addassprg 7288 distrlem1prl 7291 distrlem1pru 7292 distrlem4prl 7293 distrlem4pru 7294 distrlem5prl 7295 distrlem5pru 7296 ltaddpr 7306 ltexprlemfl 7318 ltexprlemrl 7319 ltexprlemfu 7320 ltexprlemru 7321 addcanprleml 7323 addcanprlemu 7324 cauappcvgprlemladdfu 7363 cauappcvgprlemladdfl 7364 caucvgprlemladdfu 7386 |
Copyright terms: Public domain | W3C validator |