Theorem remim 15194

Description: Value of the conjugate of a complex number. The value is the real part minus i times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)

Assertion

Ref	Expression
remim	⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))

Proof of Theorem remim

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cjval 15179	. 2 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)))
2		replim 15193	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 𝐴 = ((ℜ‘𝐴) + (i · (ℑ‘𝐴))))
3	2	oveq1d 7438	. . . . 5 ⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
4		recl 15187	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℝ)
5	4	recnd 11255	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (ℜ‘𝐴) ∈ ℂ)
6		ax-icn 11177	. . . . . . 7 ⊢ i ∈ ℂ
7		imcl 15188	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℝ)
8	7	recnd 11255	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (ℑ‘𝐴) ∈ ℂ)
9		mulcl 11202	. . . . . . 7 ⊢ ((i ∈ ℂ ∧ (ℑ‘𝐴) ∈ ℂ) → (i · (ℑ‘𝐴)) ∈ ℂ)
10	6, 8, 9	sylancr 599	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (i · (ℑ‘𝐴)) ∈ ℂ)
11	5, 10, 5	ppncand 11627	. . . . 5 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
12	3, 11	eqtrd 2801	. . . 4 ⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = ((ℜ‘𝐴) + (ℜ‘𝐴)))
13	4, 4	readdcld 11256	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) + (ℜ‘𝐴)) ∈ ℝ)
14	12, 13	eqeltrd 2866	. . 3 ⊢ (𝐴 ∈ ℂ → (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ)
15	5, 10, 10	pnncand 11626	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = ((i · (ℑ‘𝐴)) + (i · (ℑ‘𝐴))))
16	2	oveq1d 7438	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = (((ℜ‘𝐴) + (i · (ℑ‘𝐴))) − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
17	6	a1i 11	. . . . . . . 8 ⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
18	17, 8, 8	adddid 11251	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → (i · ((ℑ‘𝐴) + (ℑ‘𝐴))) = ((i · (ℑ‘𝐴)) + (i · (ℑ‘𝐴))))
19	15, 16, 18	3eqtr4d 2811	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) = (i · ((ℑ‘𝐴) + (ℑ‘𝐴))))
20	19	oveq2d 7439	. . . . 5 ⊢ (𝐴 ∈ ℂ → (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) = (i · (i · ((ℑ‘𝐴) + (ℑ‘𝐴)))))
21	7, 7	readdcld 11256	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℝ)
22	21	recnd 11255	. . . . . 6 ⊢ (𝐴 ∈ ℂ → ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℂ)
23		mulass 11206	. . . . . 6 ⊢ ((i ∈ ℂ ∧ i ∈ ℂ ∧ ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℂ) → ((i · i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) = (i · (i · ((ℑ‘𝐴) + (ℑ‘𝐴)))))
24	6, 6, 22, 23	mp3an12i 1494	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((i · i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) = (i · (i · ((ℑ‘𝐴) + (ℑ‘𝐴)))))
25	20, 24	eqtr4d 2804	. . . 4 ⊢ (𝐴 ∈ ℂ → (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) = ((i · i) · ((ℑ‘𝐴) + (ℑ‘𝐴))))
26		ixi 11861	. . . . . 6 ⊢ (i · i) = -1
27		neg1rr 12222	. . . . . 6 ⊢ -1 ∈ ℝ
28	26, 27	eqeltri 2862	. . . . 5 ⊢ (i · i) ∈ ℝ
29		remulcl 11203	. . . . 5 ⊢ (((i · i) ∈ ℝ ∧ ((ℑ‘𝐴) + (ℑ‘𝐴)) ∈ ℝ) → ((i · i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) ∈ ℝ)
30	28, 21, 29	sylancr 599	. . . 4 ⊢ (𝐴 ∈ ℂ → ((i · i) · ((ℑ‘𝐴) + (ℑ‘𝐴))) ∈ ℝ)
31	25, 30	eqeltrd 2866	. . 3 ⊢ (𝐴 ∈ ℂ → (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ)
32	5, 10	subcld 11587	. . . 4 ⊢ (𝐴 ∈ ℂ → ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) ∈ ℂ)
33		cju 12232	. . . 4 ⊢ (𝐴 ∈ ℂ → ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ))
34		oveq2 7431	. . . . . . 7 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → (𝐴 + 𝑥) = (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
35	34	eleq1d 2851	. . . . . 6 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → ((𝐴 + 𝑥) ∈ ℝ ↔ (𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ))
36		oveq2 7431	. . . . . . . 8 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → (𝐴 − 𝑥) = (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
37	36	oveq2d 7439	. . . . . . 7 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → (i · (𝐴 − 𝑥)) = (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))))
38	37	eleq1d 2851	. . . . . 6 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → ((i · (𝐴 − 𝑥)) ∈ ℝ ↔ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ))
39	35, 38	anbi12d 644	. . . . 5 ⊢ (𝑥 = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))) → (((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ) ↔ ((𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ ∧ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ)))
40	39	riota2 7405	. . . 4 ⊢ ((((ℜ‘𝐴) − (i · (ℑ‘𝐴))) ∈ ℂ ∧ ∃!𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) → (((𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ ∧ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ) ↔ (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
41	32, 33, 40	syl2anc 596	. . 3 ⊢ (𝐴 ∈ ℂ → (((𝐴 + ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))) ∈ ℝ ∧ (i · (𝐴 − ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))) ∈ ℝ) ↔ (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴)))))
42	14, 31, 41	mpbi2and 725	. 2 ⊢ (𝐴 ∈ ℂ → (℩𝑥 ∈ ℂ ((𝐴 + 𝑥) ∈ ℝ ∧ (i · (𝐴 − 𝑥)) ∈ ℝ)) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))
43	1, 42	eqtrd 2801	1 ⊢ (𝐴 ∈ ℂ → (∗‘𝐴) = ((ℜ‘𝐴) − (i · (ℑ‘𝐴))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∃!wreu 3370  ‘cfv 6543  ℩crio 7379  (class class class)co 7423  ℂcc 11116  ℝcr 11117  1c1 11119  ici 11120   + caddc 11121   · cmul 11123   − cmin 11459  -cneg 11460  ∗ccj 15173  ℜcre 15174  ℑcim 15175

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-div 11890  df-nn 12252  df-2 12321  df-cj 15176  df-re 15177  df-im 15178

This theorem is used by:  cjreb  15200  recj  15201  remullem  15205  imcj  15209  cjadd  15218  cjneg  15224  imval2  15228  cji  15236  remimd  15275