![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nn0cnd | GIF version |
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nn0red.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Ref | Expression |
---|---|
nn0cnd | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0red.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ0) | |
2 | 1 | nn0red 9206 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 7963 | 1 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2148 ℂcc 7787 ℕ0cn0 9152 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4118 ax-cnex 7880 ax-resscn 7881 ax-1re 7883 ax-addrcl 7886 ax-rnegex 7898 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rex 2461 df-v 2739 df-un 3133 df-in 3135 df-ss 3142 df-sn 3597 df-int 3843 df-inn 8896 df-n0 9153 |
This theorem is referenced by: modsumfzodifsn 10369 addmodlteq 10371 uzennn 10409 expaddzaplem 10536 expaddzap 10537 expmulzap 10539 nn0le2msqd 10670 nn0opthlem1d 10671 nn0opthd 10673 nn0opth2d 10674 facdiv 10689 bcp1n 10712 bcn2m1 10720 bcn2p1 10721 omgadd 10753 fihashssdif 10769 hashdifpr 10771 hashxp 10777 zfz1isolemsplit 10789 zfz1isolem1 10791 fsumconst 11433 hash2iun1dif1 11459 binomlem 11462 bcxmas 11468 arisum 11477 arisum2 11478 mertensabs 11516 effsumlt 11671 dvdsexp 11837 nn0ob 11883 divalglemnn 11893 divalgmod 11902 bezoutlemnewy 11967 bezoutlema 11970 bezoutlemb 11971 mulgcd 11987 absmulgcd 11988 mulgcdr 11989 gcddiv 11990 lcmgcd 12048 lcmid 12050 lcm1 12051 3lcm2e6woprm 12056 6lcm4e12 12057 mulgcddvds 12064 qredeu 12067 divgcdcoprm0 12071 divgcdcoprmex 12072 cncongr1 12073 cncongr2 12074 pw2dvdseulemle 12137 phiprmpw 12192 eulerthlema 12200 prmdiveq 12206 odzdvds 12215 powm2modprm 12222 coprimeprodsq 12227 pceulem 12264 pczpre 12267 pcqmul 12273 pcaddlem 12308 pcmpt 12311 pcmpt2 12312 sumhashdc 12315 pcfac 12318 oddprmdvds 12322 mul4sq 12362 mulgnn0dir 12888 mulgnn0ass 12894 lgslem1 14034 lgsvalmod 14053 2sqlem8 14092 |
Copyright terms: Public domain | W3C validator |