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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
Assertion	sqrtcvallem1	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ¬ 𝐴 ∈ ℝ+ ) )

Proof

Step	Hyp	Ref	Expression
1		sqrtcvallem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		eldif	⊢ ( 𝐴 ∈ ( ℂ ∖ ℝ+ ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) )
3	2	a1i	⊢ ( 𝜑 → ( 𝐴 ∈ ( ℂ ∖ ℝ+ ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) ) )
4		imor	⊢ ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( ¬ ( ℑ ‘ 𝐴 ) = 0 ∨ ( ℜ ‘ 𝐴 ) ≤ 0 ) )
5	1	biantrurd	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) ) )
6		reim0b	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
7	1 6	syl	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
8	7	notbid	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ ↔ ¬ ( ℑ ‘ 𝐴 ) = 0 ) )
9	8	bicomd	⊢ ( 𝜑 → ( ¬ ( ℑ ‘ 𝐴 ) = 0 ↔ ¬ 𝐴 ∈ ℝ ) )
10		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ ℝ ↔ 𝐴 ∈ ℝ ) )
11	10	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 ∈ ℝ ↔ ¬ 𝐴 ∈ ℝ ) )
12	11	elrab	⊢ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) )
13	12	a1i	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ ) ) )
14	5 9 13	3bitr4d	⊢ ( 𝜑 → ( ¬ ( ℑ ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ) )
15	1	biantrurd	⊢ ( 𝜑 → ( ¬ 0 < ( ℜ ‘ 𝐴 ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) )
16	1	recld	⊢ ( 𝜑 → ( ℜ ‘ 𝐴 ) ∈ ℝ )
17		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
18	16 17	lenltd	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ ¬ 0 < ( ℜ ‘ 𝐴 ) ) )
19		fveq2	⊢ ( 𝑥 = 𝐴 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝐴 ) )
20	19	breq2d	⊢ ( 𝑥 = 𝐴 → ( 0 < ( ℜ ‘ 𝑥 ) ↔ 0 < ( ℜ ‘ 𝐴 ) ) )
21	20	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ 0 < ( ℜ ‘ 𝑥 ) ↔ ¬ 0 < ( ℜ ‘ 𝐴 ) ) )
22	21	elrab	⊢ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) )
23	22	a1i	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ↔ ( 𝐴 ∈ ℂ ∧ ¬ 0 < ( ℜ ‘ 𝐴 ) ) ) )
24	15 18 23	3bitr4d	⊢ ( 𝜑 → ( ( ℜ ‘ 𝐴 ) ≤ 0 ↔ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) )
25	14 24	orbi12d	⊢ ( 𝜑 → ( ( ¬ ( ℑ ‘ 𝐴 ) = 0 ∨ ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) )
26	4 25	bitrid	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) )
27		elun	⊢ ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) )
28	27	a1i	⊢ ( 𝜑 → ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ ( 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∨ 𝐴 ∈ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ) )
29		ianor	⊢ ( ¬ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) )
30	29	bicomi	⊢ ( ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ¬ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) )
31		elrp	⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
32		rere	⊢ ( 𝑥 ∈ ℝ → ( ℜ ‘ 𝑥 ) = 𝑥 )
33	32	breq2d	⊢ ( 𝑥 ∈ ℝ → ( 0 < ( ℜ ‘ 𝑥 ) ↔ 0 < 𝑥 ) )
34	33	bicomd	⊢ ( 𝑥 ∈ ℝ → ( 0 < 𝑥 ↔ 0 < ( ℜ ‘ 𝑥 ) ) )
35	34	pm5.32i	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) )
36	31 35	bitri	⊢ ( 𝑥 ∈ ℝ+ ↔ ( 𝑥 ∈ ℝ ∧ 0 < ( ℜ ‘ 𝑥 ) ) )
37	30 36	xchbinxr	⊢ ( ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) ↔ ¬ 𝑥 ∈ ℝ+ )
38	37	rabbii	⊢ { 𝑥 ∈ ℂ ∣ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) } = { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ+ }
39		unrab	⊢ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = { 𝑥 ∈ ℂ ∣ ( ¬ 𝑥 ∈ ℝ ∨ ¬ 0 < ( ℜ ‘ 𝑥 ) ) }
40		dfdif2	⊢ ( ℂ ∖ ℝ+ ) = { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ+ }
41	38 39 40	3eqtr4i	⊢ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = ( ℂ ∖ ℝ+ )
42	41	a1i	⊢ ( 𝜑 → ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) = ( ℂ ∖ ℝ+ ) )
43	42	eleq2d	⊢ ( 𝜑 → ( 𝐴 ∈ ( { 𝑥 ∈ ℂ ∣ ¬ 𝑥 ∈ ℝ } ∪ { 𝑥 ∈ ℂ ∣ ¬ 0 < ( ℜ ‘ 𝑥 ) } ) ↔ 𝐴 ∈ ( ℂ ∖ ℝ+ ) ) )
44	26 28 43	3bitr2d	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ 𝐴 ∈ ( ℂ ∖ ℝ+ ) ) )
45	1	biantrurd	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ℝ+ ) ) )
46	3 44 45	3bitr4d	⊢ ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 0 → ( ℜ ‘ 𝐴 ) ≤ 0 ) ↔ ¬ 𝐴 ∈ ℝ+ ) )