ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2re GIF version

Theorem 2re 7985
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re 2 ∈ ℝ

Proof of Theorem 2re
StepHypRef Expression
1 df-2 7973 . 2 2 = (1 + 1)
2 1re 7026 . . 3 1 ∈ ℝ
32, 2readdcli 7040 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2110 1 2 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1393  (class class class)co 5512  cr 6888  1c1 6890   + caddc 6892  2c2 7964
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-ext 2022  ax-1re 6978  ax-addrcl 6981
This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-clel 2036  df-2 7973
This theorem is referenced by:  2cn  7986  3re  7989  2ne0  8008  2ap0  8009  3pos  8010  2lt3  8087  1lt3  8088  2lt4  8090  1lt4  8091  2lt5  8094  2lt6  8099  1lt6  8100  2lt7  8105  1lt7  8106  2lt8  8112  1lt8  8113  2lt9  8120  1lt9  8121  2lt10  8129  1lt10  8130  1le2  8133  2rene0  8135  halfre  8138  halfgt0  8140  halflt1  8142  rehalfcl  8152  halfpos2  8155  halfnneg2  8157  addltmul  8161  nominpos  8162  avglt1  8163  avglt2  8164  div4p1lem1div2  8177  nn0lele2xi  8233  nn0ge2m1nn  8242  halfnz  8336  uzuzle23  8513  uz3m2nn  8515  2rp  8588  fztpval  8945  fzo0to42pr  9076  qbtwnrelemcalc  9110  qbtwnre  9111  2tnp1ge0ge0  9143  flhalf  9144  fldiv4p1lem1div2  9147  expubnd  9311  cvg1nlemres  9584  resqrexlemover  9608  resqrexlemga  9621  sqrt4  9645  sqrt2gt1lt2  9647  abstri  9700  amgm2  9714  sqr2irrlem  9877  sqrt2re  9879  ex-fl  9895
  Copyright terms: Public domain W3C validator