Metamath Proof Explorer

Theorem addsq2reu

Description: For each complex number C , there exists a unique complex number a added to the square of a unique another complex number b resulting in the given complex number C . The unique complex number a is C , and the unique another complex number b is 0 .

Remark: This, together with addsqnreup , is an example showing that the pattern E! a e. A E! b e. B ph does not necessarily mean "There are unique sets a and b fulfilling ph ). See also comments for df-eu and 2eu4 . For more details see comment for addsqnreup . (Contributed by AV, 21-Jun-2023)

Ref Expression
Assertion addsq2reu ⊢ C ∈ ℂ → ∃! a ∈ ℂ ∃! b ∈ ℂ a + b 2 = C

Proof

Step Hyp Ref Expression
1 id ⊢ C ∈ ℂ → C ∈ ℂ
2 oveq1 ⊢ a = C → a + b 2 = C + b 2
3 2 eqeq1d ⊢ a = C → a + b 2 = C ↔ C + b 2 = C
4 3 reubidv ⊢ a = C → ∃! b ∈ ℂ a + b 2 = C ↔ ∃! b ∈ ℂ C + b 2 = C
5 eqeq1 ⊢ a = C → a = c ↔ C = c
6 5 imbi2d ⊢ a = C → ∃! b ∈ ℂ c + b 2 = C → a = c ↔ ∃! b ∈ ℂ c + b 2 = C → C = c
7 6 ralbidv ⊢ a = C → ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → a = c ↔ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → C = c
8 4 7 anbi12d ⊢ a = C → ∃! b ∈ ℂ a + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → a = c ↔ ∃! b ∈ ℂ C + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → C = c
9 8 adantl ⊢ C ∈ ℂ ∧ a = C → ∃! b ∈ ℂ a + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → a = c ↔ ∃! b ∈ ℂ C + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → C = c
10 0cnd ⊢ C ∈ ℂ → 0 ∈ ℂ
11 reueq ⊢ 0 ∈ ℂ ↔ ∃! b ∈ ℂ b = 0
12 10 11 sylib ⊢ C ∈ ℂ → ∃! b ∈ ℂ b = 0
13 subid ⊢ C ∈ ℂ → C − C = 0
14 13 adantr ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C = 0
15 14 eqeq1d ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C = b 2 ↔ 0 = b 2
16 simpl ⊢ C ∈ ℂ ∧ b ∈ ℂ → C ∈ ℂ
17 simpr ⊢ C ∈ ℂ ∧ b ∈ ℂ → b ∈ ℂ
18 17 sqcld ⊢ C ∈ ℂ ∧ b ∈ ℂ → b 2 ∈ ℂ
19 16 16 18 subaddd ⊢ C ∈ ℂ ∧ b ∈ ℂ → C − C = b 2 ↔ C + b 2 = C
20 eqcom ⊢ 0 = b 2 ↔ b 2 = 0
21 sqeq0 ⊢ b ∈ ℂ → b 2 = 0 ↔ b = 0
22 20 21 bitrid ⊢ b ∈ ℂ → 0 = b 2 ↔ b = 0
23 22 adantl ⊢ C ∈ ℂ ∧ b ∈ ℂ → 0 = b 2 ↔ b = 0
24 15 19 23 3bitr3d ⊢ C ∈ ℂ ∧ b ∈ ℂ → C + b 2 = C ↔ b = 0
25 24 reubidva ⊢ C ∈ ℂ → ∃! b ∈ ℂ C + b 2 = C ↔ ∃! b ∈ ℂ b = 0
26 12 25 mpbird ⊢ C ∈ ℂ → ∃! b ∈ ℂ C + b 2 = C
27 simpr ⊢ C ∈ ℂ ∧ c ∈ ℂ → c ∈ ℂ
28 27 adantr ⊢ C ∈ ℂ ∧ c ∈ ℂ ∧ b ∈ ℂ → c ∈ ℂ
29 sqcl ⊢ b ∈ ℂ → b 2 ∈ ℂ
30 29 adantl ⊢ C ∈ ℂ ∧ c ∈ ℂ ∧ b ∈ ℂ → b 2 ∈ ℂ
31 simpl ⊢ C ∈ ℂ ∧ c ∈ ℂ → C ∈ ℂ
32 31 adantr ⊢ C ∈ ℂ ∧ c ∈ ℂ ∧ b ∈ ℂ → C ∈ ℂ
33 28 30 32 addrsub ⊢ C ∈ ℂ ∧ c ∈ ℂ ∧ b ∈ ℂ → c + b 2 = C ↔ b 2 = C − c
34 33 reubidva ⊢ C ∈ ℂ ∧ c ∈ ℂ → ∃! b ∈ ℂ c + b 2 = C ↔ ∃! b ∈ ℂ b 2 = C − c
35 subcl ⊢ C ∈ ℂ ∧ c ∈ ℂ → C − c ∈ ℂ
36 reusq0 ⊢ C − c ∈ ℂ → ∃! b ∈ ℂ b 2 = C − c ↔ C − c = 0
37 35 36 syl ⊢ C ∈ ℂ ∧ c ∈ ℂ → ∃! b ∈ ℂ b 2 = C − c ↔ C − c = 0
38 subeq0 ⊢ C ∈ ℂ ∧ c ∈ ℂ → C − c = 0 ↔ C = c
39 38 biimpd ⊢ C ∈ ℂ ∧ c ∈ ℂ → C − c = 0 → C = c
40 37 39 sylbid ⊢ C ∈ ℂ ∧ c ∈ ℂ → ∃! b ∈ ℂ b 2 = C − c → C = c
41 34 40 sylbid ⊢ C ∈ ℂ ∧ c ∈ ℂ → ∃! b ∈ ℂ c + b 2 = C → C = c
42 41 ralrimiva ⊢ C ∈ ℂ → ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → C = c
43 26 42 jca ⊢ C ∈ ℂ → ∃! b ∈ ℂ C + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → C = c
44 1 9 43 rspcedvd ⊢ C ∈ ℂ → ∃ a ∈ ℂ ∃! b ∈ ℂ a + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → a = c
45 oveq1 ⊢ a = c → a + b 2 = c + b 2
46 45 eqeq1d ⊢ a = c → a + b 2 = C ↔ c + b 2 = C
47 46 reubidv ⊢ a = c → ∃! b ∈ ℂ a + b 2 = C ↔ ∃! b ∈ ℂ c + b 2 = C
48 47 reu8 ⊢ ∃! a ∈ ℂ ∃! b ∈ ℂ a + b 2 = C ↔ ∃ a ∈ ℂ ∃! b ∈ ℂ a + b 2 = C ∧ ∀ c ∈ ℂ ∃! b ∈ ℂ c + b 2 = C → a = c
49 44 48 sylibr ⊢ C ∈ ℂ → ∃! a ∈ ℂ ∃! b ∈ ℂ a + b 2 = C