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 ⊢ ( 𝜑 → 𝑟 ∈ ℝ )
cnreeu.s ⊢ ( 𝜑 → 𝑠 ∈ ℝ )
cnreeu.t ⊢ ( 𝜑 → 𝑡 ∈ ℝ )
cnreeu.u ⊢ ( 𝜑 → 𝑢 ∈ ℝ )
Assertion cnreeu ( 𝜑 → ( ( 𝑟 + ( i · 𝑠 ) ) = ( 𝑡 + ( i · 𝑢 ) ) ↔ ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )

Proof

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