Metamath Proof Explorer

Theorem addsq2nreurex

Description: For each complex number C , there is no unique complex number a added to the square of another complex number b resulting in the given complex number C . (Contributed by AV, 2-Jul-2023)

Ref Expression
Assertion addsq2nreurex 
|- ( C e. CC -> -. E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C )

Proof

Step Hyp Ref Expression
1 peano2cnm 
 |-  ( C e. CC -> ( C - 1 ) e. CC )
2 id 
 |-  ( C e. CC -> C e. CC )
3 4cn 
 |-  4 e. CC
4 3 a1i 
 |-  ( C e. CC -> 4 e. CC )
5 2 4 subcld 
 |-  ( C e. CC -> ( C - 4 ) e. CC )
6 1cnd 
 |-  ( C e. CC -> 1 e. CC )
7 1re 
 |-  1 e. RR
8 1lt4 
 |-  1 < 4
9 7 8 ltneii 
 |-  1 =/= 4
10 9 a1i 
 |-  ( C e. CC -> 1 =/= 4 )
11 2 6 4 10 subneintrd 
 |-  ( C e. CC -> ( C - 1 ) =/= ( C - 4 ) )
12 oveq1 
 |-  ( b = 1 -> ( b ^ 2 ) = ( 1 ^ 2 ) )
13 12 oveq2d 
 |-  ( b = 1 -> ( ( C - 1 ) + ( b ^ 2 ) ) = ( ( C - 1 ) + ( 1 ^ 2 ) ) )
14 13 eqeq1d 
 |-  ( b = 1 -> ( ( ( C - 1 ) + ( b ^ 2 ) ) = C <-> ( ( C - 1 ) + ( 1 ^ 2 ) ) = C ) )
15 14 adantl 
 |-  ( ( C e. CC /\ b = 1 ) -> ( ( ( C - 1 ) + ( b ^ 2 ) ) = C <-> ( ( C - 1 ) + ( 1 ^ 2 ) ) = C ) )
16 sq1 
 |-  ( 1 ^ 2 ) = 1
17 16 oveq2i 
 |-  ( ( C - 1 ) + ( 1 ^ 2 ) ) = ( ( C - 1 ) + 1 )
18 npcan1 
 |-  ( C e. CC -> ( ( C - 1 ) + 1 ) = C )
19 17 18 eqtrid 
 |-  ( C e. CC -> ( ( C - 1 ) + ( 1 ^ 2 ) ) = C )
20 6 15 19 rspcedvd 
 |-  ( C e. CC -> E. b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C )
21 2cnd 
 |-  ( C e. CC -> 2 e. CC )
22 oveq1 
 |-  ( b = 2 -> ( b ^ 2 ) = ( 2 ^ 2 ) )
23 22 oveq2d 
 |-  ( b = 2 -> ( ( C - 4 ) + ( b ^ 2 ) ) = ( ( C - 4 ) + ( 2 ^ 2 ) ) )
24 23 eqeq1d 
 |-  ( b = 2 -> ( ( ( C - 4 ) + ( b ^ 2 ) ) = C <-> ( ( C - 4 ) + ( 2 ^ 2 ) ) = C ) )
25 24 adantl 
 |-  ( ( C e. CC /\ b = 2 ) -> ( ( ( C - 4 ) + ( b ^ 2 ) ) = C <-> ( ( C - 4 ) + ( 2 ^ 2 ) ) = C ) )
26 2cn 
 |-  2 e. CC
27 26 sqcli 
 |-  ( 2 ^ 2 ) e. CC
28 27 a1i 
 |-  ( C e. CC -> ( 2 ^ 2 ) e. CC )
29 2 4 28 subadd23d 
 |-  ( C e. CC -> ( ( C - 4 ) + ( 2 ^ 2 ) ) = ( C + ( ( 2 ^ 2 ) - 4 ) ) )
30 sq2 
 |-  ( 2 ^ 2 ) = 4
31 30 a1i 
 |-  ( C e. CC -> ( 2 ^ 2 ) = 4 )
32 28 31 subeq0bd 
 |-  ( C e. CC -> ( ( 2 ^ 2 ) - 4 ) = 0 )
33 27 3 subcli 
 |-  ( ( 2 ^ 2 ) - 4 ) e. CC
34 addid0 
 |-  ( ( C e. CC /\ ( ( 2 ^ 2 ) - 4 ) e. CC ) -> ( ( C + ( ( 2 ^ 2 ) - 4 ) ) = C <-> ( ( 2 ^ 2 ) - 4 ) = 0 ) )
35 33 34 mpan2 
 |-  ( C e. CC -> ( ( C + ( ( 2 ^ 2 ) - 4 ) ) = C <-> ( ( 2 ^ 2 ) - 4 ) = 0 ) )
36 32 35 mpbird 
 |-  ( C e. CC -> ( C + ( ( 2 ^ 2 ) - 4 ) ) = C )
37 29 36 eqtrd 
 |-  ( C e. CC -> ( ( C - 4 ) + ( 2 ^ 2 ) ) = C )
38 21 25 37 rspcedvd 
 |-  ( C e. CC -> E. b e. CC ( ( C - 4 ) + ( b ^ 2 ) ) = C )
39 oveq1 
 |-  ( a = ( C - 1 ) -> ( a + ( b ^ 2 ) ) = ( ( C - 1 ) + ( b ^ 2 ) ) )
40 39 eqeq1d 
 |-  ( a = ( C - 1 ) -> ( ( a + ( b ^ 2 ) ) = C <-> ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
41 40 rexbidv 
 |-  ( a = ( C - 1 ) -> ( E. b e. CC ( a + ( b ^ 2 ) ) = C <-> E. b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C ) )
42 oveq1 
 |-  ( a = ( C - 4 ) -> ( a + ( b ^ 2 ) ) = ( ( C - 4 ) + ( b ^ 2 ) ) )
43 42 eqeq1d 
 |-  ( a = ( C - 4 ) -> ( ( a + ( b ^ 2 ) ) = C <-> ( ( C - 4 ) + ( b ^ 2 ) ) = C ) )
44 43 rexbidv 
 |-  ( a = ( C - 4 ) -> ( E. b e. CC ( a + ( b ^ 2 ) ) = C <-> E. b e. CC ( ( C - 4 ) + ( b ^ 2 ) ) = C ) )
45 41 44 2nreu 
 |-  ( ( ( C - 1 ) e. CC /\ ( C - 4 ) e. CC /\ ( C - 1 ) =/= ( C - 4 ) ) -> ( ( E. b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C /\ E. b e. CC ( ( C - 4 ) + ( b ^ 2 ) ) = C ) -> -. E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C ) )
46 45 imp 
 |-  ( ( ( ( C - 1 ) e. CC /\ ( C - 4 ) e. CC /\ ( C - 1 ) =/= ( C - 4 ) ) /\ ( E. b e. CC ( ( C - 1 ) + ( b ^ 2 ) ) = C /\ E. b e. CC ( ( C - 4 ) + ( b ^ 2 ) ) = C ) ) -> -. E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C )
47 1 5 11 20 38 46 syl32anc 
 |-  ( C e. CC -> -. E! a e. CC E. b e. CC ( a + ( b ^ 2 ) ) = C )