Theorem npcan1 11734

Description: Cancellation law for subtraction and addition with 1. (Contributed by Alexander van der Vekens, 5-Oct-2018.)

Assertion

Ref	Expression
npcan1	⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴)

Proof of Theorem npcan1

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
2		1cnd 11295	. 2 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℂ)
3	1, 2	npcand 11666	1 ⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7418  ℂcc 11191  1c1 11194   + caddc 11196   − cmin 11534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-ltxr 11341  df-sub 11536

This theorem is used by:  elnnnn0  12642  fzm1  13734  fzosplitprm1  13906  modm1p1mod0  14058  facnn2  14419  cshimadifsn0  14974  pwdif  16030  mod2eq1n2dvds  16510  zob  16522  pwp1fsum  16554  prmonn2  17210  mulgfval  19272  psdpw  22484  cpmadugsumlemF  23187  addsq2nreurex  27764  axlowdimlem13  29525  wlk1walk  30212  wlkdlem2  30255  pthhashvtx  30308  clwwlkccatlem  30573  clwwlknwwlksn  30622  clwwlkinwwlk  30624  clwwlkwwlksb  30638  wwlksubclwwlk  30642  eucrct2eupth  30839  frrusgrord0  30934  1arithidomlem2  34061  1arithidom  34062  poimirlem1  38519  poimirlem2  38520  poimirlem6  38524  poimirlem7  38525  poimirlem8  38526  poimirlem9  38527  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem13  38531  poimirlem14  38532  poimirlem15  38533  poimirlem16  38534  poimirlem17  38535  poimirlem18  38536  poimirlem19  38537  poimirlem20  38538  poimirlem21  38539  poimirlem22  38540  poimirlem23  38541  poimirlem24  38542  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  poimirlem32  38550  trclfvdecomr  44713  flmrecm1  48382  m1mod0mod1  48399  iccpartgtprec  48471  sqrtpwpw2p  48592  fmtnorec2lem  48596  fmtnodvds  48598  fmtnorec3  48602  fmtnorec4  48603  lighneallem3  48661  lighneallem4  48664  dfodd6  48704  evenm1odd  48706  m1expoddALTV  48715  zofldiv2ALTV  48729  oddflALTV  48730  nn0onn0exALTV  48766  fppr2odd  48798  bgoldbtbndlem2  48873  gpgedgvtx0  49128  gpg5nbgrvtx03starlem2  49136  bcpascm1  49432  altgsumbcALT  49434  nn0onn0ex  49604  zofldiv2  49612  logbpw2m1  49648  blenpw2m1  49660  nnolog2flm1  49671  blennngt2o2  49673  blengt1fldiv2p1  49674  blennn0e2  49675