Theorem stoweidlem25

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

	Ref	Expression
Hypotheses	stoweidlem25.1	⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
	stoweidlem25.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	stoweidlem25.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	stoweidlem25.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
	stoweidlem25.6	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
	stoweidlem25.7	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
	stoweidlem25.8	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
	stoweidlem25.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	stoweidlem25.11	⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) < 𝐸 )
Assertion	stoweidlem25	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) < 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem25.1	⊢ 𝑄 = ( 𝑡 ∈ 𝑇 ↦ ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
2		stoweidlem25.2	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3		stoweidlem25.3	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
4		stoweidlem25.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
5		stoweidlem25.6	⊢ ( 𝜑 → 𝑃 : 𝑇 ⟶ ℝ )
6		stoweidlem25.7	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
7		stoweidlem25.8	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
8		stoweidlem25.9	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
9		stoweidlem25.11	⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) < 𝐸 )
10		eldifi	⊢ ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → 𝑡 ∈ 𝑇 )
11	2	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12	3	nnnn0d	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
13	1 5 11 12	stoweidlem12	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
14		1red	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 1 ∈ ℝ )
15	5	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
16	11	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑁 ∈ ℕ0 )
17	15 16	reexpcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ∈ ℝ )
18	14 17	resubcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ∈ ℝ )
19	3 11	nnexpcld	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ )
20	19	nnnn0d	⊢ ( 𝜑 → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐾 ↑ 𝑁 ) ∈ ℕ0 )
22	18 21	reexpcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ∈ ℝ )
23	13 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑄 ‘ 𝑡 ) ∈ ℝ )
24	10 23	sylan2	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) ∈ ℝ )
25	3	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
26	4	rpred	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
27	25 26	remulcld	⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ∈ ℝ )
28	27 11	reexpcld	⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ∈ ℝ )
29	3	nncnd	⊢ ( 𝜑 → 𝐾 ∈ ℂ )
30	3	nnne0d	⊢ ( 𝜑 → 𝐾 ≠ 0 )
31	4	rpcnne0d	⊢ ( 𝜑 → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
32		mulne0	⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐾 · 𝐷 ) ≠ 0 )
33	29 30 31 32	syl21anc	⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ≠ 0 )
34	4	rpcnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
35	29 34	mulcld	⊢ ( 𝜑 → ( 𝐾 · 𝐷 ) ∈ ℂ )
36		expne0	⊢ ( ( ( 𝐾 · 𝐷 ) ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐷 ) ≠ 0 ) )
37	35 2 36	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 ↔ ( 𝐾 · 𝐷 ) ≠ 0 ) )
38	33 37	mpbird	⊢ ( 𝜑 → ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ≠ 0 )
39	28 38	rereccld	⊢ ( 𝜑 → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) ∈ ℝ )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) ∈ ℝ )
41	8	rpred	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
42	41	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐸 ∈ ℝ )
43	10 13	sylan2	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) = ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) )
44	2	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑁 ∈ ℕ )
45	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐾 ∈ ℕ )
46	4	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐷 ∈ ℝ+ )
47	5	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑃 : 𝑇 ⟶ ℝ )
48	10	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑡 ∈ 𝑇 )
49	47 48	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ )
50		0red	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 ∈ ℝ )
51	26	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐷 ∈ ℝ )
52	4	rpgt0d	⊢ ( 𝜑 → 0 < 𝐷 )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 < 𝐷 )
54	7	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐷 ≤ ( 𝑃 ‘ 𝑡 ) )
55	50 51 49 53 54	ltletrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 < ( 𝑃 ‘ 𝑡 ) )
56	49 55	elrpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑃 ‘ 𝑡 ) ∈ ℝ+ )
57	6	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
58		rsp	⊢ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) → ( 𝑡 ∈ 𝑇 → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) ) )
59	57 48 58	sylc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 0 ≤ ( 𝑃 ‘ 𝑡 ) ∧ ( 𝑃 ‘ 𝑡 ) ≤ 1 ) )
60	59	simpld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 0 ≤ ( 𝑃 ‘ 𝑡 ) )
61	59	simprd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑃 ‘ 𝑡 ) ≤ 1 )
62	44 45 46 56 60 61 54	stoweidlem1	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( ( 1 − ( ( 𝑃 ‘ 𝑡 ) ↑ 𝑁 ) ) ↑ ( 𝐾 ↑ 𝑁 ) ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )
63	43 62	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) ≤ ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) )
64	9	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 1 / ( ( 𝐾 · 𝐷 ) ↑ 𝑁 ) ) < 𝐸 )
65	24 40 42 63 64	lelttrd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 𝑄 ‘ 𝑡 ) < 𝐸 )