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 12094 | . 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ℂcc 10982 ℕcn 12086 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-un 7662 ax-1cn 11042 ax-addcl 11044 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3927 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-tr 5221 df-id 5528 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5585 df-we 5587 df-xp 5636 df-rel 5637 df-cnv 5638 df-co 5639 df-dm 5640 df-rn 5641 df-res 5642 df-ima 5643 df-pred 6249 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6443 df-fun 6493 df-fn 6494 df-f 6495 df-f1 6496 df-fo 6497 df-f1o 6498 df-fv 6499 df-ov 7352 df-om 7793 df-2nd 7912 df-frecs 8179 df-wrecs 8210 df-recs 8284 df-rdg 8323 df-nn 12087 |
This theorem is referenced by: 9p1e10 12552 numnncl2 12573 dec10p 12593 3dec 14093 faclbnd4lem1 14120 4bc2eq6 14156 ef01bndlem 16000 3dvds 16147 divalglem8 16216 pockthi 16713 dec5nprm 16872 dec2nprm 16873 modxai 16874 modxp1i 16876 mod2xnegi 16877 modsubi 16878 23prm 16925 37prm 16927 43prm 16928 83prm 16929 139prm 16930 163prm 16931 1259lem1 16937 1259lem4 16940 2503lem2 16944 4001lem1 16947 4001lem3 16949 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 29200 dpmul10 31545 decdiv10 31546 dp3mul10 31548 dpadd2 31560 dpadd 31561 dpadd3 31562 dpmul 31563 dpmul4 31564 ballotlem2 32861 ballotlemfmpn 32867 ballotth 32910 cnndvlem1 34895 addassnni 40337 addcomnni 40338 mulassnni 40339 mulcomnni 40340 gcdaddmzz2nncomi 40348 lcmeprodgcdi 40359 lcmineqlem6 40386 lcmineqlem23 40403 3lexlogpow5ineq5 40412 1t10e1p1e11 45291 deccarry 45292 fmtnoprmfac2lem1 45507 139prmALT 45537 3exp4mod41 45557 41prothprmlem1 45558 2exp340mod341 45674 bgoldbtbndlem1 45746 tgblthelfgott 45756 tgoldbachlt 45757 |
Copyright terms: Public domain | W3C validator |