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

Theorem cnegexlem1 7981
 Description: Addition cancellation of a real number from two complex numbers. Lemma for cnegex 7984. (Contributed by Eric Schmidt, 22-May-2007.)
Assertion
Ref Expression
cnegexlem1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))

Proof of Theorem cnegexlem1
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ax-rnegex 7773 . . . 4 (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
213ad2ant1 1003 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0)
3 recn 7797 . . . 4 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4 recn 7797 . . . . . . 7 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
5 oveq2 5791 . . . . . . . . . . 11 ((𝐴 + 𝐵) = (𝐴 + 𝐶) → (𝑥 + (𝐴 + 𝐵)) = (𝑥 + (𝐴 + 𝐶)))
6 simpr 109 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
7 simpll 519 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐴 ∈ ℂ)
8 simplrl 525 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ)
96, 7, 8addassd 7832 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) + 𝐵) = (𝑥 + (𝐴 + 𝐵)))
10 simplrr 526 . . . . . . . . . . . . 13 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → 𝐶 ∈ ℂ)
116, 7, 10addassd 7832 . . . . . . . . . . . 12 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) + 𝐶) = (𝑥 + (𝐴 + 𝐶)))
129, 11eqeq12d 2155 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (𝑥 + (𝐴 + 𝐵)) = (𝑥 + (𝐴 + 𝐶))))
135, 12syl5ibr 155 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → ((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶)))
1413adantr 274 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → ((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶)))
15 addcom 7943 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (𝐴 + 𝑥) = (𝑥 + 𝐴))
1615eqeq1d 2149 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 ↔ (𝑥 + 𝐴) = 0))
1716adantlr 469 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 ↔ (𝑥 + 𝐴) = 0))
18 oveq1 5790 . . . . . . . . . . . . . . 15 ((𝑥 + 𝐴) = 0 → ((𝑥 + 𝐴) + 𝐵) = (0 + 𝐵))
19 oveq1 5790 . . . . . . . . . . . . . . 15 ((𝑥 + 𝐴) = 0 → ((𝑥 + 𝐴) + 𝐶) = (0 + 𝐶))
2018, 19eqeq12d 2155 . . . . . . . . . . . . . 14 ((𝑥 + 𝐴) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (0 + 𝐵) = (0 + 𝐶)))
2120adantl 275 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ (0 + 𝐵) = (0 + 𝐶)))
22 addid2 7945 . . . . . . . . . . . . . . . 16 (𝐵 ∈ ℂ → (0 + 𝐵) = 𝐵)
23 addid2 7945 . . . . . . . . . . . . . . . 16 (𝐶 ∈ ℂ → (0 + 𝐶) = 𝐶)
2422, 23eqeqan12d 2156 . . . . . . . . . . . . . . 15 ((𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((0 + 𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶))
2524adantl 275 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) → ((0 + 𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶))
2625ad2antrr 480 . . . . . . . . . . . . 13 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → ((0 + 𝐵) = (0 + 𝐶) ↔ 𝐵 = 𝐶))
2721, 26bitrd 187 . . . . . . . . . . . 12 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝑥 + 𝐴) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶))
2827ex 114 . . . . . . . . . . 11 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝑥 + 𝐴) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶)))
2917, 28sylbid 149 . . . . . . . . . 10 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶)))
3029imp 123 . . . . . . . . 9 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → (((𝑥 + 𝐴) + 𝐵) = ((𝑥 + 𝐴) + 𝐶) ↔ 𝐵 = 𝐶))
3114, 30sylibd 148 . . . . . . . 8 ((((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) ∧ (𝐴 + 𝑥) = 0) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))
3231ex 114 . . . . . . 7 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℂ) → ((𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)))
334, 32sylan2 284 . . . . . 6 (((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) ∧ 𝑥 ∈ ℝ) → ((𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)))
3433rexlimdva 2553 . . . . 5 ((𝐴 ∈ ℂ ∧ (𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ)) → (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)))
35343impb 1178 . . . 4 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)))
363, 35syl3an1 1250 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (∃𝑥 ∈ ℝ (𝐴 + 𝑥) = 0 → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶)))
372, 36mpd 13 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) → 𝐵 = 𝐶))
38 oveq2 5791 . 2 (𝐵 = 𝐶 → (𝐴 + 𝐵) = (𝐴 + 𝐶))
3937, 38impbid1 141 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) = (𝐴 + 𝐶) ↔ 𝐵 = 𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  ∃wrex 2418  (class class class)co 5783  ℂcc 7662  ℝcr 7663  0cc0 7664   + caddc 7667 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-resscn 7756  ax-1cn 7757  ax-icn 7759  ax-addcl 7760  ax-mulcl 7762  ax-addcom 7764  ax-addass 7766  ax-i2m1 7769  ax-0id 7772  ax-rnegex 7773 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rex 2423  df-v 2692  df-un 3081  df-in 3083  df-ss 3090  df-sn 3539  df-pr 3540  df-op 3542  df-uni 3746  df-br 3939  df-iota 5097  df-fv 5140  df-ov 5786 This theorem is referenced by:  cnegexlem3  7983
 Copyright terms: Public domain W3C validator