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+b2=C

Proof

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