![]() |
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 11218 | . 2 ⊢ 1 ∈ ℂ | |
2 | addcl 11242 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ) | |
3 | 1, 2 | mpan2 689 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 (class class class)co 7426 ℂcc 11158 1c1 11161 + caddc 11163 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-1cn 11218 ax-addcl 11220 |
This theorem depends on definitions: df-bi 206 df-an 395 |
This theorem is referenced by: nnsscn 12271 xp1d2m1eqxm1d2 12520 zeo 12702 zeo2 12703 zesq 14245 facndiv 14307 faclbnd 14309 faclbnd6 14318 iseralt 15691 bcxmas 15841 trireciplem 15868 fallfacfwd 16040 bpolydiflem 16058 fsumcube 16064 odd2np1 16345 srgbinomlem3 20213 srgbinomlem4 20214 pcoass 25045 dvfsumabs 26051 ply1divex 26167 qaa 26354 aaliou3lem2 26374 abssinper 26551 advlogexp 26685 atantayl2 26969 basellem3 27114 basellem8 27119 lgseisenlem1 27407 lgsquadlem1 27412 pntrsumo1 27597 crctcshwlkn0lem6 29752 clwlkclwwlklem3 29937 fwddifnp1 35991 ltflcei 37311 itg2addnclem3 37376 pell14qrgapw 42551 binomcxplemrat 44042 sumnnodd 45269 dirkertrigeqlem1 45737 dirkertrigeqlem3 45739 dirkertrigeq 45740 fourierswlem 45869 fmtnorec4 47139 lighneallem4b 47199 ackval1 48087 ackval2 48088 |
Copyright terms: Public domain | W3C validator |