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 · ( √ ‘ 𝐴 ) ) ) ∉ ℝ+ ) )