![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1e0p1 | Structured version Visualization version GIF version |
Description: The successor of zero. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Ref | Expression |
---|---|
1e0p1 | ⊢ 1 = (0 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0p1e1 11572 | . 2 ⊢ (0 + 1) = 1 | |
2 | 1 | eqcomi 2787 | 1 ⊢ 1 = (0 + 1) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 (class class class)co 6978 0cc0 10337 1c1 10338 + caddc 10340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 ax-resscn 10394 ax-1cn 10395 ax-icn 10396 ax-addcl 10397 ax-addrcl 10398 ax-mulcl 10399 ax-mulrcl 10400 ax-mulcom 10401 ax-addass 10402 ax-mulass 10403 ax-distr 10404 ax-i2m1 10405 ax-1ne0 10406 ax-1rid 10407 ax-rnegex 10408 ax-rrecex 10409 ax-cnre 10410 ax-pre-lttri 10411 ax-pre-lttrn 10412 ax-pre-ltadd 10413 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-nel 3074 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-po 5327 df-so 5328 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-rn 5419 df-res 5420 df-ima 5421 df-iota 6154 df-fun 6192 df-fn 6193 df-f 6194 df-f1 6195 df-fo 6196 df-f1o 6197 df-fv 6198 df-ov 6981 df-er 8091 df-en 8309 df-dom 8310 df-sdom 8311 df-pnf 10478 df-mnf 10479 df-ltxr 10481 |
This theorem is referenced by: 6p5e11 11989 7p4e11 11992 8p3e11 11997 9p2e11 12003 fz1ssfz0 12822 fz0to3un2pr 12828 fzo01 12937 bcp1nk 13495 pfx1 13888 arisum2 15079 ege2le3 15306 ef4p 15329 efgt1p2 15330 efgt1p 15331 bitsmod 15648 prmdiv 15981 prmreclem2 16112 vdwap1 16172 11prm 16307 631prm 16319 mulgnn0p1 18027 gsummptfzsplitl 18809 itgcnlem 24096 dveflem 24282 ply1rem 24463 vieta1lem2 24606 vieta1 24607 pserdvlem2 24722 pserdv2 24724 abelthlem6 24730 abelthlem9 24734 cosne0 24818 logf1o2 24937 logtayl 24947 ang180lem3 25093 birthdaylem2 25235 ftalem5 25359 ppi2 25452 ppiublem2 25484 ppiub 25485 bclbnd 25561 bposlem2 25566 lgsdir2lem3 25608 lgseisenlem1 25656 axlowdimlem13 26446 spthispth 27218 uhgrwkspthlem2 27246 upgr3v3e3cycl 27712 upgr4cycl4dv4e 27717 ballotlemii 31407 ballotlem1c 31411 subfacval2 32019 cvmliftlem5 32121 halffl 40993 sinaover2ne0 41580 stoweidlem11 41728 stoweidlem13 41730 stirlinglem7 41797 fourierdlem48 41871 fourierdlem49 41872 fourierdlem69 41892 fourierdlem79 41902 fourierdlem93 41916 etransclem7 41958 etransclem25 41976 etransclem26 41977 etransclem37 41988 iccpartlt 42957 31prm 43129 1odd 43447 |
Copyright terms: Public domain | W3C validator |