![]() |
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 11498. (Contributed by NM, 17-Aug-2005.) |
Ref | Expression |
---|---|
peano2cn | ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10441 | . 2 ⊢ 1 ∈ ℂ | |
2 | addcl 10465 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ) | |
3 | 1, 2 | mpan2 687 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2081 (class class class)co 7016 ℂcc 10381 1c1 10384 + caddc 10386 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-1cn 10441 ax-addcl 10443 |
This theorem depends on definitions: df-bi 208 df-an 397 |
This theorem is referenced by: nnsscn 11491 xp1d2m1eqxm1d2 11739 nneo 11915 zeo 11917 zeo2 11918 zesq 13437 facndiv 13498 faclbnd 13500 faclbnd6 13509 iseralt 14875 bcxmas 15023 trireciplem 15050 fallfacfwd 15223 bpolydiflem 15241 fsumcube 15247 odd2np1 15523 srgbinomlem3 18982 srgbinomlem4 18983 pcoass 23311 dvfsumabs 24303 ply1divex 24413 qaa 24595 aaliou3lem2 24615 abssinper 24789 advlogexp 24919 atantayl2 25197 basellem3 25342 basellem8 25347 lgseisenlem1 25633 lgsquadlem1 25638 pntrsumo1 25823 crctcshwlkn0lem6 27280 clwlkclwwlklem3 27466 fwddifnp1 33235 ltflcei 34411 itg2addnclem3 34476 pell14qrgapw 38958 binomcxplemrat 40220 sumnnodd 41453 dirkertrigeqlem1 41925 dirkertrigeqlem3 41927 dirkertrigeq 41928 fourierswlem 42057 fmtnorec4 43193 lighneallem4b 43256 |
Copyright terms: Public domain | W3C validator |