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 ⊢ Ⅎ 𝑡 𝑃
stoweidlem45.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem45.3 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
stoweidlem45.4 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
stoweidlem45.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
stoweidlem45.6 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
stoweidlem45.7 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem45.8 ⊢ ( 𝜑 → 𝐷 < 1 )
stoweidlem45.9 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
stoweidlem45.10 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
stoweidlem45.11 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
stoweidlem45.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
stoweidlem45.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem45.14 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem45.15 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem45.16 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem45.17 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem45.18 ⊢ ( 𝜑 → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) )
stoweidlem45.19 ⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) < 𝐸 )
Assertion stoweidlem45 ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem45.1 ⊢ Ⅎ 𝑡 𝑃
2 stoweidlem45.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem45.3 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
4 stoweidlem45.4 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
5 stoweidlem45.5 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6 stoweidlem45.6 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
7 stoweidlem45.7 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
8 stoweidlem45.8 ⊢ ( 𝜑 → 𝐷 < 1 )
9 stoweidlem45.9 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
10 stoweidlem45.10 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
11 stoweidlem45.11 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
12 stoweidlem45.12 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
13 stoweidlem45.13 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
14 stoweidlem45.14 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
15 stoweidlem45.15 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
16 stoweidlem45.16 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
17 stoweidlem45.17 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
18 stoweidlem45.18 ⊢ ( 𝜑 → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) )
19 stoweidlem45.19 ⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) < 𝐸 )
20 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
21 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ 1 ) = ( 𝑡 ∈ 𝑇 ↦ 1 )
22 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) )
23 5 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
24 6 23 nnexpcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ )
25 1 2 4 20 21 22 9 10 13 14 15 16 5 24 stoweidlem40 ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
26 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
27 10 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
28 23 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℕ0 )
29 27 28 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ )
30 26 29 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ )
31 6 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
32 31 23 nn0expcld ⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
34 1m1e0 ⊢ ( 1 − 1 ) = 0
35 11 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
36 35 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑃 ‘ 𝑡 ) )
37 35 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) ≤ 1 )
38 exple1 ⊢ ( ( ( ( 𝑃 ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ≤ 1 )
39 27 36 37 28 38 syl31anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ≤ 1 )
40 29 26 26 39 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − 1 ) ≤ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
41 34 40 eqbrtrrid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
42 30 33 41 expge0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
43 4 10 23 31 stoweidlem12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
44 42 43 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑄 ‘ 𝑡 ) )
45 0red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ∈ ℝ )
46 27 28 36 expge0d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) )
47 45 29 26 46 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ≤ ( 1 − 0 ) )
48 1m0e1 ⊢ ( 1 − 0 ) = 1
49 47 48 breqtrdi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ≤ 1 )
50 exple1 ⊢ ( ( ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ ∧ 0 ≤ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∧ ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ≤ 1 ) ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 )
51 30 41 49 33 50 syl31anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ 1 )
52 43 51 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) ≤ 1 )
53 44 52 jca ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) )
54 53 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) ) )
55 2 54 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) )
56 3 4 10 23 31 7 17 18 11 stoweidlem24 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) )
57 56 ex ⊢ ( 𝜑 → ( 𝑡 ∈ 𝑉 → ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) ) )
58 2 57 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) )
59 4 5 6 7 10 11 12 17 19 stoweidlem25 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) < 𝐸 )
60 59 ex ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → ( 𝑄 ‘ 𝑡 ) < 𝐸 ) )
61 2 60 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑄 ‘ 𝑡 ) < 𝐸 )
62 nfmpt1 ⊢ Ⅎ 𝑡 ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
63 4 62 nfcxfr ⊢ Ⅎ 𝑡 𝑄
64 63 nfeq2 ⊢ Ⅎ 𝑡 𝑦 = 𝑄
65 fveq1 ⊢ ( 𝑦 = 𝑄 → ( 𝑦 ‘ 𝑡 ) = ( 𝑄 ‘ 𝑡 ) )
66 65 breq2d ⊢ ( 𝑦 = 𝑄 → ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ↔ 0 ≤ ( 𝑄 ‘ 𝑡 ) ) )
67 65 breq1d ⊢ ( 𝑦 = 𝑄 → ( ( 𝑦 ‘ 𝑡 ) ≤ 1 ↔ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) )
68 66 67 anbi12d ⊢ ( 𝑦 = 𝑄 → ( ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) ) )
69 64 68 ralbid ⊢ ( 𝑦 = 𝑄 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) ) )
70 65 breq2d ⊢ ( 𝑦 = 𝑄 → ( ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ↔ ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) ) )
71 64 70 ralbid ⊢ ( 𝑦 = 𝑄 → ( ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) ) )
72 65 breq1d ⊢ ( 𝑦 = 𝑄 → ( ( 𝑦 ‘ 𝑡 ) < 𝐸 ↔ ( 𝑄 ‘ 𝑡 ) < 𝐸 ) )
73 64 72 ralbid ⊢ ( 𝑦 = 𝑄 → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑄 ‘ 𝑡 ) < 𝐸 ) )
74 69 71 73 3anbi123d ⊢ ( 𝑦 = 𝑄 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑄 ‘ 𝑡 ) < 𝐸 ) ) )
75 74 rspcev ⊢ ( ( 𝑄 ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑄 ‘ 𝑡 ) ∧ ( 𝑄 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑄 ‘ 𝑡 ) < 𝐸 ) ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )
76 25 55 58 61 75 syl13anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )