# Metamath Proof Explorer

## Theorem stoweidlem45

Description: This lemma proves that, given an appropriate K (in another theorem we prove such a K exists), there exists a function q_n as in the proof of Lemma 1 in BrosowskiDeutsh p. 91 ( at the top of page 91): 0 <= q_n <= 1 , q_n < ε on T \ U, and q_n > 1 - ε on V . We use y to represent the final q_n in the paper (the one with n large enough), N to represent n in the paper, K to represent k , D to represent δ, E to represent ε, and P to represent p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem45.1 $⊢ Ⅎ _ t P$
stoweidlem45.2 $⊢ Ⅎ t φ$
stoweidlem45.3 $⊢ V = t ∈ T | P ⁡ t < D 2$
stoweidlem45.4 $⊢ Q = t ∈ T ⟼ 1 − P ⁡ t N K N$
stoweidlem45.5 $⊢ φ → N ∈ ℕ$
stoweidlem45.6 $⊢ φ → K ∈ ℕ$
stoweidlem45.7 $⊢ φ → D ∈ ℝ +$
stoweidlem45.8 $⊢ φ → D < 1$
stoweidlem45.9 $⊢ φ → P ∈ A$
stoweidlem45.10 $⊢ φ → P : T ⟶ ℝ$
stoweidlem45.11 $⊢ φ → ∀ t ∈ T 0 ≤ P ⁡ t ∧ P ⁡ t ≤ 1$
stoweidlem45.12 $⊢ φ → ∀ t ∈ T ∖ U D ≤ P ⁡ t$
stoweidlem45.13 $⊢ φ ∧ f ∈ A → f : T ⟶ ℝ$
stoweidlem45.14 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A$
stoweidlem45.15 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A$
stoweidlem45.16 $⊢ φ ∧ x ∈ ℝ → t ∈ T ⟼ x ∈ A$
stoweidlem45.17 $⊢ φ → E ∈ ℝ +$
stoweidlem45.18 $⊢ φ → 1 − E < 1 − K ⁢ D 2 N$
stoweidlem45.19 $⊢ φ → 1 K ⁢ D N < E$
Assertion stoweidlem45 $⊢ φ → ∃ y ∈ A ∀ t ∈ T 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < y ⁡ t ∧ ∀ t ∈ T ∖ U y ⁡ t < E$

### Proof

