![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0cnd | Unicode version |
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nn0red.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nn0cnd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0red.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nn0red 9244 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | recnd 8000 |
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 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-ext 2169 ax-sep 4133 ax-cnex 7916 ax-resscn 7917 ax-1re 7919 ax-addrcl 7922 ax-rnegex 7934 |
This theorem depends on definitions: df-bi 117 df-tru 1366 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-un 3145 df-in 3147 df-ss 3154 df-sn 3610 df-int 3857 df-inn 8934 df-n0 9191 |
This theorem is referenced by: modsumfzodifsn 10410 addmodlteq 10412 uzennn 10450 expaddzaplem 10577 expaddzap 10578 expmulzap 10580 nn0le2msqd 10713 nn0opthlem1d 10714 nn0opthd 10716 nn0opth2d 10717 facdiv 10732 bcp1n 10755 bcn2m1 10763 bcn2p1 10764 omgadd 10796 fihashssdif 10812 hashdifpr 10814 hashxp 10820 zfz1isolemsplit 10832 zfz1isolem1 10834 fsumconst 11476 hash2iun1dif1 11502 binomlem 11505 bcxmas 11511 arisum 11520 arisum2 11521 mertensabs 11559 effsumlt 11714 dvdsexp 11881 nn0ob 11927 divalglemnn 11937 divalgmod 11946 bezoutlemnewy 12011 bezoutlema 12014 bezoutlemb 12015 mulgcd 12031 absmulgcd 12032 mulgcdr 12033 gcddiv 12034 lcmgcd 12092 lcmid 12094 lcm1 12095 3lcm2e6woprm 12100 6lcm4e12 12101 mulgcddvds 12108 qredeu 12111 divgcdcoprm0 12115 divgcdcoprmex 12116 cncongr1 12117 cncongr2 12118 pw2dvdseulemle 12181 phiprmpw 12236 eulerthlema 12244 prmdiveq 12250 odzdvds 12259 powm2modprm 12266 coprimeprodsq 12271 pceulem 12308 pczpre 12311 pcqmul 12317 pcaddlem 12352 pcmpt 12355 pcmpt2 12356 sumhashdc 12359 pcfac 12362 oddprmdvds 12366 mul4sq 12406 mulgnn0dir 13053 mulgnn0ass 13059 lgslem1 14754 lgsvalmod 14773 lgseisenlem2 14804 m1lgs 14805 2sqlem8 14823 |
Copyright terms: Public domain | W3C validator |