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

Theorem cnegexlem1 6963
Description: Addition cancellation of a real number from two complex numbers. Lemma for cnegex 6966. (Contributed by Eric Schmidt, 22-May-2007.)
Assertion
Ref Expression
cnegexlem1 ((A B 𝐶 ℂ) → ((A + B) = (A + 𝐶) ↔ B = 𝐶))

Proof of Theorem cnegexlem1
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 ax-rnegex 6772 . . . 4 (A ℝ → x ℝ (A + x) = 0)
213ad2ant1 924 . . 3 ((A B 𝐶 ℂ) → x ℝ (A + x) = 0)
3 recn 6792 . . . 4 (A ℝ → A ℂ)
4 recn 6792 . . . . . . 7 (x ℝ → x ℂ)
5 oveq2 5463 . . . . . . . . . . 11 ((A + B) = (A + 𝐶) → (x + (A + B)) = (x + (A + 𝐶)))
6 simpr 103 . . . . . . . . . . . . 13 (((A (B 𝐶 ℂ)) x ℂ) → x ℂ)
7 simpll 481 . . . . . . . . . . . . 13 (((A (B 𝐶 ℂ)) x ℂ) → A ℂ)
8 simplrl 487 . . . . . . . . . . . . 13 (((A (B 𝐶 ℂ)) x ℂ) → B ℂ)
96, 7, 8addassd 6827 . . . . . . . . . . . 12 (((A (B 𝐶 ℂ)) x ℂ) → ((x + A) + B) = (x + (A + B)))
10 simplrr 488 . . . . . . . . . . . . 13 (((A (B 𝐶 ℂ)) x ℂ) → 𝐶 ℂ)
116, 7, 10addassd 6827 . . . . . . . . . . . 12 (((A (B 𝐶 ℂ)) x ℂ) → ((x + A) + 𝐶) = (x + (A + 𝐶)))
129, 11eqeq12d 2051 . . . . . . . . . . 11 (((A (B 𝐶 ℂ)) x ℂ) → (((x + A) + B) = ((x + A) + 𝐶) ↔ (x + (A + B)) = (x + (A + 𝐶))))
135, 12syl5ibr 145 . . . . . . . . . 10 (((A (B 𝐶 ℂ)) x ℂ) → ((A + B) = (A + 𝐶) → ((x + A) + B) = ((x + A) + 𝐶)))
1413adantr 261 . . . . . . . . 9 ((((A (B 𝐶 ℂ)) x ℂ) (A + x) = 0) → ((A + B) = (A + 𝐶) → ((x + A) + B) = ((x + A) + 𝐶)))
15 addcom 6927 . . . . . . . . . . . . 13 ((A x ℂ) → (A + x) = (x + A))
1615eqeq1d 2045 . . . . . . . . . . . 12 ((A x ℂ) → ((A + x) = 0 ↔ (x + A) = 0))
1716adantlr 446 . . . . . . . . . . 11 (((A (B 𝐶 ℂ)) x ℂ) → ((A + x) = 0 ↔ (x + A) = 0))
18 oveq1 5462 . . . . . . . . . . . . . . 15 ((x + A) = 0 → ((x + A) + B) = (0 + B))
19 oveq1 5462 . . . . . . . . . . . . . . 15 ((x + A) = 0 → ((x + A) + 𝐶) = (0 + 𝐶))
2018, 19eqeq12d 2051 . . . . . . . . . . . . . 14 ((x + A) = 0 → (((x + A) + B) = ((x + A) + 𝐶) ↔ (0 + B) = (0 + 𝐶)))
2120adantl 262 . . . . . . . . . . . . 13 ((((A (B 𝐶 ℂ)) x ℂ) (x + A) = 0) → (((x + A) + B) = ((x + A) + 𝐶) ↔ (0 + B) = (0 + 𝐶)))
22 addid2 6929 . . . . . . . . . . . . . . . 16 (B ℂ → (0 + B) = B)
23 addid2 6929 . . . . . . . . . . . . . . . 16 (𝐶 ℂ → (0 + 𝐶) = 𝐶)
2422, 23eqeqan12d 2052 . . . . . . . . . . . . . . 15 ((B 𝐶 ℂ) → ((0 + B) = (0 + 𝐶) ↔ B = 𝐶))
2524adantl 262 . . . . . . . . . . . . . 14 ((A (B 𝐶 ℂ)) → ((0 + B) = (0 + 𝐶) ↔ B = 𝐶))
2625ad2antrr 457 . . . . . . . . . . . . 13 ((((A (B 𝐶 ℂ)) x ℂ) (x + A) = 0) → ((0 + B) = (0 + 𝐶) ↔ B = 𝐶))
2721, 26bitrd 177 . . . . . . . . . . . 12 ((((A (B 𝐶 ℂ)) x ℂ) (x + A) = 0) → (((x + A) + B) = ((x + A) + 𝐶) ↔ B = 𝐶))
2827ex 108 . . . . . . . . . . 11 (((A (B 𝐶 ℂ)) x ℂ) → ((x + A) = 0 → (((x + A) + B) = ((x + A) + 𝐶) ↔ B = 𝐶)))
2917, 28sylbid 139 . . . . . . . . . 10 (((A (B 𝐶 ℂ)) x ℂ) → ((A + x) = 0 → (((x + A) + B) = ((x + A) + 𝐶) ↔ B = 𝐶)))
3029imp 115 . . . . . . . . 9 ((((A (B 𝐶 ℂ)) x ℂ) (A + x) = 0) → (((x + A) + B) = ((x + A) + 𝐶) ↔ B = 𝐶))
3114, 30sylibd 138 . . . . . . . 8 ((((A (B 𝐶 ℂ)) x ℂ) (A + x) = 0) → ((A + B) = (A + 𝐶) → B = 𝐶))
3231ex 108 . . . . . . 7 (((A (B 𝐶 ℂ)) x ℂ) → ((A + x) = 0 → ((A + B) = (A + 𝐶) → B = 𝐶)))
334, 32sylan2 270 . . . . . 6 (((A (B 𝐶 ℂ)) x ℝ) → ((A + x) = 0 → ((A + B) = (A + 𝐶) → B = 𝐶)))
3433rexlimdva 2427 . . . . 5 ((A (B 𝐶 ℂ)) → (x ℝ (A + x) = 0 → ((A + B) = (A + 𝐶) → B = 𝐶)))
35343impb 1099 . . . 4 ((A B 𝐶 ℂ) → (x ℝ (A + x) = 0 → ((A + B) = (A + 𝐶) → B = 𝐶)))
363, 35syl3an1 1167 . . 3 ((A B 𝐶 ℂ) → (x ℝ (A + x) = 0 → ((A + B) = (A + 𝐶) → B = 𝐶)))
372, 36mpd 13 . 2 ((A B 𝐶 ℂ) → ((A + B) = (A + 𝐶) → B = 𝐶))
38 oveq2 5463 . 2 (B = 𝐶 → (A + B) = (A + 𝐶))
3937, 38impbid1 130 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  cr 6690  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-mulcl 6761  ax-addcom 6763  ax-addass 6765  ax-i2m1 6768  ax-0id 6771  ax-rnegex 6772
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:  cnegexlem3  6965
  Copyright terms: Public domain W3C validator