stoweidlem5

Description: There exists a δ as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: 0 < δ < 1 , p >= δ on T \ U . Here D is used to represent δ in the paper and Q to represent T \ U in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem5.1	⊢ Ⅎ 𝑡 𝜑
	stoweidlem5.2	⊢ 𝐷 = if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) )
	stoweidlem5.3	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
	stoweidlem5.4	⊢ ( 𝜑 → 𝑄 ⊆ 𝑇 )
	stoweidlem5.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
	stoweidlem5.6	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑄 𝐶 ≤ ( 𝑃 ‘ 𝑡 ) )
Assertion	stoweidlem5	⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ ℝ⁺ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem5.1	⊢ Ⅎ 𝑡 𝜑
2		stoweidlem5.2	⊢ 𝐷 = if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) )
3		stoweidlem5.3	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
4		stoweidlem5.4	⊢ ( 𝜑 → 𝑄 ⊆ 𝑇 )
5		stoweidlem5.5	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
6		stoweidlem5.6	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑄 𝐶 ≤ ( 𝑃 ‘ 𝑡 ) )
7		halfre	⊢ ( 1 / 2 ) ∈ ℝ
8		halfgt0	⊢ 0 < ( 1 / 2 )
9	7 8	elrpii	⊢ ( 1 / 2 ) ∈ ℝ⁺
10		ifcl	⊢ ( ( 𝐶 ∈ ℝ⁺ ∧ ( 1 / 2 ) ∈ ℝ⁺ ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ∈ ℝ⁺ )
11	5 9 10	sylancl	⊢ ( 𝜑 → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ∈ ℝ⁺ )
12	2 11	eqeltrid	⊢ ( 𝜑 → 𝐷 ∈ ℝ⁺ )
13	12	rpred	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
14	7	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
15		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
16	5	rpred	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
17		min2	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ ( 1 / 2 ) )
18	16 7 17	sylancl	⊢ ( 𝜑 → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ ( 1 / 2 ) )
19	2 18	eqbrtrid	⊢ ( 𝜑 → 𝐷 ≤ ( 1 / 2 ) )
20		halflt1	⊢ ( 1 / 2 ) < 1
21	20	a1i	⊢ ( 𝜑 → ( 1 / 2 ) < 1 )
22	13 14 15 19 21	lelttrd	⊢ ( 𝜑 → 𝐷 < 1 )
23	11	rpred	⊢ ( 𝜑 → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ∈ ℝ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ∈ ℝ )
25	16	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → 𝐶 ∈ ℝ )
26	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → 𝑃 : 𝑇 ⟶ ℝ )
27	4	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → 𝑡 ∈ 𝑇 )
28	26 27	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
29		min1	⊢ ( ( 𝐶 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ 𝐶 )
30	16 7 29	sylancl	⊢ ( 𝜑 → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ 𝐶 )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ 𝐶 )
32	6	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → 𝐶 ≤ ( 𝑃 ‘ 𝑡 ) )
33	24 25 28 31 32	letrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → if ( 𝐶 ≤ ( 1 / 2 ) , 𝐶 , ( 1 / 2 ) ) ≤ ( 𝑃 ‘ 𝑡 ) )
34	2 33	eqbrtrid	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑄 ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
35	34	ex	⊢ ( 𝜑 → ( 𝑡 ∈ 𝑄 → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) )
36	1 35	ralrimi	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑄 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
37		eleq1	⊢ ( 𝑑 = 𝐷 → ( 𝑑 ∈ ℝ⁺ ↔ 𝐷 ∈ ℝ⁺ ) )
38		breq1	⊢ ( 𝑑 = 𝐷 → ( 𝑑 < 1 ↔ 𝐷 < 1 ) )
39		breq1	⊢ ( 𝑑 = 𝐷 → ( 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ↔ 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) )
40	39	ralbidv	⊢ ( 𝑑 = 𝐷 → ( ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑄 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) )
41	37 38 40	3anbi123d	⊢ ( 𝑑 = 𝐷 → ( ( 𝑑 ∈ ℝ⁺ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) ↔ ( 𝐷 ∈ ℝ⁺ ∧ 𝐷 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) ) )
42	41	spcegv	⊢ ( 𝐷 ∈ ℝ⁺ → ( ( 𝐷 ∈ ℝ⁺ ∧ 𝐷 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ⁺ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) ) )
43	12 42	syl	⊢ ( 𝜑 → ( ( 𝐷 ∈ ℝ⁺ ∧ 𝐷 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) ) → ∃ 𝑑 ( 𝑑 ∈ ℝ⁺ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) ) )
44	12 22 36 43	mp3and	⊢ ( 𝜑 → ∃ 𝑑 ( 𝑑 ∈ ℝ⁺ ∧ 𝑑 < 1 ∧ ∀ 𝑡 ∈ 𝑄 𝑑 ≤ ( 𝑃 ‘ 𝑡 ) ) )

Metamath Proof Explorer

Theorem stoweidlem5

Proof