Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  addcan2 Structured version   GIF version

 Description: Cancellation law for addition. (Contributed by NM, 30-Jul-2004.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
addcan2 ((A B 𝐶 ℂ) → ((A + 𝐶) = (B + 𝐶) ↔ A = B))

Proof of Theorem addcan2
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 cnegex 6966 . . 3 (𝐶 ℂ → x ℂ (𝐶 + x) = 0)
213ad2ant3 926 . 2 ((A B 𝐶 ℂ) → x ℂ (𝐶 + x) = 0)
3 oveq1 5462 . . . 4 ((A + 𝐶) = (B + 𝐶) → ((A + 𝐶) + x) = ((B + 𝐶) + x))
4 simpl1 906 . . . . . . 7 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → A ℂ)
5 simpl3 908 . . . . . . 7 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → 𝐶 ℂ)
6 simprl 483 . . . . . . 7 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → x ℂ)
74, 5, 6addassd 6827 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((A + 𝐶) + x) = (A + (𝐶 + x)))
8 simprr 484 . . . . . . 7 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (𝐶 + x) = 0)
98oveq2d 5471 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (A + (𝐶 + x)) = (A + 0))
10 addid1 6928 . . . . . . 7 (A ℂ → (A + 0) = A)
114, 10syl 14 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (A + 0) = A)
127, 9, 113eqtrd 2073 . . . . 5 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((A + 𝐶) + x) = A)
13 simpl2 907 . . . . . . 7 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → B ℂ)
1413, 5, 6addassd 6827 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((B + 𝐶) + x) = (B + (𝐶 + x)))
158oveq2d 5471 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (B + (𝐶 + x)) = (B + 0))
16 addid1 6928 . . . . . . 7 (B ℂ → (B + 0) = B)
1713, 16syl 14 . . . . . 6 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (B + 0) = B)
1814, 15, 173eqtrd 2073 . . . . 5 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((B + 𝐶) + x) = B)
1912, 18eqeq12d 2051 . . . 4 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → (((A + 𝐶) + x) = ((B + 𝐶) + x) ↔ A = B))
203, 19syl5ib 143 . . 3 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((A + 𝐶) = (B + 𝐶) → A = B))
21 oveq1 5462 . . 3 (A = B → (A + 𝐶) = (B + 𝐶))
2220, 21impbid1 130 . 2 (((A B 𝐶 ℂ) (x (𝐶 + x) = 0)) → ((A + 𝐶) = (B + 𝐶) ↔ A = B))
232, 22rexlimddv 2431 1 ((A B 𝐶 ℂ) → ((A + 𝐶) = (B + 𝐶) ↔ A = B))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∃wrex 2301  (class class class)co 5455  ℂcc 6689  0cc0 6691   + caddc 6694 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-resscn 6755  ax-1cn 6756  ax-icn 6758  ax-addcl 6759  ax-addrcl 6760  ax-mulcl 6761  ax-addcom 6763  ax-addass 6765  ax-distr 6767  ax-i2m1 6768  ax-0id 6771  ax-rnegex 6772  ax-cnre 6774 This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-iota 4810  df-fv 4853  df-ov 5458 This theorem is referenced by:  addcan2i  6971  addcan2d  6973  muleqadd  7411
 Copyright terms: Public domain W3C validator