bndatandm

Description: A point in the open unit disk is in the domain of the arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

		Ref	Expression
	Assertion	bndatandm	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in dom arctan$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in ℂ$
2		sqcl	$⊢ A \in ℂ \to A^{2} \in ℂ$
3	2	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to A^{2} \in ℂ$
4	3	abscld	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A^{2}\| \in ℝ$
5		2nn0	$⊢ 2 \in ℕ_{0}$
6		absexp	$⊢ (A \in ℂ \land 2 \in ℕ_{0}) \to \|A^{2}\| = {\|A\|}^{2}$
7	1 5 6	sylancl	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A^{2}\| = {\|A\|}^{2}$
8		simpr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| < 1$
9		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
10	9	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A\| \in ℝ$
11		1red	$⊢ (A \in ℂ \land \|A\| < 1) \to 1 \in ℝ$
12		absge0	$⊢ A \in ℂ \to 0 \leq \|A\|$
13	12	adantr	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \leq \|A\|$
14		0le1	$⊢ 0 \leq 1$
15	14	a1i	$⊢ (A \in ℂ \land \|A\| < 1) \to 0 \leq 1$
16	10 11 13 15	lt2sqd	$⊢ (A \in ℂ \land \|A\| < 1) \to (\|A\| < 1 \leftrightarrow {\|A\|}^{2} < 1^{2})$
17	8 16	mpbid	$⊢ (A \in ℂ \land \|A\| < 1) \to {\|A\|}^{2} < 1^{2}$
18		sq1	$⊢ 1^{2} = 1$
19	17 18	breqtrdi	$⊢ (A \in ℂ \land \|A\| < 1) \to {\|A\|}^{2} < 1$
20	7 19	eqbrtrd	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A^{2}\| < 1$
21	4 20	ltned	$⊢ (A \in ℂ \land \|A\| < 1) \to \|A^{2}\| \neq 1$
22		fveq2	$⊢ A^{2} = - 1 \to \|A^{2}\| = \|- 1\|$
23		ax-1cn	$⊢ 1 \in ℂ$
24	23	absnegi	$⊢ \|- 1\| = \|1\|$
25		abs1	$⊢ \|1\| = 1$
26	24 25	eqtri	$⊢ \|- 1\| = 1$
27	22 26	eqtrdi	$⊢ A^{2} = - 1 \to \|A^{2}\| = 1$
28	27	necon3i	$⊢ \|A^{2}\| \neq 1 \to A^{2} \neq - 1$
29	21 28	syl	$⊢ (A \in ℂ \land \|A\| < 1) \to A^{2} \neq - 1$
30		atandm3	$⊢ A \in dom arctan \leftrightarrow (A \in ℂ \land A^{2} \neq - 1)$
31	1 29 30	sylanbrc	$⊢ (A \in ℂ \land \|A\| < 1) \to A \in dom arctan$

Metamath Proof Explorer

Theorem bndatandm

Proof