Metamath Proof Explorer

Theorem stoweidlem14

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)

Ref Expression
Hypotheses stoweidlem14.1 
|- A = { j e. NN | ( 1 / D ) < j }
stoweidlem14.2 
|- ( ph -> D e. RR+ )
stoweidlem14.3 
|- ( ph -> D < 1 )
Assertion stoweidlem14 
|- ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )

Proof

Step Hyp Ref Expression
1 stoweidlem14.1 
 |-  A = { j e. NN | ( 1 / D ) < j }
2 stoweidlem14.2 
 |-  ( ph -> D e. RR+ )
3 stoweidlem14.3 
 |-  ( ph -> D < 1 )
4 ssrab2 
 |-  { j e. NN | ( 1 / D ) < j } C_ NN
5 4 a1i 
 |-  ( ph -> { j e. NN | ( 1 / D ) < j } C_ NN )
6 1 5 eqsstrid 
 |-  ( ph -> A C_ NN )
7 2 rprecred 
 |-  ( ph -> ( 1 / D ) e. RR )
8 arch 
 |-  ( ( 1 / D ) e. RR -> E. k e. NN ( 1 / D ) < k )
9 breq2 
 |-  ( j = k -> ( ( 1 / D ) < j <-> ( 1 / D ) < k ) )
10 9 elrab 
 |-  ( k e. { j e. NN | ( 1 / D ) < j } <-> ( k e. NN /\ ( 1 / D ) < k ) )
11 10 biimpri 
 |-  ( ( k e. NN /\ ( 1 / D ) < k ) -> k e. { j e. NN | ( 1 / D ) < j } )
12 11 1 eleqtrrdi 
 |-  ( ( k e. NN /\ ( 1 / D ) < k ) -> k e. A )
13 simpr 
 |-  ( ( k e. NN /\ ( 1 / D ) < k ) -> ( 1 / D ) < k )
14 12 13 jca 
 |-  ( ( k e. NN /\ ( 1 / D ) < k ) -> ( k e. A /\ ( 1 / D ) < k ) )
15 14 reximi2 
 |-  ( E. k e. NN ( 1 / D ) < k -> E. k e. A ( 1 / D ) < k )
16 rexn0 
 |-  ( E. k e. A ( 1 / D ) < k -> A =/= (/) )
17 7 8 15 16 4syl 
 |-  ( ph -> A =/= (/) )
18 nnwo 
 |-  ( ( A C_ NN /\ A =/= (/) ) -> E. k e. A A. z e. A k <_ z )
19 6 17 18 syl2anc 
 |-  ( ph -> E. k e. A A. z e. A k <_ z )
20 df-rex 
 |-  ( E. k e. A A. z e. A k <_ z <-> E. k ( k e. A /\ A. z e. A k <_ z ) )
21 19 20 sylib 
 |-  ( ph -> E. k ( k e. A /\ A. z e. A k <_ z ) )
22 9 1 elrab2 
 |-  ( k e. A <-> ( k e. NN /\ ( 1 / D ) < k ) )
23 22 simplbi 
 |-  ( k e. A -> k e. NN )
24 23 ad2antrl 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. NN )
25 simpl 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ph )
26 simprl 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. A )
27 simprr 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> A. z e. A k <_ z )
28 nfcv 
 |-  F/_ z A
29 nfrab1 
 |-  F/_ j { j e. NN | ( 1 / D ) < j }
30 1 29 nfcxfr 
 |-  F/_ j A
31 nfv 
 |-  F/ j k <_ z
32 nfv 
 |-  F/ z k <_ j
33 breq2 
 |-  ( z = j -> ( k <_ z <-> k <_ j ) )
34 28 30 31 32 33 cbvralfw 
 |-  ( A. z e. A k <_ z <-> A. j e. A k <_ j )
35 27 34 sylib 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> A. j e. A k <_ j )
36 22 simprbi 
 |-  ( k e. A -> ( 1 / D ) < k )
37 36 ad2antrl 
 |-  ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( 1 / D ) < k )
38 23 ad2antrl 
 |-  ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> k e. NN )
39 1red 
 |-  ( ( ph /\ k e. NN ) -> 1 e. RR )
40 nnre 
 |-  ( k e. NN -> k e. RR )
41 40 adantl 
 |-  ( ( ph /\ k e. NN ) -> k e. RR )
42 2 rpregt0d 
 |-  ( ph -> ( D e. RR /\ 0 < D ) )
43 42 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( D e. RR /\ 0 < D ) )
44 ltdivmul2 
 |-  ( ( 1 e. RR /\ k e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
45 39 41 43 44 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
46 38 45 syldan 
 |-  ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
47 37 46 mpbid 
 |-  ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> 1 < ( k x. D ) )
48 25 26 35 47 syl12anc 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> 1 < ( k x. D ) )
49 oveq1 
 |-  ( k = 1 -> ( k x. D ) = ( 1 x. D ) )
50 49 adantl 
 |-  ( ( ph /\ k = 1 ) -> ( k x. D ) = ( 1 x. D ) )
51 2 rpcnd 
 |-  ( ph -> D e. CC )
