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 26632

Description: Lemma for abelth 26641. 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 11220	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ ℂ)
4		0le0 12360	. . . . 5 ⊢ 0 ≤ 0
5		simpl 488	. . . . . . 7 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℝ)
6	5	recnd 11255	. . . . . 6 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑀 ∈ ℂ)
7	6	mul01d 11427	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → (𝑀 · 0) = 0)
8	4, 7	breqtrrid 5154	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 0 ≤ (𝑀 · 0))
9		oveq2 7431	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − 𝑧) = (1 − 1))
10		1m1e0 12331	. . . . . . . 8 ⊢ (1 − 1) = 0
11	9, 10	eqtrdi 2817	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − 𝑧) = 0)
12	11	abs00bd 15368	. . . . . 6 ⊢ (𝑧 = 1 → (abs‘(1 − 𝑧)) = 0)
13		fveq2 6888	. . . . . . . . . 10 ⊢ (𝑧 = 1 → (abs‘𝑧) = (abs‘1))
14		abs1 15374	. . . . . . . . . 10 ⊢ (abs‘1) = 1
15	13, 14	eqtrdi 2817	. . . . . . . . 9 ⊢ (𝑧 = 1 → (abs‘𝑧) = 1)
16	15	oveq2d 7439	. . . . . . . 8 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = (1 − 1))
17	16, 10	eqtrdi 2817	. . . . . . 7 ⊢ (𝑧 = 1 → (1 − (abs‘𝑧)) = 0)
18	17	oveq2d 7439	. . . . . 6 ⊢ (𝑧 = 1 → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 · 0))
19	12, 18	breq12d 5127	. . . . 5 ⊢ (𝑧 = 1 → ((abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧))) ↔ 0 ≤ (𝑀 · 0)))
20		abelth.5	. . . . 5 ⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
21	19, 20	elrab2 3657	. . . 4 ⊢ (1 ∈ 𝑆 ↔ (1 ∈ ℂ ∧ 0 ≤ (𝑀 · 0)))
22	3, 8, 21	sylanbrc 595	. . 3 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 1 ∈ 𝑆)
23		velsn 4610	. . . . . . . . . 10 ⊢ (𝑧 ∈ {1} ↔ 𝑧 = 1)
24	23	necon3bbii 3008	. . . . . . . . 9 ⊢ (¬ 𝑧 ∈ {1} ↔ 𝑧 ≠ 1)
25		simprll 791	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑧 ∈ ℂ)
26		0cn 11216	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ ℂ
27		eqid 2766	. . . . . . . . . . . . . . . 16 ⊢ (abs ∘ − ) = (abs ∘ − )
28	27	cnmetdval 24964	. . . . . . . . . . . . . . 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 11576	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧 − 0) = 𝑧)
31	30	fveq2d 6892	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(𝑧 − 0)) = (abs‘𝑧))
32	29, 31	eqtrd 2801	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) = (abs‘𝑧))
33	25	abscld 15516	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℝ)
34		1red 11227	. . . . . . . . . . . . . 14 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℝ)
35		1re 11226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ ℝ
36		resubcl 11540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((abs‘𝑧) ∈ ℝ ∧ 1 ∈ ℝ) → ((abs‘𝑧) − 1) ∈ ℝ)
37	33, 35, 36	sylancl 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ∈ ℝ)
38		ax-1cn 11176	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 1 ∈ ℂ
39		subcl 11474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (1 − 𝑧) ∈ ℂ)
40	38, 25, 39	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − 𝑧) ∈ ℂ)
41	40	abscld 15516	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘(1 − 𝑧)) ∈ ℝ)
42		simpll 779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 ∈ ℝ)
43		resubcl 11540	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℝ ∧ (abs‘𝑧) ∈ ℝ) → (1 − (abs‘𝑧)) ∈ ℝ)
44	35, 33, 43	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (1 − (abs‘𝑧)) ∈ ℝ)
45	42, 44	remulcld 11257	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) ∈ ℝ)
46	14	oveq2i 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((abs‘𝑧) − (abs‘1)) = ((abs‘𝑧) − 1)
47		abs2dif 15410	. . . . . . . . . . . . . . . . . . . . . . 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 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (abs‘(𝑧 − 1)))
50		abssub 15404	. . . . . . . . . . . . . . . . . . . . . 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 5142	. . . . . . . . . . . . . . . . . . . 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 11385	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((abs‘𝑧) − 1) ≤ (𝑀 · (1 − (abs‘𝑧))))
55	33, 34, 45	lesubaddd 11829	. . . . . . . . . . . . . . . . . . 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 11220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ∈ ℂ)
59	42, 33	remulcld 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℝ)
60	59	recnd 11255	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (abs‘𝑧)) ∈ ℂ)
61	57, 58, 60	addsubd 11608	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
62	33	recnd 11255	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ∈ ℂ)
63	57, 58, 62	subdid 11688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = ((𝑀 · 1) − (𝑀 · (abs‘𝑧))))
64	57	mulridd 11244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 1) = 𝑀)
65	64	oveq1d 7438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · 1) − (𝑀 · (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
66	63, 65	eqtrd 2801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · (1 − (abs‘𝑧))) = (𝑀 − (𝑀 · (abs‘𝑧))))
67	66	oveq1d 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 · (1 − (abs‘𝑧))) + 1) = ((𝑀 − (𝑀 · (abs‘𝑧))) + 1))
68	61, 67	eqtr4d 2804	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) − (𝑀 · (abs‘𝑧))) = ((𝑀 · (1 − (abs‘𝑧))) + 1))
69	56, 68	breqtrrd 5144	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) ≤ ((𝑀 + 1) − (𝑀 · (abs‘𝑧))))
70		peano2re 11401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
71	42, 70	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℝ)
72	59, 33, 71	leaddsub2d 11834	. . . . . . . . . . . . . . . . 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 11253	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) = ((𝑀 · (abs‘𝑧)) + (abs‘𝑧)))
75	71	recnd 11255	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 + 1) ∈ ℂ)
76	75	mulridd 11244	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · 1) = (𝑀 + 1))
77	73, 74, 76	3brtr4d 5148	. . . . . . . . . . . . . . 15 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → ((𝑀 + 1) · (abs‘𝑧)) ≤ ((𝑀 + 1) · 1))
78		0red 11229	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ∈ ℝ)
79		simplr 781	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 ≤ 𝑀)
80	42	ltp1d 12163	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 𝑀 < (𝑀 + 1))
81	78, 42, 71, 79, 80	lelttrd 11386	. . . . . . . . . . . . . . . 16 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 0 < (𝑀 + 1))
82		lemul2 12086	. . . . . . . . . . . . . . . 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 11379	. . . . . . . . . . . . . . 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 3016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → 1 ≠ 𝑧)
89		subeq0 11502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((1 ∈ ℂ ∧ 𝑧 ∈ ℂ) → ((1 − 𝑧) = 0 ↔ 1 = 𝑧))
90	89	necon3bid 3005	. . . . . . . . . . . . . . . . . . . . 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 15402	. . . . . . . . . . . . . . . . . . . 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 5138	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑀 · 0) < (abs‘(1 − 𝑧)))
97		oveq2 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 = (abs‘𝑧) → (1 − 1) = (1 − (abs‘𝑧)))
98	10, 97	eqtr3id 2815	. . . . . . . . . . . . . . . . . . 19 ⊢ (1 = (abs‘𝑧) → 0 = (1 − (abs‘𝑧)))
99	98	oveq2d 7439	. . . . . . . . . . . . . . . . . 18 ⊢ (1 = (abs‘𝑧) → (𝑀 · 0) = (𝑀 · (1 − (abs‘𝑧))))
100	99	breq1d 5124	. . . . . . . . . . . . . . . . 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 2975	. . . . . . . . . . . . . . 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 11382	. . . . . . . . . . . . 13 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (abs‘𝑧) < 1)
105	32, 104	eqbrtrd 5138	. . . . . . . . . . . 12 ⊢ (((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) ∧ ((𝑧 ∈ ℂ ∧ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))) ∧ 𝑧 ≠ 1)) → (𝑧(abs ∘ − )0) < 1)
106		cnxmet 24966	. . . . . . . . . . . . . 14 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
107		1xr 11286	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ^*
108		elbl3 24586	. . . . . . . . . . . . . 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 4110	. . . . . . 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 4031	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
119	20, 118	eqsstrid 3978	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 0 ≤ 𝑀) → 𝑆 ⊆ ({1} ∪ (0(ball‘(abs ∘ − ))1)))
120		ssundif 4453	. . . 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 2146 ≠ wne 2961 {crab 3419 ∖ cdif 3905 ∪ cun 3906 ⊆ wss 3908 {csn 4594 class class class wbr 5114 dom cdm 5666 ∘ ccom 5670 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 − cmin 11459 ℕ₀cn0 12522 seqcseq 14057 abscabs 15311 ⇝ cli 15561 ∞Metcxmet 21544 ballcbl 21546

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-sup 9412 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-n0 12523 df-z 12610 df-uz 12881 df-rp 13035 df-xadd 13156 df-seq 14058 df-exp 14118 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-psmet 21551 df-xmet 21552 df-met 21553 df-bl 21554

This theorem is used by: abelthlem3 26633 abelthlem6 26636 abelthlem7 26638 abelthlem8 26639 abelthlem9 26640 abelth 26641

W3C validator