Theorem npcan1 11746

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 11307	. 2 ⊢ (𝐴 ∈ ℂ → 1 ∈ ℂ)
3	1, 2	npcand 11678	1 ⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7422  ℂcc 11203  1c1 11206   + caddc 11208   − cmin 11546

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753  ax-resscn 11262  ax-1cn 11263  ax-icn 11264  ax-addcl 11265  ax-addrcl 11266  ax-mulcl 11267  ax-mulrcl 11268  ax-mulcom 11269  ax-addass 11270  ax-mulass 11271  ax-distr 11272  ax-i2m1 11273  ax-1ne0 11274  ax-1rid 11275  ax-rnegex 11276  ax-rrecex 11277  ax-cnre 11278  ax-pre-lttri 11279  ax-pre-lttrn 11280  ax-pre-ltadd 11281

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-po 5558  df-so 5559  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7379  df-ov 7425  df-oprab 7426  df-mpo 7427  df-er 8722  df-en 8979  df-dom 8980  df-sdom 8981  df-pnf 11350  df-mnf 11351  df-ltxr 11353  df-sub 11548

This theorem is used by:  elnnnn0  12654  fzm1  13746  fzosplitprm1  13918  modm1p1mod0  14070  facnn2  14431  cshimadifsn0  14987  pwdif  16044  mod2eq1n2dvds  16524  zob  16536  pwp1fsum  16568  prmonn2  17224  mulgfval  19286  psdpw  22498  cpmadugsumlemF  23201  addsq2nreurex  27778  axlowdimlem13  29539  wlk1walk  30226  wlkdlem2  30269  pthhashvtx  30322  clwwlkccatlem  30587  clwwlknwwlksn  30636  clwwlkinwwlk  30638  clwwlkwwlksb  30652  wwlksubclwwlk  30656  eucrct2eupth  30853  frrusgrord0  30948  1arithidomlem2  34116  1arithidom  34117  poimirlem1  38646  poimirlem2  38647  poimirlem6  38651  poimirlem7  38652  poimirlem8  38653  poimirlem9  38654  poimirlem10  38655  poimirlem11  38656  poimirlem12  38657  poimirlem13  38658  poimirlem14  38659  poimirlem15  38660  poimirlem16  38661  poimirlem17  38662  poimirlem18  38663  poimirlem19  38664  poimirlem20  38665  poimirlem21  38666  poimirlem22  38667  poimirlem23  38668  poimirlem24  38669  poimirlem26  38671  poimirlem27  38672  poimirlem31  38676  poimirlem32  38677  trclfvdecomr  44835  flmrecm1  48520  m1mod0mod1  48537  iccpartgtprec  48609  sqrtpwpw2p  48730  fmtnorec2lem  48734  fmtnodvds  48736  fmtnorec3  48740  fmtnorec4  48741  lighneallem3  48799  lighneallem4  48802  dfodd6  48842  evenm1odd  48844  m1expoddALTV  48853  zofldiv2ALTV  48867  oddflALTV  48868  nn0onn0exALTV  48904  fppr2odd  48936  bgoldbtbndlem2  49011  gpgedgvtx0  49266  gpg5nbgrvtx03starlem2  49274  bcpascm1  49570  altgsumbcALT  49572  nn0onn0ex  49742  zofldiv2  49750  logbpw2m1  49786  blenpw2m1  49798  nnolog2flm1  49809  blennngt2o2  49811  blengt1fldiv2p1  49812  blennn0e2  49813