Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem14 Structured version   Unicode version

Theorem stoweidlem14 37757
Description: There exists a  k as in the proof of Lemma 1 in [BrosowskiDeutsh] p. 90:  k is an integer and 1 < k * δ < 2.  D is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem14.1  |-  A  =  { j  e.  NN  |  ( 1  /  D )  <  j }
stoweidlem14.2  |-  ( ph  ->  D  e.  RR+ )
stoweidlem14.3  |-  ( ph  ->  D  <  1 )
Assertion
Ref Expression
stoweidlem14  |-  ( ph  ->  E. k  e.  NN  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) )
Distinct variable groups:    j, k, D    A, k    ph, k
Allowed substitution hints:    ph( j)    A( j)

Proof of Theorem stoweidlem14
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 stoweidlem14.1 . . . . . 6  |-  A  =  { j  e.  NN  |  ( 1  /  D )  <  j }
2 ssrab2 3484 . . . . . . 7  |-  { j  e.  NN  |  ( 1  /  D )  <  j }  C_  NN
32a1i 11 . . . . . 6  |-  ( ph  ->  { j  e.  NN  |  ( 1  /  D )  <  j }  C_  NN )
41, 3syl5eqss 3446 . . . . 5  |-  ( ph  ->  A  C_  NN )
5 stoweidlem14.2 . . . . . . 7  |-  ( ph  ->  D  e.  RR+ )
65rprecred 11298 . . . . . 6  |-  ( ph  ->  ( 1  /  D
)  e.  RR )
7 arch 10812 . . . . . 6  |-  ( ( 1  /  D )  e.  RR  ->  E. k  e.  NN  ( 1  /  D )  <  k
)
8 breq2 4365 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( 1  /  D
)  <  j  <->  ( 1  /  D )  < 
k ) )
98elrab 3166 . . . . . . . . . 10  |-  ( k  e.  { j  e.  NN  |  ( 1  /  D )  < 
j }  <->  ( k  e.  NN  /\  ( 1  /  D )  < 
k ) )
109biimpri 209 . . . . . . . . 9  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  k  e.  { j  e.  NN  |  ( 1  /  D )  <  j } )
1110, 1syl6eleqr 2512 . . . . . . . 8  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  k  e.  A )
12 simpr 462 . . . . . . . 8  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  ( 1  /  D
)  <  k )
1311, 12jca 534 . . . . . . 7  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  ( k  e.  A  /\  ( 1  /  D
)  <  k )
)
1413reximi2 2826 . . . . . 6  |-  ( E. k  e.  NN  (
1  /  D )  <  k  ->  E. k  e.  A  ( 1  /  D )  < 
k )
15 rexn0 3840 . . . . . 6  |-  ( E. k  e.  A  ( 1  /  D )  <  k  ->  A  =/=  (/) )
166, 7, 14, 154syl 19 . . . . 5  |-  ( ph  ->  A  =/=  (/) )
17 nnwo 11170 . . . . 5  |-  ( ( A  C_  NN  /\  A  =/=  (/) )  ->  E. k  e.  A  A. z  e.  A  k  <_  z )
184, 16, 17syl2anc 665 . . . 4  |-  ( ph  ->  E. k  e.  A  A. z  e.  A  k  <_  z )
19 df-rex 2715 . . . 4  |-  ( E. k  e.  A  A. z  e.  A  k  <_  z  <->  E. k ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
2018, 19sylib 199 . . 3  |-  ( ph  ->  E. k ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
218, 1elrab2 3168 . . . . . . . 8  |-  ( k  e.  A  <->  ( k  e.  NN  /\  ( 1  /  D )  < 
k ) )
2221simplbi 461 . . . . . . 7  |-  ( k  e.  A  ->  k  e.  NN )
2322ad2antrl 732 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  k  e.  NN )
24 simpl 458 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  ph )
25 simprl 762 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  k  e.  A )
26 simprr 764 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  A. z  e.  A  k  <_  z )
27 nfcv 2564 . . . . . . . . 9  |-  F/_ z A
28 nfrab1 2943 . . . . . . . . . 10  |-  F/_ j { j  e.  NN  |  ( 1  /  D )  <  j }
291, 28nfcxfr 2562 . . . . . . . . 9  |-  F/_ j A
30 nfv 1755 . . . . . . . . 9  |-  F/ j  k  <_  z
31 nfv 1755 . . . . . . . . 9  |-  F/ z  k  <_  j
32 breq2 4365 . . . . . . . . 9  |-  ( z  =  j  ->  (
k  <_  z  <->  k  <_  j ) )
3327, 29, 30, 31, 32cbvralf 2985 . . . . . . . 8  |-  ( A. z  e.  A  k  <_  z  <->  A. j  e.  A  k  <_  j )
3426, 33sylib 199 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  A. j  e.  A  k  <_  j )
3521simprbi 465 . . . . . . . . 9  |-  ( k  e.  A  ->  (
1  /  D )  <  k )
3635ad2antrl 732 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  (
1  /  D )  <  k )
3722ad2antrl 732 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  k  e.  NN )
38 1red 9604 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  RR )
39 nnre 10562 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR )
4039adantl 467 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR )
415rpregt0d 11293 . . . . . . . . . . 11  |-  ( ph  ->  ( D  e.  RR  /\  0  <  D ) )
4241adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( D  e.  RR  /\  0  <  D ) )
43 ltdivmul2 10428 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  k  e.  RR  /\  ( D  e.  RR  /\  0  <  D ) )  -> 
( ( 1  /  D )  <  k  <->  1  <  ( k  x.  D ) ) )
4438, 40, 42, 43syl3anc 1264 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1  /  D )  <  k  <->  1  <  ( k  x.  D ) ) )
4537, 44syldan 472 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  (
( 1  /  D
)  <  k  <->  1  <  ( k  x.  D ) ) )
4636, 45mpbid 213 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  1  <  ( k  x.  D
) )
4724, 25, 34, 46syl12anc 1262 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  1  <  ( k  x.  D
) )
48 oveq1 6251 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  x.  D )  =  ( 1  x.  D ) )
4948adantl 467 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
1 )  ->  (
k  x.  D )  =  ( 1  x.  D ) )
505rpcnd 11289 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  CC )
5150adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  = 
1 )  ->  D  e.  CC )
5251mulid2d 9607 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
1 )  ->  (
1  x.  D )  =  D )
5349, 52eqtrd 2457 . . . . . . . . . 10  |-  ( (
ph  /\  k  = 
1 )  ->  (
k  x.  D )  =  D )
5453oveq1d 6259 . . . . . . . . 9  |-  ( (
ph  /\  k  = 
1 )  ->  (
( k  x.  D
)  /  2 )  =  ( D  / 
2 ) )
555rpred 11287 . . . . . . . . . . . 12  |-  ( ph  ->  D  e.  RR )
5655rehalfcld 10805 . . . . . . . . . . 11  |-  ( ph  ->  ( D  /  2
)  e.  RR )
57 halfre 10774 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
5857a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
59 1red 9604 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  RR )
60 stoweidlem14.3 . . . . . . . . . . . 12  |-  ( ph  ->  D  <  1 )
61 2re 10625 . . . . . . . . . . . . . 14  |-  2  e.  RR
6261a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  RR )
63 2pos 10647 . . . . . . . . . . . . . 14  |-  0  <  2
6463a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  2 )
65 ltdiv1 10415 . . . . . . . . . . . . 13  |-  ( ( D  e.  RR  /\  1  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( D  <  1  <->  ( D  / 
2 )  <  (
1  /  2 ) ) )
6655, 59, 62, 64, 65syl112anc 1268 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  <  1  <->  ( D  /  2 )  <  ( 1  / 
2 ) ) )
6760, 66mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( D  /  2
)  <  ( 1  /  2 ) )
68 halflt1 10777 . . . . . . . . . . . 12  |-  ( 1  /  2 )  <  1
6968a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  2
)  <  1 )
7056, 58, 59, 67, 69lttrd 9742 . . . . . . . . . 10  |-  ( ph  ->  ( D  /  2
)  <  1 )
7170adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  k  = 
1 )  ->  ( D  /  2 )  <  1 )
7254, 71eqbrtrd 4382 . . . . . . . 8  |-  ( (
ph  /\  k  = 
1 )  ->  (
( k  x.  D
)  /  2 )  <  1 )
7372adantlr 719 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  k  =  1 )  ->  ( (
k  x.  D )  /  2 )  <  1 )
74 simpll 758 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  ph )
75 simplrl 768 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  A )
7675, 22syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  NN )
77 neqne 37290 . . . . . . . . . 10  |-  ( -.  k  =  1  -> 
k  =/=  1 )
7877adantl 467 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  =/=  1 )
79 eluz2b3 11178 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  2
)  <->  ( k  e.  NN  /\  k  =/=  1 ) )
8076, 78, 79sylanbrc 668 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  ( ZZ>= `  2 )
)
81 peano2rem 9887 . . . . . . . . . 10  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
8275, 22, 39, 814syl 19 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  e.  RR )
8355ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  D  e.  RR )
845rpne0d 11292 . . . . . . . . . . 11  |-  ( ph  ->  D  =/=  0 )
8584ad2antrr 730 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  D  =/=  0 )
8683, 85rereccld 10380 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
1  /  D )  e.  RR )
87 1zzd 10914 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  1  e.  ZZ )
88 df-2 10614 . . . . . . . . . . . . . . 15  |-  2  =  ( 1  +  1 )
8988fveq2i 5823 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
2 )  =  (
ZZ>= `  ( 1  +  1 ) )
9089eleq2i 2493 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  2
)  <->  k  e.  (
ZZ>= `  ( 1  +  1 ) ) )
91 eluzsub 11134 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  ( 1  +  1 ) ) )  ->  ( k  -  1 )  e.  ( ZZ>= `  1 )
)
9290, 91syl3an3b 1302 . . . . . . . . . . . 12  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  -  1 )  e.  ( ZZ>= `  1 )
)
93 nnuz 11140 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
9492, 93syl6eleqr 2512 . . . . . . . . . . 11  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  -  1 )  e.  NN )
9587, 87, 80, 94syl3anc 1264 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  e.  NN )
9622, 39syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  A  ->  k  e.  RR )
9796adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  k  e.  RR )
9897, 81syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  ( k  -  1 )  e.  RR )
99 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  k  e.  RR )
10099ltm1d 10485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  ( k  -  1 )  <  k )
101 ltnle 9659 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  ( ( k  - 
1 )  <  k  <->  -.  k  <_  ( k  -  1 ) ) )
102100, 101mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  -.  k  <_  (
k  -  1 ) )
10398, 97, 102syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  -.  k  <_  (
k  -  1 ) )
104 breq2 4365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( k  - 
1 )  ->  (
k  <_  z  <->  k  <_  ( k  -  1 ) ) )
105104notbid 295 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( k  - 
1 )  ->  ( -.  k  <_  z  <->  -.  k  <_  ( k  -  1 ) ) )
106105rspcev 3120 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  -  1 )  e.  A  /\  -.  k  <_  ( k  -  1 ) )  ->  E. z  e.  A  -.  k  <_  z )
107103, 106syldan 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  E. z  e.  A  -.  k  <_  z )
108 rexnal 2808 . . . . . . . . . . . . . . . . . 18  |-  ( E. z  e.  A  -.  k  <_  z  <->  -.  A. z  e.  A  k  <_  z )
109107, 108sylib 199 . . . . . . . . . . . . . . . . 17  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  -.  A. z  e.  A  k  <_  z
)
110109ex 435 . . . . . . . . . . . . . . . 16  |-  ( ( k  -  1 )  e.  A  ->  (
k  e.  A  ->  -.  A. z  e.  A  k  <_  z ) )
111 imnan 423 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  A  ->  -.  A. z  e.  A  k  <_  z )  <->  -.  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )
112110, 111sylib 199 . . . . . . . . . . . . . . 15  |-  ( ( k  -  1 )  e.  A  ->  -.  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
113112con2i 123 . . . . . . . . . . . . . 14  |-  ( ( k  e.  A  /\  A. z  e.  A  k  <_  z )  ->  -.  ( k  -  1 )  e.  A )
114113ad2antlr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( k  -  1 )  e.  A )
115 breq2 4365 . . . . . . . . . . . . . 14  |-  ( j  =  ( k  - 
1 )  ->  (
( 1  /  D
)  <  j  <->  ( 1  /  D )  < 
( k  -  1 ) ) )
116115, 1elrab2 3168 . . . . . . . . . . . . 13  |-  ( ( k  -  1 )  e.  A  <->  ( (
k  -  1 )  e.  NN  /\  (
1  /  D )  <  ( k  - 
1 ) ) )
117114, 116sylnib 305 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( ( k  - 
1 )  e.  NN  /\  ( 1  /  D
)  <  ( k  -  1 ) ) )
118 ianor 490 . . . . . . . . . . . 12  |-  ( -.  ( ( k  - 
1 )  e.  NN  /\  ( 1  /  D
)  <  ( k  -  1 ) )  <-> 
( -.  ( k  -  1 )  e.  NN  \/  -.  (
1  /  D )  <  ( k  - 
1 ) ) )
119117, 118sylib 199 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  ( -.  ( k  -  1 )  e.  NN  \/  -.  ( 1  /  D
)  <  ( k  -  1 ) ) )
120 imor 413 . . . . . . . . . . 11  |-  ( ( ( k  -  1 )  e.  NN  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) )  <-> 
( -.  ( k  -  1 )  e.  NN  \/  -.  (
1  /  D )  <  ( k  - 
1 ) ) )
121119, 120sylibr 215 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
( k  -  1 )  e.  NN  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) ) )
12295, 121mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) )
12382, 86, 122nltled 9731 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  <_  ( 1  /  D ) )
124 eluzelre 11115 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  2
)  ->  k  e.  RR )
125124adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  k  e.  RR )
12655adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  D  e.  RR )
127125, 126remulcld 9617 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  x.  D )  e.  RR )
128127rehalfcld 10805 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  /  2 )  e.  RR )
1291283adant3 1025 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  e.  RR )
13059, 55readdcld 9616 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  D
)  e.  RR )
131130adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( 1  +  D )  e.  RR )
132131rehalfcld 10805 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
1  +  D )  /  2 )  e.  RR )
1331323adant3 1025 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  +  D )  / 
2 )  e.  RR )
134 1red 9604 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  1  e.  RR )
135 eluzelcn 11116 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( ZZ>= `  2
)  ->  k  e.  CC )
136135adantl 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  k  e.  CC )
13750adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  D  e.  CC )
138136, 137mulcld 9609 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  x.  D )  e.  CC )
1391383adant3 1025 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  e.  CC )
140503ad2ant1 1026 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  D  e.  CC )
141139, 140npcand 9936 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( ( k  x.  D )  -  D )  +  D )  =  ( k  x.  D ) )
142127, 126resubcld 9993 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  -  D )  e.  RR )
1431423adant3 1025 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  -  D )  e.  RR )
144553ad2ant1 1026 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  D  e.  RR )
145 simp3 1007 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  - 
1 )  <_  (
1  /  D ) )
146 1red 9604 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ZZ>= `  2
)  ->  1  e.  RR )
147124, 146resubcld 9993 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  2
)  ->  ( k  -  1 )  e.  RR )
1481473ad2ant2 1027 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  - 
1 )  e.  RR )
14963ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  /  D )  e.  RR )
150413ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( D  e.  RR  /\  0  < 
D ) )
151 lemul1 10403 . . . . . . . . . . . . . . 15  |-  ( ( ( k  -  1 )  e.  RR  /\  ( 1  /  D
)  e.  RR  /\  ( D  e.  RR  /\  0  <  D ) )  ->  ( (
k  -  1 )  <_  ( 1  /  D )  <->  ( (
k  -  1 )  x.  D )  <_ 
( ( 1  /  D )  x.  D
) ) )
152148, 149, 150, 151syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  <_ 
( 1  /  D
)  <->  ( ( k  -  1 )  x.  D )  <_  (
( 1  /  D
)  x.  D ) ) )
153145, 152mpbid 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  x.  D )  <_  (
( 1  /  D
)  x.  D ) )
154 1cnd 9605 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  1  e.  CC )
155136, 154, 137subdird 10021 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  -  1 )  x.  D )  =  ( ( k  x.  D )  -  (
1  x.  D ) ) )
156137mulid2d 9607 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( 1  x.  D )  =  D )
157156oveq2d 6260 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  -  ( 1  x.  D ) )  =  ( ( k  x.  D )  -  D
) )
158155, 157eqtrd 2457 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  -  1 )  x.  D )  =  ( ( k  x.  D )  -  D
) )
1591583adant3 1025 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  x.  D )  =  ( ( k  x.  D
)  -  D ) )
160 1cnd 9605 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  CC )
161160, 50, 843jca 1185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 ) )
1621613ad2ant1 1026 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 ) )
163 divcan1 10225 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 )  ->  (
( 1  /  D
)  x.  D )  =  1 )
164162, 163syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  /  D )  x.  D )  =  1 )
165153, 159, 1643brtr3d 4391 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  -  D )  <_  1
)
166143, 134, 144, 165leadd1dd 10173 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( ( k  x.  D )  -  D )  +  D )  <_  (
1  +  D ) )
167141, 166eqbrtrrd 4384 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  <_  (
1  +  D ) )
1681273adant3 1025 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  e.  RR )
1691303ad2ant1 1026 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  +  D )  e.  RR )
17061, 63pm3.2i 456 . . . . . . . . . . . 12  |-  ( 2  e.  RR  /\  0  <  2 )
171170a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
172 lediv1 10416 . . . . . . . . . . 11  |-  ( ( ( k  x.  D
)  e.  RR  /\  ( 1  +  D
)  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
k  x.  D )  <_  ( 1  +  D )  <->  ( (
k  x.  D )  /  2 )  <_ 
( ( 1  +  D )  /  2
) ) )
173168, 169, 171, 172syl3anc 1264 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  <_ 
( 1  +  D
)  <->  ( ( k  x.  D )  / 
2 )  <_  (
( 1  +  D
)  /  2 ) ) )
174167, 173mpbid 213 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  <_  (
( 1  +  D
)  /  2 ) )
17555, 59, 59, 60ltadd2dd 9740 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  +  D
)  <  ( 1  +  1 ) )
176 1p1e2 10669 . . . . . . . . . . . . 13  |-  ( 1  +  1 )  =  2
177175, 176syl6breq 4401 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  D
)  <  2 )
178 ltdiv1 10415 . . . . . . . . . . . . 13  |-  ( ( ( 1  +  D
)  e.  RR  /\  2  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 1  +  D )  <  2  <->  ( ( 1  +  D )  / 
2 )  <  (
2  /  2 ) ) )
179130, 62, 62, 64, 178syl112anc 1268 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  +  D )  <  2  <->  ( ( 1  +  D
)  /  2 )  <  ( 2  / 
2 ) ) )
180177, 179mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  D )  /  2
)  <  ( 2  /  2 ) )
181 2div2e1 10678 . . . . . . . . . . 11  |-  ( 2  /  2 )  =  1
182180, 181syl6breq 4401 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  D )  /  2
)  <  1 )
1831823ad2ant1 1026 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  +  D )  / 
2 )  <  1
)
184129, 133, 134, 174, 183lelttrd 9739 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  <  1
)
18574, 80, 123, 184syl3anc 1264 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
( k  x.  D
)  /  2 )  <  1 )
18673, 185pm2.61dan 798 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  (
( k  x.  D
)  /  2 )  <  1 )
18723, 47, 186jca32 537 . . . . 5  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  (
k  e.  NN  /\  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) ) )
188187ex 435 . . . 4  |-  ( ph  ->  ( ( k  e.  A  /\  A. z  e.  A  k  <_  z )  ->  ( k  e.  NN  /\  ( 1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 ) ) ) )
189188eximdv 1758 . . 3  |-  ( ph  ->  ( E. k ( k  e.  A  /\  A. z  e.  A  k  <_  z )  ->  E. k ( k  e.  NN  /\  ( 1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 ) ) ) )
19020, 189mpd 15 . 2  |-  ( ph  ->  E. k ( k  e.  NN  /\  (
1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 ) ) )
191 df-rex 2715 . 2  |-  ( E. k  e.  NN  (
1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 )  <->  E. k
( k  e.  NN  /\  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) ) )
192190, 191sylibr 215 1  |-  ( ph  ->  E. k  e.  NN  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2594   A.wral 2709   E.wrex 2710   {crab 2713    C_ wss 3374   (/)c0 3699   class class class wbr 4361   ` cfv 5539  (class class class)co 6244   CCcc 9483   RRcr 9484   0cc0 9485   1c1 9486    + caddc 9488    x. cmul 9490    < clt 9621    <_ cle 9622    - cmin 9806    / cdiv 10215   NNcn 10555   2c2 10605   ZZcz 10883   ZZ>=cuz 11105   RR+crp 11248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536  ax-cnex 9541  ax-resscn 9542  ax-1cn 9543  ax-icn 9544  ax-addcl 9545  ax-addrcl 9546  ax-mulcl 9547  ax-mulrcl 9548  ax-mulcom 9549  ax-addass 9550  ax-mulass 9551  ax-distr 9552  ax-i2m1 9553  ax-1ne0 9554  ax-1rid 9555  ax-rnegex 9556  ax-rrecex 9557  ax-cnre 9558  ax-pre-lttri 9559  ax-pre-lttrn 9560  ax-pre-ltadd 9561  ax-pre-mulgt0 9562  ax-pre-sup 9563
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-pss 3390  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-tr 4457  df-eprel 4702  df-id 4706  df-po 4712  df-so 4713  df-fr 4750  df-we 4752  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-pred 5337  df-ord 5383  df-on 5384  df-lim 5385  df-suc 5386  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-riota 6206  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-om 6646  df-wrecs 6978  df-recs 7040  df-rdg 7078  df-er 7313  df-en 7520  df-dom 7521  df-sdom 7522  df-pnf 9623  df-mnf 9624  df-xr 9625  df-ltxr 9626  df-le 9627  df-sub 9808  df-neg 9809  df-div 10216  df-nn 10556  df-2 10614  df-n0 10816  df-z 10884  df-uz 11106  df-rp 11249
This theorem is referenced by:  stoweidlem49  37793
  Copyright terms: Public domain W3C validator