Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > zre | Unicode version |
Description: An integer is a real. (Contributed by NM, 8-Jan-2002.) |
Ref | Expression |
---|---|
zre |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elz 9056 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3o 961 wceq 1331 wcel 1480 cr 7619 cc0 7620 cneg 7934 cn 8720 cz 9054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-3or 963 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-rab 2425 df-v 2688 df-un 3075 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-iota 5088 df-fv 5131 df-ov 5777 df-neg 7936 df-z 9055 |
This theorem is referenced by: zcn 9059 zrei 9060 zssre 9061 elnn0z 9067 elnnz1 9077 peano2z 9090 zaddcl 9094 ztri3or0 9096 ztri3or 9097 zletric 9098 zlelttric 9099 zltnle 9100 zleloe 9101 zletr 9103 znnsub 9105 nzadd 9106 zltp1le 9108 zleltp1 9109 znn0sub 9119 zapne 9125 zdceq 9126 zdcle 9127 zdclt 9128 zltlen 9129 nn0ge0div 9138 zextle 9142 btwnnz 9145 suprzclex 9149 msqznn 9151 peano2uz2 9158 uzind 9162 fzind 9166 fnn0ind 9167 eluzuzle 9334 uzid 9340 uzneg 9344 uz11 9348 eluzp1m1 9349 eluzp1p1 9351 eluzaddi 9352 eluzsubi 9353 uzin 9358 uz3m2nn 9368 peano2uz 9378 nn0pzuz 9382 eluz2b2 9397 uz2mulcl 9402 eqreznegel 9406 lbzbi 9408 qre 9417 zltaddlt1le 9789 elfz1eq 9815 fznlem 9821 fzen 9823 uzsubsubfz 9827 fzaddel 9839 fzsuc2 9859 fzp1disj 9860 fzrev 9864 elfz1b 9870 fzneuz 9881 fzp1nel 9884 elfz0fzfz0 9903 fz0fzelfz0 9904 fznn0sub2 9905 fz0fzdiffz0 9907 elfzmlbp 9909 difelfznle 9912 elfzouz2 9938 fzonlt0 9944 fzossrbm1 9950 fzo1fzo0n0 9960 elfzo0z 9961 fzofzim 9965 eluzgtdifelfzo 9974 fzossfzop1 9989 ssfzo12bi 10002 elfzomelpfzo 10008 fzosplitprm1 10011 fzostep1 10014 flid 10057 flqbi2 10064 2tnp1ge0ge0 10074 flhalf 10075 fldiv4p1lem1div2 10078 ceiqle 10086 uzsinds 10215 zsqcl2 10370 nn0abscl 10857 zmaxcl 10996 2zsupmax 10997 evennn02n 11579 evennn2n 11580 ltoddhalfle 11590 infssuzex 11642 dfgcd2 11702 algcvga 11732 isprm3 11799 dvdsnprmd 11806 sqnprm 11816 zgcdsq 11879 hashdvds 11897 coskpi 12929 |
Copyright terms: Public domain | W3C validator |