![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4re | Structured version Visualization version Unicode version |
Description: The number 4 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
4re |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 10659 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3re 10672 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 1re 9629 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2, 3 | readdcli 9643 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | eqeltri 2526 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 ax-1cn 9584 ax-icn 9585 ax-addcl 9586 ax-addrcl 9587 ax-mulcl 9588 ax-mulrcl 9589 ax-i2m1 9594 ax-1ne0 9595 ax-rrecex 9598 ax-cnre 9599 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3015 df-dif 3375 df-un 3377 df-in 3379 df-ss 3386 df-nul 3700 df-if 3850 df-sn 3937 df-pr 3939 df-op 3943 df-uni 4169 df-br 4375 df-iota 5525 df-fv 5569 df-ov 6279 df-2 10657 df-3 10658 df-4 10659 |
This theorem is referenced by: 4cn 10676 5re 10677 4ne0 10695 5pos 10696 2lt4 10770 1lt4 10771 4lt5 10772 3lt5 10773 2lt5 10774 1lt5 10775 4lt6 10777 3lt6 10778 4lt7 10783 3lt7 10784 4lt8 10790 3lt8 10791 4lt9 10798 3lt9 10799 4lt10 10807 3lt10 10808 fzo0to42pr 11993 iexpcyc 12373 discr 12403 faclbnd2 12470 4bc2eq6 12508 sqrt2gt1lt2 13349 amgm2 13443 bpoly4 14123 ef01bndlem 14249 sin01bnd 14250 cos01bnd 14251 cos2bnd 14253 4sqlem12 14911 pcoass 22066 csbren 22364 minveclem2 22379 minveclem2OLD 22391 uniioombllem5 22557 dveflem 22943 pilem2 23419 pilem2OLD 23420 pilem3 23421 pilem3OLD 23422 sinhalfpilem 23430 sincosq1lem 23464 tangtx 23472 sincos4thpi 23480 log2cnv 23882 ppiublem1 24142 chtublem 24151 bposlem2 24225 bposlem6 24229 bposlem7 24230 bposlem8 24231 bposlem9 24232 2sqlem11 24315 chebbnd1lem2 24320 chebbnd1lem3 24321 chebbnd1 24322 pntibndlem1 24439 pntlemb 24447 pntlemg 24448 pntlemr 24452 pntlemf 24455 usgraexmplvtxlem 25134 usgraex0elv 25135 usgraex1elv 25136 usgraex2elv 25137 usgraex3elv 25138 4cycl4v4e 25406 4cycl4dv4e 25408 ex-id 25896 ex-1st 25906 ex-2nd 25907 dipcj 26365 minvecolem2 26529 minvecolem3 26530 minvecolem2OLD 26539 minvecolem3OLD 26540 normlem6 26780 lnophmlem2 27682 sqsscirc1 28721 problem2 30304 problem3 30305 limclner 37774 stoweidlem13 37930 stoweidlem26 37943 stoweidlem34 37952 stoweid 37982 stirlinglem12 38004 stirlinglem13 38005 gbogt5 38954 bgoldbwt 38969 bgoldbst 38970 sgoldbaltlem1 38971 sgoldbalt 38973 nnsum4primes4 38975 nnsum4primesprm 38977 nnsum4primesgbe 38979 nnsum3primesle9 38980 nnsum4primesle9 38981 nnsum4primeseven 38986 nnsum4primesevenALTV 38987 wtgoldbnnsum4prm 38988 bgoldbnnsum3prm 38990 bgoldbtbndlem2 38992 bgoldbtbndlem3 38993 bgoldbtbnd 38995 tgblthelfgott 38999 upgr4cycl4dv4e 39978 2p2ne5 40862 |
Copyright terms: Public domain | W3C validator |