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

Theorem stoweidlem14 27777
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 3414 . . . . . . 7  |-  { j  e.  NN  |  ( 1  /  D )  <  j }  C_  NN
32a1i 11 . . . . . 6  |-  ( ph  ->  { j  e.  NN  |  ( 1  /  D )  <  j }  C_  NN )
41, 3syl5eqss 3378 . . . . 5  |-  ( ph  ->  A  C_  NN )
5 stoweidlem14.2 . . . . . . 7  |-  ( ph  ->  D  e.  RR+ )
65rprecred 10690 . . . . . 6  |-  ( ph  ->  ( 1  /  D
)  e.  RR )
7 arch 10249 . . . . . 6  |-  ( ( 1  /  D )  e.  RR  ->  E. k  e.  NN  ( 1  /  D )  <  k
)
8 breq2 4241 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( 1  /  D
)  <  j  <->  ( 1  /  D )  < 
k ) )
98elrab 3098 . . . . . . . . . 10  |-  ( k  e.  { j  e.  NN  |  ( 1  /  D )  < 
j }  <->  ( k  e.  NN  /\  ( 1  /  D )  < 
k ) )
109biimpri 199 . . . . . . . . 9  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  k  e.  { j  e.  NN  |  ( 1  /  D )  <  j } )
1110, 1syl6eleqr 2533 . . . . . . . 8  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  k  e.  A )
12 simpr 449 . . . . . . . 8  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  ( 1  /  D
)  <  k )
1311, 12jca 520 . . . . . . 7  |-  ( ( k  e.  NN  /\  ( 1  /  D
)  <  k )  ->  ( k  e.  A  /\  ( 1  /  D
)  <  k )
)
1413reximi2 2818 . . . . . 6  |-  ( E. k  e.  NN  (
1  /  D )  <  k  ->  E. k  e.  A  ( 1  /  D )  < 
k )
15 rexn0 3754 . . . . . 6  |-  ( E. k  e.  A  ( 1  /  D )  <  k  ->  A  =/=  (/) )
166, 7, 14, 154syl 20 . . . . 5  |-  ( ph  ->  A  =/=  (/) )
17 nnwo 10573 . . . . 5  |-  ( ( A  C_  NN  /\  A  =/=  (/) )  ->  E. k  e.  A  A. z  e.  A  k  <_  z )
184, 16, 17syl2anc 644 . . . 4  |-  ( ph  ->  E. k  e.  A  A. z  e.  A  k  <_  z )
19 df-rex 2717 . . . 4  |-  ( E. k  e.  A  A. z  e.  A  k  <_  z  <->  E. k ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
2018, 19sylib 190 . . 3  |-  ( ph  ->  E. k ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
218, 1elrab2 3100 . . . . . . . 8  |-  ( k  e.  A  <->  ( k  e.  NN  /\  ( 1  /  D )  < 
k ) )
2221simplbi 448 . . . . . . 7  |-  ( k  e.  A  ->  k  e.  NN )
2322ad2antrl 710 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  k  e.  NN )
24 simpl 445 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  ph )
25 simprl 734 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  k  e.  A )
26 simprr 735 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  A. z  e.  A  k  <_  z )
27 nfcv 2578 . . . . . . . . 9  |-  F/_ z A
28 nfrab1 2894 . . . . . . . . . 10  |-  F/_ j { j  e.  NN  |  ( 1  /  D )  <  j }
291, 28nfcxfr 2575 . . . . . . . . 9  |-  F/_ j A
30 nfv 1630 . . . . . . . . 9  |-  F/ j  k  <_  z
31 nfv 1630 . . . . . . . . 9  |-  F/ z  k  <_  j
32 breq2 4241 . . . . . . . . 9  |-  ( z  =  j  ->  (
k  <_  z  <->  k  <_  j ) )
3327, 29, 30, 31, 32cbvralf 2932 . . . . . . . 8  |-  ( A. z  e.  A  k  <_  z  <->  A. j  e.  A  k  <_  j )
3426, 33sylib 190 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  A. j  e.  A  k  <_  j )
3521simprbi 452 . . . . . . . . 9  |-  ( k  e.  A  ->  (
1  /  D )  <  k )
3635ad2antrl 710 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  (
1  /  D )  <  k )
3722ad2antrl 710 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  k  e.  NN )
38 1re 9121 . . . . . . . . . . 11  |-  1  e.  RR
3938a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  1  e.  RR )
40 nnre 10038 . . . . . . . . . . 11  |-  ( k  e.  NN  ->  k  e.  RR )
4140adantl 454 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  k  e.  RR )
425rpregt0d 10685 . . . . . . . . . . 11  |-  ( ph  ->  ( D  e.  RR  /\  0  <  D ) )
4342adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  NN )  ->  ( D  e.  RR  /\  0  <  D ) )
44 ltdivmul2 9916 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  k  e.  RR  /\  ( D  e.  RR  /\  0  <  D ) )  -> 
( ( 1  /  D )  <  k  <->  1  <  ( k  x.  D ) ) )
4539, 41, 43, 44syl3anc 1185 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN )  ->  ( ( 1  /  D )  <  k  <->  1  <  ( k  x.  D ) ) )
4637, 45syldan 458 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  (
( 1  /  D
)  <  k  <->  1  <  ( k  x.  D ) ) )
4736, 46mpbid 203 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  A  /\  A. j  e.  A  k  <_  j ) )  ->  1  <  ( k  x.  D
) )
4824, 25, 34, 47syl12anc 1183 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  1  <  ( k  x.  D
) )
49 oveq1 6117 . . . . . . . . . . . 12  |-  ( k  =  1  ->  (
k  x.  D )  =  ( 1  x.  D ) )
5049adantl 454 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
1 )  ->  (
k  x.  D )  =  ( 1  x.  D ) )
515rpcnd 10681 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  CC )
5251adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  = 
1 )  ->  D  e.  CC )
5352mulid2d 9137 . . . . . . . . . . 11  |-  ( (
ph  /\  k  = 
1 )  ->  (
1  x.  D )  =  D )
5450, 53eqtrd 2474 . . . . . . . . . 10  |-  ( (
ph  /\  k  = 
1 )  ->  (
k  x.  D )  =  D )
5554oveq1d 6125 . . . . . . . . 9  |-  ( (
ph  /\  k  = 
1 )  ->  (
( k  x.  D
)  /  2 )  =  ( D  / 
2 ) )
565rpred 10679 . . . . . . . . . . . 12  |-  ( ph  ->  D  e.  RR )
5756rehalfcld 10245 . . . . . . . . . . 11  |-  ( ph  ->  ( D  /  2
)  e.  RR )
5838rehalfcli 10247 . . . . . . . . . . . 12  |-  ( 1  /  2 )  e.  RR
5958a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  2
)  e.  RR )
6038a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  RR )
61 stoweidlem14.3 . . . . . . . . . . . 12  |-  ( ph  ->  D  <  1 )
62 2re 10100 . . . . . . . . . . . . . 14  |-  2  e.  RR
6362a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  2  e.  RR )
64 2pos 10113 . . . . . . . . . . . . . 14  |-  0  <  2
6564a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <  2 )
66 ltdiv1 9905 . . . . . . . . . . . . 13  |-  ( ( D  e.  RR  /\  1  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( D  <  1  <->  ( D  / 
2 )  <  (
1  /  2 ) ) )
6756, 60, 63, 65, 66syl112anc 1189 . . . . . . . . . . . 12  |-  ( ph  ->  ( D  <  1  <->  ( D  /  2 )  <  ( 1  / 
2 ) ) )
6861, 67mpbid 203 . . . . . . . . . . 11  |-  ( ph  ->  ( D  /  2
)  <  ( 1  /  2 ) )
69 halflt1 10220 . . . . . . . . . . . 12  |-  ( 1  /  2 )  <  1
7069a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  2
)  <  1 )
7157, 59, 60, 68, 70lttrd 9262 . . . . . . . . . 10  |-  ( ph  ->  ( D  /  2
)  <  1 )
7271adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  k  = 
1 )  ->  ( D  /  2 )  <  1 )
7355, 72eqbrtrd 4257 . . . . . . . 8  |-  ( (
ph  /\  k  = 
1 )  ->  (
( k  x.  D
)  /  2 )  <  1 )
7473adantlr 697 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  k  =  1 )  ->  ( (
k  x.  D )  /  2 )  <  1 )
75 simpll 732 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  ph )
76 simplrl 738 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  A )
7776, 22syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  NN )
78 df-ne 2607 . . . . . . . . . . 11  |-  ( k  =/=  1  <->  -.  k  =  1 )
7978biimpri 199 . . . . . . . . . 10  |-  ( -.  k  =  1  -> 
k  =/=  1 )
8079adantl 454 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  =/=  1 )
81 eluz2b3 10580 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  2
)  <->  ( k  e.  NN  /\  k  =/=  1 ) )
8277, 80, 81sylanbrc 647 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  k  e.  ( ZZ>= `  2 )
)
83 1z 10342 . . . . . . . . . . . 12  |-  1  e.  ZZ
8483a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  1  e.  ZZ )
85 df-2 10089 . . . . . . . . . . . . . . 15  |-  2  =  ( 1  +  1 )
8685fveq2i 5760 . . . . . . . . . . . . . 14  |-  ( ZZ>= ` 
2 )  =  (
ZZ>= `  ( 1  +  1 ) )
8786eleq2i 2506 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  2
)  <->  k  e.  (
ZZ>= `  ( 1  +  1 ) ) )
88 eluzsub 10546 . . . . . . . . . . . . 13  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  ( 1  +  1 ) ) )  ->  ( k  -  1 )  e.  ( ZZ>= `  1 )
)
8987, 88syl3an3b 1223 . . . . . . . . . . . 12  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  -  1 )  e.  ( ZZ>= `  1 )
)
90 nnuz 10552 . . . . . . . . . . . 12  |-  NN  =  ( ZZ>= `  1 )
9189, 90syl6eleqr 2533 . . . . . . . . . . 11  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  -  1 )  e.  NN )
9284, 84, 82, 91syl3anc 1185 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  e.  NN )
9322, 40syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  A  ->  k  e.  RR )
9493adantl 454 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  k  e.  RR )
95 peano2rem 9398 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  RR  ->  (
k  -  1 )  e.  RR )
9694, 95syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  ( k  -  1 )  e.  RR )
97 simpr 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  k  e.  RR )
9897ltm1d 9974 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  ( k  -  1 )  <  k )
99 ltnle 9186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  ( ( k  - 
1 )  <  k  <->  -.  k  <_  ( k  -  1 ) ) )
10098, 99mpbid 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( k  -  1 )  e.  RR  /\  k  e.  RR )  ->  -.  k  <_  (
k  -  1 ) )
10196, 94, 100syl2anc 644 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  -.  k  <_  (
k  -  1 ) )
102 breq2 4241 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  =  ( k  - 
1 )  ->  (
k  <_  z  <->  k  <_  ( k  -  1 ) ) )
103102notbid 287 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  ( k  - 
1 )  ->  ( -.  k  <_  z  <->  -.  k  <_  ( k  -  1 ) ) )
104103rspcev 3058 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  -  1 )  e.  A  /\  -.  k  <_  ( k  -  1 ) )  ->  E. z  e.  A  -.  k  <_  z )
105101, 104syldan 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  E. z  e.  A  -.  k  <_  z )
106 rexnal 2722 . . . . . . . . . . . . . . . . . 18  |-  ( E. z  e.  A  -.  k  <_  z  <->  -.  A. z  e.  A  k  <_  z )
107105, 106sylib 190 . . . . . . . . . . . . . . . . 17  |-  ( ( ( k  -  1 )  e.  A  /\  k  e.  A )  ->  -.  A. z  e.  A  k  <_  z
)
108107ex 425 . . . . . . . . . . . . . . . 16  |-  ( ( k  -  1 )  e.  A  ->  (
k  e.  A  ->  -.  A. z  e.  A  k  <_  z ) )
109 imnan 413 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  A  ->  -.  A. z  e.  A  k  <_  z )  <->  -.  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )
110108, 109sylib 190 . . . . . . . . . . . . . . 15  |-  ( ( k  -  1 )  e.  A  ->  -.  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )
111110con2i 115 . . . . . . . . . . . . . 14  |-  ( ( k  e.  A  /\  A. z  e.  A  k  <_  z )  ->  -.  ( k  -  1 )  e.  A )
112111ad2antlr 709 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( k  -  1 )  e.  A )
113 breq2 4241 . . . . . . . . . . . . . 14  |-  ( j  =  ( k  - 
1 )  ->  (
( 1  /  D
)  <  j  <->  ( 1  /  D )  < 
( k  -  1 ) ) )
114113, 1elrab2 3100 . . . . . . . . . . . . 13  |-  ( ( k  -  1 )  e.  A  <->  ( (
k  -  1 )  e.  NN  /\  (
1  /  D )  <  ( k  - 
1 ) ) )
115112, 114sylnib 297 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( ( k  - 
1 )  e.  NN  /\  ( 1  /  D
)  <  ( k  -  1 ) ) )
116 ianor 476 . . . . . . . . . . . 12  |-  ( -.  ( ( k  - 
1 )  e.  NN  /\  ( 1  /  D
)  <  ( k  -  1 ) )  <-> 
( -.  ( k  -  1 )  e.  NN  \/  -.  (
1  /  D )  <  ( k  - 
1 ) ) )
117115, 116sylib 190 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  ( -.  ( k  -  1 )  e.  NN  \/  -.  ( 1  /  D
)  <  ( k  -  1 ) ) )
118 imor 403 . . . . . . . . . . 11  |-  ( ( ( k  -  1 )  e.  NN  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) )  <-> 
( -.  ( k  -  1 )  e.  NN  \/  -.  (
1  /  D )  <  ( k  - 
1 ) ) )
119117, 118sylibr 205 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
( k  -  1 )  e.  NN  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) ) )
12092, 119mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  -.  ( 1  /  D
)  <  ( k  -  1 ) )
12176, 22, 40, 954syl 20 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  e.  RR )
12256ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  D  e.  RR )
1235rpne0d 10684 . . . . . . . . . . . 12  |-  ( ph  ->  D  =/=  0 )
124123ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  D  =/=  0 )
125122, 124rereccld 9872 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
1  /  D )  e.  RR )
126121, 125lenltd 9250 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
( k  -  1 )  <_  ( 1  /  D )  <->  -.  (
1  /  D )  <  ( k  - 
1 ) ) )
127120, 126mpbird 225 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
k  -  1 )  <_  ( 1  /  D ) )
128 eluzelre 10528 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  2
)  ->  k  e.  RR )
129128adantl 454 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  k  e.  RR )
13056adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  D  e.  RR )
131129, 130remulcld 9147 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  x.  D )  e.  RR )
132131rehalfcld 10245 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  /  2 )  e.  RR )
1331323adant3 978 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  e.  RR )
13460, 56readdcld 9146 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  D
)  e.  RR )
135134adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( 1  +  D )  e.  RR )
136135rehalfcld 10245 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
1  +  D )  /  2 )  e.  RR )
1371363adant3 978 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  +  D )  / 
2 )  e.  RR )
13838a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  1  e.  RR )
139 eluzelcn 27738 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( ZZ>= `  2
)  ->  k  e.  CC )
140139adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  k  e.  CC )
14151adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  D  e.  CC )
142140, 141mulcld 9139 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( k  x.  D )  e.  CC )
1431423adant3 978 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  e.  CC )
144513ad2ant1 979 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  D  e.  CC )
145143, 144npcand 9446 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( ( k  x.  D )  -  D )  +  D )  =  ( k  x.  D ) )
146131, 130resubcld 9496 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  -  D )  e.  RR )
1471463adant3 978 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  -  D )  e.  RR )
148563ad2ant1 979 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  D  e.  RR )
149 simp3 960 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  - 
1 )  <_  (
1  /  D ) )
15038a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ZZ>= `  2
)  ->  1  e.  RR )
151128, 150resubcld 9496 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ZZ>= `  2
)  ->  ( k  -  1 )  e.  RR )
1521513ad2ant2 980 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  - 
1 )  e.  RR )
15363ad2ant1 979 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  /  D )  e.  RR )
154423ad2ant1 979 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( D  e.  RR  /\  0  < 
D ) )
155 lemul1 9893 . . . . . . . . . . . . . . 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
) ) )
156152, 153, 154, 155syl3anc 1185 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  <_ 
( 1  /  D
)  <->  ( ( k  -  1 )  x.  D )  <_  (
( 1  /  D
)  x.  D ) ) )
157149, 156mpbid 203 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  x.  D )  <_  (
( 1  /  D
)  x.  D ) )
158 ax-1cn 9079 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
159158a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  1  e.  CC )
160140, 159, 141subdird 9521 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  -  1 )  x.  D )  =  ( ( k  x.  D )  -  (
1  x.  D ) ) )
161141mulid2d 9137 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( 1  x.  D )  =  D )
162161oveq2d 6126 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  x.  D )  -  ( 1  x.  D ) )  =  ( ( k  x.  D )  -  D
) )
163160, 162eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )
)  ->  ( (
k  -  1 )  x.  D )  =  ( ( k  x.  D )  -  D
) )
1641633adant3 978 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  -  1 )  x.  D )  =  ( ( k  x.  D
)  -  D ) )
165158a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  CC )
166165, 51, 1233jca 1135 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 ) )
1671663ad2ant1 979 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 ) )
168 divcan1 9718 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  CC  /\  D  e.  CC  /\  D  =/=  0 )  ->  (
( 1  /  D
)  x.  D )  =  1 )
169167, 168syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  /  D )  x.  D )  =  1 )
170157, 164, 1693brtr3d 4266 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  -  D )  <_  1
)
171147, 138, 148, 170leadd1dd 9671 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( ( k  x.  D )  -  D )  +  D )  <_  (
1  +  D ) )
172145, 171eqbrtrrd 4259 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  <_  (
1  +  D ) )
1731313adant3 978 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( k  x.  D )  e.  RR )
1741343ad2ant1 979 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 1  +  D )  e.  RR )
17562, 64pm3.2i 443 . . . . . . . . . . . 12  |-  ( 2  e.  RR  /\  0  <  2 )
176175a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( 2  e.  RR  /\  0  <  2 ) )
177 lediv1 9906 . . . . . . . . . . 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
) ) )
178173, 174, 176, 177syl3anc 1185 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  <_ 
( 1  +  D
)  <->  ( ( k  x.  D )  / 
2 )  <_  (
( 1  +  D
)  /  2 ) ) )
179172, 178mpbid 203 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  <_  (
( 1  +  D
)  /  2 ) )
18056, 60, 60, 61ltadd2dd 9260 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  +  D
)  <  ( 1  +  1 ) )
181 1p1e2 10125 . . . . . . . . . . . . 13  |-  ( 1  +  1 )  =  2
182180, 181syl6breq 4276 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  +  D
)  <  2 )
183 ltdiv1 9905 . . . . . . . . . . . . 13  |-  ( ( ( 1  +  D
)  e.  RR  /\  2  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 1  +  D )  <  2  <->  ( ( 1  +  D )  / 
2 )  <  (
2  /  2 ) ) )
184134, 63, 63, 65, 183syl112anc 1189 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1  +  D )  <  2  <->  ( ( 1  +  D
)  /  2 )  <  ( 2  / 
2 ) ) )
185182, 184mpbid 203 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1  +  D )  /  2
)  <  ( 2  /  2 ) )
186 2cn 10101 . . . . . . . . . . . 12  |-  2  e.  CC
187 2ne0 10114 . . . . . . . . . . . 12  |-  2  =/=  0
188186, 187dividi 9778 . . . . . . . . . . 11  |-  ( 2  /  2 )  =  1
189185, 188syl6breq 4276 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1  +  D )  /  2
)  <  1 )
1901893ad2ant1 979 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( 1  +  D )  / 
2 )  <  1
)
191133, 137, 138, 179, 190lelttrd 9259 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( ZZ>= `  2 )  /\  ( k  -  1 )  <_  ( 1  /  D ) )  ->  ( ( k  x.  D )  / 
2 )  <  1
)
19275, 82, 127, 191syl3anc 1185 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  A  /\  A. z  e.  A  k  <_  z ) )  /\  -.  k  =  1 )  ->  (
( k  x.  D
)  /  2 )  <  1 )
19374, 192pm2.61dan 768 . . . . . 6  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  (
( k  x.  D
)  /  2 )  <  1 )
19423, 48, 193jca32 523 . . . . 5  |-  ( (
ph  /\  ( k  e.  A  /\  A. z  e.  A  k  <_  z ) )  ->  (
k  e.  NN  /\  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) ) )
195194ex 425 . . . 4  |-  ( ph  ->  ( ( k  e.  A  /\  A. z  e.  A  k  <_  z )  ->  ( k  e.  NN  /\  ( 1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 ) ) ) )
196195eximdv 1633 . . 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 ) ) ) )
19720, 196mpd 15 . 2  |-  ( ph  ->  E. k ( k  e.  NN  /\  (
1  <  ( k  x.  D )  /\  (
( k  x.  D
)  /  2 )  <  1 ) ) )
198 df-rex 2717 . 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
) ) )
199197, 198sylibr 205 1  |-  ( ph  ->  E. k  e.  NN  ( 1  <  (
k  x.  D )  /\  ( ( k  x.  D )  / 
2 )  <  1
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    /\ w3a 937   E.wex 1551    = wceq 1653    e. wcel 1727    =/= wne 2605   A.wral 2711   E.wrex 2712   {crab 2715    C_ wss 3306   (/)c0 3613   class class class wbr 4237   ` cfv 5483  (class class class)co 6110   CCcc 9019   RRcr 9020   0cc0 9021   1c1 9022    + caddc 9024    x. cmul 9026    < clt 9151    <_ cle 9152    - cmin 9322    / cdiv 9708   NNcn 10031   2c2 10080   ZZcz 10313   ZZ>=cuz 10519   RR+crp 10643
This theorem is referenced by:  stoweidlem49  27812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-13 1729  ax-14 1731  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423  ax-sep 4355  ax-nul 4363  ax-pow 4406  ax-pr 4432  ax-un 4730  ax-cnex 9077  ax-resscn 9078  ax-1cn 9079  ax-icn 9080  ax-addcl 9081  ax-addrcl 9082  ax-mulcl 9083  ax-mulrcl 9084  ax-mulcom 9085  ax-addass 9086  ax-mulass 9087  ax-distr 9088  ax-i2m1 9089  ax-1ne0 9090  ax-1rid 9091  ax-rnegex 9092  ax-rrecex 9093  ax-cnre 9094  ax-pre-lttri 9095  ax-pre-lttrn 9096  ax-pre-ltadd 9097  ax-pre-mulgt0 9098  ax-pre-sup 9099
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2291  df-mo 2292  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2716  df-rex 2717  df-reu 2718  df-rmo 2719  df-rab 2720  df-v 2964  df-sbc 3168  df-csb 3268  df-dif 3309  df-un 3311  df-in 3313  df-ss 3320  df-pss 3322  df-nul 3614  df-if 3764  df-pw 3825  df-sn 3844  df-pr 3845  df-tp 3846  df-op 3847  df-uni 4040  df-iun 4119  df-br 4238  df-opab 4292  df-mpt 4293  df-tr 4328  df-eprel 4523  df-id 4527  df-po 4532  df-so 4533  df-fr 4570  df-we 4572  df-ord 4613  df-on 4614  df-lim 4615  df-suc 4616  df-om 4875  df-xp 4913  df-rel 4914  df-cnv 4915  df-co 4916  df-dm 4917  df-rn 4918  df-res 4919  df-ima 4920  df-iota 5447  df-fun 5485  df-fn 5486  df-f 5487  df-f1 5488  df-fo 5489  df-f1o 5490  df-fv 5491  df-ov 6113  df-oprab 6114  df-mpt2 6115  df-riota 6578  df-recs 6662  df-rdg 6697  df-er 6934  df-en 7139  df-dom 7140  df-sdom 7141  df-pnf 9153  df-mnf 9154  df-xr 9155  df-ltxr 9156  df-le 9157  df-sub 9324  df-neg 9325  df-div 9709  df-nn 10032  df-2 10089  df-n0 10253  df-z 10314  df-uz 10520  df-rp 10644
  Copyright terms: Public domain W3C validator