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 26494

Description: Lemma for abelth 26503. 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 11285	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ ℂ)
4		0le0 12394	. . . . 5 ⊢ 0 ≤ 0
5		simpl 482	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
6	5	recnd 11318	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
7	6	mul01d 11489	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑀 · 0) = 0)
8	4, 7	breqtrrid 5204	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 0 ≤ (𝑀 · 0))
9		oveq2 7456	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − 𝑧) = (1 − 1))
10		1m1e0 12365	. . . . . . . 8 ⊢ (1 − 1) = 0
11	9, 10	eqtrdi 2796	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − 𝑧) = 0)
12	11	abs00bd 15340	. . . . . 6 ⊢ (𝑧 = 1 → (abs‘(1 − 𝑧)) = 0)
13		fveq2 6920	. . . . . . . . . 10 ⊢ (𝑧 = 1 → (abs‘𝑧) = (abs‘1))
14		abs1 15346	. . . . . . . . . 10 ⊢ (abs‘1) = 1
15	13, 14	eqtrdi 2796	. . . . . . . . 9 ⊢ (𝑧 = 1 → (abs‘𝑧) = 1)
16	15	oveq2d 7464	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = (1 − 1))
17	16, 10	eqtrdi 2796	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = 0)
18	17	oveq2d 7464	. . . . . 6 ⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0))
19	12, 18	breq12d 5179	. . . . 5 ⊢ (𝑧 = 1 → ((abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ 0 ≤ (𝑀 · 0)))
20		abelth.5	. . . . 5 ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
21	19, 20	elrab2 3711	. . . 4 ⊢ (1 ∈ 𝑆 ↔ (1 ∈ ℂ ∧ 0 ≤ (𝑀 · 0)))
22	3, 8, 21	sylanbrc 582	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ 𝑆)
23		velsn 4664	. . . . . . . . . 10 ⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1)
24	23	necon3bbii 2994	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ {1} ↔ 𝑧 ≠ 1)
25		simprll 778	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ ℂ)
26		0cn 11282	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℂ
27		eqid 2740	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
28	27	cnmetdval 24812	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ ℂ ∧ 0 ∈ ℂ) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
29	25, 26, 28	sylancl 585	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘(𝑧 − 0)))
30	25	subid1d 11636	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧)
31	30	fveq2d 6924	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
32	29, 31	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
33	25	abscld 15485	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℝ)
34		1red 11291	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℝ)
35		1re 11290	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ
36		resubcl 11600	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ)
37	33, 35, 36	sylancl 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ∈ ℝ)
38		ax-1cn 11242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
39		subcl 11535	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − 𝑧) ∈ ℂ)
40	38, 25, 39	sylancr 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ∈ ℂ)
41	40	abscld 15485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ∈ ℝ)
42		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℝ)
43		resubcl 11600	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 − (abs‘𝑧)) ∈ ℝ)
44	35, 33, 43	sylancr 586	. . . . . . . . . . . . . . . . . . . . 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 7459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘𝑧) − (abs‘1)) = ((abs‘𝑧) − 1)
47		abs2dif 15381	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
48	25, 38, 47	sylancl 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − (abs‘1)) ≤ (abs‘(𝑧 − 1)))
49	46, 48	eqbrtrrid 5202	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(𝑧 − 1)))
50		abssub 15375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℂ ∧ 1 ∈ ℂ) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
51	25, 38, 50	sylancl 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 1)) = (abs‘(1 − 𝑧)))
52	49, 51	breqtrd 5192	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(1 − 𝑧)))
53		simprlr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))))
54	37, 41, 45, 52, 53	letrd 11447	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))))
55	33, 34, 45	lesubaddd 11887	. . . . . . . . . . . . . . . . . . 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 11285	. . . . . . . . . . . . . . . . . . . 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 11668	. . . . . . . . . . . . . . . . . . 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 11746	. . . . . . . . . . . . . . . . . . . . 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 7463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
66	63, 65	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
67	66	oveq1d 7463	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (1 − (abs‘𝑧))) + 1) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
68	61, 67	eqtr4d 2783	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1))
69	56, 68	breqtrrd 5194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))
70		peano2re 11463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
71	42, 70	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℝ)
72	59, 33, 71	leaddsub2d 11892	. . . . . . . . . . . . . . . . 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 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 5198	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))
78		0red 11293	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ∈ ℝ)
79		simplr 768	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ≤ 𝑀)
80	42	ltp1d 12225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1))
81	78, 42, 71, 79, 80	lelttrd 11448	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (𝑀 + 1))
82		lemul2 12147	. . . . . . . . . . . . . . . 16 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝑀 + 1) ∈ ℝ ∧ 0 < (𝑀 + 1))) → ((abs‘𝑧) ≤ 1 ↔ ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1)))
83	33, 34, 71, 81, 82	syl112anc 1374	. . . . . . . . . . . . . . 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 11441	. . . . . . . . . . . . . . 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 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ≠ 1)
88	87	necomd 3002	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ 𝑧)
89		subeq0 11562	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧))
90	89	necon3bid 2991	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) ≠ 0 ↔ 1 ≠ 𝑧))
91	38, 25, 90	sylancr 586	. . . . . . . . . . . . . . . . . . . 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 15373	. . . . . . . . . . . . . . . . . . . 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 5188	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1 − 𝑧)))
97		oveq2 7456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 = (abs‘𝑧) → (1 − 1) = (1 − (abs‘𝑧)))
98	10, 97	eqtr3id 2794	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 = (abs‘𝑧) → 0 = (1 − (abs‘𝑧)))
99	98	oveq2d 7464	. . . . . . . . . . . . . . . . . 18 ⊢ (1 = (abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 − (abs‘𝑧))))
100	99	breq1d 5176	. . . . . . . . . . . . . . . . 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 2960	. . . . . . . . . . . . . . 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 11444	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) < 1)
105	32, 104	eqbrtrd 5188	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) < 1)
106		cnxmet 24814	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
107		1xr 11349	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ^*
108		elbl3 24423	. . . . . . . . . . . . . 14 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ ℝ^*) ∧ (0 ∈ ℂ ∧ 𝑧 ∈ ℂ)) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
109	106, 107, 108	mpanl12 701	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑧 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑧(abs ∘ − )0) < 1))
110	26, 25, 109	sylancr 586	. . . . . . . . . . . 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 862	. . . . . . 7 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ 𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) → (𝑧 ∈ {1} ∨ 𝑧 ∈ (0(ball‘(abs ∘ − ))1)))
116		elun 4176	. . . . . . 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 4098	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
119	20, 118	eqsstrid 4057	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
120		ssundif 4511	. . . 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 583	1 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 ∧ w3a 1087 = wceq 1537 ∈ wcel 2108 ≠ wne 2946 {crab 3443 ∖ cdif 3973 ∪ cun 3974 ⊆ wss 3976 {csn 4648 class class class wbr 5166 dom cdm 5700 ∘ ccom 5704 ⟶wf 6569 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 ℝcr 11183 0cc0 11184 1c1 11185 + caddc 11187 · cmul 11189 ℝ^*cxr 11323 < clt 11324 ≤ cle 11325 − cmin 11520 ℕ₀cn0 12553 seqcseq 14052 abscabs 15283 ⇝ cli 15530 ∞Metcxmet 21372 ballcbl 21374

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-er 8763 df-map 8886 df-en 9004 df-dom 9005 df-sdom 9006 df-sup 9511 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-n0 12554 df-z 12640 df-uz 12904 df-rp 13058 df-xadd 13176 df-seq 14053 df-exp 14113 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-psmet 21379 df-xmet 21380 df-met 21381 df-bl 21382

This theorem is referenced by: abelthlem3 26495 abelthlem6 26498 abelthlem7 26500 abelthlem8 26501 abelthlem9 26502 abelth 26503

W3C validator