Theorem npcan1 11741

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  (class class class)co 7420  ℂcc 11198  1c1 11201   + caddc 11203   − cmin 11541

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 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

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 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  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 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-ltxr 11348  df-sub 11543

This theorem is used by:  elnnnn0  12649  fzm1  13741  fzosplitprm1  13913  modm1p1mod0  14065  facnn2  14426  cshimadifsn0  14981  pwdif  16037  mod2eq1n2dvds  16517  zob  16529  pwp1fsum  16561  prmonn2  17217  mulgfval  19279  psdpw  22491  cpmadugsumlemF  23194  addsq2nreurex  27771  axlowdimlem13  29532  wlk1walk  30219  wlkdlem2  30262  pthhashvtx  30315  clwwlkccatlem  30580  clwwlknwwlksn  30629  clwwlkinwwlk  30631  clwwlkwwlksb  30645  wwlksubclwwlk  30649  eucrct2eupth  30846  frrusgrord0  30941  1arithidomlem2  34068  1arithidom  34069  poimirlem1  38540  poimirlem2  38541  poimirlem6  38545  poimirlem7  38546  poimirlem8  38547  poimirlem9  38548  poimirlem10  38549  poimirlem11  38550  poimirlem12  38551  poimirlem13  38552  poimirlem14  38553  poimirlem15  38554  poimirlem16  38555  poimirlem17  38556  poimirlem18  38557  poimirlem19  38558  poimirlem20  38559  poimirlem21  38560  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem26  38565  poimirlem27  38566  poimirlem31  38570  poimirlem32  38571  trclfvdecomr  44728  flmrecm1  48413  m1mod0mod1  48430  iccpartgtprec  48502  sqrtpwpw2p  48623  fmtnorec2lem  48627  fmtnodvds  48629  fmtnorec3  48633  fmtnorec4  48634  lighneallem3  48692  lighneallem4  48695  dfodd6  48735  evenm1odd  48737  m1expoddALTV  48746  zofldiv2ALTV  48760  oddflALTV  48761  nn0onn0exALTV  48797  fppr2odd  48829  bgoldbtbndlem2  48904  gpgedgvtx0  49159  gpg5nbgrvtx03starlem2  49167  bcpascm1  49463  altgsumbcALT  49465  nn0onn0ex  49635  zofldiv2  49643  logbpw2m1  49679  blenpw2m1  49691  nnolog2flm1  49702  blennngt2o2  49704  blengt1fldiv2p1  49705  blennn0e2  49706