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 6566 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 6392 | . 2 | |
2 | vx | . . 3 | |
3 | vy | . . 3 | |
4 | cnp 6389 | . . 3 | |
5 | vr | . . . . . . . . . 10 | |
6 | 5 | cv 1242 | . . . . . . . . 9 |
7 | 2 | cv 1242 | . . . . . . . . . 10 |
8 | c1st 5765 | . . . . . . . . . 10 | |
9 | 7, 8 | cfv 4902 | . . . . . . . . 9 |
10 | 6, 9 | wcel 1393 | . . . . . . . 8 |
11 | vs | . . . . . . . . . 10 | |
12 | 11 | cv 1242 | . . . . . . . . 9 |
13 | 3 | cv 1242 | . . . . . . . . . 10 |
14 | 13, 8 | cfv 4902 | . . . . . . . . 9 |
15 | 12, 14 | wcel 1393 | . . . . . . . 8 |
16 | vq | . . . . . . . . . 10 | |
17 | 16 | cv 1242 | . . . . . . . . 9 |
18 | cmq 6381 | . . . . . . . . . 10 | |
19 | 6, 12, 18 | co 5512 | . . . . . . . . 9 |
20 | 17, 19 | wceq 1243 | . . . . . . . 8 |
21 | 10, 15, 20 | w3a 885 | . . . . . . 7 |
22 | cnq 6378 | . . . . . . 7 | |
23 | 21, 11, 22 | wrex 2307 | . . . . . 6 |
24 | 23, 5, 22 | wrex 2307 | . . . . 5 |
25 | 24, 16, 22 | crab 2310 | . . . 4 |
26 | c2nd 5766 | . . . . . . . . . 10 | |
27 | 7, 26 | cfv 4902 | . . . . . . . . 9 |
28 | 6, 27 | wcel 1393 | . . . . . . . 8 |
29 | 13, 26 | cfv 4902 | . . . . . . . . 9 |
30 | 12, 29 | wcel 1393 | . . . . . . . 8 |
31 | 28, 30, 20 | w3a 885 | . . . . . . 7 |
32 | 31, 11, 22 | wrex 2307 | . . . . . 6 |
33 | 32, 5, 22 | wrex 2307 | . . . . 5 |
34 | 33, 16, 22 | crab 2310 | . . . 4 |
35 | 25, 34 | cop 3378 | . . 3 |
36 | 2, 3, 4, 4, 35 | cmpt2 5514 | . 2 |
37 | 1, 36 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: mpvlu 6637 dmmp 6639 mulnqprl 6666 mulnqpru 6667 mulclpr 6670 mulnqprlemrl 6671 mulnqprlemru 6672 mulassprg 6679 distrlem1prl 6680 distrlem1pru 6681 distrlem4prl 6682 distrlem4pru 6683 distrlem5prl 6684 distrlem5pru 6685 1idprl 6688 1idpru 6689 recexprlem1ssl 6731 recexprlem1ssu 6732 recexprlemss1l 6733 recexprlemss1u 6734 |
Copyright terms: Public domain | W3C validator |