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	⊢ ( 𝜑 → 𝐴 : ℕ₀ ⟶ ℂ )
	abelth.2	⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
	abelth.3	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	abelth.4	⊢ ( 𝜑 → 0 ≤ 𝑀 )
	abelth.5	⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
Assertion	abelthlem2	⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )

Proof

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

Metamath Proof Explorer

Theorem abelthlem2

Proof