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	$$⊢\left(A\in ℝ\wedge A<0\right)\to \neg \sqrt{A}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A<0\wedge A\in ℝ\right)\to A\in ℝ$$
2		id	$$⊢A\in ℝ\to A\in ℝ$$
3		0red	$$⊢A\in ℝ\to 0\in ℝ$$
4	2 3	ltnled	$$⊢A\in ℝ\to \left(A<0\leftrightarrow \neg 0\le A\right)$$
5	4	biimpd	$$⊢A\in ℝ\to \left(A<0\to \neg 0\le A\right)$$
6	5	impcom	$$⊢\left(A<0\wedge A\in ℝ\right)\to \neg 0\le A$$
7	1 6	jcnd	$$⊢\left(A<0\wedge A\in ℝ\right)\to \neg \left(A\in ℝ\to 0\le A\right)$$
8	7	ancoms	$$⊢\left(A\in ℝ\wedge A<0\right)\to \neg \left(A\in ℝ\to 0\le A\right)$$
9		recn	$$⊢A\in ℝ\to A\in ℂ$$
10	9	sqsqrtd	$$⊢A\in ℝ\to {\sqrt{A}}^2=A$$
11		sqge0	$$⊢\sqrt{A}\in ℝ\to 0\le {\sqrt{A}}^2$$
12		breq2	$$⊢{\sqrt{A}}^2=A\to \left(0\le {\sqrt{A}}^2\leftrightarrow 0\le A\right)$$
13	12	biimpd	$$⊢{\sqrt{A}}^2=A\to \left(0\le {\sqrt{A}}^2\to 0\le A\right)$$
14	10 11 13	syl2imc	$$⊢\sqrt{A}\in ℝ\to \left(A\in ℝ\to 0\le A\right)$$
15	8 14	nsyl	$$⊢\left(A\in ℝ\wedge A<0\right)\to \neg \sqrt{A}\in ℝ$$