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 26741

Description: Lemma for abelth 26750. 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 11283	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ ℂ)
4		0le0 12425	. . . . 5 ⊢ 0 ≤ 0
5		simpl 488	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
6	5	recnd 11318	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
7	6	mul01d 11490	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑀 · 0) = 0)
8	4, 7	breqtrrid 5143	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 0 ≤ (𝑀 · 0))
9		oveq2 7420	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − 𝑧) = (1 − 1))
10		1m1e0 12396	. . . . . . . 8 ⊢ (1 − 1) = 0
11	9, 10	eqtrdi 2812	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − 𝑧) = 0)
12	11	abs00bd 15438	. . . . . 6 ⊢ (𝑧 = 1 → (abs‘(1 − 𝑧)) = 0)
13		fveq2 6877	. . . . . . . . . 10 ⊢ (𝑧 = 1 → (abs‘𝑧) = (abs‘1))
14		abs1 15444	. . . . . . . . . 10 ⊢ (abs‘1) = 1
15	13, 14	eqtrdi 2812	. . . . . . . . 9 ⊢ (𝑧 = 1 → (abs‘𝑧) = 1)
16	15	oveq2d 7428	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = (1 − 1))
17	16, 10	eqtrdi 2812	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = 0)
18	17	oveq2d 7428	. . . . . 6 ⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0))
19	12, 18	breq12d 5116	. . . . 5 ⊢ (𝑧 = 1 → ((abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ 0 ≤ (𝑀 · 0)))
20		abelth.5	. . . . 5 ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
21	19, 20	elrab2 3649	. . . 4 ⊢ (1 ∈ 𝑆 ↔ (1 ∈ ℂ ∧ 0 ≤ (𝑀 · 0)))
22	3, 8, 21	sylanbrc 595	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ 𝑆)
23		velsn 4600	. . . . . . . . . 10 ⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1)
24	23	necon3bbii 3003	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ {1} ↔ 𝑧 ≠ 1)
25		simprll 791	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ ℂ)
26		0cn 11279	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℂ
27		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
28	27	cnmetdval 25069	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
29	25, 26, 28	sylancl 598	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
30	25	subid1d 11639	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧)
31	30	fveq2d 6881	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
32	29, 31	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
33	25	abscld 15586	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℝ)
34		1red 11290	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℝ)
35		1re 11289	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ
36		resubcl 11603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ)
37	33, 35, 36	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ∈ ℝ)
38		ax-1cn 11239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
39		subcl 11537	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − 𝑧) ∈ ℂ)
40	38, 25, 39	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ∈ ℂ)
41	40	abscld 15586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ∈ ℝ)
42		simpll 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℝ)
43		resubcl 11603	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 − (abs‘𝑧)) ∈ ℝ)
44	35, 33, 43	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − (abs‘𝑧)) ∈ ℝ)
45	42, 44	remulcld 11320	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) ∈ ℝ)
46	14	oveq2i 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘𝑧) − (abs‘1)) = ((abs‘𝑧) − 1)
47		abs2dif 15480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
48	25, 38, 47	sylancl 598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
49	46, 48	eqbrtrrid 5141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(𝑧 − 1)))
50		abssub 15474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
51	25, 38, 50	sylancl 598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
52	49, 51	breqtrd 5131	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(1 − 𝑧)))
53		simprlr 792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))))
54	37, 41, 45, 52, 53	letrd 11448	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))))
55	33, 34, 45	lesubaddd 11894	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ (abs‘𝑧) ≤ ((𝑀 · (1 − (abs‘𝑧))) + 1)))
56	54, 55	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 · (1 − (abs‘𝑧))) + 1))
57	6	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℂ)
58		1cnd 11283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℂ)
59	42, 33	remulcld 11320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℝ)
60	59	recnd 11318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℂ)
61	57, 58, 60	addsubd 11671	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
62	33	recnd 11318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℂ)
63	57, 58, 62	subdid 11753	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = ((𝑀 · 1) − (𝑀 · (abs‘𝑧))))
64	57	mulridd 11307	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 1) = 𝑀)
65	64	oveq1d 7427	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
66	63, 65	eqtrd 2796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
67	66	oveq1d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (1 − (abs‘𝑧))) + 1) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
68	61, 67	eqtr4d 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1))
69	56, 68	breqtrrd 5133	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))
70		peano2re 11464	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
71	42, 70	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℝ)
72	59, 33, 71	leaddsub2d 11899	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1) ↔ (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧)))))
73	69, 72	mpbird 260	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)) ≤ (𝑀 + 1))
74	57, 62	adddirp1d 11316	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)))
75	71	recnd 11318	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℂ)
76	75	mulridd 11307	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · 1) = (𝑀 + 1))
77	73, 74, 76	3brtr4d 5137	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))
78		0red 11292	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ∈ ℝ)
79		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ≤ 𝑀)
80	42	ltp1d 12228	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1))
81	78, 42, 71, 79, 80	lelttrd 11449	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (𝑀 + 1))
82		lemul2 12151	. . . . . . . . . . . . . . . 16 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑀 + 1) ∈ ℝ ∧ 0 < (𝑀 + 1))) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)))
83	33, 34, 71, 81, 82	syl112anc 1401	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)))
84	77, 83	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ 1)
85	41, 45, 53	lensymd 11442	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ¬ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧)))
86	7	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) = 0)
87		simprr 785	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ≠ 1)
88	87	necomd 3011	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ 𝑧)
89		subeq0 11565	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧))
90	89	necon3bid 3000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧))
91	38, 25, 90	sylancr 599	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧))
92	88, 91	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ≠ 0)
93		absgt0 15472	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 𝑧) ∈ ℂ → ((1 − 𝑧) ≠ 0 ↔ 0 < (abs‘(1 − 𝑧))))
94	40, 93	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((1 − 𝑧) ≠ 0 ↔ 0 < (abs‘(1 − 𝑧))))
95	92, 94	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (abs‘(1 − 𝑧)))
96	86, 95	eqbrtrd 5127	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1 − 𝑧)))
97		oveq2 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 = (abs‘𝑧) → (1 − 1) = (1 − (abs‘𝑧)))
98	10, 97	eqtr3id 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 = (abs‘𝑧) → 0 = (1 − (abs‘𝑧)))
99	98	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (1 = (abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 − (abs‘𝑧))))
100	99	breq1d 5113	. . . . . . . . . . . . . . . . 17 ⊢ (1 = (abs‘𝑧) → ((𝑀 · 0) < (abs‘(1 − 𝑧)) ↔ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧))))
101	96, 100	syl5ibcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 = (abs‘𝑧) → (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧))))
102	101	necon3bd 2970	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (¬ (𝑀 · (1 − (abs‘𝑧))) < (abs‘(1 − 𝑧)) → 1 ≠ (abs‘𝑧)))
103	85, 102	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ (abs‘𝑧))
104	33, 34, 84, 103	leneltd 11445	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) < 1)
105	32, 104	eqbrtrd 5127	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) < 1)
106		cnxmet 25071	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
107		1xr 11349	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ^*
108		elbl3 24691	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
109	106, 107, 108	mpanl12 715	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
110	26, 25, 109	sylancr 599	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
111	105, 110	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ (0(ball‘(abs ∘ − ))1))
112	111	expr 462	. . . . . . . . . 10 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ (𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
113	112	3impb 1132	. . . . . . . . 9 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ≠ 1 → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
114	24, 113	biimtrid 245	. . . . . . . 8 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (¬ 𝑧 ∈ {1} → 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
115	114	orrd 877	. . . . . . 7 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
116		elun 4100	. . . . . . 7 ⊢ (𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘ − ))1)) ↔ (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
117	115, 116	sylibr 237	. . . . . 6 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → 𝑧 ∈ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
118	117	rabssdv 4022	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
119	20, 118	eqsstrid 3969	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
120		ssundif 4443	. . . 4 ⊢ (𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)) ↔ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
121	119, 120	sylib 221	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
122	22, 121	jca 521	. 2 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
123	1, 2, 122	syl2anc 596	1 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 {crab 3413 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 {csn 4584 class class class wbr 5103 dom cdm 5651 ∘ ccom 5655 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ℂcc 11179 ℝcr 11180 0cc0 11181 1c1 11182 + caddc 11184 · cmul 11186 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11522 ℕ₀cn0 12587 seqcseq 14124 abscabs 15381 ⇝ cli 15631 ∞Metcxmet 21643 ballcbl 21645

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258 ax-pre-sup 11259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-sup 9418 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-div 11955 df-nn 12317 df-2 12386 df-3 12387 df-n0 12588 df-z 12675 df-uz 12947 df-rp 13102 df-xadd 13223 df-seq 14125 df-exp 14185 df-cj 15246 df-re 15247 df-im 15248 df-sqrt 15382 df-abs 15383 df-psmet 21650 df-xmet 21651 df-met 21652 df-bl 21653

This theorem is used by: abelthlem3 26742 abelthlem6 26745 abelthlem7 26747 abelthlem8 26748 abelthlem9 26749 abelth 26750

W3C validator