Metamath Proof Explorer


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 syl5bb ( 𝜑 → ( ( ( ℑ ‘ 𝐴 ) = 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 ) ↔ ¬ 𝐴 ∈ ℝ+ ) )