![]() |
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 8635 | . 2 ⊢ ℕ ⊆ ℂ | |
2 | nnred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
3 | 1, 2 | sseldi 3061 | 1 ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1463 ℂcc 7545 ℕcn 8630 |
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 |
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-v 2659 df-in 3043 df-ss 3050 df-int 3738 df-inn 8631 |
This theorem is referenced by: peano5uzti 9063 qapne 9333 qtri3or 9913 exbtwnzlemstep 9918 intfracq 9986 flqdiv 9987 modqmulnn 10008 addmodid 10038 modaddmodup 10053 modsumfzodifsn 10062 addmodlteq 10064 facdiv 10377 facndiv 10378 faclbnd 10380 faclbnd6 10383 facubnd 10384 facavg 10385 bccmpl 10393 bcn0 10394 bcn1 10397 bcm1k 10399 bcp1n 10400 bcp1nk 10401 bcval5 10402 bcpasc 10405 permnn 10410 cvg1nlemcxze 10646 cvg1nlemcau 10648 resqrexlemcalc3 10680 binom11 11147 binom1dif 11148 divcnv 11158 arisum2 11160 trireciplem 11161 trirecip 11162 expcnvap0 11163 geo2sum 11175 geo2lim 11177 cvgratnnlembern 11184 cvgratnnlemnexp 11185 cvgratnnlemmn 11186 cvgratnnlemsumlt 11189 cvgratnnlemfm 11190 cvgratnnlemrate 11191 cvgratz 11193 eftcl 11211 eftabs 11213 efcllemp 11215 ege2le3 11228 efcj 11230 efaddlem 11231 eftlub 11247 eirraplem 11331 oexpneg 11422 divalglemnn 11463 bezoutlemnewy 11530 mulgcd 11550 rplpwr 11561 sqgcd 11563 lcmgcdlem 11604 3lcm2e6woprm 11613 cncongr1 11630 cncongr2 11631 prmind2 11647 divgcdodd 11667 prmdvdsexpr 11674 sqrt2irrlem 11685 oddpwdclemxy 11692 oddpwdclemodd 11695 oddpwdclemdc 11696 oddpwdc 11697 sqpweven 11698 2sqpwodd 11699 sqrt2irraplemnn 11702 sqrt2irrap 11703 qmuldeneqnum 11718 divnumden 11719 qnumgt0 11721 numdensq 11725 hashdvds 11742 phiprmpw 11743 oddennn 11750 evenennn 11751 trilpolemeq1 12925 trilpolemlt1 12926 |
Copyright terms: Public domain | W3C validator |