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 
|- ( ph -> r e. RR )
cnreeu.s 
|- ( ph -> s e. RR )
cnreeu.t 
|- ( ph -> t e. RR )
cnreeu.u 
|- ( ph -> u e. RR )
Assertion cnreeu 
|- ( ph -> ( ( r + ( _i x. s ) ) = ( t + ( _i x. u ) ) <-> ( r = t /\ s = u ) ) )

Proof

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