![]() |
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 12218 | . 2 ⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℂ) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ∈ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2098 ℂcc 11105 ℕcn 12210 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5290 ax-nul 5297 ax-pr 5418 ax-un 7719 ax-1cn 11165 ax-addcl 11167 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-pss 3960 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-iun 4990 df-br 5140 df-opab 5202 df-mpt 5223 df-tr 5257 df-id 5565 df-eprel 5571 df-po 5579 df-so 5580 df-fr 5622 df-we 5624 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-pred 6291 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-ov 7405 df-om 7850 df-2nd 7970 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-nn 12211 |
This theorem is referenced by: 9p1e10 12677 numnncl2 12698 dec10p 12718 3dec 14224 faclbnd4lem1 14251 4bc2eq6 14287 ef01bndlem 16126 3dvds 16273 divalglem8 16342 pockthi 16841 dec5nprm 17000 dec2nprm 17001 modxai 17002 modxp1i 17004 mod2xnegi 17005 modsubi 17006 23prm 17053 37prm 17055 43prm 17056 83prm 17057 139prm 17058 163prm 17059 1259lem1 17065 1259lem4 17068 2503lem2 17072 4001lem1 17075 4001lem3 17077 mcubic 26698 cubic2 26699 cubic 26700 quart1cl 26705 quart1lem 26706 quart1 26707 quartlem1 26708 quartlem2 26709 log2ublem1 26797 log2ublem2 26798 log2ub 26800 bclbnd 27132 bposlem8 27143 pntlemf 27457 ex-lcm 30183 dpmul10 32531 decdiv10 32532 dp3mul10 32534 dpadd2 32546 dpadd 32547 dpadd3 32548 dpmul 32549 dpmul4 32550 ballotlem2 33979 ballotlemfmpn 33985 ballotth 34028 cnndvlem1 35904 addassnni 41347 addcomnni 41348 mulassnni 41349 mulcomnni 41350 gcdaddmzz2nncomi 41358 lcmeprodgcdi 41369 lcmineqlem6 41396 lcmineqlem23 41413 3lexlogpow5ineq5 41422 1t10e1p1e11 46528 deccarry 46529 fmtnoprmfac2lem1 46744 139prmALT 46774 3exp4mod41 46794 41prothprmlem1 46795 2exp340mod341 46911 bgoldbtbndlem1 46983 tgblthelfgott 46993 tgoldbachlt 46994 |
Copyright terms: Public domain | W3C validator |