![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-imp | Unicode version |
Description: Define multiplication on
positive reals. Here we use a simple
definition which is similar to df-iplp 7480 or the definition of
multiplication on positive reals in Metamath Proof Explorer. This is as
opposed to the more complicated definition of multiplication given in
Section 11.2.1 of [HoTT], p. (varies),
which appears to be motivated by
handling negative numbers or handling modified Dedekind cuts in which
locatedness is omitted.
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, 29-Sep-2019.) |
Ref | Expression |
---|---|
df-imp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmp 7306 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cnp 7303 |
. . 3
![]() ![]() | |
5 | vr |
. . . . . . . . . 10
![]() ![]() | |
6 | 5 | cv 1362 |
. . . . . . . . 9
![]() ![]() |
7 | 2 | cv 1362 |
. . . . . . . . . 10
![]() ![]() |
8 | c1st 6152 |
. . . . . . . . . 10
![]() ![]() | |
9 | 7, 8 | cfv 5228 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wcel 2158 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vs |
. . . . . . . . . 10
![]() ![]() | |
12 | 11 | cv 1362 |
. . . . . . . . 9
![]() ![]() |
13 | 3 | cv 1362 |
. . . . . . . . . 10
![]() ![]() |
14 | 13, 8 | cfv 5228 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 12, 14 | wcel 2158 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | vq |
. . . . . . . . . 10
![]() ![]() | |
17 | 16 | cv 1362 |
. . . . . . . . 9
![]() ![]() |
18 | cmq 7295 |
. . . . . . . . . 10
![]() ![]() | |
19 | 6, 12, 18 | co 5888 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | wceq 1363 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 10, 15, 20 | w3a 979 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cnq 7292 |
. . . . . . 7
![]() ![]() | |
23 | 21, 11, 22 | wrex 2466 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 5, 22 | wrex 2466 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24, 16, 22 | crab 2469 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | c2nd 6153 |
. . . . . . . . . 10
![]() ![]() | |
27 | 7, 26 | cfv 5228 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
28 | 6, 27 | wcel 2158 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 13, 26 | cfv 5228 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
30 | 12, 29 | wcel 2158 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 28, 30, 20 | w3a 979 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 31, 11, 22 | wrex 2466 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 5, 22 | wrex 2466 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 33, 16, 22 | crab 2469 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 25, 34 | cop 3607 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 2, 3, 4, 4, 35 | cmpo 5890 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 1, 36 | wceq 1363 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpvlu 7551 dmmp 7553 mulnqprl 7580 mulnqpru 7581 mulclpr 7584 mulnqprlemrl 7585 mulnqprlemru 7586 mulassprg 7593 distrlem1prl 7594 distrlem1pru 7595 distrlem4prl 7596 distrlem4pru 7597 distrlem5prl 7598 distrlem5pru 7599 1idprl 7602 1idpru 7603 recexprlem1ssl 7645 recexprlem1ssu 7646 recexprlemss1l 7647 recexprlemss1u 7648 |
Copyright terms: Public domain | W3C validator |