Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nncni | Structured version Visualization version GIF version |
Description: A positive integer is a complex number. (Contributed by NM, 18-Aug-1999.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022.) |
Ref | Expression |
---|---|
nnre.1 | ⊢ 𝐴 ∈ ℕ |
Ref | Expression |
---|---|
nncni | ⊢ 𝐴 ∈ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnre.1 | . 2 ⊢ 𝐴 ∈ ℕ | |
2 | nncn 12095 | . 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ℂcc 10983 ℕcn 12087 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pr 5383 ax-un 7663 ax-1cn 11043 ax-addcl 11045 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-pss 3928 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-iun 4955 df-br 5105 df-opab 5167 df-mpt 5188 df-tr 5222 df-id 5529 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6250 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7353 df-om 7794 df-2nd 7913 df-frecs 8180 df-wrecs 8211 df-recs 8285 df-rdg 8324 df-nn 12088 |
This theorem is referenced by: 9p1e10 12553 numnncl2 12574 dec10p 12594 3dec 14094 faclbnd4lem1 14121 4bc2eq6 14157 ef01bndlem 16001 3dvds 16148 divalglem8 16217 pockthi 16714 dec5nprm 16873 dec2nprm 16874 modxai 16875 modxp1i 16877 mod2xnegi 16878 modsubi 16879 23prm 16926 37prm 16928 43prm 16929 83prm 16930 139prm 16931 163prm 16932 1259lem1 16938 1259lem4 16941 2503lem2 16945 4001lem1 16948 4001lem3 16950 mcubic 26119 cubic2 26120 cubic 26121 quart1cl 26126 quart1lem 26127 quart1 26128 quartlem1 26129 quartlem2 26130 log2ublem1 26218 log2ublem2 26219 log2ub 26221 bclbnd 26550 bposlem8 26561 pntlemf 26875 ex-lcm 29188 dpmul10 31533 decdiv10 31534 dp3mul10 31536 dpadd2 31548 dpadd 31549 dpadd3 31550 dpmul 31551 dpmul4 31552 ballotlem2 32849 ballotlemfmpn 32855 ballotth 32898 cnndvlem1 34886 addassnni 40328 addcomnni 40329 mulassnni 40330 mulcomnni 40331 gcdaddmzz2nncomi 40339 lcmeprodgcdi 40350 lcmineqlem6 40377 lcmineqlem23 40394 3lexlogpow5ineq5 40403 1t10e1p1e11 45260 deccarry 45261 fmtnoprmfac2lem1 45476 139prmALT 45506 3exp4mod41 45526 41prothprmlem1 45527 2exp340mod341 45643 bgoldbtbndlem1 45715 tgblthelfgott 45725 tgoldbachlt 45726 |
Copyright terms: Public domain | W3C validator |