Metamath Proof Explorer

Theorem sqrmo

Description: Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013) (Revised by NM, 17-Jun-2017)

Ref Expression
Assertion sqrmo ( 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )

Proof

Step Hyp Ref Expression
1 simplr1 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑥 ↑ 2 ) = 𝐴 )
2 simprr1 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑦 ↑ 2 ) = 𝐴 )
3 1 2 eqtr4d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
4 sqeqor ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) ↔ ( 𝑥 = 𝑦 ∨ 𝑥 = - 𝑦 ) ) )
5 4 ad2ant2r ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) ↔ ( 𝑥 = 𝑦 ∨ 𝑥 = - 𝑦 ) ) )
6 3 5 mpbid ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑥 = 𝑦 ∨ 𝑥 = - 𝑦 ) )
7 6 ord ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( ¬ 𝑥 = 𝑦 → 𝑥 = - 𝑦 ) )
8 3simpc ⊢ ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
9 fveq2 ⊢ ( 𝑥 = - 𝑦 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ - 𝑦 ) )
10 9 breq2d ⊢ ( 𝑥 = - 𝑦 → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ - 𝑦 ) ) )
11 oveq2 ⊢ ( 𝑥 = - 𝑦 → ( i · 𝑥 ) = ( i · - 𝑦 ) )
12 neleq1 ⊢ ( ( i · 𝑥 ) = ( i · - 𝑦 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · - 𝑦 ) ∉ ℝ+ ) )
13 11 12 syl ⊢ ( 𝑥 = - 𝑦 → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · - 𝑦 ) ∉ ℝ+ ) )
14 10 13 anbi12d ⊢ ( 𝑥 = - 𝑦 → ( ( 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
15 8 14 syl5ibcom ⊢ ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → ( 𝑥 = - 𝑦 → ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
16 15 ad2antlr ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑥 = - 𝑦 → ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
17 7 16 syld ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( ¬ 𝑥 = 𝑦 → ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
18 negeq ⊢ ( 𝑦 = 0 → - 𝑦 = - 0 )
19 neg0 ⊢ - 0 = 0
20 18 19 eqtrdi ⊢ ( 𝑦 = 0 → - 𝑦 = 0 )
21 20 eqeq2d ⊢ ( 𝑦 = 0 → ( 𝑥 = - 𝑦 ↔ 𝑥 = 0 ) )
22 eqeq2 ⊢ ( 𝑦 = 0 → ( 𝑥 = 𝑦 ↔ 𝑥 = 0 ) )
23 21 22 bitr4d ⊢ ( 𝑦 = 0 → ( 𝑥 = - 𝑦 ↔ 𝑥 = 𝑦 ) )
24 23 biimpcd ⊢ ( 𝑥 = - 𝑦 → ( 𝑦 = 0 → 𝑥 = 𝑦 ) )
25 24 necon3bd ⊢ ( 𝑥 = - 𝑦 → ( ¬ 𝑥 = 𝑦 → 𝑦 ≠ 0 ) )
26 7 25 syli ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( ¬ 𝑥 = 𝑦 → 𝑦 ≠ 0 ) )
27 3simpc ⊢ ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) → ( 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) )
28 cnpart ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ↔ ¬ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
29 27 28 syl5ib ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) → ¬ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
30 29 impancom ⊢ ( ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) → ( 𝑦 ≠ 0 → ¬ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
31 30 adantl ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( 𝑦 ≠ 0 → ¬ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
32 26 31 syld ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ( ¬ 𝑥 = 𝑦 → ¬ ( 0 ≤ ( ℜ ‘ - 𝑦 ) ∧ ( i · - 𝑦 ) ∉ ℝ+ ) ) )
33 17 32 pm2.65d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → ¬ ¬ 𝑥 = 𝑦 )
34 33 notnotrd ⊢ ( ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ∧ ( 𝑦 ∈ ℂ ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → 𝑥 = 𝑦 )
35 34 an4s ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ∧ ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) ) → 𝑥 = 𝑦 )
36 35 ex ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) → 𝑥 = 𝑦 ) )
37 36 a1i ⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) → 𝑥 = 𝑦 ) ) )
38 37 ralrimivv ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) → 𝑥 = 𝑦 ) )
39 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
40 39 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( 𝑦 ↑ 2 ) = 𝐴 ) )
41 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝑦 ) )
42 41 breq2d ⊢ ( 𝑥 = 𝑦 → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ 𝑦 ) ) )
43 oveq2 ⊢ ( 𝑥 = 𝑦 → ( i · 𝑥 ) = ( i · 𝑦 ) )
44 neleq1 ⊢ ( ( i · 𝑥 ) = ( i · 𝑦 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
45 43 44 syl ⊢ ( 𝑥 = 𝑦 → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
46 40 42 45 3anbi123d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )
47 46 rmo4 ⊢ ( ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℂ ( ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) → 𝑥 = 𝑦 ) )
48 38 47 sylibr ⊢ ( 𝐴 ∈ ℂ → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )