Metamath Proof Explorer

Theorem stoweidlem49

Description: 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 . Here y is used to represent the final q_n in the paper (the one with n large enough), N represents n in the paper, K represents k , D represents δ, E represents ε, and P represents p . (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem49.1 ⊢ Ⅎ 𝑡 𝑃
stoweidlem49.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem49.3 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
stoweidlem49.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem49.5 ⊢ ( 𝜑 → 𝐷 < 1 )
stoweidlem49.6 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
stoweidlem49.7 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
stoweidlem49.8 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
stoweidlem49.9 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
stoweidlem49.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
stoweidlem49.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem49.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem49.13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem49.14 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
Assertion stoweidlem49 ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem49.1 ⊢ Ⅎ 𝑡 𝑃
2 stoweidlem49.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem49.3 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
4 stoweidlem49.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
5 stoweidlem49.5 ⊢ ( 𝜑 → 𝐷 < 1 )
6 stoweidlem49.6 ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
7 stoweidlem49.7 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
8 stoweidlem49.8 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
9 stoweidlem49.9 ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
10 stoweidlem49.10 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
11 stoweidlem49.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem49.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem49.13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
14 stoweidlem49.14 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
15 breq2 ⊢ ( 𝑗 = 𝑖 → ( ( 1 / 𝐷 ) < 𝑗 ↔ ( 1 / 𝐷 ) < 𝑖 ) )
16 15 cbvrabv ⊢ { 𝑗 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑗 } = { 𝑖 ∈ ℕ ∣ ( 1 / 𝐷 ) < 𝑖 }
17 16 4 5 stoweidlem14 ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℕ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) )
18 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( 1 / ( 𝑘 · 𝐷 ) ) ↑ 𝑖 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( 1 / ( 𝑘 · 𝐷 ) ) ↑ 𝑖 ) )
19 eqid ⊢ ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑖 ) ) = ( 𝑖 ∈ ℕ0 ↦ ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑖 ) )
20 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
22 4 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 𝐷 ∈ ℝ )
24 21 23 remulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝐷 ) ∈ ℝ )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → ( 𝑘 · 𝐷 ) ∈ ℝ )
26 simprl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → 1 < ( 𝑘 · 𝐷 ) )
27 24 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · 𝐷 ) / 2 ) ∈ ℝ )
28 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < 𝑘 )
30 4 rpgt0d ⊢ ( 𝜑 → 0 < 𝐷 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < 𝐷 )
32 21 23 29 31 mulgt0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < ( 𝑘 · 𝐷 ) )
33 2re ⊢ 2 ∈ ℝ
34 2pos ⊢ 0 < 2
35 33 34 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
37 divgt0 ⊢ ( ( ( ( 𝑘 · 𝐷 ) ∈ ℝ ∧ 0 < ( 𝑘 · 𝐷 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 < ( ( 𝑘 · 𝐷 ) / 2 ) )
38 24 32 36 37 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → 0 < ( ( 𝑘 · 𝐷 ) / 2 ) )
39 27 38 elrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 · 𝐷 ) / 2 ) ∈ ℝ+ )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) ∈ ℝ+ )
41 simprr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → ( ( 𝑘 · 𝐷 ) / 2 ) < 1 )
42 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → 𝐸 ∈ ℝ+ )
43 18 19 25 26 40 41 42 stoweidlem7 ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) ∧ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) ) → ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) )
44 43 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) → ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) )
45 44 reximdva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℕ ( 1 < ( 𝑘 · 𝐷 ) ∧ ( ( 𝑘 · 𝐷 ) / 2 ) < 1 ) → ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) )
46 17 45 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) )
47 nfv ⊢ Ⅎ 𝑡 ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ )
48 2 47 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) )
49 nfv ⊢ Ⅎ 𝑡 ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 )
50 48 49 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) )
51 eqid ⊢ ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑛 ) ) ↑ ( 𝑘 ↑ 𝑛 ) ) ) = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑛 ) ) ↑ ( 𝑘 ↑ 𝑛 ) ) )
52 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝑛 ∈ ℕ )
53 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝑘 ∈ ℕ )
54 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝐷 ∈ ℝ+ )
55 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝐷 < 1 )
56 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝑃 ∈ 𝐴 )
57 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝑃 : 𝑇 ⟶ ℝ )
58 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
59 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
60 10 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) ∧ 𝑓 ∈ 𝐴 ) → 𝑓 : 𝑇 ⟶ ℝ )
61 simp1ll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → 𝜑 )
62 61 11 syld3an1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
63 61 12 syld3an1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
64 13 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
65 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → 𝐸 ∈ ℝ+ )
66 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) )
67 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 )
68 1 50 3 51 52 53 54 55 56 57 58 59 60 62 63 64 65 66 67 stoweidlem45 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) ∧ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )
69 68 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ ) ) → ( ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) ) )
70 69 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ℕ ∃ 𝑛 ∈ ℕ ( ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝑘 · 𝐷 ) / 2 ) ↑ 𝑛 ) ) ∧ ( 1 / ( ( 𝑘 · 𝐷 ) ↑ 𝑛 ) ) < 𝐸 ) → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) ) )
71 46 70 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑦 ‘ 𝑡 ) ∧ ( 𝑦 ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑉 ( 1 − 𝐸 ) < ( 𝑦 ‘ 𝑡 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 𝑦 ‘ 𝑡 ) < 𝐸 ) )