Metamath Proof Explorer


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 φ r
cnreeu.s φ s
cnreeu.t φ t
cnreeu.u φ u
Assertion cnreeu φ r + i s = t + i u r = t s = u

Proof

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