![]() |
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 12099. (Contributed by NM, 17-Aug-2005.) |
Ref | Expression |
---|---|
peano2cn | ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 11043 | . 2 ⊢ 1 ∈ ℂ | |
2 | addcl 11067 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 1 ∈ ℂ) → (𝐴 + 1) ∈ ℂ) | |
3 | 1, 2 | mpan2 690 | 1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 1) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 (class class class)co 7350 ℂcc 10983 1c1 10986 + caddc 10988 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-1cn 11043 ax-addcl 11045 |
This theorem depends on definitions: df-bi 206 df-an 398 |
This theorem is referenced by: nnsscn 12092 xp1d2m1eqxm1d2 12341 zeo 12523 zeo2 12524 zesq 14056 facndiv 14117 faclbnd 14119 faclbnd6 14128 iseralt 15505 bcxmas 15656 trireciplem 15683 fallfacfwd 15855 bpolydiflem 15873 fsumcube 15879 odd2np1 16159 srgbinomlem3 19889 srgbinomlem4 19890 pcoass 24315 dvfsumabs 25315 ply1divex 25429 qaa 25611 aaliou3lem2 25631 abssinper 25805 advlogexp 25938 atantayl2 26216 basellem3 26360 basellem8 26365 lgseisenlem1 26651 lgsquadlem1 26656 pntrsumo1 26841 crctcshwlkn0lem6 28565 clwlkclwwlklem3 28750 fwddifnp1 34681 ltflcei 35997 itg2addnclem3 36062 pell14qrgapw 41101 binomcxplemrat 42431 sumnnodd 43662 dirkertrigeqlem1 44130 dirkertrigeqlem3 44132 dirkertrigeq 44133 fourierswlem 44262 fmtnorec4 45532 lighneallem4b 45592 ackval1 46558 ackval2 46559 |
Copyright terms: Public domain | W3C validator |