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 10957 | . 2 ⊢ 1 ∈ ℂ | |
2 | subcl 11248 | . 2 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 − 1) ∈ ℂ) | |
3 | 1, 2 | mpan2 687 | 1 ⊢ (𝑁 ∈ ℂ → (𝑁 − 1) ∈ ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2101 (class class class)co 7295 ℂcc 10897 1c1 10900 − cmin 11233 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7608 ax-resscn 10956 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-addrcl 10960 ax-mulcl 10961 ax-mulrcl 10962 ax-mulcom 10963 ax-addass 10964 ax-mulass 10965 ax-distr 10966 ax-i2m1 10967 ax-1ne0 10968 ax-1rid 10969 ax-rnegex 10970 ax-rrecex 10971 ax-cnre 10972 ax-pre-lttri 10973 ax-pre-lttrn 10974 ax-pre-ltadd 10975 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-op 4571 df-uni 4842 df-br 5078 df-opab 5140 df-mpt 5161 df-id 5491 df-po 5505 df-so 5506 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-riota 7252 df-ov 7298 df-oprab 7299 df-mpo 7300 df-er 8518 df-en 8754 df-dom 8755 df-sdom 8756 df-pnf 11039 df-mnf 11040 df-ltxr 11042 df-sub 11235 |
This theorem is referenced by: kcnktkm1cn 11434 xp1d2m1eqxm1d2 12255 elnnnn0 12304 hash2iun1dif1 15564 pwdif 15608 nn0ob 16121 2lgslem1a1 26565 addsqrexnreu 26618 addsqnreup 26619 addsq2nreurex 26620 clwlkclwwlklem2a1 28384 clwlkclwwlklem2a 28390 clwlkclwwlklem3 28393 frrusgrord0 28732 numclwwlk7 28783 dirkertrigeqlem2 43675 fmtnoprmfac2 45059 lighneallem3 45099 proththd 45106 zofldiv2ALTV 45154 nn0onn0exALTV 45191 nn0onn0ex 45909 nn0sumshdiglemB 46006 |
Copyright terms: Public domain | W3C validator |