![]() |
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 8885 |
. 2
![]() ![]() ![]() ![]() | |
2 | nn0red.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseldi 3061 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-cnex 7636 ax-resscn 7637 ax-1re 7639 ax-addrcl 7642 ax-rnegex 7654 |
This theorem depends on definitions: df-bi 116 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-un 3041 df-in 3043 df-ss 3050 df-sn 3499 df-int 3738 df-inn 8631 df-n0 8882 |
This theorem is referenced by: nn0cnd 8936 nn0readdcl 8940 nn01to3 9311 flqmulnn0 9965 modifeq2int 10052 modaddmodup 10053 modaddmodlo 10054 modsumfzodifsn 10062 expnegap0 10194 nn0le2msqd 10358 nn0opthlem2d 10360 nn0opthd 10361 faclbnd6 10383 bcval5 10402 filtinf 10431 zfz1isolemiso 10475 mertenslemi1 11196 efcllemp 11215 eftlub 11247 oddge22np1 11426 nn0oddm1d2 11454 gcdaddm 11520 bezoutlemsup 11543 gcdzeq 11556 dvdssqlem 11564 nn0seqcvgd 11568 lcmneg 11601 mulgcddvds 11621 qredeu 11624 pw2dvdseulemle 11690 pw2dvdseu 11691 nn0sqrtelqelz 11729 nonsq 11730 ennnfoneleminc 11769 ennnfonelemkh 11770 ennnfonelemex 11772 ennnfonelemim 11782 |
Copyright terms: Public domain | W3C validator |