52 51 adantr 
 |-  ( ( ph /\ k = 1 ) -> D e. CC )
53 52 mulid2d 
 |-  ( ( ph /\ k = 1 ) -> ( 1 x. D ) = D )
54 50 53 eqtrd 
 |-  ( ( ph /\ k = 1 ) -> ( k x. D ) = D )
55 54 oveq1d 
 |-  ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) = ( D / 2 ) )
56 2 rpred 
 |-  ( ph -> D e. RR )
57 56 rehalfcld 
 |-  ( ph -> ( D / 2 ) e. RR )
58 halfre 
 |-  ( 1 / 2 ) e. RR
59 58 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
60 1red 
 |-  ( ph -> 1 e. RR )
61 2re 
 |-  2 e. RR
62 61 a1i 
 |-  ( ph -> 2 e. RR )
63 2pos 
 |-  0 < 2
64 63 a1i 
 |-  ( ph -> 0 < 2 )
65 ltdiv1 
 |-  ( ( D e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
66 56 60 62 64 65 syl112anc 
 |-  ( ph -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
67 3 66 mpbid 
 |-  ( ph -> ( D / 2 ) < ( 1 / 2 ) )
68 halflt1 
 |-  ( 1 / 2 ) < 1
69 68 a1i 
 |-  ( ph -> ( 1 / 2 ) < 1 )
70 57 59 60 67 69 lttrd 
 |-  ( ph -> ( D / 2 ) < 1 )
71 70 adantr 
 |-  ( ( ph /\ k = 1 ) -> ( D / 2 ) < 1 )
72 55 71 eqbrtrd 
 |-  ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
73 72 adantlr 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
74 simpll 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ph )
75 simplrl 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. A )
76 75 23 syl 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. NN )
77 neqne 
 |-  ( -. k = 1 -> k =/= 1 )
78 77 adantl 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k =/= 1 )
79 eluz2b3 
 |-  ( k e. ( ZZ>= ` 2 ) <-> ( k e. NN /\ k =/= 1 ) )
80 76 78 79 sylanbrc 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. ( ZZ>= ` 2 ) )
81 peano2rem 
 |-  ( k e. RR -> ( k - 1 ) e. RR )
82 75 23 40 81 4syl 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
83 56 ad2antrr 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D e. RR )
84 2 rpne0d 
 |-  ( ph -> D =/= 0 )
85 84 ad2antrr 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D =/= 0 )
86 83 85 rereccld 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( 1 / D ) e. RR )
87 1zzd 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> 1 e. ZZ )
88 df-2 
 |-  2 = ( 1 + 1 )
89 88 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
90 89 eleq2i 
 |-  ( k e. ( ZZ>= ` 2 ) <-> k e. ( ZZ>= ` ( 1 + 1 ) ) )
91 eluzsub 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
92 90 91 syl3an3b 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
93 nnuz 
 |-  NN = ( ZZ>= ` 1 )
94 92 93 eleqtrrdi 
 |-  ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. NN )
95 87 87 80 94 syl3anc 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. NN )
96 23 40 syl 
 |-  ( k e. A -> k e. RR )
97 96 adantl 
 |-  ( ( ( k - 1 ) e. A /\ k e. A ) -> k e. RR )
98 97 81 syl 
 |-  ( ( ( k - 1 ) e. A /\ k e. A ) -> ( k - 1 ) e. RR )
99 simpr 
 |-  ( ( ( k - 1 ) e. RR /\ k e. RR ) -> k e. RR )
100 99 ltm1d 
 |-  ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( k - 1 ) < k )
101 ltnle 
 |-  ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( ( k - 1 ) < k <-> -. k <_ ( k - 1 ) ) )
102 100 101 mpbid 
 |-  ( ( ( k - 1 ) e. RR /\ k e. RR ) -> -. k <_ ( k - 1 ) )
103 98 97 102 syl2anc 
 |-  ( ( ( k - 1 ) e. A /\ k e. A ) -> -. k <_ ( k - 1 ) )
104 breq2 
 |-  ( z = ( k - 1 ) -> ( k <_ z <-> k <_ ( k - 1 ) ) )
105 104 notbid 
 |-  ( z = ( k - 1 ) -> ( -. k <_ z <-> -. k <_ ( k - 1 ) ) )
106 105 rspcev 
 |-  ( ( ( k - 1 ) e. A /\ -. k <_ ( k - 1 ) ) -> E. z e. A -. k <_ z )
107 103 106 syldan 
 |-  ( ( ( k - 1 ) e. A /\ k e. A ) -> E. z e. A -. k <_ z )
108 rexnal 
 |-  ( E. z e. A -. k <_ z <-> -. A. z e. A k <_ z )
109 107 108 sylib 
 |-  ( ( ( k - 1 ) e. A /\ k e. A ) -> -. A. z e. A k <_ z )
110 109 ex 
 |-  ( ( k - 1 ) e. A -> ( k e. A -> -. A. z e. A k <_ z ) )
111 imnan 
 |-  ( ( k e. A -> -. A. z e. A k <_ z ) <-> -. ( k e. A /\ A. z e. A k <_ z ) )
112 110 111 sylib 
 |-  ( ( k - 1 ) e. A -> -. ( k e. A /\ A. z e. A k <_ z ) )
113 112 con2i 
 |-  ( ( k e. A /\ A. z e. A k <_ z ) -> -. ( k - 1 ) e. A )
114 113 ad2antlr 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( k - 1 ) e. A )
115 breq2 
 |-  ( j = ( k - 1 ) -> ( ( 1 / D ) < j <-> ( 1 / D ) < ( k - 1 ) ) )
116 115 1 elrab2 
 |-  ( ( k - 1 ) e. A <-> ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
117 114 116 sylnib 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
118 ianor 
 |-  ( -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
119 117 118 sylib 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
120 imor 
 |-  ( ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
121 119 120 sylibr 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) )
122 95 121 mpd 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( 1 / D ) < ( k - 1 ) )
123 82 86 122 nltled 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( 1 / D ) )
124 eluzelre 
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. RR )
125 124 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. RR )
126 56 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. RR )
127 125 126 remulcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. RR )
128 127 rehalfcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) / 2 ) e. RR )
129 128 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) e. RR )
130 60 56 readdcld 
 |-  ( ph -> ( 1 + D ) e. RR )
131 130 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 + D ) e. RR )
132 131 rehalfcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 1 + D ) / 2 ) e. RR )
133 132 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) e. RR )
134 1red 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> 1 e. RR )
135 eluzelcn 
 |-  ( k e. ( ZZ>= ` 2 ) -> k e. CC )
