Metamath Proof Explorer

Theorem et-sqrtnegnre

Description: The square root of a negative number is not a real number. (Contributed by Ender Ting, 5-Jan-2025)

Ref Expression
Assertion et-sqrtnegnre ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ¬ ( √ ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 < 0 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
2 id ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
3 0red ⊢ ( 𝐴 ∈ ℝ → 0 ∈ ℝ )
4 2 3 ltnled ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ ¬ 0 ≤ 𝐴 ) )
5 4 biimpd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < 0 → ¬ 0 ≤ 𝐴 ) )
6 5 impcom ⊢ ( ( 𝐴 < 0 ∧ 𝐴 ∈ ℝ ) → ¬ 0 ≤ 𝐴 )
7 1 6 jcnd ⊢ ( ( 𝐴 < 0 ∧ 𝐴 ∈ ℝ ) → ¬ ( 𝐴 ∈ ℝ → 0 ≤ 𝐴 ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ¬ ( 𝐴 ∈ ℝ → 0 ≤ 𝐴 ) )
9 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10 9 sqsqrtd ⊢ ( 𝐴 ∈ ℝ → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 )
11 sqge0 ⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → 0 ≤ ( ( √ ‘ 𝐴 ) ↑ 2 ) )
12 breq2 ⊢ ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 → ( 0 ≤ ( ( √ ‘ 𝐴 ) ↑ 2 ) ↔ 0 ≤ 𝐴 ) )
13 12 biimpd ⊢ ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 → ( 0 ≤ ( ( √ ‘ 𝐴 ) ↑ 2 ) → 0 ≤ 𝐴 ) )
14 10 11 13 syl2imc ⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( 𝐴 ∈ ℝ → 0 ≤ 𝐴 ) )
15 8 14 nsyl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 < 0 ) → ¬ ( √ ‘ 𝐴 ) ∈ ℝ )