abelthlem2

Description: Lemma for abelth . The peculiar region S , known as aStolz angle , is a teardrop-shaped subset of the closed unit ball containing 1 . Indeed, except for 1 itself, the rest of the Stolz angle is enclosed in the open unit ball. (Contributed by Mario Carneiro, 31-Mar-2015)

	Ref	Expression
Hypotheses	abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
	abelth.3	$⊢ φ \to M \in ℝ$
	abelth.4	$⊢ φ \to 0 \leq M$
	abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
Assertion	abelthlem2	$⊢ φ \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$

Proof

Step	Hyp	Ref	Expression
1		abelth.1	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
2		abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
3		abelth.3	$⊢ φ \to M \in ℝ$
4		abelth.4	$⊢ φ \to 0 \leq M$
5		abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
6		1cnd	$⊢ (M \in ℝ \land 0 \leq M) \to 1 \in ℂ$
7		0le0	$⊢ 0 \leq 0$
8		simpl	$⊢ (M \in ℝ \land 0 \leq M) \to M \in ℝ$
9	8	recnd	$⊢ (M \in ℝ \land 0 \leq M) \to M \in ℂ$
10	9	mul01d	$⊢ (M \in ℝ \land 0 \leq M) \to M \cdot 0 = 0$
11	7 10	breqtrrid	$⊢ (M \in ℝ \land 0 \leq M) \to 0 \leq M \cdot 0$
12		oveq2	$⊢ z = 1 \to 1 - z = 1 - 1$
13		1m1e0	$⊢ 1 - 1 = 0$
14	12 13	eqtrdi	$⊢ z = 1 \to 1 - z = 0$
15	14	abs00bd	$⊢ z = 1 \to \|1 - z\| = 0$
16		fveq2	$⊢ z = 1 \to \|z\| = \|1\|$
17		abs1	$⊢ \|1\| = 1$
18	16 17	eqtrdi	$⊢ z = 1 \to \|z\| = 1$
19	18	oveq2d	$⊢ z = 1 \to 1 - \|z\| = 1 - 1$
20	19 13	eqtrdi	$⊢ z = 1 \to 1 - \|z\| = 0$
21	20	oveq2d	$⊢ z = 1 \to M (1 - \|z\|) = M \cdot 0$
22	15 21	breq12d	$⊢ z = 1 \to (\|1 - z\| \leq M (1 - \|z\|) \leftrightarrow 0 \leq M \cdot 0)$
23	22 5	elrab2	$⊢ 1 \in S \leftrightarrow (1 \in ℂ \land 0 \leq M \cdot 0)$
24	6 11 23	sylanbrc	$⊢ (M \in ℝ \land 0 \leq M) \to 1 \in S$
25		velsn	$⊢ z \in \{1\} \leftrightarrow z = 1$
26	25	necon3bbii	$⊢ \neg z \in \{1\} \leftrightarrow z \neq 1$
27		simprll	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z \in ℂ$
28		0cn	$⊢ 0 \in ℂ$
29		eqid	$⊢ abs \circ - = abs \circ -$
30	29	cnmetdval	$⊢ (z \in ℂ \land 0 \in ℂ) \to z (abs \circ -) 0 = \|z - 0\|$
31	27 28 30	sylancl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z (abs \circ -) 0 = \|z - 0\|$
32	27	subid1d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z - 0 = z$
33	32	fveq2d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z - 0\| = \|z\|$
34	31 33	eqtrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z (abs \circ -) 0 = \|z\|$
35	27	abscld	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| \in ℝ$
36		1red	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 \in ℝ$
37		1re	$⊢ 1 \in ℝ$
38		resubcl	$⊢ (\|z\| \in ℝ \land 1 \in ℝ) \to \|z\| - 1 \in ℝ$
39	35 37 38	sylancl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| - 1 \in ℝ$
40		ax-1cn	$⊢ 1 \in ℂ$
41		subcl	$⊢ (1 \in ℂ \land z \in ℂ) \to 1 - z \in ℂ$
42	40 27 41	sylancr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 - z \in ℂ$
43	42	abscld	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|1 - z\| \in ℝ$
44		simpll	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \in ℝ$
45		resubcl	$⊢ (1 \in ℝ \land \|z\| \in ℝ) \to 1 - \|z\| \in ℝ$
46	37 35 45	sylancr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 - \|z\| \in ℝ$
47	44 46	remulcld	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M (1 - \|z\|) \in ℝ$
48	17	oveq2i	$⊢ \|z\| - \|1\| = \|z\| - 1$
49		abs2dif	$⊢ (z \in ℂ \land 1 \in ℂ) \to \|z\| - \|1\| \leq \|z - 1\|$
50	27 40 49	sylancl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| - \|1\| \leq \|z - 1\|$
51	48 50	eqbrtrrid	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| - 1 \leq \|z - 1\|$
52		abssub	$⊢ (z \in ℂ \land 1 \in ℂ) \to \|z - 1\| = \|1 - z\|$
53	27 40 52	sylancl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z - 1\| = \|1 - z\|$
54	51 53	breqtrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| - 1 \leq \|1 - z\|$
55		simprlr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|1 - z\| \leq M (1 - \|z\|)$
56	39 43 47 54 55	letrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| - 1 \leq M (1 - \|z\|)$
57	35 36 47	lesubaddd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (\|z\| - 1 \leq M (1 - \|z\|) \leftrightarrow \|z\| \leq M (1 - \|z\|) + 1)$
58	56 57	mpbid	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| \leq M (1 - \|z\|) + 1$
59	9	adantr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \in ℂ$
60		1cnd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 \in ℂ$
61	44 35	remulcld	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \|z\| \in ℝ$
62	61	recnd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \|z\| \in ℂ$
63	59 60 62	addsubd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M + 1 - M \|z\| = M - M \|z\| + 1$
64	35	recnd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| \in ℂ$
65	59 60 64	subdid	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M (1 - \|z\|) = M \cdot 1 - M \|z\|$
66	59	mulridd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \cdot 1 = M$
67	66	oveq1d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \cdot 1 - M \|z\| = M - M \|z\|$
68	65 67	eqtrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M (1 - \|z\|) = M - M \|z\|$
69	68	oveq1d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M (1 - \|z\|) + 1 = M - M \|z\| + 1$
70	63 69	eqtr4d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M + 1 - M \|z\| = M (1 - \|z\|) + 1$
71	58 70	breqtrrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| \leq M + 1 - M \|z\|$
72		peano2re	$⊢ M \in ℝ \to M + 1 \in ℝ$
73	44 72	syl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M + 1 \in ℝ$
74	61 35 73	leaddsub2d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (M \|z\| + \|z\| \leq M + 1 \leftrightarrow \|z\| \leq M + 1 - M \|z\|)$
75	71 74	mpbird	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \|z\| + \|z\| \leq M + 1$
76	59 64	adddirp1d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (M + 1) \|z\| = M \|z\| + \|z\|$
77	73	recnd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M + 1 \in ℂ$
78	77	mulridd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (M + 1) \cdot 1 = M + 1$
79	75 76 78	3brtr4d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (M + 1) \|z\| \leq (M + 1) \cdot 1$
80		0red	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 0 \in ℝ$
81		simplr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 0 \leq M$
82	44	ltp1d	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M < M + 1$
83	80 44 73 81 82	lelttrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 0 < M + 1$
84		lemul2	$⊢ (\|z\| \in ℝ \land 1 \in ℝ \land (M + 1 \in ℝ \land 0 < M + 1)) \to (\|z\| \leq 1 \leftrightarrow (M + 1) \|z\| \leq (M + 1) \cdot 1)$
85	35 36 73 83 84	syl112anc	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (\|z\| \leq 1 \leftrightarrow (M + 1) \|z\| \leq (M + 1) \cdot 1)$
86	79 85	mpbird	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| \leq 1$
87	43 47 55	lensymd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \neg M (1 - \|z\|) < \|1 - z\|$
88	10	adantr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \cdot 0 = 0$
89		simprr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z \neq 1$
90	89	necomd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 \neq z$
91		subeq0	$⊢ (1 \in ℂ \land z \in ℂ) \to (1 - z = 0 \leftrightarrow 1 = z)$
92	91	necon3bid	$⊢ (1 \in ℂ \land z \in ℂ) \to (1 - z \neq 0 \leftrightarrow 1 \neq z)$
93	40 27 92	sylancr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (1 - z \neq 0 \leftrightarrow 1 \neq z)$
94	90 93	mpbird	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 - z \neq 0$
95		absgt0	$⊢ 1 - z \in ℂ \to (1 - z \neq 0 \leftrightarrow 0 < \|1 - z\|)$
96	42 95	syl	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (1 - z \neq 0 \leftrightarrow 0 < \|1 - z\|)$
97	94 96	mpbid	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 0 < \|1 - z\|$
98	88 97	eqbrtrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to M \cdot 0 < \|1 - z\|$
99		oveq2	$⊢ 1 = \|z\| \to 1 - 1 = 1 - \|z\|$
100	13 99	eqtr3id	$⊢ 1 = \|z\| \to 0 = 1 - \|z\|$
101	100	oveq2d	$⊢ 1 = \|z\| \to M \cdot 0 = M (1 - \|z\|)$
102	101	breq1d	$⊢ 1 = \|z\| \to (M \cdot 0 < \|1 - z\| \leftrightarrow M (1 - \|z\|) < \|1 - z\|)$
103	98 102	syl5ibcom	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (1 = \|z\| \to M (1 - \|z\|) < \|1 - z\|)$
104	103	necon3bd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (\neg M (1 - \|z\|) < \|1 - z\| \to 1 \neq \|z\|)$
105	87 104	mpd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to 1 \neq \|z\|$
106	35 36 86 105	leneltd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to \|z\| < 1$
107	34 106	eqbrtrd	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z (abs \circ -) 0 < 1$
108		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
109		1xr	$⊢ 1 \in ℝ^{*}$
110		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land 1 \in ℝ^{*}) \land (0 \in ℂ \land z \in ℂ)) \to (z \in (0 ball (abs \circ -) 1) \leftrightarrow z (abs \circ -) 0 < 1)$
111	108 109 110	mpanl12	$⊢ (0 \in ℂ \land z \in ℂ) \to (z \in (0 ball (abs \circ -) 1) \leftrightarrow z (abs \circ -) 0 < 1)$
112	28 27 111	sylancr	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to (z \in (0 ball (abs \circ -) 1) \leftrightarrow z (abs \circ -) 0 < 1)$
113	107 112	mpbird	$⊢ ((M \in ℝ \land 0 \leq M) \land ((z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \land z \neq 1)) \to z \in (0 ball (abs \circ -) 1)$
114	113	expr	$⊢ ((M \in ℝ \land 0 \leq M) \land (z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|))) \to (z \neq 1 \to z \in (0 ball (abs \circ -) 1))$
115	114	3impb	$⊢ ((M \in ℝ \land 0 \leq M) \land z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \to (z \neq 1 \to z \in (0 ball (abs \circ -) 1))$
116	26 115	biimtrid	$⊢ ((M \in ℝ \land 0 \leq M) \land z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \to (\neg z \in \{1\} \to z \in (0 ball (abs \circ -) 1))$
117	116	orrd	$⊢ ((M \in ℝ \land 0 \leq M) \land z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \to (z \in \{1\} \lor z \in (0 ball (abs \circ -) 1))$
118		elun	$⊢ z \in (\{1\} \cup (0 ball (abs \circ -) 1)) \leftrightarrow (z \in \{1\} \lor z \in (0 ball (abs \circ -) 1))$
119	117 118	sylibr	$⊢ ((M \in ℝ \land 0 \leq M) \land z \in ℂ \land \|1 - z\| \leq M (1 - \|z\|)) \to z \in (\{1\} \cup (0 ball (abs \circ -) 1))$
120	119	rabssdv	$⊢ (M \in ℝ \land 0 \leq M) \to \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\} \subseteq \{1\} \cup (0 ball (abs \circ -) 1)$
121	5 120	eqsstrid	$⊢ (M \in ℝ \land 0 \leq M) \to S \subseteq \{1\} \cup (0 ball (abs \circ -) 1)$
122		ssundif	$⊢ S \subseteq \{1\} \cup (0 ball (abs \circ -) 1) \leftrightarrow S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1$
123	121 122	sylib	$⊢ (M \in ℝ \land 0 \leq M) \to S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1$
124	24 123	jca	$⊢ (M \in ℝ \land 0 \leq M) \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$
125	3 4 124	syl2anc	$⊢ φ \to (1 \in S \land S ∖ \{1\} \subseteq 0 ball (abs \circ -) 1)$

Metamath Proof Explorer

Theorem abelthlem2

Proof