# 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
|- F/_ t P
stoweidlem49.2
|- F/ t ph
stoweidlem49.3
|- V = { t e. T | ( P ` t ) < ( D / 2 ) }
stoweidlem49.4
|- ( ph -> D e. RR+ )
stoweidlem49.5
|- ( ph -> D < 1 )
stoweidlem49.6
|- ( ph -> P e. A )
stoweidlem49.7
|- ( ph -> P : T --> RR )
stoweidlem49.8
|- ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
stoweidlem49.9
|- ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
stoweidlem49.10
|- ( ( ph /\ f e. A ) -> f : T --> RR )
stoweidlem49.11
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem49.12
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem49.13
|- ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
stoweidlem49.14
|- ( ph -> E e. RR+ )
Assertion stoweidlem49
|- ( ph -> E. y e. A ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) /\ A. t e. V ( 1 - E ) < ( y ` t ) /\ A. t e. ( T \ U ) ( y ` t ) < E ) )

### Proof

Step Hyp Ref Expression
1 stoweidlem49.1
|-  F/_ t P
2 stoweidlem49.2
|-  F/ t ph
3 stoweidlem49.3
|-  V = { t e. T | ( P ` t ) < ( D / 2 ) }
4 stoweidlem49.4
|-  ( ph -> D e. RR+ )
5 stoweidlem49.5
|-  ( ph -> D < 1 )
6 stoweidlem49.6
|-  ( ph -> P e. A )
7 stoweidlem49.7
|-  ( ph -> P : T --> RR )
8 stoweidlem49.8
|-  ( ph -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
9 stoweidlem49.9
|-  ( ph -> A. t e. ( T \ U ) D <_ ( P ` t ) )
10 stoweidlem49.10
|-  ( ( ph /\ f e. A ) -> f : T --> RR )
11 stoweidlem49.11
|-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
12 stoweidlem49.12
|-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
13 stoweidlem49.13
|-  ( ( ph /\ x e. RR ) -> ( t e. T |-> x ) e. A )
14 stoweidlem49.14
|-  ( ph -> E e. RR+ )
15 breq2
|-  ( j = i -> ( ( 1 / D ) < j <-> ( 1 / D ) < i ) )
16 15 cbvrabv
|-  { j e. NN | ( 1 / D ) < j } = { i e. NN | ( 1 / D ) < i }
17 16 4 5 stoweidlem14
|-  ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )
18 eqid
|-  ( i e. NN0 |-> ( ( 1 / ( k x. D ) ) ^ i ) ) = ( i e. NN0 |-> ( ( 1 / ( k x. D ) ) ^ i ) )
19 eqid
|-  ( i e. NN0 |-> ( ( ( k x. D ) / 2 ) ^ i ) ) = ( i e. NN0 |-> ( ( ( k x. D ) / 2 ) ^ i ) )
20 nnre
|-  ( k e. NN -> k e. RR )
|-  ( ( ph /\ k e. NN ) -> k e. RR )
22 4 rpred
|-  ( ph -> D e. RR )
|-  ( ( ph /\ k e. NN ) -> D e. RR )
24 21 23 remulcld
|-  ( ( ph /\ k e. NN ) -> ( k x. D ) e. RR )
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( k x. D ) e. RR )
26 simprl
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> 1 < ( k x. D ) )
27 24 rehalfcld
|-  ( ( ph /\ k e. NN ) -> ( ( k x. D ) / 2 ) e. RR )
28 nngt0
|-  ( k e. NN -> 0 < k )
|-  ( ( ph /\ k e. NN ) -> 0 < k )
30 4 rpgt0d
|-  ( ph -> 0 < D )
|-  ( ( ph /\ k e. NN ) -> 0 < D )
32 21 23 29 31 mulgt0d
|-  ( ( ph /\ k e. NN ) -> 0 < ( k x. D ) )
33 2re
|-  2 e. RR
34 2pos
|-  0 < 2
35 33 34 pm3.2i
|-  ( 2 e. RR /\ 0 < 2 )
36 35 a1i
|-  ( ( ph /\ k e. NN ) -> ( 2 e. RR /\ 0 < 2 ) )
37 divgt0
|-  ( ( ( ( k x. D ) e. RR /\ 0 < ( k x. D ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 < ( ( k x. D ) / 2 ) )
38 24 32 36 37 syl21anc
|-  ( ( ph /\ k e. NN ) -> 0 < ( ( k x. D ) / 2 ) )
39 27 38 elrpd
|-  ( ( ph /\ k e. NN ) -> ( ( k x. D ) / 2 ) e. RR+ )
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( ( k x. D ) / 2 ) e. RR+ )
41 simprr
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> ( ( k x. D ) / 2 ) < 1 )
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> E e. RR+ )
43 18 19 25 26 40 41 42 stoweidlem7
|-  ( ( ( ph /\ k e. NN ) /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) -> E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
44 43 ex
|-  ( ( ph /\ k e. NN ) -> ( ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) -> E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) )
45 44 reximdva
|-  ( ph -> ( E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) -> E. k e. NN E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) )
46 17 45 mpd
|-  ( ph -> E. k e. NN E. n e. NN ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
47 nfv
|-  F/ t ( k e. NN /\ n e. NN )
48 2 47 nfan
|-  F/ t ( ph /\ ( k e. NN /\ n e. NN ) )
49 nfv
|-  F/ t ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E )
50 48 49 nfan
|-  F/ t ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) )
51 eqid
|-  ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ n ) ) ^ ( k ^ n ) ) ) = ( t e. T |-> ( ( 1 - ( ( P ` t ) ^ n ) ) ^ ( k ^ n ) ) )
52 simplrr
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> n e. NN )
53 simplrl
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> k e. NN )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> D e. RR+ )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> D < 1 )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> P e. A )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> P : T --> RR )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> A. t e. T ( 0 <_ ( P ` t ) /\ ( P ` t ) <_ 1 ) )
|-  ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) -> A. t e. ( T \ U ) D <_ ( P ` t ) )
|-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A ) -> f : T --> RR )
61 simp1ll
|-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ph )
62 61 11 syld3an1
|-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
63 61 12 syld3an1
|-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
|-  ( ( ( ( ph /\ ( k e. NN /\ n e. NN ) ) /\ ( ( 1 - E ) < ( 1 - ( ( ( k x. D ) / 2 ) ^ n ) ) /\ ( 1 / ( ( k x. D ) ^ n ) ) < E ) ) /\ x e. RR ) -> ( t e. T |-> x ) e. A )