MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  5re Unicode version

Theorem 5re 9669
Description: The number 5 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
5re  |-  5  e.  RR

Proof of Theorem 5re
StepHypRef Expression
1 df-5 9655 . 2  |-  5  =  ( 4  +  1 )
2 4re 9667 . . 3  |-  4  e.  RR
3 1re 8714 . . 3  |-  1  e.  RR
42, 3readdcli 8727 . 2  |-  ( 4  +  1 )  e.  RR
51, 4eqeltri 2323 1  |-  5  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1621  (class class class)co 5707   RRcr 8613   1c1 8615    + caddc 8617   4c4 9645   5c5 9646
This theorem is referenced by:  6re  9670  6pos  9682  5p2e7  9707  5p3e8  9708  5p4e9  9709  5p5e10  9710  5t2e10  9722  3lt5  9740  2lt5  9741  1lt5  9742  5lt6  9743  4lt6  9744  5lt7  9749  4lt7  9750  5lt8  9756  4lt8  9757  5lt9  9764  4lt9  9765  5lt10  9773  4lt10  9774  ef01bndlem  12300  prmlem1  12945  sralem  15724  srasca  15728  zlmlem  16265  zlmsca  16269  ppiublem1  20207  ppiub  20209  bposlem3  20291  bposlem4  20292  bposlem5  20293  bposlem6  20294  bposlem8  20296  bposlem9  20297  lgsdir2lem1  20328  ex-id  20568  5recm6rec  23202  bpoly4  23899
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-1cn 8672  ax-icn 8673  ax-addcl 8674  ax-addrcl 8675  ax-mulcl 8676  ax-mulrcl 8677  ax-i2m1 8682  ax-1ne0 8683  ax-rrecex 8686  ax-cnre 8687
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2511  df-rex 2512  df-rab 2514  df-v 2727  df-dif 3078  df-un 3080  df-in 3082  df-ss 3086  df-nul 3360  df-if 3468  df-sn 3547  df-pr 3548  df-op 3550  df-uni 3725  df-br 3918  df-opab 3972  df-xp 4591  df-cnv 4593  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-fv 4605  df-ov 5710  df-2 9652  df-3 9653  df-4 9654  df-5 9655
  Copyright terms: Public domain W3C validator