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