HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem 5re 8843
Description: The number 5 is real.
Assertion
Ref Expression
5re

Proof of Theorem 5re
StepHypRef Expression
1 df-5 8832 . 2
2 4re 8842 . . 3
3 1re 8172 . . 3
42, 3readdcli 8168 . 2
51, 4eqeltri 2159 1
Colors of variables: wff set class
Syntax hints:   wcel 1533  (class class class)co 5296  cr 8060  c1 8062   caddc 8064  c4 8822  c5 8823
This theorem is referenced by:  6re  8844  6pos  8855  5p2e7  8879  5p3e8  8880  5p4e9  8881  5p5e10  8882  5t2e10  8893  3lt5  8911  2lt5  8912  1lt5  8913  5lt6  8914  4lt6  8915  5lt7  8920  4lt7  8921  5lt8  8927  4lt8  8928  5lt9  8935  4lt9  8936  5lt10  8944  4lt10  8945  ef01bndlem  10775  prmlem1  11306  mgpsca  12388  ppiublem1  16009  ppiub  16011  bposlem3  16026  bposlem4  16027  bposlem5  16028  bposlem6  16029  bposlem8  16031  bposlem9  16032  lgsdir2lem1  16063  ex-id  16157  phllem  24517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-1cn 8118  ax-icn 8119  ax-addcl 8120  ax-addrcl 8121  ax-mulcl 8122  ax-mulrcl 8123  ax-i2m1 8128  ax-1ne0 8129  ax-rrecex 8132  ax-cnre 8133
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-uni 3435  df-br 3592  df-opab 3645  df-xp 4263  df-cnv 4265  df-dm 4267  df-rn 4268  df-res 4269  df-ima 4270  df-fv 4277  df-ov 5298  df-2 8829  df-3 8830  df-4 8831  df-5 8832
Copyright terms: Public domain