Metamath Proof Explorer


Theorem sqrtneglem

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrtneglem ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )

Proof

Step Hyp Ref Expression
1 ax-icn i ∈ ℂ
2 resqrtcl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )
3 recn ( ( √ ‘ 𝐴 ) ∈ ℝ → ( √ ‘ 𝐴 ) ∈ ℂ )
4 2 3 syl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℂ )
5 sqmul ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) )
6 1 4 5 sylancr ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) )
7 i2 ( i ↑ 2 ) = - 1
8 7 a1i ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i ↑ 2 ) = - 1 )
9 resqrtth ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
10 8 9 oveq12d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i ↑ 2 ) · ( ( √ ‘ 𝐴 ) ↑ 2 ) ) = ( - 1 · 𝐴 ) )
11 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
12 11 adantr ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
13 12 mulm1d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - 1 · 𝐴 ) = - 𝐴 )
14 6 10 13 3eqtrd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 )
15 renegcl ( ( √ ‘ 𝐴 ) ∈ ℝ → - ( √ ‘ 𝐴 ) ∈ ℝ )
16 0re 0 ∈ ℝ
17 reim0 ( - ( √ ‘ 𝐴 ) ∈ ℝ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = 0 )
18 recn ( - ( √ ‘ 𝐴 ) ∈ ℝ → - ( √ ‘ 𝐴 ) ∈ ℂ )
19 imre ( - ( √ ‘ 𝐴 ) ∈ ℂ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
20 18 19 syl ( - ( √ ‘ 𝐴 ) ∈ ℝ → ( ℑ ‘ - ( √ ‘ 𝐴 ) ) = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
21 17 20 eqtr3d ( - ( √ ‘ 𝐴 ) ∈ ℝ → 0 = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
22 eqle ( ( 0 ∈ ℝ ∧ 0 = ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) ) → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
23 16 21 22 sylancr ( - ( √ ‘ 𝐴 ) ∈ ℝ → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
24 2 15 23 3syl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) )
25 mul2neg ( ( i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( - i · - ( √ ‘ 𝐴 ) ) = ( i · ( √ ‘ 𝐴 ) ) )
26 1 4 25 sylancr ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - i · - ( √ ‘ 𝐴 ) ) = ( i · ( √ ‘ 𝐴 ) ) )
27 26 fveq2d ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ℜ ‘ ( - i · - ( √ ‘ 𝐴 ) ) ) = ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) )
28 24 27 breqtrd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) )
29 ixi ( i · i ) = - 1
30 29 oveq1i ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( - 1 · ( √ ‘ 𝐴 ) )
31 mulass ( ( i ∈ ℂ ∧ i ∈ ℂ ∧ ( √ ‘ 𝐴 ) ∈ ℂ ) → ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) )
32 1 1 31 mp3an12 ( ( √ ‘ 𝐴 ) ∈ ℂ → ( ( i · i ) · ( √ ‘ 𝐴 ) ) = ( i · ( i · ( √ ‘ 𝐴 ) ) ) )
33 mulm1 ( ( √ ‘ 𝐴 ) ∈ ℂ → ( - 1 · ( √ ‘ 𝐴 ) ) = - ( √ ‘ 𝐴 ) )
34 30 32 33 3eqtr3a ( ( √ ‘ 𝐴 ) ∈ ℂ → ( i · ( i · ( √ ‘ 𝐴 ) ) ) = - ( √ ‘ 𝐴 ) )
35 4 34 syl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i · ( i · ( √ ‘ 𝐴 ) ) ) = - ( √ ‘ 𝐴 ) )
36 sqrtge0 ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) )
37 le0neg2 ( ( √ ‘ 𝐴 ) ∈ ℝ → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ - ( √ ‘ 𝐴 ) ≤ 0 ) )
38 lenlt ( ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( - ( √ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) )
39 15 16 38 sylancl ( ( √ ‘ 𝐴 ) ∈ ℝ → ( - ( √ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) )
40 37 39 bitrd ( ( √ ‘ 𝐴 ) ∈ ℝ → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) )
41 2 40 syl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 ≤ ( √ ‘ 𝐴 ) ↔ ¬ 0 < - ( √ ‘ 𝐴 ) ) )
42 36 41 mpbid ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ 0 < - ( √ ‘ 𝐴 ) )
43 elrp ( - ( √ ‘ 𝐴 ) ∈ ℝ+ ↔ ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( √ ‘ 𝐴 ) ) )
44 2 15 syl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → - ( √ ‘ 𝐴 ) ∈ ℝ )
45 44 biantrurd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 0 < - ( √ ‘ 𝐴 ) ↔ ( - ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 < - ( √ ‘ 𝐴 ) ) ) )
46 43 45 bitr4id ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( - ( √ ‘ 𝐴 ) ∈ ℝ+ ↔ 0 < - ( √ ‘ 𝐴 ) ) )
47 42 46 mtbird ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ - ( √ ‘ 𝐴 ) ∈ ℝ+ )
48 35 47 eqneltrd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ¬ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∈ ℝ+ )
49 df-nel ( ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ↔ ¬ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∈ ℝ+ )
50 48 49 sylibr ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ )
51 14 28 50 3jca ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( ( i · ( √ ‘ 𝐴 ) ) ↑ 2 ) = - 𝐴 ∧ 0 ≤ ( ℜ ‘ ( i · ( √ ‘ 𝐴 ) ) ) ∧ ( i · ( i · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )