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 · 𝐴 ) ) ∈ 𝐷 ) )