| 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 6759 and df-1 6760).
Note: Only the digits 0 through 9 (df-0 6759
through df-9 7494) and the
number 10 (df-10 7495) 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 7478 |
. 2
| |
| 2 | c1 6753 |
. . 3
| |
| 3 | caddc 6755 |
. . 3
| |
| 4 | 2, 2, 3 | co 4981 |
. 2
|
| 5 | 1, 4 | wceq 1586 |
1
|
| Colors of variables: wff set class |
| This definition is referenced by: 2re 7496 2pos 7506 2nn 7516 2p2e4 7518 2timesi 7520 3p2e5 7524 4p2e6 7526 5p2e7 7529 6p2e8 7533 7p2e9 7536 8p2e10 7538 1lt2 7547 halfpos 7562 addltmul 7569 nneoi 7752 zeo 7754 eluz2b1 7979 fztp 8049 fzprval 8050 fztpval 8051 sqval 8238 discrlem1 8290 fac2 8574 faclbnd4lem1 8585 fsum3 8680 ege2lem2 8988 ege2le3lem2 8989 efaddlem8 9005 eirrlem1 9049 eirrlem3 9051 ef4pi 9062 cos2tsin 9127 cos2bnd 9139 isprm3 9370 2prm 9374 prmunb 9392 dscmet 10062 vc2 10375 ipval2 10565 ip2i 10697 cos2pi 10905 coskpi 10935 1p1e2 11016 hv2times 11398 ho2times 12214 stm1addi 12648 staddi 12649 stadd3i 12651 addltmulALT 12849 mettrifi 16671 heiborlem30 16808 heiborlem32 16810 heiborlem33 16811 heiborlem35 16813 phtpyco 16880 pcoass 16909 |