Theorem sqrtcvallem1

Description: Two ways of saying a complex number does not lie on the positive real axis. Lemma for sqrtcval . (Contributed by RP, 17-May-2024)

	Ref	Expression
Hypothesis	sqrtcvallem1.1	$$⊢\phi \to A\in ℂ$$
Assertion	sqrtcvallem1	$$⊢\phi \to \left(\left(\Im \left(A\right)=0\to \Re \left(A\right)\le 0\right)\leftrightarrow \neg A\in {ℝ}^{+}\right)$$

Proof

Step	Hyp	Ref	Expression
1		sqrtcvallem1.1	$$⊢\phi \to A\in ℂ$$
2		eldif	$$⊢A\in \left(ℂ\setminus {ℝ}^{+}\right)\leftrightarrow \left(A\in ℂ\wedge \neg A\in {ℝ}^{+}\right)$$
3	2	a1i	$$⊢\phi \to \left(A\in \left(ℂ\setminus {ℝ}^{+}\right)\leftrightarrow \left(A\in ℂ\wedge \neg A\in {ℝ}^{+}\right)\right)$$
4		imor	$$⊢\left(\Im \left(A\right)=0\to \Re \left(A\right)\le 0\right)\leftrightarrow \left(\neg \Im \left(A\right)=0\vee \Re \left(A\right)\le 0\right)$$
5	1	biantrurd	$$⊢\phi \to \left(\neg A\in ℝ\leftrightarrow \left(A\in ℂ\wedge \neg A\in ℝ\right)\right)$$
6		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
7	1 6	syl	$$⊢\phi \to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
8	7	notbid	$$⊢\phi \to \left(\neg A\in ℝ\leftrightarrow \neg \Im \left(A\right)=0\right)$$
9	8	bicomd	$$⊢\phi \to \left(\neg \Im \left(A\right)=0\leftrightarrow \neg A\in ℝ\right)$$
10		eleq1	$$⊢x=A\to \left(x\in ℝ\leftrightarrow A\in ℝ\right)$$
11	10	notbid	$$⊢x=A\to \left(\neg x\in ℝ\leftrightarrow \neg A\in ℝ\right)$$
12	11	elrab	$$⊢A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\leftrightarrow \left(A\in ℂ\wedge \neg A\in ℝ\right)$$
13	12	a1i	$$⊢\phi \to \left(A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\leftrightarrow \left(A\in ℂ\wedge \neg A\in ℝ\right)\right)$$
14	5 9 13	3bitr4d	$$⊢\phi \to \left(\neg \Im \left(A\right)=0\leftrightarrow A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\right)$$
15	1	biantrurd	$$⊢\phi \to \left(\neg 0<\Re \left(A\right)\leftrightarrow \left(A\in ℂ\wedge \neg 0<\Re \left(A\right)\right)\right)$$
16	1	recld	$$⊢\phi \to \Re \left(A\right)\in ℝ$$
17		0red	$$⊢\phi \to 0\in ℝ$$
18	16 17	lenltd	$$⊢\phi \to \left(\Re \left(A\right)\le 0\leftrightarrow \neg 0<\Re \left(A\right)\right)$$
19		fveq2	$$⊢x=A\to \Re \left(x\right)=\Re \left(A\right)$$
20	19	breq2d	$$⊢x=A\to \left(0<\Re \left(x\right)\leftrightarrow 0<\Re \left(A\right)\right)$$
21	20	notbid	$$⊢x=A\to \left(\neg 0<\Re \left(x\right)\leftrightarrow \neg 0<\Re \left(A\right)\right)$$
22	21	elrab	$$⊢A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\leftrightarrow \left(A\in ℂ\wedge \neg 0<\Re \left(A\right)\right)$$
23	22	a1i	$$⊢\phi \to \left(A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\leftrightarrow \left(A\in ℂ\wedge \neg 0<\Re \left(A\right)\right)\right)$$
24	15 18 23	3bitr4d	$$⊢\phi \to \left(\Re \left(A\right)\le 0\leftrightarrow A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)$$
25	14 24	orbi12d	$$⊢\phi \to \left(\left(\neg \Im \left(A\right)=0\vee \Re \left(A\right)\le 0\right)\leftrightarrow \left(A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\vee A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\right)$$
26	4 25	syl5bb	$$⊢\phi \to \left(\left(\Im \left(A\right)=0\to \Re \left(A\right)\le 0\right)\leftrightarrow \left(A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\vee A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\right)$$
27		elun	$$⊢A\in \left(\left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\leftrightarrow \left(A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\vee A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)$$
28	27	a1i	$$⊢\phi \to \left(A\in \left(\left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\leftrightarrow \left(A\in \left\{x\in ℂ|\neg x\in ℝ\right\}\vee A\in \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\right)$$
29		ianor	$$⊢\neg \left(x\in ℝ\wedge 0<\Re \left(x\right)\right)\leftrightarrow \left(\neg x\in ℝ\vee \neg 0<\Re \left(x\right)\right)$$
30	29	bicomi	$$⊢\left(\neg x\in ℝ\vee \neg 0<\Re \left(x\right)\right)\leftrightarrow \neg \left(x\in ℝ\wedge 0<\Re \left(x\right)\right)$$
31		elrp	$$⊢x\in {ℝ}^{+}\leftrightarrow \left(x\in ℝ\wedge 0<x\right)$$
32		rere	$$⊢x\in ℝ\to \Re \left(x\right)=x$$
33	32	breq2d	$$⊢x\in ℝ\to \left(0<\Re \left(x\right)\leftrightarrow 0<x\right)$$
34	33	bicomd	$$⊢x\in ℝ\to \left(0<x\leftrightarrow 0<\Re \left(x\right)\right)$$
35	34	pm5.32i	$$⊢\left(x\in ℝ\wedge 0<x\right)\leftrightarrow \left(x\in ℝ\wedge 0<\Re \left(x\right)\right)$$
36	31 35	bitri	$$⊢x\in {ℝ}^{+}\leftrightarrow \left(x\in ℝ\wedge 0<\Re \left(x\right)\right)$$
37	30 36	xchbinxr	$$⊢\left(\neg x\in ℝ\vee \neg 0<\Re \left(x\right)\right)\leftrightarrow \neg x\in {ℝ}^{+}$$
38	37	rabbii	$$⊢\left\{x\in ℂ|\left(\neg x\in ℝ\vee \neg 0<\Re \left(x\right)\right)\right\}=\left\{x\in ℂ|\neg x\in {ℝ}^{+}\right\}$$
39		unrab	$$⊢\left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}=\left\{x\in ℂ|\left(\neg x\in ℝ\vee \neg 0<\Re \left(x\right)\right)\right\}$$
40		dfdif2	$$⊢ℂ\setminus {ℝ}^{+}=\left\{x\in ℂ|\neg x\in {ℝ}^{+}\right\}$$
41	38 39 40	3eqtr4i	$$⊢\left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}=ℂ\setminus {ℝ}^{+}$$
42	41	a1i	$$⊢\phi \to \left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}=ℂ\setminus {ℝ}^{+}$$
43	42	eleq2d	$$⊢\phi \to \left(A\in \left(\left\{x\in ℂ|\neg x\in ℝ\right\}\cup \left\{x\in ℂ|\neg 0<\Re \left(x\right)\right\}\right)\leftrightarrow A\in \left(ℂ\setminus {ℝ}^{+}\right)\right)$$
44	26 28 43	3bitr2d	$$⊢\phi \to \left(\left(\Im \left(A\right)=0\to \Re \left(A\right)\le 0\right)\leftrightarrow A\in \left(ℂ\setminus {ℝ}^{+}\right)\right)$$
45	1	biantrurd	$$⊢\phi \to \left(\neg A\in {ℝ}^{+}\leftrightarrow \left(A\in ℂ\wedge \neg A\in {ℝ}^{+}\right)\right)$$
46	3 44 45	3bitr4d	$$⊢\phi \to \left(\left(\Im \left(A\right)=0\to \Re \left(A\right)\le 0\right)\leftrightarrow \neg A\in {ℝ}^{+}\right)$$