Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > peano2cnm | Structured version Visualization version GIF version |
Description: "Reverse" second Peano postulate analogue for complex numbers: A complex number minus 1 is a complex number. (Contributed by Alexander van der Vekens, 18-Mar-2018.) |
Ref | Expression |
---|---|
peano2cnm | ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 10676 | . 2 ⊢ 1 ∈ ℂ | |
2 | subcl 10966 | . 2 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ) | |
3 | 1, 2 | mpan2 691 | 1 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 (class class class)co 7173 ℂcc 10616 1c1 10619 − cmin 10951 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pow 5233 ax-pr 5297 ax-un 7482 ax-resscn 10675 ax-1cn 10676 ax-icn 10677 ax-addcl 10678 ax-addrcl 10679 ax-mulcl 10680 ax-mulrcl 10681 ax-mulcom 10682 ax-addass 10683 ax-mulass 10684 ax-distr 10685 ax-i2m1 10686 ax-1ne0 10687 ax-1rid 10688 ax-rnegex 10689 ax-rrecex 10690 ax-cnre 10691 ax-pre-lttri 10692 ax-pre-lttrn 10693 ax-pre-ltadd 10694 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-nel 3040 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3401 df-sbc 3682 df-csb 3792 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-pw 4491 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-mpt 5112 df-id 5430 df-po 5443 df-so 5444 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-res 5538 df-ima 5539 df-iota 6298 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7130 df-ov 7176 df-oprab 7177 df-mpo 7178 df-er 8323 df-en 8559 df-dom 8560 df-sdom 8561 df-pnf 10758 df-mnf 10759 df-ltxr 10761 df-sub 10953 |
This theorem is referenced by: kcnktkm1cn 11152 xp1d2m1eqxm1d2 11973 elnnnn0 12022 hash2iun1dif1 15275 pwdif 15319 nn0ob 15832 2lgslem1a1 26128 addsqrexnreu 26181 addsqnreup 26182 addsq2nreurex 26183 clwlkclwwlklem2a1 27932 clwlkclwwlklem2a 27938 clwlkclwwlklem3 27941 frrusgrord0 28280 numclwwlk7 28331 dirkertrigeqlem2 43205 fmtnoprmfac2 44583 lighneallem3 44623 proththd 44630 zofldiv2ALTV 44678 nn0onn0exALTV 44715 nn0onn0ex 45433 nn0sumshdiglemB 45530 |
Copyright terms: Public domain | W3C validator |