Step Hyp Ref Expression
1 stoweidlem45.1 $⊢ Ⅎ _ t P$
2 stoweidlem45.2 $⊢ Ⅎ t φ$
3 stoweidlem45.3 $⊢ V = t ∈ T | P ⁡ t < D 2$
4 stoweidlem45.4 $⊢ Q = t ∈ T ⟼ 1 − P ⁡ t N K N$
5 stoweidlem45.5 $⊢ φ → N ∈ ℕ$
6 stoweidlem45.6 $⊢ φ → K ∈ ℕ$
7 stoweidlem45.7 $⊢ φ → D ∈ ℝ +$
8 stoweidlem45.8 $⊢ φ → D < 1$
9 stoweidlem45.9 $⊢ φ → P ∈ A$
10 stoweidlem45.10 $⊢ φ → P : T ⟶ ℝ$
11 stoweidlem45.11 $⊢ φ → ∀ t ∈ T 0 ≤ P ⁡ t ∧ P ⁡ t ≤ 1$
12 stoweidlem45.12 $⊢ φ → ∀ t ∈ T ∖ U D ≤ P ⁡ t$
13 stoweidlem45.13 $⊢ φ ∧ f ∈ A → f : T ⟶ ℝ$
14 stoweidlem45.14 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t + g ⁡ t ∈ A$
15 stoweidlem45.15 $⊢ φ ∧ f ∈ A ∧ g ∈ A → t ∈ T ⟼ f ⁡ t ⁢ g ⁡ t ∈ A$
16 stoweidlem45.16 $⊢ φ ∧ x ∈ ℝ → t ∈ T ⟼ x ∈ A$
17 stoweidlem45.17 $⊢ φ → E ∈ ℝ +$
18 stoweidlem45.18 $⊢ φ → 1 − E < 1 − K ⁢ D 2 N$
19 stoweidlem45.19 $⊢ φ → 1 K ⁢ D N < E$
20 eqid $⊢ t ∈ T ⟼ 1 − P ⁡ t N = t ∈ T ⟼ 1 − P ⁡ t N$
21 eqid $⊢ t ∈ T ⟼ 1 = t ∈ T ⟼ 1$
22 eqid $⊢ t ∈ T ⟼ P ⁡ t N = t ∈ T ⟼ P ⁡ t N$
23 5 nnnn0d $⊢ φ → N ∈ ℕ 0$
24 6 23 nnexpcld $⊢ φ → K N ∈ ℕ$
25 1 2 4 20 21 22 9 10 13 14 15 16 5 24 stoweidlem40 $⊢ φ → Q ∈ A$
26 1red $⊢ φ ∧ t ∈ T → 1 ∈ ℝ$
27 10 ffvelrnda $⊢ φ ∧ t ∈ T → P ⁡ t ∈ ℝ$
28 23 adantr $⊢ φ ∧ t ∈ T → N ∈ ℕ 0$
29 27 28 reexpcld $⊢ φ ∧ t ∈ T → P ⁡ t N ∈ ℝ$
30 26 29 resubcld $⊢ φ ∧ t ∈ T → 1 − P ⁡ t N ∈ ℝ$
31 6 nnnn0d $⊢ φ → K ∈ ℕ 0$
32 31 23 nn0expcld $⊢ φ → K N ∈ ℕ 0$
33 32 adantr $⊢ φ ∧ t ∈ T → K N ∈ ℕ 0$
34 1m1e0 $⊢ 1 − 1 = 0$
35 11 r19.21bi $⊢ φ ∧ t ∈ T → 0 ≤ P ⁡ t ∧ P ⁡ t ≤ 1$
36 35 simpld $⊢ φ ∧ t ∈ T → 0 ≤ P ⁡ t$
37 35 simprd $⊢ φ ∧ t ∈ T → P ⁡ t ≤ 1$
38 exple1 $⊢ P ⁡ t ∈ ℝ ∧ 0 ≤ P ⁡ t ∧ P ⁡ t ≤ 1 ∧ N ∈ ℕ 0 → P ⁡ t N ≤ 1$
39 27 36 37 28 38 syl31anc $⊢ φ ∧ t ∈ T → P ⁡ t N ≤ 1$
40 29 26 26 39 lesub2dd $⊢ φ ∧ t ∈ T → 1 − 1 ≤ 1 − P ⁡ t N$
41 34 40 eqbrtrrid $⊢ φ ∧ t ∈ T → 0 ≤ 1 − P ⁡ t N$
42 30 33 41 expge0d $⊢ φ ∧ t ∈ T → 0 ≤ 1 − P ⁡ t N K N$
43 4 10 23 31 stoweidlem12 $⊢ φ ∧ t ∈ T → Q ⁡ t = 1 − P ⁡ t N K N$
44 42 43 breqtrrd $⊢ φ ∧ t ∈ T → 0 ≤ Q ⁡ t$
45 0red $⊢ φ ∧ t ∈ T → 0 ∈ ℝ$
46 27 28 36 expge0d $⊢ φ ∧ t ∈ T → 0 ≤ P ⁡ t N$
47 45 29 26 46 lesub2dd $⊢ φ ∧ t ∈ T → 1 − P ⁡ t N ≤ 1 − 0$
48 1m0e1 $⊢ 1 − 0 = 1$
49 47 48 breqtrdi $⊢ φ ∧ t ∈ T → 1 − P ⁡ t N ≤ 1$
50 exple1 $⊢ 1 − P ⁡ t N ∈ ℝ ∧ 0 ≤ 1 − P ⁡ t N ∧ 1 − P ⁡ t N ≤ 1 ∧ K N ∈ ℕ 0 → 1 − P ⁡ t N K N ≤ 1$
51 30 41 49 33 50 syl31anc $⊢ φ ∧ t ∈ T → 1 − P ⁡ t N K N ≤ 1$
52 43 51 eqbrtrd $⊢ φ ∧ t ∈ T → Q ⁡ t ≤ 1$
53 44 52 jca $⊢ φ ∧ t ∈ T → 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1$
54 53 ex $⊢ φ → t ∈ T → 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1$
55 2 54 ralrimi $⊢ φ → ∀ t ∈ T 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1$
56 3 4 10 23 31 7 17 18 11 stoweidlem24 $⊢ φ ∧ t ∈ V → 1 − E < Q ⁡ t$
57 56 ex $⊢ φ → t ∈ V → 1 − E < Q ⁡ t$
58 2 57 ralrimi $⊢ φ → ∀ t ∈ V 1 − E < Q ⁡ t$
59 4 5 6 7 10 11 12 17 19 stoweidlem25 $⊢ φ ∧ t ∈ T ∖ U → Q ⁡ t < E$
60 59 ex $⊢ φ → t ∈ T ∖ U → Q ⁡ t < E$
61 2 60 ralrimi $⊢ φ → ∀ t ∈ T ∖ U Q ⁡ t < E$
62 nfmpt1 $⊢ Ⅎ _ t t ∈ T ⟼ 1 − P ⁡ t N K N$
63 4 62 nfcxfr $⊢ Ⅎ _ t Q$
64 63 nfeq2 $⊢ Ⅎ t y = Q$
65 fveq1 $⊢ y = Q → y ⁡ t = Q ⁡ t$
66 65 breq2d $⊢ y = Q → 0 ≤ y ⁡ t ↔ 0 ≤ Q ⁡ t$
67 65 breq1d $⊢ y = Q → y ⁡ t ≤ 1 ↔ Q ⁡ t ≤ 1$
68 66 67 anbi12d $⊢ y = Q → 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ↔ 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1$
69 64 68 ralbid $⊢ y = Q → ∀ t ∈ T 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1$
70 65 breq2d $⊢ y = Q → 1 − E < y ⁡ t ↔ 1 − E < Q ⁡ t$
71 64 70 ralbid $⊢ y = Q → ∀ t ∈ V 1 − E < y ⁡ t ↔ ∀ t ∈ V 1 − E < Q ⁡ t$
72 65 breq1d $⊢ y = Q → y ⁡ t < E ↔ Q ⁡ t < E$
73 64 72 ralbid $⊢ y = Q → ∀ t ∈ T ∖ U y ⁡ t < E ↔ ∀ t ∈ T ∖ U Q ⁡ t < E$
74 69 71 73 3anbi123d $⊢ y = Q → ∀ t ∈ T 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < y ⁡ t ∧ ∀ t ∈ T ∖ U y ⁡ t < E ↔ ∀ t ∈ T 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < Q ⁡ t ∧ ∀ t ∈ T ∖ U Q ⁡ t < E$
75 74 rspcev $⊢ Q ∈ A ∧ ∀ t ∈ T 0 ≤ Q ⁡ t ∧ Q ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < Q ⁡ t ∧ ∀ t ∈ T ∖ U Q ⁡ t < E → ∃ y ∈ A ∀ t ∈ T 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < y ⁡ t ∧ ∀ t ∈ T ∖ U y ⁡ t < E$
76 25 55 58 61 75 syl13anc $⊢ φ → ∃ y ∈ A ∀ t ∈ T 0 ≤ y ⁡ t ∧ y ⁡ t ≤ 1 ∧ ∀ t ∈ V 1 − E < y ⁡ t ∧ ∀ t ∈ T ∖ U y ⁡ t < E$