| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simplr1 1215 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑥↑2) = 𝐴) | 
| 2 |  | simprr1 1221 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑦↑2) = 𝐴) | 
| 3 | 1, 2 | eqtr4d 2779 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑥↑2) = (𝑦↑2)) | 
| 4 |  | sqeqor 14256 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝑥↑2) = (𝑦↑2) ↔ (𝑥 = 𝑦 ∨ 𝑥 = -𝑦))) | 
| 5 | 4 | ad2ant2r 747 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → ((𝑥↑2) = (𝑦↑2) ↔ (𝑥 = 𝑦 ∨ 𝑥 = -𝑦))) | 
| 6 | 3, 5 | mpbid 232 | . . . . . . . . . 10
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑥 = 𝑦 ∨ 𝑥 = -𝑦)) | 
| 7 | 6 | ord 864 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (¬ 𝑥 = 𝑦 → 𝑥 = -𝑦)) | 
| 8 |  | 3simpc 1150 | . . . . . . . . . . 11
⊢ (((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
→ (0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉
ℝ+)) | 
| 9 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑥 = -𝑦 → (ℜ‘𝑥) = (ℜ‘-𝑦)) | 
| 10 | 9 | breq2d 5154 | . . . . . . . . . . . 12
⊢ (𝑥 = -𝑦 → (0 ≤ (ℜ‘𝑥) ↔ 0 ≤
(ℜ‘-𝑦))) | 
| 11 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑥 = -𝑦 → (i · 𝑥) = (i · -𝑦)) | 
| 12 |  | neleq1 3051 | . . . . . . . . . . . . 13
⊢ ((i
· 𝑥) = (i ·
-𝑦) → ((i ·
𝑥) ∉
ℝ+ ↔ (i · -𝑦) ∉
ℝ+)) | 
| 13 | 11, 12 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑥 = -𝑦 → ((i · 𝑥) ∉ ℝ+ ↔ (i
· -𝑦) ∉
ℝ+)) | 
| 14 | 10, 13 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑥 = -𝑦 → ((0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
↔ (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 15 | 8, 14 | syl5ibcom 245 | . . . . . . . . . 10
⊢ (((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
→ (𝑥 = -𝑦 → (0 ≤
(ℜ‘-𝑦) ∧ (i
· -𝑦) ∉
ℝ+))) | 
| 16 | 15 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑥 = -𝑦 → (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 17 | 7, 16 | syld 47 | . . . . . . . 8
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (¬ 𝑥 = 𝑦 → (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 18 |  | negeq 11501 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 0 → -𝑦 = -0) | 
| 19 |  | neg0 11556 | . . . . . . . . . . . . . . 15
⊢ -0 =
0 | 
| 20 | 18, 19 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 0 → -𝑦 = 0) | 
| 21 | 20 | eqeq2d 2747 | . . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑥 = -𝑦 ↔ 𝑥 = 0)) | 
| 22 |  | eqeq2 2748 | . . . . . . . . . . . . 13
⊢ (𝑦 = 0 → (𝑥 = 𝑦 ↔ 𝑥 = 0)) | 
| 23 | 21, 22 | bitr4d 282 | . . . . . . . . . . . 12
⊢ (𝑦 = 0 → (𝑥 = -𝑦 ↔ 𝑥 = 𝑦)) | 
| 24 | 23 | biimpcd 249 | . . . . . . . . . . 11
⊢ (𝑥 = -𝑦 → (𝑦 = 0 → 𝑥 = 𝑦)) | 
| 25 | 24 | necon3bd 2953 | . . . . . . . . . 10
⊢ (𝑥 = -𝑦 → (¬ 𝑥 = 𝑦 → 𝑦 ≠ 0)) | 
| 26 | 7, 25 | syli 39 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (¬ 𝑥 = 𝑦 → 𝑦 ≠ 0)) | 
| 27 |  | 3simpc 1150 | . . . . . . . . . . . 12
⊢ (((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
→ (0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉
ℝ+)) | 
| 28 |  | cnpart 15280 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → ((0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+) ↔ ¬ (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 29 | 27, 28 | imbitrid 244 | . . . . . . . . . . 11
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
→ ¬ (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 30 | 29 | impancom 451 | . . . . . . . . . 10
⊢ ((𝑦 ∈ ℂ ∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
→ (𝑦 ≠ 0 →
¬ (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 31 | 30 | adantl 481 | . . . . . . . . 9
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (𝑦 ≠ 0 → ¬ (0 ≤
(ℜ‘-𝑦) ∧ (i
· -𝑦) ∉
ℝ+))) | 
| 32 | 26, 31 | syld 47 | . . . . . . . 8
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → (¬ 𝑥 = 𝑦 → ¬ (0 ≤ (ℜ‘-𝑦) ∧ (i · -𝑦) ∉
ℝ+))) | 
| 33 | 17, 32 | pm2.65d 196 | . . . . . . 7
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → ¬ ¬ 𝑥 = 𝑦) | 
| 34 | 33 | notnotrd 133 | . . . . . 6
⊢ (((𝑥 ∈ ℂ ∧ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
∧ (𝑦 ∈ ℂ
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → 𝑥 = 𝑦) | 
| 35 | 34 | an4s 660 | . . . . 5
⊢ (((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) ∧ (((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) → 𝑥 = 𝑦) | 
| 36 | 35 | ex 412 | . . . 4
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+) ∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
→ 𝑥 = 𝑦)) | 
| 37 | 36 | a1i 11 | . . 3
⊢ (𝐴 ∈ ℂ → ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) →
((((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+) ∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
→ 𝑥 = 𝑦))) | 
| 38 | 37 | ralrimivv 3199 | . 2
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ ℂ
∀𝑦 ∈ ℂ
((((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+) ∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
→ 𝑥 = 𝑦)) | 
| 39 |  | oveq1 7439 | . . . . 5
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) | 
| 40 | 39 | eqeq1d 2738 | . . . 4
⊢ (𝑥 = 𝑦 → ((𝑥↑2) = 𝐴 ↔ (𝑦↑2) = 𝐴)) | 
| 41 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = 𝑦 → (ℜ‘𝑥) = (ℜ‘𝑦)) | 
| 42 | 41 | breq2d 5154 | . . . 4
⊢ (𝑥 = 𝑦 → (0 ≤ (ℜ‘𝑥) ↔ 0 ≤
(ℜ‘𝑦))) | 
| 43 |  | oveq2 7440 | . . . . 5
⊢ (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦)) | 
| 44 |  | neleq1 3051 | . . . . 5
⊢ ((i
· 𝑥) = (i ·
𝑦) → ((i ·
𝑥) ∉
ℝ+ ↔ (i · 𝑦) ∉
ℝ+)) | 
| 45 | 43, 44 | syl 17 | . . . 4
⊢ (𝑥 = 𝑦 → ((i · 𝑥) ∉ ℝ+ ↔ (i
· 𝑦) ∉
ℝ+)) | 
| 46 | 40, 42, 45 | 3anbi123d 1437 | . . 3
⊢ (𝑥 = 𝑦 → (((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
↔ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) | 
| 47 | 46 | rmo4 3735 | . 2
⊢
(∃*𝑥 ∈
ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+) ↔ ∀𝑥 ∈ ℂ ∀𝑦 ∈ ℂ ((((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
∧ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+)) → 𝑥 = 𝑦)) | 
| 48 | 38, 47 | sylibr 234 | 1
⊢ (𝐴 ∈ ℂ →
∃*𝑥 ∈ ℂ
((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+)) |