Theorem sqrtnegnre

Description: The square root of a negative number is not a real number. (Contributed by AV, 28-Feb-2023)

	Ref	Expression
Assertion	sqrtnegnre	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{X}\notin ℝ$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢X\in ℝ\to X\in ℂ$$
2	1	negnegd	$$⊢X\in ℝ\to -\left(-X\right)=X$$
3	2	adantr	$$⊢\left(X\in ℝ\wedge X<0\right)\to -\left(-X\right)=X$$
4	3	eqcomd	$$⊢\left(X\in ℝ\wedge X<0\right)\to X=-\left(-X\right)$$
5	4	fveq2d	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{X}=\sqrt{-\left(-X\right)}$$
6		simpl	$$⊢\left(X\in ℝ\wedge X<0\right)\to X\in ℝ$$
7	6	renegcld	$$⊢\left(X\in ℝ\wedge X<0\right)\to -X\in ℝ$$
8		0re	$$⊢0\in ℝ$$
9		ltle	$$⊢\left(X\in ℝ\wedge 0\in ℝ\right)\to \left(X<0\to X\le 0\right)$$
10	8 9	mpan2	$$⊢X\in ℝ\to \left(X<0\to X\le 0\right)$$
11	10	imp	$$⊢\left(X\in ℝ\wedge X<0\right)\to X\le 0$$
12		le0neg1	$$⊢X\in ℝ\to \left(X\le 0\leftrightarrow 0\le -X\right)$$
13	12	adantr	$$⊢\left(X\in ℝ\wedge X<0\right)\to \left(X\le 0\leftrightarrow 0\le -X\right)$$
14	11 13	mpbid	$$⊢\left(X\in ℝ\wedge X<0\right)\to 0\le -X$$
15	7 14	sqrtnegd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{-\left(-X\right)}=\mathrm{i}\sqrt{-X}$$
16	5 15	eqtrd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{X}=\mathrm{i}\sqrt{-X}$$
17		ax-icn	$$⊢\mathrm{i}\in ℂ$$
18	17	a1i	$$⊢\left(X\in ℝ\wedge X<0\right)\to \mathrm{i}\in ℂ$$
19	1	adantr	$$⊢\left(X\in ℝ\wedge X<0\right)\to X\in ℂ$$
20	19	negcld	$$⊢\left(X\in ℝ\wedge X<0\right)\to -X\in ℂ$$
21	20	sqrtcld	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{-X}\in ℂ$$
22	18 21	mulcomd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \mathrm{i}\sqrt{-X}=\sqrt{-X}\mathrm{i}$$
23	7 14	resqrtcld	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{-X}\in ℝ$$
24		inelr	$$⊢\neg \mathrm{i}\in ℝ$$
25	24	a1i	$$⊢\left(X\in ℝ\wedge X<0\right)\to \neg \mathrm{i}\in ℝ$$
26	18 25	eldifd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \mathrm{i}\in \left(ℂ\setminus ℝ\right)$$
27		lt0neg1	$$⊢X\in ℝ\to \left(X<0\leftrightarrow 0<-X\right)$$
28	8	a1i	$$⊢X\in ℝ\to 0\in ℝ$$
29		ltne	$$⊢\left(0\in ℝ\wedge 0<-X\right)\to -X\ne 0$$
30	28 29	sylan	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to -X\ne 0$$
31		simpl	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to X\in ℝ$$
32	31	renegcld	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to -X\in ℝ$$
33	10 27 12	3imtr3d	$$⊢X\in ℝ\to \left(0<-X\to 0\le -X\right)$$
34	33	imp	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to 0\le -X$$
35		sqrt00	$$⊢\left(-X\in ℝ\wedge 0\le -X\right)\to \left(\sqrt{-X}=0\leftrightarrow -X=0\right)$$
36	32 34 35	syl2anc	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to \left(\sqrt{-X}=0\leftrightarrow -X=0\right)$$
37	36	bicomd	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to \left(-X=0\leftrightarrow \sqrt{-X}=0\right)$$
38	37	necon3bid	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to \left(-X\ne 0\leftrightarrow \sqrt{-X}\ne 0\right)$$
39	30 38	mpbid	$$⊢\left(X\in ℝ\wedge 0<-X\right)\to \sqrt{-X}\ne 0$$
40	39	ex	$$⊢X\in ℝ\to \left(0<-X\to \sqrt{-X}\ne 0\right)$$
41	27 40	sylbid	$$⊢X\in ℝ\to \left(X<0\to \sqrt{-X}\ne 0\right)$$
42	41	imp	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{-X}\ne 0$$
43	23 26 42	recnmulnred	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{-X}\mathrm{i}\notin ℝ$$
44		df-nel	$$⊢\sqrt{-X}\mathrm{i}\notin ℝ\leftrightarrow \neg \sqrt{-X}\mathrm{i}\in ℝ$$
45	43 44	sylib	$$⊢\left(X\in ℝ\wedge X<0\right)\to \neg \sqrt{-X}\mathrm{i}\in ℝ$$
46	22 45	eqneltrd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \neg \mathrm{i}\sqrt{-X}\in ℝ$$
47	16 46	eqneltrd	$$⊢\left(X\in ℝ\wedge X<0\right)\to \neg \sqrt{X}\in ℝ$$
48		df-nel	$$⊢\sqrt{X}\notin ℝ\leftrightarrow \neg \sqrt{X}\in ℝ$$
49	47 48	sylibr	$$⊢\left(X\in ℝ\wedge X<0\right)\to \sqrt{X}\notin ℝ$$