This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atans2

Description: It suffices to show that 1 -i A and 1 + i A are in the continuity domain of log to show that A is in the continuity domain of arctangent. (Contributed by Mario Carneiro, 7-Apr-2015)

Ref Expression
Hypotheses atansopn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
atansopn.s ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
Assertion atans2 ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 atansopn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 atansopn.s ⊢ 𝑆 = { 𝑦 ∈ ℂ ∣ ( 1 + ( 𝑦 ↑ 2 ) ) ∈ 𝐷 }
3 sqcl ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
5 4 sqsqrtd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( √ ‘ ( 𝐴 ↑ 2 ) ) ↑ 2 ) = ( 𝐴 ↑ 2 ) )
6 5 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 ↑ 2 ) = ( ( √ ‘ ( 𝐴 ↑ 2 ) ) ↑ 2 ) )
7 4 sqrtcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℂ )
8 sqeqor ⊢ ( ( 𝐴 ∈ ℂ ∧ ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) = ( ( √ ‘ ( 𝐴 ↑ 2 ) ) ↑ 2 ) ↔ ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) ∨ 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
9 7 8 syldan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 𝐴 ↑ 2 ) = ( ( √ ‘ ( 𝐴 ↑ 2 ) ) ↑ 2 ) ↔ ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) ∨ 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
10 6 9 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) ∨ 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
11 1re ⊢ 1 ∈ ℝ
12 11 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 1 ∈ ℝ )
13 4 negnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → - - ( 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
14 13 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ - - ( 𝐴 ↑ 2 ) ) = ( √ ‘ ( 𝐴 ↑ 2 ) ) )
15 ax-1cn ⊢ 1 ∈ ℂ
16 pncan2 ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) − 1 ) = ( 𝐴 ↑ 2 ) )
17 15 4 16 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) − 1 ) = ( 𝐴 ↑ 2 ) )
18 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) )
19 mnfxr ⊢ -∞ ∈ ℝ*
20 0re ⊢ 0 ∈ ℝ
21 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( 𝐴 ↑ 2 ) ) ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≤ 0 ) ) )
22 19 20 21 mp2an ⊢ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( 𝐴 ↑ 2 ) ) ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≤ 0 ) )
23 18 22 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( 𝐴 ↑ 2 ) ) ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ≤ 0 ) )
24 23 simp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℝ )
25 resubcl ⊢ ( ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) − 1 ) ∈ ℝ )
26 24 11 25 sylancl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( 𝐴 ↑ 2 ) ) − 1 ) ∈ ℝ )
27 17 26 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
28 27 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → - ( 𝐴 ↑ 2 ) ∈ ℝ )
29 0red ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ )
30 0le1 ⊢ 0 ≤ 1
31 30 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ≤ 1 )
32 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 − - ( 𝐴 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
33 15 4 32 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − - ( 𝐴 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
34 23 simp3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( 𝐴 ↑ 2 ) ) ≤ 0 )
35 33 34 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − - ( 𝐴 ↑ 2 ) ) ≤ 0 )
36 suble0 ⊢ ( ( 1 ∈ ℝ ∧ - ( 𝐴 ↑ 2 ) ∈ ℝ ) → ( ( 1 − - ( 𝐴 ↑ 2 ) ) ≤ 0 ↔ 1 ≤ - ( 𝐴 ↑ 2 ) ) )
37 11 28 36 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 − - ( 𝐴 ↑ 2 ) ) ≤ 0 ↔ 1 ≤ - ( 𝐴 ↑ 2 ) ) )
38 35 37 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 1 ≤ - ( 𝐴 ↑ 2 ) )
39 29 12 28 31 38 letrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ≤ - ( 𝐴 ↑ 2 ) )
40 28 39 sqrtnegd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ - - ( 𝐴 ↑ 2 ) ) = ( i · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
41 14 40 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ ( 𝐴 ↑ 2 ) ) = ( i · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
42 41 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) = ( i · ( i · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) ) )
43 ax-icn ⊢ i ∈ ℂ
44 43 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → i ∈ ℂ )
45 28 39 resqrtcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ - ( 𝐴 ↑ 2 ) ) ∈ ℝ )
46 45 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( √ ‘ - ( 𝐴 ↑ 2 ) ) ∈ ℂ )
47 44 44 46 mulassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( i · i ) · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = ( i · ( i · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) ) )
48 ixi ⊢ ( i · i ) = - 1
49 48 oveq1i ⊢ ( ( i · i ) · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = ( - 1 · ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
50 46 mulm1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( - 1 · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = - ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
51 49 50 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( i · i ) · ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = - ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
52 42 47 51 3eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) = - ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
53 45 renegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → - ( √ ‘ - ( 𝐴 ↑ 2 ) ) ∈ ℝ )
54 52 53 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ∈ ℝ )
55 12 54 readdcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ )
56 55 mnfltd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → -∞ < ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
57 52 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 + - ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
58 negsub ⊢ ( ( 1 ∈ ℂ ∧ ( √ ‘ - ( 𝐴 ↑ 2 ) ) ∈ ℂ ) → ( 1 + - ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = ( 1 − ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
59 15 46 58 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + - ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) = ( 1 − ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
60 57 59 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 − ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
61 sq1 ⊢ ( 1 ↑ 2 ) = 1
62 61 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 ↑ 2 ) = 1 )
63 28 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → - ( 𝐴 ↑ 2 ) ∈ ℂ )
64 63 sqsqrtd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( √ ‘ - ( 𝐴 ↑ 2 ) ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
65 38 62 64 3brtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 ↑ 2 ) ≤ ( ( √ ‘ - ( 𝐴 ↑ 2 ) ) ↑ 2 ) )
66 28 39 sqrtge0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ≤ ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
67 12 45 31 66 le2sqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 ≤ ( √ ‘ - ( 𝐴 ↑ 2 ) ) ↔ ( 1 ↑ 2 ) ≤ ( ( √ ‘ - ( 𝐴 ↑ 2 ) ) ↑ 2 ) ) )
68 65 67 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → 1 ≤ ( √ ‘ - ( 𝐴 ↑ 2 ) ) )
69 12 45 suble0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 − ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) ≤ 0 ↔ 1 ≤ ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) )
70 68 69 mpbird ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( √ ‘ - ( 𝐴 ↑ 2 ) ) ) ≤ 0 )
71 60 70 eqbrtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ≤ 0 )
72 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∧ ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ≤ 0 ) ) )
73 19 20 72 mp2an ⊢ ( ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ℝ ∧ -∞ < ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∧ ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ≤ 0 ) )
74 55 56 71 73 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) )
75 oveq2 ⊢ ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( i · 𝐴 ) = ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
76 75 oveq2d ⊢ ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( 1 + ( i · 𝐴 ) ) = ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
77 76 eleq1d ⊢ ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ) )
78 74 77 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
79 mulneg2 ⊢ ( ( i ∈ ℂ ∧ ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℂ ) → ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) = - ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
80 43 7 79 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) = - ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
81 80 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 − - ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
82 mulcl ⊢ ( ( i ∈ ℂ ∧ ( √ ‘ ( 𝐴 ↑ 2 ) ) ∈ ℂ ) → ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
83 43 7 82 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ∈ ℂ )
84 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ∈ ℂ ) → ( 1 − - ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
85 15 83 84 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − - ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
86 81 85 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) = ( 1 + ( i · ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
87 86 74 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) )
88 oveq2 ⊢ ( 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( i · 𝐴 ) = ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) )
89 88 oveq2d ⊢ ( 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( 1 − ( i · 𝐴 ) ) = ( 1 − ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) )
90 89 eleq1d ⊢ ( 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( 1 − ( i · - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) ) ∈ ( -∞ (,] 0 ) ) )
91 87 90 syl5ibrcom ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
92 78 91 orim12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 𝐴 = ( √ ‘ ( 𝐴 ↑ 2 ) ) ∨ 𝐴 = - ( √ ‘ ( 𝐴 ↑ 2 ) ) ) → ( ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) )
93 10 92 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
94 93 orcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
95 61 a1i ⊢ ( 𝐴 ∈ ℂ → ( 1 ↑ 2 ) = 1 )
96 sqmul ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
97 43 96 mpan ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
98 i2 ⊢ ( i ↑ 2 ) = - 1
99 98 oveq1i ⊢ ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = ( - 1 · ( 𝐴 ↑ 2 ) )
100 3 mulm1d ⊢ ( 𝐴 ∈ ℂ → ( - 1 · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
101 99 100 eqtrid ⊢ ( 𝐴 ∈ ℂ → ( ( i ↑ 2 ) · ( 𝐴 ↑ 2 ) ) = - ( 𝐴 ↑ 2 ) )
102 97 101 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) ↑ 2 ) = - ( 𝐴 ↑ 2 ) )
103 95 102 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( 1 − - ( 𝐴 ↑ 2 ) ) )
104 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
105 43 104 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
106 subsq ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
107 15 105 106 sylancr ⊢ ( 𝐴 ∈ ℂ → ( ( 1 ↑ 2 ) − ( ( i · 𝐴 ) ↑ 2 ) ) = ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
108 15 3 32 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − - ( 𝐴 ↑ 2 ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
109 103 107 108 3eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
110 109 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( 𝐴 ↑ 2 ) ) )
111 2cn ⊢ 2 ∈ ℂ
112 111 a1i ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
113 15 a1i ⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
114 112 113 105 subsubd ⊢ ( 𝐴 ∈ ℂ → ( 2 − ( 1 − ( i · 𝐴 ) ) ) = ( ( 2 − 1 ) + ( i · 𝐴 ) ) )
115 2m1e1 ⊢ ( 2 − 1 ) = 1
116 115 oveq1i ⊢ ( ( 2 − 1 ) + ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) )
117 114 116 eqtrdi ⊢ ( 𝐴 ∈ ℂ → ( 2 − ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( i · 𝐴 ) ) )
118 117 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( i · 𝐴 ) ) )
119 2re ⊢ 2 ∈ ℝ
120 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) )
121 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( i · 𝐴 ) ) ∧ ( 1 − ( i · 𝐴 ) ) ≤ 0 ) ) )
122 19 20 121 mp2an ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( i · 𝐴 ) ) ∧ ( 1 − ( i · 𝐴 ) ) ≤ 0 ) )
123 120 122 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 − ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 − ( i · 𝐴 ) ) ∧ ( 1 − ( i · 𝐴 ) ) ≤ 0 ) )
124 123 simp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ℝ )
125 resubcl ⊢ ( ( 2 ∈ ℝ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ℝ ) → ( 2 − ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ )
126 119 124 125 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ )
127 118 126 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ℝ )
128 127 124 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ )
129 128 mnfltd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → -∞ < ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
130 123 simp3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · 𝐴 ) ) ≤ 0 )
131 0red ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ )
132 119 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ∈ ℝ )
133 2pos ⊢ 0 < 2
134 133 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 < 2 )
135 111 subid1i ⊢ ( 2 − 0 ) = 2
136 124 131 132 130 lesub2dd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − 0 ) ≤ ( 2 − ( 1 − ( i · 𝐴 ) ) ) )
137 135 136 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ≤ ( 2 − ( 1 − ( i · 𝐴 ) ) ) )
138 137 118 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ≤ ( 1 + ( i · 𝐴 ) ) )
139 131 132 127 134 138 ltletrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 < ( 1 + ( i · 𝐴 ) ) )
140 lemul2 ⊢ ( ( ( 1 − ( i · 𝐴 ) ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 1 + ( i · 𝐴 ) ) ∈ ℝ ∧ 0 < ( 1 + ( i · 𝐴 ) ) ) ) → ( ( 1 − ( i · 𝐴 ) ) ≤ 0 ↔ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( ( 1 + ( i · 𝐴 ) ) · 0 ) ) )
141 124 131 127 139 140 syl112anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 − ( i · 𝐴 ) ) ≤ 0 ↔ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( ( 1 + ( i · 𝐴 ) ) · 0 ) ) )
142 130 141 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( ( 1 + ( i · 𝐴 ) ) · 0 ) )
143 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
144 15 105 143 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
145 144 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
146 145 mul01d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · 0 ) = 0 )
147 142 146 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ 0 )
148 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ ∧ -∞ < ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∧ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ 0 ) ) )
149 19 20 148 mp2an ⊢ ( ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ ∧ -∞ < ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∧ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ 0 ) )
150 128 129 147 149 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ( -∞ (,] 0 ) )
151 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) )
152 elioc2 ⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( i · 𝐴 ) ) ∧ ( 1 + ( i · 𝐴 ) ) ≤ 0 ) ) )
153 19 20 152 mp2an ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 + ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( i · 𝐴 ) ) ∧ ( 1 + ( i · 𝐴 ) ) ≤ 0 ) )
154 151 153 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) ∈ ℝ ∧ -∞ < ( 1 + ( i · 𝐴 ) ) ∧ ( 1 + ( i · 𝐴 ) ) ≤ 0 ) )
155 154 simp1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ℝ )
156 112 113 105 subsub4d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 − 1 ) − ( i · 𝐴 ) ) = ( 2 − ( 1 + ( i · 𝐴 ) ) ) )
157 115 oveq1i ⊢ ( ( 2 − 1 ) − ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) )
158 156 157 eqtr3di ⊢ ( 𝐴 ∈ ℂ → ( 2 − ( 1 + ( i · 𝐴 ) ) ) = ( 1 − ( i · 𝐴 ) ) )
159 158 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − ( 1 + ( i · 𝐴 ) ) ) = ( 1 − ( i · 𝐴 ) ) )
160 resubcl ⊢ ( ( 2 ∈ ℝ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ℝ ) → ( 2 − ( 1 + ( i · 𝐴 ) ) ) ∈ ℝ )
161 119 155 160 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − ( 1 + ( i · 𝐴 ) ) ) ∈ ℝ )
162 159 161 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ℝ )
163 155 162 remulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ℝ )
164 163 mnfltd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → -∞ < ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) )
165 154 simp3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 + ( i · 𝐴 ) ) ≤ 0 )
166 0red ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 ∈ ℝ )
167 119 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ∈ ℝ )
168 133 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 < 2 )
169 155 166 167 165 lesub2dd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 2 − 0 ) ≤ ( 2 − ( 1 + ( i · 𝐴 ) ) ) )
170 135 169 eqbrtrrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ≤ ( 2 − ( 1 + ( i · 𝐴 ) ) ) )
171 170 159 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 2 ≤ ( 1 − ( i · 𝐴 ) ) )
172 166 167 162 168 171 ltletrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → 0 < ( 1 − ( i · 𝐴 ) ) )
173 lemul1 ⊢ ( ( ( 1 + ( i · 𝐴 ) ) ∈ ℝ ∧ 0 ∈ ℝ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ ℝ ∧ 0 < ( 1 − ( i · 𝐴 ) ) ) ) → ( ( 1 + ( i · 𝐴 ) ) ≤ 0 ↔ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( 0 · ( 1 − ( i · 𝐴 ) ) ) ) )
174 155 166 162 172 173 syl112anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) ≤ 0 ↔ ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( 0 · ( 1 − ( i · 𝐴 ) ) ) ) )
175 165 174 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ ( 0 · ( 1 − ( i · 𝐴 ) ) ) )
176 162 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
177 176 mul02d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( 0 · ( 1 − ( i · 𝐴 ) ) ) = 0 )
178 175 177 breqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ≤ 0 )
179 163 164 178 149 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ( -∞ (,] 0 ) )
180 150 179 jaodan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) → ( ( 1 + ( i · 𝐴 ) ) · ( 1 − ( i · 𝐴 ) ) ) ∈ ( -∞ (,] 0 ) )
181 110 180 eqeltrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) )
182 94 181 impbida ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) )
183 182 notbid ⊢ ( 𝐴 ∈ ℂ → ( ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ¬ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) )
184 ioran ⊢ ( ¬ ( ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∨ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ↔ ( ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∧ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
185 183 184 bitrdi ⊢ ( 𝐴 ∈ ℂ → ( ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ↔ ( ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∧ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) )
186 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) ∈ ℂ ) → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
187 15 3 186 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ )
188 1 eleq2i ⊢ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ↔ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
189 eldif ⊢ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ ∧ ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) )
190 188 189 bitri ⊢ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ↔ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ ∧ ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) )
191 190 baib ⊢ ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ℂ → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ↔ ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) )
192 187 191 syl ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ↔ ¬ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ ( -∞ (,] 0 ) ) )
193 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
194 15 105 193 sylancr ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
195 1 eleq2i ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ↔ ( 1 − ( i · 𝐴 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
196 eldif ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ ∧ ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
197 195 196 bitri ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ ∧ ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
198 197 baib ⊢ ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ → ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ↔ ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
199 194 198 syl ⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ↔ ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
200 1 eleq2i ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ↔ ( 1 + ( i · 𝐴 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
201 eldif ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ ∧ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
202 200 201 bitri ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ↔ ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ ∧ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
203 202 baib ⊢ ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ↔ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
204 144 203 syl ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ↔ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) )
205 199 204 anbi12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) ↔ ( ¬ ( 1 − ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ∧ ¬ ( 1 + ( i · 𝐴 ) ) ∈ ( -∞ (,] 0 ) ) ) )
206 185 192 205 3bitr4d ⊢ ( 𝐴 ∈ ℂ → ( ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ↔ ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) ) )
207 206 pm5.32i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ) ↔ ( 𝐴 ∈ ℂ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) ) )
208 1 2 atans ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℂ ∧ ( 1 + ( 𝐴 ↑ 2 ) ) ∈ 𝐷 ) )
209 3anass ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) ↔ ( 𝐴 ∈ ℂ ∧ ( ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) ) )
210 207 208 209 3bitr4i ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ∈ 𝐷 ∧ ( 1 + ( i · 𝐴 ) ) ∈ 𝐷 ) )