Metamath Proof Explorer

Theorem stoweidlem24

Description: This lemma proves that for n sufficiently large, q_n( t ) > ( 1 - epsilon ), for all t in V : see Lemma 1 BrosowskiDeutsh p. 90, (at the bottom of page 90). Q is used to represent q_n in the paper, N to represent n in the paper, K to represent k , D to represent δ, and E to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem24.1 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
stoweidlem24.2 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
stoweidlem24.3 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
stoweidlem24.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
stoweidlem24.5 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
stoweidlem24.6 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
stoweidlem24.8 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem24.9 ⊢ ( 𝜑 → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) )
stoweidlem24.10 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
Assertion stoweidlem24 ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem24.1 ⊢ 𝑉 = { 𝑡 ∈ 𝑇 ∣ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) }
2 stoweidlem24.2 ⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
3 stoweidlem24.3 ⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
4 stoweidlem24.4 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 stoweidlem24.5 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
6 stoweidlem24.6 ⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
7 stoweidlem24.8 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
8 stoweidlem24.9 ⊢ ( 𝜑 → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) )
9 stoweidlem24.10 ⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
10 1red ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 1 ∈ ℝ )
11 7 rpred ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐸 ∈ ℝ )
13 10 12 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) ∈ ℝ )
14 5 nn0red ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐾 ∈ ℝ )
16 3 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑃 : 𝑇 ⟶ ℝ )
17 1 rabeq2i ⊢ ( 𝑡 ∈ 𝑉 ↔ ( 𝑡 ∈ 𝑇 ∧ ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) ) )
18 17 simplbi ⊢ ( 𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑇 )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑡 ∈ 𝑇 )
20 16 19 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
21 15 20 remulcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ∈ ℝ )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝑁 ∈ ℕ0 )
23 21 22 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ∈ ℝ )
24 10 23 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ) ∈ ℝ )
25 20 22 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ )
26 10 25 resubcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ )
27 5 4 jca ⊢ ( 𝜑 → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) )
29 nn0expcl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
30 28 29 syl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
31 26 30 reexpcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
32 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
33 6 rpred ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
34 14 33 remulcld ⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ∈ ℝ )
35 34 rehalfcld ⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) / 2 ) ∈ ℝ )
36 35 4 reexpcld ⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ∈ ℝ )
37 32 36 resubcld ⊢ ( 𝜑 → ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) ∈ ℝ )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) ∈ ℝ )
39 8 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) )
40 36 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ∈ ℝ )
41 35 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 · 𝐷 ) / 2 ) ∈ ℝ )
42 5 nn0ge0d ⊢ ( 𝜑 → 0 ≤ 𝐾 )
43 14 42 jca ⊢ ( 𝜑 → ( 𝐾 ∈ ℝ ∧ 0 ≤ 𝐾 ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 ∈ ℝ ∧ 0 ≤ 𝐾 ) )
45 9 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
46 45 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 0 ≤ ( 𝑃 ‘ 𝑡 ) )
47 18 46 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 0 ≤ ( 𝑃 ‘ 𝑡 ) )
48 mulge0 ⊢ ( ( ( 𝐾 ∈ ℝ ∧ 0 ≤ 𝐾 ) ∧ ( ( 𝑃 ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ‘ 𝑡 ) ) ) → 0 ≤ ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) )
49 44 20 47 48 syl12anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 0 ≤ ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) )
50 33 rehalfcld ⊢ ( 𝜑 → ( 𝐷 / 2 ) ∈ ℝ )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐷 / 2 ) ∈ ℝ )
52 17 simprbi ⊢ ( 𝑡 ∈ 𝑉 → ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) < ( 𝐷 / 2 ) )
54 20 51 53 ltled ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ≤ ( 𝐷 / 2 ) )
55 lemul2a ⊢ ( ( ( ( 𝑃 ‘ 𝑡 ) ∈ ℝ ∧ ( 𝐷 / 2 ) ∈ ℝ ∧ ( 𝐾 ∈ ℝ ∧ 0 ≤ 𝐾 ) ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ ( 𝐷 / 2 ) ) → ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ≤ ( 𝐾 · ( 𝐷 / 2 ) ) )
56 20 51 44 54 55 syl31anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ≤ ( 𝐾 · ( 𝐷 / 2 ) ) )
57 5 nn0cnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
58 57 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐾 ∈ ℂ )
59 6 rpcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → 𝐷 ∈ ℂ )
61 2cnne0 ⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 )
62 61 a1i ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 2 ∈ ℂ ∧ 2 ≠ 0 ) )
63 divass ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝐷 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( 𝐾 · 𝐷 ) / 2 ) = ( 𝐾 · ( 𝐷 / 2 ) ) )
64 58 60 62 63 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 · 𝐷 ) / 2 ) = ( 𝐾 · ( 𝐷 / 2 ) ) )
65 56 64 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ≤ ( ( 𝐾 · 𝐷 ) / 2 ) )
66 leexp1a ⊢ ( ( ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ∈ ℝ ∧ ( ( 𝐾 · 𝐷 ) / 2 ) ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ ( 0 ≤ ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ∧ ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ≤ ( ( 𝐾 · 𝐷 ) / 2 ) ) ) → ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ≤ ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) )
67 21 41 22 49 65 66 syl32anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ≤ ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) )
68 23 40 10 67 lesub2dd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( ( 𝐾 · 𝐷 ) / 2 ) ↑ 𝑁 ) ) ≤ ( 1 − ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ) )
69 13 38 24 39 68 ltletrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 1 − ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ) )
70 20 recnd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℂ )
71 58 70 22 mulexpd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) = ( ( 𝐾 ↑ 𝑁 ) · ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) )
72 71 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝐾 ↑ 𝑁 ) · ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) = ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) )
73 72 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( 𝐾 ↑ 𝑁 ) · ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ) = ( 1 − ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ) )
74 18 45 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
75 74 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑃 ‘ 𝑡 ) ≤ 1 )
76 exple1 ⊢ ( ( ( ( 𝑃 ‘ 𝑡 ) ∈ ℝ ∧ 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ≤ 1 )
77 20 47 75 22 76 syl31anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ≤ 1 )
78 stoweidlem10 ⊢ ( ( ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ ∧ ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 ∧ ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ≤ 1 ) → ( 1 − ( ( 𝐾 ↑ 𝑁 ) · ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ) ≤ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
79 25 30 77 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( 𝐾 ↑ 𝑁 ) · ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ) ≤ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
80 73 79 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − ( ( 𝐾 · ( 𝑃 ‘ 𝑡 ) ) ↑ 𝑁 ) ) ≤ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
81 13 24 31 69 80 ltletrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
82 2 3 4 5 stoweidlem12 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
83 18 82 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
84 81 83 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑉 ) → ( 1 − 𝐸 ) < ( 𝑄 ‘ 𝑡 ) )