![]() |
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 6622 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cnp 6620 |
. . 3
![]() ![]() | |
5 | vr |
. . . . . . . . . 10
![]() ![]() | |
6 | 5 | cv 1284 |
. . . . . . . . 9
![]() ![]() |
7 | 2 | cv 1284 |
. . . . . . . . . 10
![]() ![]() |
8 | c1st 5818 |
. . . . . . . . . 10
![]() ![]() | |
9 | 7, 8 | cfv 4953 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wcel 1434 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vs |
. . . . . . . . . 10
![]() ![]() | |
12 | 11 | cv 1284 |
. . . . . . . . 9
![]() ![]() |
13 | 3 | cv 1284 |
. . . . . . . . . 10
![]() ![]() |
14 | 13, 8 | cfv 4953 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 12, 14 | wcel 1434 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | vq |
. . . . . . . . . 10
![]() ![]() | |
17 | 16 | cv 1284 |
. . . . . . . . 9
![]() ![]() |
18 | cplq 6611 |
. . . . . . . . . 10
![]() ![]() | |
19 | 6, 12, 18 | co 5565 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | wceq 1285 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 10, 15, 20 | w3a 920 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cnq 6609 |
. . . . . . 7
![]() ![]() | |
23 | 21, 11, 22 | wrex 2354 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 5, 22 | wrex 2354 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24, 16, 22 | crab 2357 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | c2nd 5819 |
. . . . . . . . . 10
![]() ![]() | |
27 | 7, 26 | cfv 4953 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
28 | 6, 27 | wcel 1434 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 13, 26 | cfv 4953 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
30 | 12, 29 | wcel 1434 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 28, 30, 20 | w3a 920 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 31, 11, 22 | wrex 2354 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 5, 22 | wrex 2354 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 33, 16, 22 | crab 2357 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 25, 34 | cop 3420 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 2, 3, 4, 4, 35 | cmpt2 5567 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 1, 36 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: addnqprl 6858 addnqpru 6859 addclpr 6866 plpvlu 6867 dmplp 6869 addnqprlemrl 6886 addnqprlemru 6887 addassprg 6908 distrlem1prl 6911 distrlem1pru 6912 distrlem4prl 6913 distrlem4pru 6914 distrlem5prl 6915 distrlem5pru 6916 ltaddpr 6926 ltexprlemfl 6938 ltexprlemrl 6939 ltexprlemfu 6940 ltexprlemru 6941 addcanprleml 6943 addcanprlemu 6944 cauappcvgprlemladdfu 6983 cauappcvgprlemladdfl 6984 caucvgprlemladdfu 7006 |
Copyright terms: Public domain | W3C validator |