![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0red | Unicode version |
Description: A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nn0red.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nn0red |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0ssre 9210 |
. 2
![]() ![]() ![]() ![]() | |
2 | nn0red.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sselid 3168 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-sep 4136 ax-cnex 7932 ax-resscn 7933 ax-1re 7935 ax-addrcl 7938 ax-rnegex 7950 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ral 2473 df-rex 2474 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-sn 3613 df-int 3860 df-inn 8950 df-n0 9207 |
This theorem is referenced by: nn0cnd 9261 nn0readdcl 9265 nn01to3 9647 xnn0dcle 9832 flqmulnn0 10330 modifeq2int 10417 modaddmodup 10418 modaddmodlo 10419 modsumfzodifsn 10427 expnegap0 10559 nn0leexp2 10722 nn0le2msqd 10731 nn0opthlem2d 10733 nn0opthd 10734 faclbnd6 10756 bcval5 10775 filtinf 10803 zfz1isolemiso 10851 mertenslemi1 11575 efcllemp 11698 eftlub 11730 oddge22np1 11918 nn0oddm1d2 11946 gcdaddm 12017 bezoutlemsup 12042 gcdzeq 12055 dvdssqlem 12063 nn0seqcvgd 12073 lcmneg 12106 mulgcddvds 12126 qredeu 12129 pw2dvdseulemle 12199 pw2dvdseu 12200 nn0sqrtelqelz 12238 nonsq 12239 pythagtriplem3 12299 pythagtriplem6 12302 pythagtriplem7 12303 pclemub 12319 pcprendvds 12322 pcpremul 12325 pcidlem 12355 pcgcd1 12360 pc2dvds 12362 pcz 12364 pcprmpw2 12365 fldivp1 12380 pcfaclem 12381 pcfac 12382 pcbc 12383 4sqexercise1 12430 4sqexercise2 12431 4sqlemsdc 12432 4sqlem11 12433 4sqlem12 12434 4sqlem14 12436 ennnfoneleminc 12462 ennnfonelemkh 12463 ennnfonelemex 12465 ennnfonelemim 12475 psrbaglesuppg 13950 lgseisenlem1 14911 2lgsoddprmlem2 14915 2sqlem7 14929 2sqlem8 14931 |
Copyright terms: Public domain | W3C validator |