efopnlem1

		Ref	Expression
	Assertion	efopnlem1	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|ℑ (A)\| < π$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to A \in (0 ball (abs \circ -) R)$
2		rpxr	$⊢ R \in ℝ^{+} \to R \in ℝ^{*}$
3	2	ad2antrr	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to R \in ℝ^{*}$
4		eqid	$⊢ abs \circ - = abs \circ -$
5	4	cnbl0	$⊢ R \in ℝ^{*} \to {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
6	3 5	syl	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to {abs}^{-1} [[0, R)] = 0 ball (abs \circ -) R$
7	1 6	eleqtrrd	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to A \in {abs}^{-1} [[0, R)]$
8		absf	$⊢ abs : ℂ ⟶ ℝ$
9		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
10		elpreima	$⊢ abs Fn ℂ \to (A \in {abs}^{-1} [[0, R)] \leftrightarrow (A \in ℂ \land \|A\| \in [0, R)))$
11	8 9 10	mp2b	$⊢ A \in {abs}^{-1} [[0, R)] \leftrightarrow (A \in ℂ \land \|A\| \in [0, R))$
12	11	simplbi	$⊢ A \in {abs}^{-1} [[0, R)] \to A \in ℂ$
13	7 12	syl	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to A \in ℂ$
14	13	imcld	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to ℑ (A) \in ℝ$
15	14	recnd	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to ℑ (A) \in ℂ$
16	15	abscld	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|ℑ (A)\| \in ℝ$
17		rpre	$⊢ R \in ℝ^{+} \to R \in ℝ$
18	17	ad2antrr	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to R \in ℝ$
19		pire	$⊢ π \in ℝ$
20	19	a1i	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to π \in ℝ$
21	13	abscld	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|A\| \in ℝ$
22		absimle	$⊢ A \in ℂ \to \|ℑ (A)\| \leq \|A\|$
23	13 22	syl	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|ℑ (A)\| \leq \|A\|$
24	11	simprbi	$⊢ A \in {abs}^{-1} [[0, R)] \to \|A\| \in [0, R)$
25	7 24	syl	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|A\| \in [0, R)$
26		0re	$⊢ 0 \in ℝ$
27		elico2	$⊢ (0 \in ℝ \land R \in ℝ^{*}) \to (\|A\| \in [0, R) \leftrightarrow (\|A\| \in ℝ \land 0 \leq \|A\| \land \|A\| < R))$
28	26 3 27	sylancr	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to (\|A\| \in [0, R) \leftrightarrow (\|A\| \in ℝ \land 0 \leq \|A\| \land \|A\| < R))$
29	25 28	mpbid	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to (\|A\| \in ℝ \land 0 \leq \|A\| \land \|A\| < R)$
30	29	simp3d	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|A\| < R$
31	16 21 18 23 30	lelttrd	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|ℑ (A)\| < R$
32		simplr	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to R < π$
33	16 18 20 31 32	lttrd	$⊢ ((R \in ℝ^{+} \land R < π) \land A \in (0 ball (abs \circ -) R)) \to \|ℑ (A)\| < π$

Metamath Proof Explorer

Theorem efopnlem1

Proof