| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Define the number 2.
Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 6836 and df-1 6837).
Note: Only the digits 0 through 9 (df-0 6836
through df-9 7596) and the
number 10 (df-10 7597) are explicitly defined. Integers can be
exhibited
as sums of powers of 10 or as some other expression built from operations
on the numbers 0 through 10. For example, the prime number 823541 can be
expressed as A decimal representation of numbers may be added at some point in the future if it is deemed useful. Ideas for a clean, eliminable definition are welcome. (An awkward earlier definition was deleted from the database on 18-Sep-1999.) |
| Ref | Expression |
|---|---|
| df-2 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | c2 7580 |
. 2
| |
| 2 | c1 6830 |
. . 3
| |
| 3 | caddc 6832 |
. . 3
| |
| 4 | 2, 2, 3 | co 5020 |
. 2
|
| 5 | 1, 4 | wceq 1615 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: 2re 7598 2pos 7609 2nn 7620 2p2e4 7622 2timesi 7624 3p2e5 7628 4p2e6 7630 5p2e7 7633 6p2e8 7637 7p2e9 7640 8p2e10 7642 1lt2 7651 halfpos 7668 addltmul 7675 nneoi 7864 zeo 7866 eluz2b1 8093 fztp 8163 fzprval 8164 fztpval 8165 sqval 8354 discrlem1 8406 fac2 8690 faclbnd4lem1 8701 fsum3 8796 ege2lem2 9106 ege2le3lem2 9107 efaddlem8 9123 eirrlem1 9167 eirrlem3 9169 ef4pi 9180 cos2tsin 9245 cos2bnd 9257 isprm3 9506 2prm 9510 prmunb 9528 dscmet 10212 vc2 10527 ipval2 10717 ip2i 10851 cos2pi 11061 coskpi 11091 1p1e2 11174 hv2times 11556 ho2times 12372 stm1addi 12806 staddi 12807 stadd3i 12809 addltmulALT 13007 mettrifi 16932 heiborlem30 17069 heiborlem32 17071 heiborlem33 17072 heiborlem35 17074 phtpyco 17141 pcoass 17170 |