abelthlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > abelthlem2		Structured version Visualization version GIF version

Theorem abelthlem2 26410

Description: Lemma for abelth 26419. The peculiar region 𝑆, known as a Stolz 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.)

**Hypotheses**
Ref	Expression
abelth.1	⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
abelth.2	⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3	⊢ (𝜑 → 𝑀 ∈ ℝ)
abelth.4	⊢ (𝜑 → 0 ≤ 𝑀)
abelth.5	⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}

**Assertion**
Ref	Expression
abelthlem2	⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))

Distinct variable groups: 𝑧,𝑀 𝑧,𝐴 Allowed substitution hints: 𝜑(𝑧) 𝑆(𝑧)

**Proof of Theorem abelthlem2**
Step	Hyp	Ref	Expression
1		abelth.3	. 2 ⊢ (𝜑 → 𝑀 ∈ ℝ)
2		abelth.4	. 2 ⊢ (𝜑 → 0 ≤ 𝑀)
3		1cnd 11130	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ ℂ)
4		0le0 12273	. . . . 5 ⊢ 0 ≤ 0
5		simpl 482	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
6	5	recnd 11164	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
7	6	mul01d 11336	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑀 · 0) = 0)
8	4, 7	breqtrrid 5124	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 0 ≤ (𝑀 · 0))
9		oveq2 7368	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − 𝑧) = (1 − 1))
10		1m1e0 12244	. . . . . . . 8 ⊢ (1 − 1) = 0
11	9, 10	eqtrdi 2788	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − 𝑧) = 0)
12	11	abs00bd 15244	. . . . . 6 ⊢ (𝑧 = 1 → (abs‘(1 − 𝑧)) = 0)
13		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑧 = 1 → (abs‘𝑧) = (abs‘1))
14		abs1 15250	. . . . . . . . . 10 ⊢ (abs‘1) = 1
15	13, 14	eqtrdi 2788	. . . . . . . . 9 ⊢ (𝑧 = 1 → (abs‘𝑧) = 1)
16	15	oveq2d 7376	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = (1 − 1))
17	16, 10	eqtrdi 2788	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = 0)
18	17	oveq2d 7376	. . . . . 6 ⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0))
19	12, 18	breq12d 5099	. . . . 5 ⊢ (𝑧 = 1 → ((abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ 0 ≤ (𝑀 · 0)))
20		abelth.5	. . . . 5 ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
21	19, 20	elrab2 3638	. . . 4 ⊢ (1 ∈ 𝑆 ↔ (1 ∈ ℂ ∧ 0 ≤ (𝑀 · 0)))
22	3, 8, 21	sylanbrc 584	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ 𝑆)
23		velsn 4584	. . . . . . . . . 10 ⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1)
24	23	necon3bbii 2980	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ {1} ↔ 𝑧 ≠ 1)
25		simprll 779	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ ℂ)
26		0cn 11127	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℂ
27		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
28	27	cnmetdval 24745	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
29	25, 26, 28	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
30	25	subid1d 11485	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧)
31	30	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
32	29, 31	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
33	25	abscld 15392	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℝ)
34		1red 11136	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℝ)
35		1re 11135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ
36		resubcl 11449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ)
37	33, 35, 36	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ∈ ℝ)
38		ax-1cn 11087	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
39		subcl 11383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − 𝑧) ∈ ℂ)
40	38, 25, 39	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ∈ ℂ)
41	40	abscld 15392	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ∈ ℝ)
42		simpll 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℝ)
43		resubcl 11449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 − (abs‘𝑧)) ∈ ℝ)
44	35, 33, 43	sylancr 588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − (abs‘𝑧)) ∈ ℝ)
45	42, 44	remulcld 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) ∈ ℝ)
46	14	oveq2i 7371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘𝑧) − (abs‘1)) = ((abs‘𝑧) − 1)
47		abs2dif 15286	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
48	25, 38, 47	sylancl 587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
49	46, 48	eqbrtrrid 5122	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(𝑧 − 1)))
50		abssub 15280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
51	25, 38, 50	sylancl 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
52	49, 51	breqtrd 5112	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(1 − 𝑧)))
53		simprlr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))))
54	37, 41, 45, 52, 53	letrd 11294	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))))
55	33, 34, 45	lesubaddd 11738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ (abs‘𝑧) ≤ ((𝑀 · (1 − (abs‘𝑧))) + 1)))
56	54, 55	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 · (1 − (abs‘𝑧))) + 1))
57	6	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℂ)
58		1cnd 11130	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℂ)
59	42, 33	remulcld 11166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℝ)
60	59	recnd 11164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℂ)
61	57, 58, 60	addsubd 11517	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
62	33	recnd 11164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℂ)
63	57, 58, 62	subdid 11597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = ((𝑀 · 1) − (𝑀 · (abs‘𝑧))))
64	57	mulridd 11153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 1) = 𝑀)
65	64	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
66	63, 65	eqtrd 2772	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
67	66	oveq1d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (1 − (abs‘𝑧))) + 1) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
68	61, 67	eqtr4d 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1))
69	56, 68	breqtrrd 5114	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))
70		peano2re 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
71	42, 70	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℝ)
72	59, 33, 71	leaddsub2d 11743	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1) ↔ (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧)))))
73	69, 72	mpbird 257	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1))
74	57, 62	adddirp1d 11162	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)))
75	71	recnd 11164	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℂ)
76	75	mulridd 11153	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · 1) = (𝑀 + 1))
77	73, 74, 76	3brtr4d 5118	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))
78		0red 11138	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ∈ ℝ)
79		simplr 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ≤ 𝑀)
80	42	ltp1d 12077	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1))
81	78, 42, 71, 79, 80	lelttrd 11295	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (𝑀 + 1))
82		lemul2 11999	. . . . . . . . . . . . . . . 16 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑀 + 1) ∈ ℝ ∧ 0 < (𝑀 + 1))) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)))
83	33, 34, 71, 81, 82	syl112anc 1377	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)))
84	77, 83	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ 1)
85	41, 45, 53	lensymd 11288	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ¬ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧)))
86	7	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) = 0)
87		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ≠ 1)
88	87	necomd 2988	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ 𝑧)
89		subeq0 11411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧))
90	89	necon3bid 2977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧))
91	38, 25, 90	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧))
92	88, 91	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ≠ 0)
93		absgt0 15278	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 𝑧) ∈ ℂ → ((1 − 𝑧) ≠ 0 ↔ 0 < (abs‘(1 − 𝑧))))
94	40, 93	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((1 − 𝑧) ≠ 0 ↔ 0 < (abs‘(1 − 𝑧))))
95	92, 94	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (abs‘(1 − 𝑧)))
96	86, 95	eqbrtrd 5108	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1 − 𝑧)))
97		oveq2 7368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 = (abs‘𝑧) → (1 − 1) = (1 − (abs‘𝑧)))
98	10, 97	eqtr3id 2786	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 = (abs‘𝑧) → 0 = (1 − (abs‘𝑧)))
99	98	oveq2d 7376	. . . . . . . . . . . . . . . . . 18 ⊢ (1 = (abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 − (abs‘𝑧))))
100	99	breq1d 5096	. . . . . . . . . . . . . . . . 17 ⊢ (1 = (abs‘𝑧) → ((𝑀 · 0) < (abs‘(1 − 𝑧)) ↔ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧))))
101	96, 100	syl5ibcom 245	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 = (abs‘𝑧) → (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧))))
102	101	necon3bd 2947	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (¬ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧)) → 1 ≠ (abs‘𝑧)))
103	85, 102	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ (abs‘𝑧))
104	33, 34, 84, 103	leneltd 11291	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) < 1)
105	32, 104	eqbrtrd 5108	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) < 1)
106		cnxmet 24747	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
107		1xr 11195	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ^*
108		elbl3 24367	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
109	106, 107, 108	mpanl12 703	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
110	26, 25, 109	sylancr 588	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
111	105, 110	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ (0(ball‘(abs ∘ − ))1))
112	111	expr 456	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
113	112	3impb 1115	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
114	24, 113	biimtrid 242	. . . . . . . 8 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (¬ 𝑧 ∈ {1} → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
115	114	orrd 864	. . . . . . 7 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
116		elun 4094	. . . . . . 7 ⊢ (𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘ − ))1)) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
117	115, 116	sylibr 234	. . . . . 6 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → 𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
118	117	rabssdv 4015	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
119	20, 118	eqsstrid 3961	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
120		ssundif 4428	. . . 4 ⊢ (𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)) ↔ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
121	119, 120	sylib 218	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
122	22, 121	jca 511	. 2 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
123	1, 2, 122	syl2anc 585	1 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 {crab 3390 ∖ cdif 3887 ∪ cun 3888 ⊆ wss 3890 {csn 4568 class class class wbr 5086 dom cdm 5624 ∘ ccom 5628 ⟶wf 6488 ‘cfv 6492 (class class class)co 7360 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 ℕ₀cn0 12428 seqcseq 13954 abscabs 15187 ⇝ cli 15437 ∞Metcxmet 21329 ballcbl 21331

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-er 8636 df-map 8768 df-en 8887 df-dom 8888 df-sdom 8889 df-sup 9348 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-z 12516 df-uz 12780 df-rp 12934 df-xadd 13055 df-seq 13955 df-exp 14015 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-psmet 21336 df-xmet 21337 df-met 21338 df-bl 21339

This theorem is referenced by: abelthlem3 26411 abelthlem6 26414 abelthlem7 26416 abelthlem8 26417 abelthlem9 26418 abelth 26419

W3C validator