Theorem negeu 5368

Description: Existential uniqueness of negatives. Theorem I.2 of [Apostol] p. 18.

Hypotheses

Ref	Expression
negeu.1	⊢ A ∈ ℂ
negeu.2	⊢ B ∈ ℂ

Assertion

Ref	Expression
negeu	⊢ ∃!x ∈ ℂ (A + x) = B

Distinct variable groups:   x,A   x,B

Proof of Theorem negeu

Step	Hyp	Ref	Expression
1		opreq2 3983	. . . 4 ⊢ (x = y → (A + x) = (A + y))
2	1	eqeq1d 1490	. . 3 ⊢ (x = y → ((A + x) = B ↔ (A + y) = B))
3	2	reu4 1941	. 2 ⊢ (∃!x ∈ ℂ (A + x) = B ↔ (∃x ∈ ℂ (A + x) = B ⋀ ∀x ∈ ℂ ∀y ∈ ℂ (((A + x) = B ⋀ (A + y) = B) → x = y)))
4		negeu.1	. . . 4 ⊢ A ∈ ℂ
5	4	cnegex 5362	. . 3 ⊢ ∃y ∈ ℂ (A + y) = 0
6		negeu.2	. . . . . . 7 ⊢ B ∈ ℂ
7		axaddcl 5284	. . . . . . 7 ⊢ ((y ∈ ℂ ⋀ B ∈ ℂ) → (y + B) ∈ ℂ)
8	6, 7	mpan2 700	. . . . . 6 ⊢ (y ∈ ℂ → (y + B) ∈ ℂ)
9		risset 1692	. . . . . 6 ⊢ ((y + B) ∈ ℂ ↔ ∃x ∈ ℂ x = (y + B))
10	8, 9	sylib 198	. . . . 5 ⊢ (y ∈ ℂ → ∃x ∈ ℂ x = (y + B))
11		opreq2 3983	. . . . . . . . . . . . 13 ⊢ (x = (y + B) → (A + x) = (A + (y + B)))
12		axaddass 5290	. . . . . . . . . . . . . . 15 ⊢ ((A ∈ ℂ ⋀ y ∈ ℂ ⋀ B ∈ ℂ) → ((A + y) + B) = (A + (y + B)))
13	4, 6, 12	mp3an13 911	. . . . . . . . . . . . . 14 ⊢ (y ∈ ℂ → ((A + y) + B) = (A + (y + B)))
14	13	eqcomd 1487	. . . . . . . . . . . . 13 ⊢ (y ∈ ℂ → (A + (y + B)) = ((A + y) + B))
15	11, 14	sylan9eqr 1536	. . . . . . . . . . . 12 ⊢ ((y ∈ ℂ ⋀ x = (y + B)) → (A + x) = ((A + y) + B))
16		opreq1 3982	. . . . . . . . . . . . 13 ⊢ ((A + y) = 0 → ((A + y) + B) = (0 + B))
17	6	addid2 5344	. . . . . . . . . . . . 13 ⊢ (0 + B) = B
18	16, 17	syl6eq 1530	. . . . . . . . . . . 12 ⊢ ((A + y) = 0 → ((A + y) + B) = B)
19	15, 18	sylan9eqr 1536	. . . . . . . . . . 11 ⊢ (((A + y) = 0 ⋀ (y ∈ ℂ ⋀ x = (y + B))) → (A + x) = B)
20	19	exp32 379	. . . . . . . . . 10 ⊢ ((A + y) = 0 → (y ∈ ℂ → (x = (y + B) → (A + x) = B)))
21	20	impcom 351	. . . . . . . . 9 ⊢ ((y ∈ ℂ ⋀ (A + y) = 0) → (x = (y + B) → (A + x) = B))
22	21	a1d 12	. . . . . . . 8 ⊢ ((y ∈ ℂ ⋀ (A + y) = 0) → (x ∈ ℂ → (x = (y + B) → (A + x) = B)))
23	22	r19.21aiv 1720	. . . . . . 7 ⊢ ((y ∈ ℂ ⋀ (A + y) = 0) → ∀x ∈ ℂ (x = (y + B) → (A + x) = B))
24	23	ex 373	. . . . . 6 ⊢ (y ∈ ℂ → ((A + y) = 0 → ∀x ∈ ℂ (x = (y + B) → (A + x) = B)))
25		r19.22 1738	. . . . . 6 ⊢ (∀x ∈ ℂ (x = (y + B) → (A + x) = B) → (∃x ∈ ℂ x = (y + B) → ∃x ∈ ℂ (A + x) = B))
26	24, 25	syl6 22	. . . . 5 ⊢ (y ∈ ℂ → ((A + y) = 0 → (∃x ∈ ℂ x = (y + B) → ∃x ∈ ℂ (A + x) = B)))
27	10, 26	mpid 47	. . . 4 ⊢ (y ∈ ℂ → ((A + y) = 0 → ∃x ∈ ℂ (A + x) = B))
28	27	r19.23aiv 1750	. . 3 ⊢ (∃y ∈ ℂ (A + y) = 0 → ∃x ∈ ℂ (A + x) = B)
29	5, 28	ax-mp 7	. 2 ⊢ ∃x ∈ ℂ (A + x) = B
30		addcant 5365	. . . . 5 ⊢ ((A ∈ ℂ ⋀ x ∈ ℂ ⋀ y ∈ ℂ) → ((A + x) = (A + y) ↔ x = y))
31		eqtr3t 1501	. . . . 5 ⊢ (((A + x) = B ⋀ (A + y) = B) → (A + x) = (A + y))
32	30, 31	syl5bi 208	. . . 4 ⊢ ((A ∈ ℂ ⋀ x ∈ ℂ ⋀ y ∈ ℂ) → (((A + x) = B ⋀ (A + y) = B) → x = y))
33	4, 32	mp3an1 907	. . 3 ⊢ ((x ∈ ℂ ⋀ y ∈ ℂ) → (((A + x) = B ⋀ (A + y) = B) → x = y))
34	33	rgen2a 1706	. 2 ⊢ ∀x ∈ ℂ ∀y ∈ ℂ (((A + x) = B ⋀ (A + y) = B) → x = y)
35	3, 29, 34	mpbir2an 734	1 ⊢ ∃!x ∈ ℂ (A + x) = B

Syntax hints:   → wi 3   ⋀ wa 223   ⋀ w3a 779   = wceq 960   ∈ wcel 962  ∀wral 1652  ∃wrex 1653  ∃!wreu 1654  (class class class)co 3977  ℂcc 5245  0cc0 5247   + caddc 5250

This theorem is referenced by:  subcl 5379  subadd 5384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-inf2 4637

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-1p 5100  df-plp 5101  df-mp 5102  df-ltp 5103  df-plpr 5177  df-mpr 5178  df-enr 5179  df-nr 5180  df-plr 5181  df-mr 5182  df-0r 5184  df-1r 5185  df-m1r 5186  df-c 5253  df-0 5254  df-1 5255  df-i 5256  df-r 5257  df-plus 5258  df-mul 5259

Copyright terms: Public domain