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	$⊢ D = ℂ ∖ (−∞, 0]$
	atansopn.s	$⊢ S = \{y \in ℂ \| 1 + y^{2} \in D\}$
Assertion	atans2	$⊢ A \in S \leftrightarrow (A \in ℂ \land 1 - i A \in D \land 1 + i A \in D)$

Proof

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

Metamath Proof Explorer

Theorem atans2

Proof