Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nncnd | GIF version |
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnred.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
Ref | Expression |
---|---|
nncnd | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 8725 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | nnred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
3 | 1, 2 | sseldi 3095 | 1 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1480 ℂcc 7618 ℕcn 8720 |
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 |
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-v 2688 df-in 3077 df-ss 3084 df-int 3772 df-inn 8721 |
This theorem is referenced by: peano5uzti 9159 qapne 9431 qtri3or 10020 exbtwnzlemstep 10025 intfracq 10093 flqdiv 10094 modqmulnn 10115 addmodid 10145 modaddmodup 10160 modsumfzodifsn 10169 addmodlteq 10171 facdiv 10484 facndiv 10485 faclbnd 10487 faclbnd6 10490 facubnd 10491 facavg 10492 bccmpl 10500 bcn0 10501 bcn1 10504 bcm1k 10506 bcp1n 10507 bcp1nk 10508 bcval5 10509 bcpasc 10512 permnn 10517 cvg1nlemcxze 10754 cvg1nlemcau 10756 resqrexlemcalc3 10788 binom11 11255 binom1dif 11256 divcnv 11266 arisum2 11268 trireciplem 11269 trirecip 11270 expcnvap0 11271 geo2sum 11283 geo2lim 11285 cvgratnnlembern 11292 cvgratnnlemnexp 11293 cvgratnnlemmn 11294 cvgratnnlemsumlt 11297 cvgratnnlemfm 11298 cvgratnnlemrate 11299 cvgratz 11301 eftcl 11360 eftabs 11362 efcllemp 11364 ege2le3 11377 efcj 11379 efaddlem 11380 eftlub 11396 eirraplem 11483 oexpneg 11574 divalglemnn 11615 dvdsgcdidd 11682 bezoutlemnewy 11684 mulgcd 11704 rplpwr 11715 sqgcd 11717 lcmgcdlem 11758 3lcm2e6woprm 11767 cncongr1 11784 cncongr2 11785 prmind2 11801 divgcdodd 11821 prmdvdsexpr 11828 sqrt2irrlem 11839 oddpwdclemxy 11847 oddpwdclemodd 11850 oddpwdclemdc 11851 oddpwdc 11852 sqpweven 11853 2sqpwodd 11854 sqrt2irraplemnn 11857 sqrt2irrap 11858 qmuldeneqnum 11873 divnumden 11874 qnumgt0 11876 numdensq 11880 hashdvds 11897 phiprmpw 11898 oddennn 11905 evenennn 11906 trilpolemeq1 13233 trilpolemlt1 13234 |
Copyright terms: Public domain | W3C validator |