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 8247 | . 2 | |
2 | 1 | simplbi 259 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3o 884 wceq 1243 wcel 1393 cr 6888 cc0 6889 cneg 7183 cn 7914 cz 8245 |
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-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-rex 2312 df-rab 2315 df-v 2559 df-un 2922 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-br 3765 df-iota 4867 df-fv 4910 df-ov 5515 df-neg 7185 df-z 8246 |
This theorem is referenced by: zcn 8250 zrei 8251 zssre 8252 elnn0z 8258 elnnz1 8268 peano2z 8281 zaddcl 8285 ztri3or0 8287 ztri3or 8288 zletric 8289 zlelttric 8290 zltnle 8291 zleloe 8292 zletr 8294 znnsub 8296 zltp1le 8298 zleltp1 8299 znn0sub 8309 zapne 8315 zdceq 8316 zdcle 8317 zdclt 8318 zltlen 8319 nn0ge0div 8327 zextle 8331 btwnnz 8334 msqznn 8338 peano2uz2 8345 uzind 8349 fzind 8353 fnn0ind 8354 eluzuzle 8481 uzid 8487 uzneg 8491 uz11 8495 eluzp1m1 8496 eluzp1p1 8498 eluzaddi 8499 eluzsubi 8500 uzin 8505 uz3m2nn 8515 peano2uz 8526 nn0pzuz 8530 eluz2b2 8540 uz2mulcl 8545 eqreznegel 8549 lbzbi 8551 qre 8560 elfz1eq 8899 fznlem 8905 fzen 8907 uzsubsubfz 8911 fzaddel 8922 fzsuc2 8941 fzp1disj 8942 fzrev 8946 elfz1b 8952 fzneuz 8963 fzp1nel 8966 elfz0fzfz0 8983 fz0fzelfz0 8984 fznn0sub2 8985 fz0fzdiffz0 8987 elfzmlbmOLD 8989 elfzmlbp 8990 difelfznle 8993 elfzouz2 9017 fzonlt0 9023 fzossrbm1 9029 fzo1fzo0n0 9039 elfzo0z 9040 fzofzim 9044 eluzgtdifelfzo 9053 fzossfzop1 9068 ssfzo12bi 9081 elfzomelpfzo 9087 fzosplitprm1 9090 fzostep1 9093 flid 9126 flqbi2 9133 2tnp1ge0ge0 9143 flhalf 9144 fldiv4p1lem1div2 9147 ceiqle 9155 zsqcl2 9331 nn0abscl 9681 ialgcvga 9890 |
Copyright terms: Public domain | W3C validator |