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 = if C ≤ 1 2 C 1 2
stoweidlem5.3 ⊢ φ → P : T ⟶ ℝ
stoweidlem5.4 ⊢ φ → Q ⊆ T
stoweidlem5.5 ⊢ φ → C ∈ ℝ +
stoweidlem5.6 ⊢ φ → ∀ t ∈ Q C ≤ P ⁡ t
Assertion stoweidlem5 ⊢ φ → ∃ d d ∈ ℝ + ∧ d < 1 ∧ ∀ t ∈ Q d ≤ P ⁡ t

Proof

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