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 ( 𝐶 ∈ ℂ → ¬ ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 peano2cnm ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 1 ) ∈ ℂ )
2 id ⊢ ( 𝐶 ∈ ℂ → 𝐶 ∈ ℂ )
3 4cn ⊢ 4 ∈ ℂ
4 3 a1i ⊢ ( 𝐶 ∈ ℂ → 4 ∈ ℂ )
5 2 4 subcld ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 4 ) ∈ ℂ )
6 1cnd ⊢ ( 𝐶 ∈ ℂ → 1 ∈ ℂ )
7 1re ⊢ 1 ∈ ℝ
8 1lt4 ⊢ 1 < 4
9 7 8 ltneii ⊢ 1 ≠ 4
10 9 a1i ⊢ ( 𝐶 ∈ ℂ → 1 ≠ 4 )
11 2 6 4 10 subneintrd ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 − 1 ) ≠ ( 𝐶 − 4 ) )
12 oveq1 ⊢ ( 𝑏 = 1 → ( 𝑏 ↑ 2 ) = ( 1 ↑ 2 ) )
13 12 oveq2d ⊢ ( 𝑏 = 1 → ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝐶 − 1 ) + ( 1 ↑ 2 ) ) )
14 13 eqeq1d ⊢ ( 𝑏 = 1 → ( ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 1 ) + ( 1 ↑ 2 ) ) = 𝐶 ) )
15 14 adantl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 = 1 ) → ( ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 1 ) + ( 1 ↑ 2 ) ) = 𝐶 ) )
16 sq1 ⊢ ( 1 ↑ 2 ) = 1
17 16 oveq2i ⊢ ( ( 𝐶 − 1 ) + ( 1 ↑ 2 ) ) = ( ( 𝐶 − 1 ) + 1 )
18 npcan1 ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 − 1 ) + 1 ) = 𝐶 )
19 17 18 syl5eq ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 − 1 ) + ( 1 ↑ 2 ) ) = 𝐶 )
20 6 15 19 rspcedvd ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 )
21 2cnd ⊢ ( 𝐶 ∈ ℂ → 2 ∈ ℂ )
22 oveq1 ⊢ ( 𝑏 = 2 → ( 𝑏 ↑ 2 ) = ( 2 ↑ 2 ) )
23 22 oveq2d ⊢ ( 𝑏 = 2 → ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = ( ( 𝐶 − 4 ) + ( 2 ↑ 2 ) ) )
24 23 eqeq1d ⊢ ( 𝑏 = 2 → ( ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 4 ) + ( 2 ↑ 2 ) ) = 𝐶 ) )
25 24 adantl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝑏 = 2 ) → ( ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 4 ) + ( 2 ↑ 2 ) ) = 𝐶 ) )
26 2cn ⊢ 2 ∈ ℂ
27 26 sqcli ⊢ ( 2 ↑ 2 ) ∈ ℂ
28 27 a1i ⊢ ( 𝐶 ∈ ℂ → ( 2 ↑ 2 ) ∈ ℂ )
29 2 4 28 subadd23d ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 − 4 ) + ( 2 ↑ 2 ) ) = ( 𝐶 + ( ( 2 ↑ 2 ) − 4 ) ) )
30 sq2 ⊢ ( 2 ↑ 2 ) = 4
31 30 a1i ⊢ ( 𝐶 ∈ ℂ → ( 2 ↑ 2 ) = 4 )
32 28 31 subeq0bd ⊢ ( 𝐶 ∈ ℂ → ( ( 2 ↑ 2 ) − 4 ) = 0 )
33 27 3 subcli ⊢ ( ( 2 ↑ 2 ) − 4 ) ∈ ℂ
34 addid0 ⊢ ( ( 𝐶 ∈ ℂ ∧ ( ( 2 ↑ 2 ) − 4 ) ∈ ℂ ) → ( ( 𝐶 + ( ( 2 ↑ 2 ) − 4 ) ) = 𝐶 ↔ ( ( 2 ↑ 2 ) − 4 ) = 0 ) )
35 33 34 mpan2 ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 + ( ( 2 ↑ 2 ) − 4 ) ) = 𝐶 ↔ ( ( 2 ↑ 2 ) − 4 ) = 0 ) )
36 32 35 mpbird ⊢ ( 𝐶 ∈ ℂ → ( 𝐶 + ( ( 2 ↑ 2 ) − 4 ) ) = 𝐶 )
37 29 36 eqtrd ⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 − 4 ) + ( 2 ↑ 2 ) ) = 𝐶 )
38 21 25 37 rspcedvd ⊢ ( 𝐶 ∈ ℂ → ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 )
39 oveq1 ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) )
40 39 eqeq1d ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
41 40 rexbidv ⊢ ( 𝑎 = ( 𝐶 − 1 ) → ( ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
42 oveq1 ⊢ ( 𝑎 = ( 𝐶 − 4 ) → ( 𝑎 + ( 𝑏 ↑ 2 ) ) = ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) )
43 42 eqeq1d ⊢ ( 𝑎 = ( 𝐶 − 4 ) → ( ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
44 43 rexbidv ⊢ ( 𝑎 = ( 𝐶 − 4 ) → ( ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ↔ ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
45 41 44 2nreu ⊢ ( ( ( 𝐶 − 1 ) ∈ ℂ ∧ ( 𝐶 − 4 ) ∈ ℂ ∧ ( 𝐶 − 1 ) ≠ ( 𝐶 − 4 ) ) → ( ( ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) → ¬ ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 ) )
46 45 imp ⊢ ( ( ( ( 𝐶 − 1 ) ∈ ℂ ∧ ( 𝐶 − 4 ) ∈ ℂ ∧ ( 𝐶 − 1 ) ≠ ( 𝐶 − 4 ) ) ∧ ( ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 1 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ∧ ∃ 𝑏 ∈ ℂ ( ( 𝐶 − 4 ) + ( 𝑏 ↑ 2 ) ) = 𝐶 ) ) → ¬ ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 )
47 1 5 11 20 38 46 syl32anc ⊢ ( 𝐶 ∈ ℂ → ¬ ∃! 𝑎 ∈ ℂ ∃ 𝑏 ∈ ℂ ( 𝑎 + ( 𝑏 ↑ 2 ) ) = 𝐶 )