![]() |
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 7088 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 6914 |
. 2
![]() ![]() | |
2 | vx |
. . 3
![]() ![]() | |
3 | vy |
. . 3
![]() ![]() | |
4 | cnp 6911 |
. . 3
![]() ![]() | |
5 | vr |
. . . . . . . . . 10
![]() ![]() | |
6 | 5 | cv 1289 |
. . . . . . . . 9
![]() ![]() |
7 | 2 | cv 1289 |
. . . . . . . . . 10
![]() ![]() |
8 | c1st 5923 |
. . . . . . . . . 10
![]() ![]() | |
9 | 7, 8 | cfv 5028 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
10 | 6, 9 | wcel 1439 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
11 | vs |
. . . . . . . . . 10
![]() ![]() | |
12 | 11 | cv 1289 |
. . . . . . . . 9
![]() ![]() |
13 | 3 | cv 1289 |
. . . . . . . . . 10
![]() ![]() |
14 | 13, 8 | cfv 5028 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
15 | 12, 14 | wcel 1439 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | vq |
. . . . . . . . . 10
![]() ![]() | |
17 | 16 | cv 1289 |
. . . . . . . . 9
![]() ![]() |
18 | cmq 6903 |
. . . . . . . . . 10
![]() ![]() | |
19 | 6, 12, 18 | co 5666 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
20 | 17, 19 | wceq 1290 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | 10, 15, 20 | w3a 925 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
22 | cnq 6900 |
. . . . . . 7
![]() ![]() | |
23 | 21, 11, 22 | wrex 2361 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
24 | 23, 5, 22 | wrex 2361 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 24, 16, 22 | crab 2364 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | c2nd 5924 |
. . . . . . . . . 10
![]() ![]() | |
27 | 7, 26 | cfv 5028 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
28 | 6, 27 | wcel 1439 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
29 | 13, 26 | cfv 5028 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() |
30 | 12, 29 | wcel 1439 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 28, 30, 20 | w3a 925 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 31, 11, 22 | wrex 2361 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 32, 5, 22 | wrex 2361 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | 33, 16, 22 | crab 2364 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
35 | 25, 34 | cop 3453 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 2, 3, 4, 4, 35 | cmpt2 5668 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 1, 36 | wceq 1290 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: mpvlu 7159 dmmp 7161 mulnqprl 7188 mulnqpru 7189 mulclpr 7192 mulnqprlemrl 7193 mulnqprlemru 7194 mulassprg 7201 distrlem1prl 7202 distrlem1pru 7203 distrlem4prl 7204 distrlem4pru 7205 distrlem5prl 7206 distrlem5pru 7207 1idprl 7210 1idpru 7211 recexprlem1ssl 7253 recexprlem1ssu 7254 recexprlemss1l 7255 recexprlemss1u 7256 |
Copyright terms: Public domain | W3C validator |