This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reusq0

Description: A complex number is the square of exactly one complex number iff the given complex number is zero. (Contributed by AV, 21-Jun-2023)

Ref Expression
Assertion reusq0 ( 𝑋 ∈ ℂ → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 ↔ 𝑋 = 0 ) )

Proof

Step Hyp Ref Expression
1 2a1 ⊢ ( 𝑋 = 0 → ( 𝑋 ∈ ℂ → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 → 𝑋 = 0 ) ) )
2 sqrtcl ⊢ ( 𝑋 ∈ ℂ → ( √ ‘ 𝑋 ) ∈ ℂ )
3 2 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ( √ ‘ 𝑋 ) ∈ ℂ )
4 2 negcld ⊢ ( 𝑋 ∈ ℂ → - ( √ ‘ 𝑋 ) ∈ ℂ )
5 4 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → - ( √ ‘ 𝑋 ) ∈ ℂ )
6 2 eqnegd ⊢ ( 𝑋 ∈ ℂ → ( ( √ ‘ 𝑋 ) = - ( √ ‘ 𝑋 ) ↔ ( √ ‘ 𝑋 ) = 0 ) )
7 simpl ⊢ ( ( 𝑋 ∈ ℂ ∧ ( √ ‘ 𝑋 ) = 0 ) → 𝑋 ∈ ℂ )
8 simpr ⊢ ( ( 𝑋 ∈ ℂ ∧ ( √ ‘ 𝑋 ) = 0 ) → ( √ ‘ 𝑋 ) = 0 )
9 7 8 sqr00d ⊢ ( ( 𝑋 ∈ ℂ ∧ ( √ ‘ 𝑋 ) = 0 ) → 𝑋 = 0 )
10 9 ex ⊢ ( 𝑋 ∈ ℂ → ( ( √ ‘ 𝑋 ) = 0 → 𝑋 = 0 ) )
11 6 10 sylbid ⊢ ( 𝑋 ∈ ℂ → ( ( √ ‘ 𝑋 ) = - ( √ ‘ 𝑋 ) → 𝑋 = 0 ) )
12 11 necon3bd ⊢ ( 𝑋 ∈ ℂ → ( ¬ 𝑋 = 0 → ( √ ‘ 𝑋 ) ≠ - ( √ ‘ 𝑋 ) ) )
13 12 imp ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ( √ ‘ 𝑋 ) ≠ - ( √ ‘ 𝑋 ) )
14 3 5 13 3jca ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ( ( √ ‘ 𝑋 ) ∈ ℂ ∧ - ( √ ‘ 𝑋 ) ∈ ℂ ∧ ( √ ‘ 𝑋 ) ≠ - ( √ ‘ 𝑋 ) ) )
15 sqrtth ⊢ ( 𝑋 ∈ ℂ → ( ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 )
16 sqneg ⊢ ( ( √ ‘ 𝑋 ) ∈ ℂ → ( - ( √ ‘ 𝑋 ) ↑ 2 ) = ( ( √ ‘ 𝑋 ) ↑ 2 ) )
17 2 16 syl ⊢ ( 𝑋 ∈ ℂ → ( - ( √ ‘ 𝑋 ) ↑ 2 ) = ( ( √ ‘ 𝑋 ) ↑ 2 ) )
18 17 15 eqtrd ⊢ ( 𝑋 ∈ ℂ → ( - ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 )
19 15 18 jca ⊢ ( 𝑋 ∈ ℂ → ( ( ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ∧ ( - ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ) )
20 19 adantr ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ( ( ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ∧ ( - ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ) )
21 oveq1 ⊢ ( 𝑥 = ( √ ‘ 𝑋 ) → ( 𝑥 ↑ 2 ) = ( ( √ ‘ 𝑋 ) ↑ 2 ) )
22 21 eqeq1d ⊢ ( 𝑥 = ( √ ‘ 𝑋 ) → ( ( 𝑥 ↑ 2 ) = 𝑋 ↔ ( ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ) )
23 oveq1 ⊢ ( 𝑥 = - ( √ ‘ 𝑋 ) → ( 𝑥 ↑ 2 ) = ( - ( √ ‘ 𝑋 ) ↑ 2 ) )
24 23 eqeq1d ⊢ ( 𝑥 = - ( √ ‘ 𝑋 ) → ( ( 𝑥 ↑ 2 ) = 𝑋 ↔ ( - ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ) )
25 22 24 2nreu ⊢ ( ( ( √ ‘ 𝑋 ) ∈ ℂ ∧ - ( √ ‘ 𝑋 ) ∈ ℂ ∧ ( √ ‘ 𝑋 ) ≠ - ( √ ‘ 𝑋 ) ) → ( ( ( ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ∧ ( - ( √ ‘ 𝑋 ) ↑ 2 ) = 𝑋 ) → ¬ ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 ) )
26 14 20 25 sylc ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ¬ ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 )
27 26 pm2.21d ⊢ ( ( 𝑋 ∈ ℂ ∧ ¬ 𝑋 = 0 ) → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 → 𝑋 = 0 ) )
28 27 expcom ⊢ ( ¬ 𝑋 = 0 → ( 𝑋 ∈ ℂ → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 → 𝑋 = 0 ) ) )
29 1 28 pm2.61i ⊢ ( 𝑋 ∈ ℂ → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 → 𝑋 = 0 ) )
30 2nn ⊢ 2 ∈ ℕ
31 0cnd ⊢ ( 2 ∈ ℕ → 0 ∈ ℂ )
32 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ↑ 2 ) = ( 0 ↑ 2 ) )
33 32 eqeq1d ⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 2 ) = 0 ↔ ( 0 ↑ 2 ) = 0 ) )
34 eqeq1 ⊢ ( 𝑥 = 0 → ( 𝑥 = 𝑦 ↔ 0 = 𝑦 ) )
35 34 imbi2d ⊢ ( 𝑥 = 0 → ( ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) ) )
36 35 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) ) )
37 33 36 anbi12d ⊢ ( 𝑥 = 0 → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) ↔ ( ( 0 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) ) ) )
38 37 adantl ⊢ ( ( 2 ∈ ℕ ∧ 𝑥 = 0 ) → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) ↔ ( ( 0 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) ) ) )
39 0exp ⊢ ( 2 ∈ ℕ → ( 0 ↑ 2 ) = 0 )
40 sqeq0 ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 ↑ 2 ) = 0 ↔ 𝑦 = 0 ) )
41 40 biimpd ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 ↑ 2 ) = 0 → 𝑦 = 0 ) )
42 eqcom ⊢ ( 0 = 𝑦 ↔ 𝑦 = 0 )
43 41 42 imbitrrdi ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) )
44 43 adantl ⊢ ( ( 2 ∈ ℕ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) )
45 44 ralrimiva ⊢ ( 2 ∈ ℕ → ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) )
46 39 45 jca ⊢ ( 2 ∈ ℕ → ( ( 0 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 0 = 𝑦 ) ) )
47 31 38 46 rspcedvd ⊢ ( 2 ∈ ℕ → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) )
48 30 47 mp1i ⊢ ( 𝑋 = 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) )
49 eqeq2 ⊢ ( 𝑋 = 0 → ( ( 𝑥 ↑ 2 ) = 𝑋 ↔ ( 𝑥 ↑ 2 ) = 0 ) )
50 eqeq2 ⊢ ( 𝑋 = 0 → ( ( 𝑦 ↑ 2 ) = 𝑋 ↔ ( 𝑦 ↑ 2 ) = 0 ) )
51 50 imbi1d ⊢ ( 𝑋 = 0 → ( ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ↔ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) )
52 51 ralbidv ⊢ ( 𝑋 = 0 → ( ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) )
53 49 52 anbi12d ⊢ ( 𝑋 = 0 → ( ( ( 𝑥 ↑ 2 ) = 𝑋 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ) ↔ ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) ) )
54 53 rexbidv ⊢ ( 𝑋 = 0 → ( ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝑋 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 0 → 𝑥 = 𝑦 ) ) ) )
55 48 54 mpbird ⊢ ( 𝑋 = 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝑋 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ) )
56 55 a1i ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 = 0 → ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝑋 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ) ) )
57 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
58 57 eqeq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) = 𝑋 ↔ ( 𝑦 ↑ 2 ) = 𝑋 ) )
59 58 reu8 ⊢ ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 ↔ ∃ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝑋 ∧ ∀ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑋 → 𝑥 = 𝑦 ) ) )
60 56 59 imbitrrdi ⊢ ( 𝑋 ∈ ℂ → ( 𝑋 = 0 → ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 ) )
61 29 60 impbid ⊢ ( 𝑋 ∈ ℂ → ( ∃! 𝑥 ∈ ℂ ( 𝑥 ↑ 2 ) = 𝑋 ↔ 𝑋 = 0 ) )