Step | Hyp | Ref
| Expression |
1 | | 2a1 28 |
. . 3
⊢ (𝑋 = 0 → (𝑋 ∈ ℂ → (∃!𝑥 ∈ ℂ (𝑥↑2) = 𝑋 → 𝑋 = 0))) |
2 | | sqrtcl 14925 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
(√‘𝑋) ∈
ℂ) |
3 | 2 | adantr 484 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
(√‘𝑋) ∈
ℂ) |
4 | 2 | negcld 11176 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
-(√‘𝑋) ∈
ℂ) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
-(√‘𝑋) ∈
ℂ) |
6 | 2 | eqnegd 11553 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
((√‘𝑋) =
-(√‘𝑋) ↔
(√‘𝑋) =
0)) |
7 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℂ ∧
(√‘𝑋) = 0)
→ 𝑋 ∈
ℂ) |
8 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ ℂ ∧
(√‘𝑋) = 0)
→ (√‘𝑋) =
0) |
9 | 7, 8 | sqr00d 15005 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℂ ∧
(√‘𝑋) = 0)
→ 𝑋 =
0) |
10 | 9 | ex 416 |
. . . . . . . . . 10
⊢ (𝑋 ∈ ℂ →
((√‘𝑋) = 0
→ 𝑋 =
0)) |
11 | 6, 10 | sylbid 243 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ →
((√‘𝑋) =
-(√‘𝑋) →
𝑋 = 0)) |
12 | 11 | necon3bd 2954 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ → (¬
𝑋 = 0 →
(√‘𝑋) ≠
-(√‘𝑋))) |
13 | 12 | imp 410 |
. . . . . . 7
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
(√‘𝑋) ≠
-(√‘𝑋)) |
14 | 3, 5, 13 | 3jca 1130 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
((√‘𝑋) ∈
ℂ ∧ -(√‘𝑋) ∈ ℂ ∧ (√‘𝑋) ≠ -(√‘𝑋))) |
15 | | sqrtth 14928 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
((√‘𝑋)↑2)
= 𝑋) |
16 | | sqneg 13688 |
. . . . . . . . . 10
⊢
((√‘𝑋)
∈ ℂ → (-(√‘𝑋)↑2) = ((√‘𝑋)↑2)) |
17 | 2, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝑋 ∈ ℂ →
(-(√‘𝑋)↑2)
= ((√‘𝑋)↑2)) |
18 | 17, 15 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑋 ∈ ℂ →
(-(√‘𝑋)↑2)
= 𝑋) |
19 | 15, 18 | jca 515 |
. . . . . . 7
⊢ (𝑋 ∈ ℂ →
(((√‘𝑋)↑2)
= 𝑋 ∧
(-(√‘𝑋)↑2)
= 𝑋)) |
20 | 19 | adantr 484 |
. . . . . 6
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
(((√‘𝑋)↑2)
= 𝑋 ∧
(-(√‘𝑋)↑2)
= 𝑋)) |
21 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = (√‘𝑋) → (𝑥↑2) = ((√‘𝑋)↑2)) |
22 | 21 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = (√‘𝑋) → ((𝑥↑2) = 𝑋 ↔ ((√‘𝑋)↑2) = 𝑋)) |
23 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑥 = -(√‘𝑋) → (𝑥↑2) = (-(√‘𝑋)↑2)) |
24 | 23 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑥 = -(√‘𝑋) → ((𝑥↑2) = 𝑋 ↔ (-(√‘𝑋)↑2) = 𝑋)) |
25 | 22, 24 | 2nreu 4356 |
. . . . . 6
⊢
(((√‘𝑋)
∈ ℂ ∧ -(√‘𝑋) ∈ ℂ ∧ (√‘𝑋) ≠ -(√‘𝑋)) →
((((√‘𝑋)↑2) = 𝑋 ∧ (-(√‘𝑋)↑2) = 𝑋) → ¬ ∃!𝑥 ∈ ℂ (𝑥↑2) = 𝑋)) |
26 | 14, 20, 25 | sylc 65 |
. . . . 5
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) → ¬
∃!𝑥 ∈ ℂ
(𝑥↑2) = 𝑋) |
27 | 26 | pm2.21d 121 |
. . . 4
⊢ ((𝑋 ∈ ℂ ∧ ¬
𝑋 = 0) →
(∃!𝑥 ∈ ℂ
(𝑥↑2) = 𝑋 → 𝑋 = 0)) |
28 | 27 | expcom 417 |
. . 3
⊢ (¬
𝑋 = 0 → (𝑋 ∈ ℂ →
(∃!𝑥 ∈ ℂ
(𝑥↑2) = 𝑋 → 𝑋 = 0))) |
29 | 1, 28 | pm2.61i 185 |
. 2
⊢ (𝑋 ∈ ℂ →
(∃!𝑥 ∈ ℂ
(𝑥↑2) = 𝑋 → 𝑋 = 0)) |
30 | | 2nn 11903 |
. . . . . 6
⊢ 2 ∈
ℕ |
31 | | 0cnd 10826 |
. . . . . . 7
⊢ (2 ∈
ℕ → 0 ∈ ℂ) |
32 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝑥↑2) = (0↑2)) |
33 | 32 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑥 = 0 → ((𝑥↑2) = 0 ↔ (0↑2) =
0)) |
34 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝑥 = 𝑦 ↔ 0 = 𝑦)) |
35 | 34 | imbi2d 344 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (((𝑦↑2) = 0 → 𝑥 = 𝑦) ↔ ((𝑦↑2) = 0 → 0 = 𝑦))) |
36 | 35 | ralbidv 3118 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 0 = 𝑦))) |
37 | 33, 36 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑥 = 0 → (((𝑥↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦)) ↔ ((0↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 0 = 𝑦)))) |
38 | 37 | adantl 485 |
. . . . . . 7
⊢ ((2
∈ ℕ ∧ 𝑥 = 0)
→ (((𝑥↑2) = 0
∧ ∀𝑦 ∈
ℂ ((𝑦↑2) = 0
→ 𝑥 = 𝑦)) ↔ ((0↑2) = 0 ∧
∀𝑦 ∈ ℂ
((𝑦↑2) = 0 → 0 =
𝑦)))) |
39 | | 0exp 13670 |
. . . . . . . 8
⊢ (2 ∈
ℕ → (0↑2) = 0) |
40 | | sqeq0 13692 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℂ → ((𝑦↑2) = 0 ↔ 𝑦 = 0)) |
41 | 40 | biimpd 232 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℂ → ((𝑦↑2) = 0 → 𝑦 = 0)) |
42 | | eqcom 2744 |
. . . . . . . . . . 11
⊢ (0 =
𝑦 ↔ 𝑦 = 0) |
43 | 41, 42 | syl6ibr 255 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℂ → ((𝑦↑2) = 0 → 0 = 𝑦)) |
44 | 43 | adantl 485 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑦
∈ ℂ) → ((𝑦↑2) = 0 → 0 = 𝑦)) |
45 | 44 | ralrimiva 3105 |
. . . . . . . 8
⊢ (2 ∈
ℕ → ∀𝑦
∈ ℂ ((𝑦↑2)
= 0 → 0 = 𝑦)) |
46 | 39, 45 | jca 515 |
. . . . . . 7
⊢ (2 ∈
ℕ → ((0↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 0 = 𝑦))) |
47 | 31, 38, 46 | rspcedvd 3540 |
. . . . . 6
⊢ (2 ∈
ℕ → ∃𝑥
∈ ℂ ((𝑥↑2)
= 0 ∧ ∀𝑦 ∈
ℂ ((𝑦↑2) = 0
→ 𝑥 = 𝑦))) |
48 | 30, 47 | mp1i 13 |
. . . . 5
⊢ (𝑋 = 0 → ∃𝑥 ∈ ℂ ((𝑥↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦))) |
49 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑋 = 0 → ((𝑥↑2) = 𝑋 ↔ (𝑥↑2) = 0)) |
50 | | eqeq2 2749 |
. . . . . . . . 9
⊢ (𝑋 = 0 → ((𝑦↑2) = 𝑋 ↔ (𝑦↑2) = 0)) |
51 | 50 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑋 = 0 → (((𝑦↑2) = 𝑋 → 𝑥 = 𝑦) ↔ ((𝑦↑2) = 0 → 𝑥 = 𝑦))) |
52 | 51 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑋 = 0 → (∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦))) |
53 | 49, 52 | anbi12d 634 |
. . . . . 6
⊢ (𝑋 = 0 → (((𝑥↑2) = 𝑋 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦)) ↔ ((𝑥↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦)))) |
54 | 53 | rexbidv 3216 |
. . . . 5
⊢ (𝑋 = 0 → (∃𝑥 ∈ ℂ ((𝑥↑2) = 𝑋 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦)) ↔ ∃𝑥 ∈ ℂ ((𝑥↑2) = 0 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 0 → 𝑥 = 𝑦)))) |
55 | 48, 54 | mpbird 260 |
. . . 4
⊢ (𝑋 = 0 → ∃𝑥 ∈ ℂ ((𝑥↑2) = 𝑋 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦))) |
56 | 55 | a1i 11 |
. . 3
⊢ (𝑋 ∈ ℂ → (𝑋 = 0 → ∃𝑥 ∈ ℂ ((𝑥↑2) = 𝑋 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦)))) |
57 | | oveq1 7220 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
58 | 57 | eqeq1d 2739 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝑥↑2) = 𝑋 ↔ (𝑦↑2) = 𝑋)) |
59 | 58 | reu8 3646 |
. . 3
⊢
(∃!𝑥 ∈
ℂ (𝑥↑2) = 𝑋 ↔ ∃𝑥 ∈ ℂ ((𝑥↑2) = 𝑋 ∧ ∀𝑦 ∈ ℂ ((𝑦↑2) = 𝑋 → 𝑥 = 𝑦))) |
60 | 56, 59 | syl6ibr 255 |
. 2
⊢ (𝑋 ∈ ℂ → (𝑋 = 0 → ∃!𝑥 ∈ ℂ (𝑥↑2) = 𝑋)) |
61 | 29, 60 | impbid 215 |
1
⊢ (𝑋 ∈ ℂ →
(∃!𝑥 ∈ ℂ
(𝑥↑2) = 𝑋 ↔ 𝑋 = 0)) |