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