136 135 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. CC )
137 51 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. CC )
138 136 137 mulcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. CC )
139 138 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. CC )
140 51 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. CC )
141 139 140 npcand 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) = ( k x. D ) )
142 127 126 resubcld 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - D ) e. RR )
143 142 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) e. RR )
144 56 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. RR )
145 simp3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) <_ ( 1 / D ) )
146 1red 
 |-  ( k e. ( ZZ>= ` 2 ) -> 1 e. RR )
147 124 146 resubcld 
 |-  ( k e. ( ZZ>= ` 2 ) -> ( k - 1 ) e. RR )
148 147 3ad2ant2 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) e. RR )
149 7 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 / D ) e. RR )
150 42 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( D e. RR /\ 0 < D ) )
151 lemul1 
 |-  ( ( ( 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 ) ) )
152 148 149 150 151 syl3anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) <_ ( 1 / D ) <-> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) ) )
153 145 152 mpbid 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) )
154 1cnd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 e. CC )
155 136 154 137 subdird 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - ( 1 x. D ) ) )
156 137 mulid2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 x. D ) = D )
157 156 oveq2d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - ( 1 x. D ) ) = ( ( k x. D ) - D ) )
158 155 157 eqtrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
159 158 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
160 1cnd 
 |-  ( ph -> 1 e. CC )
161 160 51 84 3jca 
 |-  ( ph -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
162 161 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
163 divcan1 
 |-  ( ( 1 e. CC /\ D e. CC /\ D =/= 0 ) -> ( ( 1 / D ) x. D ) = 1 )
164 162 163 syl 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 / D ) x. D ) = 1 )
165 153 159 164 3brtr3d 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) <_ 1 )
166 143 134 144 165 leadd1dd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) <_ ( 1 + D ) )
167 141 166 eqbrtrrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) <_ ( 1 + D ) )
168 127 3adant3 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. RR )
169 130 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 + D ) e. RR )
170 61 63 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
171 170 a1i 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 2 e. RR /\ 0 < 2 ) )
172 lediv1 
 |-  ( ( ( 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 ) ) )
173 168 169 171 172 syl3anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) <_ ( 1 + D ) <-> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) ) )
174 167 173 mpbid 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) )
175 56 60 60 3 ltadd2dd 
 |-  ( ph -> ( 1 + D ) < ( 1 + 1 ) )
176 1p1e2 
 |-  ( 1 + 1 ) = 2
177 175 176 breqtrdi 
 |-  ( ph -> ( 1 + D ) < 2 )
178 ltdiv1 
 |-  ( ( ( 1 + D ) e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
179 130 62 62 64 178 syl112anc 
 |-  ( ph -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
180 177 179 mpbid 
 |-  ( ph -> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) )
181 2div2e1 
 |-  ( 2 / 2 ) = 1
182 180 181 breqtrdi 
 |-  ( ph -> ( ( 1 + D ) / 2 ) < 1 )
183 182 3ad2ant1 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) < 1 )
184 129 133 134 174 183 lelttrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) < 1 )
185 74 80 123 184 syl3anc 
 |-  ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
186 73 185 pm2.61dan 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( ( k x. D ) / 2 ) < 1 )
187 24 48 186 jca32 
 |-  ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
188 187 ex 
 |-  ( ph -> ( ( k e. A /\ A. z e. A k <_ z ) -> ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) ) )
189 188 eximdv 
 |-  ( 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 ) ) ) )
190 21 189 mpd 
 |-  ( ph -> E. k ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
191 df-rex 
 |-  ( 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 ) ) )
192 190 191 sylibr 
 |-  ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )