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 9031 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 7794 | 1 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 ℂcc 7618 ℕ0cn0 8977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-cnex 7711 ax-resscn 7712 ax-1re 7714 ax-addrcl 7717 ax-rnegex 7729 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-sn 3533 df-int 3772 df-inn 8721 df-n0 8978 |
This theorem is referenced by: modsumfzodifsn 10169 addmodlteq 10171 uzennn 10209 expaddzaplem 10336 expaddzap 10337 expmulzap 10339 nn0le2msqd 10465 nn0opthlem1d 10466 nn0opthd 10468 nn0opth2d 10469 facdiv 10484 bcp1n 10507 bcn2m1 10515 bcn2p1 10516 omgadd 10548 fihashssdif 10564 hashdifpr 10566 hashxp 10572 zfz1isolemsplit 10581 zfz1isolem1 10583 fsumconst 11223 hash2iun1dif1 11249 binomlem 11252 bcxmas 11258 arisum 11267 arisum2 11268 mertensabs 11306 effsumlt 11398 dvdsexp 11559 nn0ob 11605 divalglemnn 11615 divalgmod 11624 bezoutlemnewy 11684 bezoutlema 11687 bezoutlemb 11688 mulgcd 11704 absmulgcd 11705 mulgcdr 11706 gcddiv 11707 lcmgcd 11759 lcmid 11761 lcm1 11762 3lcm2e6woprm 11767 6lcm4e12 11768 mulgcddvds 11775 qredeu 11778 divgcdcoprm0 11782 divgcdcoprmex 11783 cncongr1 11784 cncongr2 11785 pw2dvdseulemle 11845 phiprmpw 11898 |
Copyright terms: Public domain | W3C validator |