Theorem cnreeu

Description: The reals in the expression given by cnre uniquely define a complex number. (Contributed by SN, 27-Jun-2024)

	Ref	Expression
Hypotheses	cnreeu.r	$$⊢\phi \to r\in ℝ$$
	cnreeu.s	$$⊢\phi \to s\in ℝ$$
	cnreeu.t	$$⊢\phi \to t\in ℝ$$
	cnreeu.u	$$⊢\phi \to u\in ℝ$$
Assertion	cnreeu	$$⊢\phi \to \left(r+\mathrm{i}s=t+\mathrm{i}u\leftrightarrow \left(r=t\wedge s=u\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnreeu.r	$$⊢\phi \to r\in ℝ$$
2		cnreeu.s	$$⊢\phi \to s\in ℝ$$
3		cnreeu.t	$$⊢\phi \to t\in ℝ$$
4		cnreeu.u	$$⊢\phi \to u\in ℝ$$
5		oveq1	$$⊢r+\mathrm{i}s=t+\mathrm{i}u\to r+\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)=t+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
6	5	oveq2d	$$⊢r+\mathrm{i}s=t+\mathrm{i}u\to \left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
7	1	recnd	$$⊢\phi \to r\in ℂ$$
8		ax-icn	$$⊢\mathrm{i}\in ℂ$$
9	8	a1i	$$⊢\phi \to \mathrm{i}\in ℂ$$
10	2	recnd	$$⊢\phi \to s\in ℂ$$
11	9 10	mulcld	$$⊢\phi \to \mathrm{i}s\in ℂ$$
12		rernegcl	$$⊢s\in ℝ\to 0{-}_{ℝ}s\in ℝ$$
13	2 12	syl	$$⊢\phi \to 0{-}_{ℝ}s\in ℝ$$
14	13	recnd	$$⊢\phi \to 0{-}_{ℝ}s\in ℂ$$
15	9 14	mulcld	$$⊢\phi \to \mathrm{i}\left(0{-}_{ℝ}s\right)\in ℂ$$
16	7 11 15	addassd	$$⊢\phi \to r+\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)=r+\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
17		renegid	$$⊢s\in ℝ\to s+\left(0{-}_{ℝ}s\right)=0$$
18	2 17	syl	$$⊢\phi \to s+\left(0{-}_{ℝ}s\right)=0$$
19	18	oveq2d	$$⊢\phi \to \mathrm{i}\left(s+\left(0{-}_{ℝ}s\right)\right)=\mathrm{i}\cdot 0$$
20	9 10 14	adddid	$$⊢\phi \to \mathrm{i}\left(s+\left(0{-}_{ℝ}s\right)\right)=\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
21		sn-it0e0	$$⊢\mathrm{i}\cdot 0=0$$
22	21	a1i	$$⊢\phi \to \mathrm{i}\cdot 0=0$$
23	19 20 22	3eqtr3d	$$⊢\phi \to \mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)=0$$
24	23	oveq2d	$$⊢\phi \to r+\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)=r+0$$
25		readdid1	$$⊢r\in ℝ\to r+0=r$$
26	1 25	syl	$$⊢\phi \to r+0=r$$
27	16 24 26	3eqtrd	$$⊢\phi \to r+\mathrm{i}s+\mathrm{i}\left(0{-}_{ℝ}s\right)=r$$
28	27	oveq2d	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+r$$
29		rernegcl	$$⊢t\in ℝ\to 0{-}_{ℝ}t\in ℝ$$
30	3 29	syl	$$⊢\phi \to 0{-}_{ℝ}t\in ℝ$$
31	30	recnd	$$⊢\phi \to 0{-}_{ℝ}t\in ℂ$$
32	3	recnd	$$⊢\phi \to t\in ℂ$$
33	4	recnd	$$⊢\phi \to u\in ℂ$$
34	9 33	mulcld	$$⊢\phi \to \mathrm{i}u\in ℂ$$
35	31 32 34	addassd	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+t+\mathrm{i}u=\left(0{-}_{ℝ}t\right)+t+\mathrm{i}u$$
36	35	oveq1d	$$⊢\phi \to \left(\left(0{-}_{ℝ}t\right)+t\right)+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
37		sn-addid2	$$⊢\mathrm{i}u\in ℂ\to 0+\mathrm{i}u=\mathrm{i}u$$
38	34 37	syl	$$⊢\phi \to 0+\mathrm{i}u=\mathrm{i}u$$
39	38	oveq1d	$$⊢\phi \to 0+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)=\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
40		renegid2	$$⊢t\in ℝ\to \left(0{-}_{ℝ}t\right)+t=0$$
41	3 40	syl	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+t=0$$
42	41	oveq1d	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+t+\mathrm{i}u=0+\mathrm{i}u$$
43	42	oveq1d	$$⊢\phi \to \left(\left(0{-}_{ℝ}t\right)+t\right)+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)=0+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
44	9 33 14	adddid	$$⊢\phi \to \mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)=\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
45	39 43 44	3eqtr4d	$$⊢\phi \to \left(\left(0{-}_{ℝ}t\right)+t\right)+\mathrm{i}u+\mathrm{i}\left(0{-}_{ℝ}s\right)=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)$$
46	32 34	addcld	$$⊢\phi \to t+\mathrm{i}u\in ℂ$$
47	31 46 15	addassd	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)$$
48	36 45 47	3eqtr3rd	$$⊢\phi \to \left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)$$
49	28 48	eqeq12d	$$⊢\phi \to \left(\left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)\leftrightarrow \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)$$
50	49	biimpa	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)\right)\to \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)$$
51		simpr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)$$
52	4	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to u\in ℝ$$
53	13	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to 0{-}_{ℝ}s\in ℝ$$
54	52 53	readdcld	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to u+\left(0{-}_{ℝ}s\right)\in ℝ$$
55	30	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to 0{-}_{ℝ}t\in ℝ$$
56	1	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to r\in ℝ$$
57	55 56	readdcld	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \left(0{-}_{ℝ}t\right)+r\in ℝ$$
58	51 57	eqeltrrd	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\in ℝ$$
59		itrere	$$⊢u+\left(0{-}_{ℝ}s\right)\in ℝ\to \left(\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\in ℝ\leftrightarrow u+\left(0{-}_{ℝ}s\right)=0\right)$$
60	59	biimpa	$$⊢\left(u+\left(0{-}_{ℝ}s\right)\in ℝ\wedge \mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\in ℝ\right)\to u+\left(0{-}_{ℝ}s\right)=0$$
61	54 58 60	syl2anc	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to u+\left(0{-}_{ℝ}s\right)=0$$
62	61	oveq2d	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)=\mathrm{i}\cdot 0$$
63	21	a1i	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \mathrm{i}\cdot 0=0$$
64	51 62 63	3eqtrd	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \left(0{-}_{ℝ}t\right)+r=0$$
65		oveq2	$$⊢\left(0{-}_{ℝ}t\right)+r=0\to t+\left(0{-}_{ℝ}t\right)+r=t+0$$
66	65	adantl	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+\left(0{-}_{ℝ}t\right)+r=t+0$$
67		renegid	$$⊢t\in ℝ\to t+\left(0{-}_{ℝ}t\right)=0$$
68	3 67	syl	$$⊢\phi \to t+\left(0{-}_{ℝ}t\right)=0$$
69	68	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+\left(0{-}_{ℝ}t\right)=0$$
70	69	oveq1d	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+\left(0{-}_{ℝ}t\right)+r=0+r$$
71	32	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t\in ℂ$$
72	31	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to 0{-}_{ℝ}t\in ℂ$$
73	7	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to r\in ℂ$$
74	71 72 73	addassd	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+\left(0{-}_{ℝ}t\right)+r=t+\left(0{-}_{ℝ}t\right)+r$$
75		readdid2	$$⊢r\in ℝ\to 0+r=r$$
76	1 75	syl	$$⊢\phi \to 0+r=r$$
77	76	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to 0+r=r$$
78	70 74 77	3eqtr3d	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+\left(0{-}_{ℝ}t\right)+r=r$$
79	3	adantr	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t\in ℝ$$
80		readdid1	$$⊢t\in ℝ\to t+0=t$$
81	79 80	syl	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to t+0=t$$
82	66 78 81	3eqtr3d	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=0\right)\to r=t$$
83	64 82	syldan	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to r=t$$
84	33 14 10	addassd	$$⊢\phi \to u+\left(0{-}_{ℝ}s\right)+s=u+\left(0{-}_{ℝ}s\right)+s$$
85		renegid2	$$⊢s\in ℝ\to \left(0{-}_{ℝ}s\right)+s=0$$
86	2 85	syl	$$⊢\phi \to \left(0{-}_{ℝ}s\right)+s=0$$
87	86	oveq2d	$$⊢\phi \to u+\left(0{-}_{ℝ}s\right)+s=u+0$$
88		readdid1	$$⊢u\in ℝ\to u+0=u$$
89	4 88	syl	$$⊢\phi \to u+0=u$$
90	84 87 89	3eqtrd	$$⊢\phi \to u+\left(0{-}_{ℝ}s\right)+s=u$$
91		oveq1	$$⊢u+\left(0{-}_{ℝ}s\right)=0\to u+\left(0{-}_{ℝ}s\right)+s=0+s$$
92	90 91	sylan9req	$$⊢\left(\phi \wedge u+\left(0{-}_{ℝ}s\right)=0\right)\to u=0+s$$
93		readdid2	$$⊢s\in ℝ\to 0+s=s$$
94	2 93	syl	$$⊢\phi \to 0+s=s$$
95	94	adantr	$$⊢\left(\phi \wedge u+\left(0{-}_{ℝ}s\right)=0\right)\to 0+s=s$$
96	92 95	eqtr2d	$$⊢\left(\phi \wedge u+\left(0{-}_{ℝ}s\right)=0\right)\to s=u$$
97	61 96	syldan	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to s=u$$
98	83 97	jca	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+r=\mathrm{i}\left(u+\left(0{-}_{ℝ}s\right)\right)\right)\to \left(r=t\wedge s=u\right)$$
99	50 98	syldan	$$⊢\left(\phi \wedge \left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)\right)\to \left(r=t\wedge s=u\right)$$
100	99	ex	$$⊢\phi \to \left(\left(0{-}_{ℝ}t\right)+\left(r+\mathrm{i}s\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)=\left(0{-}_{ℝ}t\right)+\left(t+\mathrm{i}u\right)+\mathrm{i}\left(0{-}_{ℝ}s\right)\to \left(r=t\wedge s=u\right)\right)$$
101	6 100	syl5	$$⊢\phi \to \left(r+\mathrm{i}s=t+\mathrm{i}u\to \left(r=t\wedge s=u\right)\right)$$
102		id	$$⊢r=t\to r=t$$
103		oveq2	$$⊢s=u\to \mathrm{i}s=\mathrm{i}u$$
104	102 103	oveqan12d	$$⊢\left(r=t\wedge s=u\right)\to r+\mathrm{i}s=t+\mathrm{i}u$$
105	101 104	impbid1	$$⊢\phi \to \left(r+\mathrm{i}s=t+\mathrm{i}u\leftrightarrow \left(r=t\wedge s=u\right)\right)$$