Metamath Proof Explorer

Theorem 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 ⊢Ⅎtφ
stoweidlem5.2 ⊢D=ifC≤12C12
stoweidlem5.3 ⊢φ→P:T⟶ℝ
stoweidlem5.4 ⊢φ→Q⊆T
stoweidlem5.5 ⊢φ→C∈ℝ+
stoweidlem5.6 ⊢φ→∀t∈QC≤P⁡t
Assertion stoweidlem5 ⊢φ→∃dd∈ℝ+∧d<1∧∀t∈Qd≤P⁡t

Proof

Step Hyp Ref Expression
1 stoweidlem5.1 ⊢Ⅎtφ
2 stoweidlem5.2 ⊢D=ifC≤12C12
3 stoweidlem5.3 ⊢φ→P:T⟶ℝ
4 stoweidlem5.4 ⊢φ→Q⊆T
5 stoweidlem5.5 ⊢φ→C∈ℝ+
6 stoweidlem5.6 ⊢φ→∀t∈QC≤P⁡t
7 halfre ⊢12∈ℝ
8 halfgt0 ⊢0<12
9 7 8 elrpii ⊢12∈ℝ+
10 ifcl ⊢C∈ℝ+∧12∈ℝ+→ifC≤12C12∈ℝ+
11 5 9 10 sylancl ⊢φ→ifC≤12C12∈ℝ+
12 2 11 eqeltrid ⊢φ→D∈ℝ+
13 12 rpred ⊢φ→D∈ℝ
14 7 a1i ⊢φ→12∈ℝ
15 1red ⊢φ→1∈ℝ
16 5 rpred ⊢φ→C∈ℝ
17 min2 ⊢C∈ℝ∧12∈ℝ→ifC≤12C12≤12
18 16 7 17 sylancl ⊢φ→ifC≤12C12≤12
19 2 18 eqbrtrid ⊢φ→D≤12
20 halflt1 ⊢12<1
21 20 a1i ⊢φ→12<1
22 13 14 15 19 21 lelttrd ⊢φ→D<1
23 11 rpred ⊢φ→ifC≤12C12∈ℝ
24 23 adantr ⊢φ∧t∈Q→ifC≤12C12∈ℝ
25 16 adantr ⊢φ∧t∈Q→C∈ℝ
26 3 adantr ⊢φ∧t∈Q→P:T⟶ℝ
27 4 sselda ⊢φ∧t∈Q→t∈T
28 26 27 ffvelcdmd ⊢φ∧t∈Q→P⁡t∈ℝ
29 min1 ⊢C∈ℝ∧12∈ℝ→ifC≤12C12≤C
30 16 7 29 sylancl ⊢φ→ifC≤12C12≤C
31 30 adantr ⊢φ∧t∈Q→ifC≤12C12≤C
32 6 r19.21bi ⊢φ∧t∈Q→C≤P⁡t
33 24 25 28 31 32 letrd ⊢φ∧t∈Q→ifC≤12C12≤P⁡t
34 2 33 eqbrtrid ⊢φ∧t∈Q→D≤P⁡t
35 34 ex ⊢φ→t∈Q→D≤P⁡t
36 1 35 ralrimi ⊢φ→∀t∈QD≤P⁡t
37 eleq1 ⊢d=D→d∈ℝ+↔D∈ℝ+
38 breq1 ⊢d=D→d<1↔D<1
39 breq1 ⊢d=D→d≤P⁡t↔D≤P⁡t
40 39 ralbidv ⊢d=D→∀t∈Qd≤P⁡t↔∀t∈QD≤P⁡t
41 37 38 40 3anbi123d ⊢d=D→d∈ℝ+∧d<1∧∀t∈Qd≤P⁡t↔D∈ℝ+∧D<1∧∀t∈QD≤P⁡t
42 41 spcegv ⊢D∈ℝ+→D∈ℝ+∧D<1∧∀t∈QD≤P⁡t→∃dd∈ℝ+∧d<1∧∀t∈Qd≤P⁡t
43 12 42 syl ⊢φ→D∈ℝ+∧D<1∧∀t∈QD≤P⁡t→∃dd∈ℝ+∧d<1∧∀t∈Qd≤P⁡t
44 12 22 36 43 mp3and ⊢φ→∃dd∈ℝ+∧d<1∧∀t∈Qd≤P⁡t