| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > peano2cn | Structured version Visualization version GIF version | ||
| Description: A theorem for complex numbers analogous the second Peano postulate peano2nn 12278. (Contributed by NM, 17-Aug-2005.) |
| Ref | Expression |
|---|---|
| peano2cn | ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1cn 11213 | . 2 ⊢ 1 ∈ ℂ | |
| 2 | addcl 11237 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ) | |
| 3 | 1, 2 | mpan2 691 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 1c1 11156 + caddc 11158 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-1cn 11213 ax-addcl 11215 |
| This theorem depends on definitions: df-bi 207 df-an 396 |
| This theorem is referenced by: nnsscn 12271 xp1d2m1eqxm1d2 12520 zeo 12704 zeo2 12705 zesq 14265 facndiv 14327 faclbnd 14329 faclbnd6 14338 iseralt 15721 bcxmas 15871 trireciplem 15898 fallfacfwd 16072 bpolydiflem 16090 fsumcube 16096 odd2np1 16378 srgbinomlem3 20225 srgbinomlem4 20226 pcoass 25057 dvfsumabs 26063 ply1divex 26176 qaa 26365 aaliou3lem2 26385 abssinper 26563 advlogexp 26697 atantayl2 26981 basellem3 27126 basellem8 27131 lgseisenlem1 27419 lgsquadlem1 27424 pntrsumo1 27609 crctcshwlkn0lem6 29835 clwlkclwwlklem3 30020 fwddifnp1 36166 ltflcei 37615 itg2addnclem3 37680 pell14qrgapw 42887 binomcxplemrat 44369 sumnnodd 45645 dirkertrigeqlem1 46113 dirkertrigeqlem3 46115 dirkertrigeq 46116 fourierswlem 46245 fmtnorec4 47536 lighneallem4b 47596 ackval1 48602 ackval2 48603 |
| Copyright terms: Public domain | W3C validator |