Theorem stoweidlem14 29809

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.

Step	Hyp	Ref	Expression
1		stoweidlem14.1	. . . . . 6 |- A = { j e. NN | ( 1 / D ) < j }
2		ssrab2 3437	. . . . . . 7 |- { j e. NN | ( 1 / D ) < j } C_ NN
3	2	a1i 11	. . . . . 6 |- ( ph -> { j e. NN | ( 1 / D ) < j } C_ NN )
4	1, 3	syl5eqss 3400	. . . . 5 |- ( ph -> A C_ NN )
5		stoweidlem14.2	. . . . . . 7 |- ( ph -> D e. RR+ )
6	5	rprecred 11038	. . . . . 6 |- ( ph -> ( 1 / D ) e. RR )
7		arch 10576	. . . . . 6 |- ( ( 1 / D ) e. RR -> E. k e. NN ( 1 / D ) < k )
8		breq2 4296	. . . . . . . . . . 11 |- ( j = k -> ( ( 1 / D ) < j <-> ( 1 / D ) < k ) )
9	8	elrab 3117	. . . . . . . . . 10 |- ( k e. { j e. NN | ( 1 / D ) < j } <-> ( k e. NN /\ ( 1 / D ) < k ) )
10	9	biimpri 206	. . . . . . . . 9 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> k e. { j e. NN | ( 1 / D ) < j } )
11	10, 1	syl6eleqr 2534	. . . . . . . 8 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> k e. A )
12		simpr 461	. . . . . . . 8 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> ( 1 / D ) < k )
13	11, 12	jca 532	. . . . . . 7 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> ( k e. A /\ ( 1 / D ) < k ) )
14	13	reximi2 2822	. . . . . 6 |- ( E. k e. NN ( 1 / D ) < k -> E. k e. A ( 1 / D ) < k )
15		rexn0 3782	. . . . . 6 |- ( E. k e. A ( 1 / D ) < k -> A =/= (/) )
16	6, 7, 14, 15	4syl 21	. . . . 5 |- ( ph -> A =/= (/) )
17		nnwo 10920	. . . . 5 |- ( ( A C_ NN /\ A =/= (/) ) -> E. k e. A A. z e. A k <_ z )
18	4, 16, 17	syl2anc 661	. . . 4 |- ( ph -> E. k e. A A. z e. A k <_ z )
19		df-rex 2721	. . . 4 |- ( E. k e. A A. z e. A k <_ z <-> E. k ( k e. A /\ A. z e. A k <_ z ) )
20	18, 19	sylib 196	. . 3 |- ( ph -> E. k ( k e. A /\ A. z e. A k <_ z ) )
21	8, 1	elrab2 3119	. . . . . . . 8 |- ( k e. A <-> ( k e. NN /\ ( 1 / D ) < k ) )
22	21	simplbi 460	. . . . . . 7 |- ( k e. A -> k e. NN )
23	22	ad2antrl 727	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. NN )
24		simpl 457	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ph )
25		simprl 755	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. A )
26		simprr 756	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> A. z e. A k <_ z )
27		nfcv 2579	. . . . . . . . 9 |- F/_ z A
28		nfrab1 2901	. . . . . . . . . 10 |- F/_ j { j e. NN | ( 1 / D ) < j }
29	1, 28	nfcxfr 2576	. . . . . . . . 9 |- F/_ j A
30		nfv 1673	. . . . . . . . 9 |- F/ j k <_ z
31		nfv 1673	. . . . . . . . 9 |- F/ z k <_ j
32		breq2 4296	. . . . . . . . 9 |- ( z = j -> ( k <_ z <-> k <_ j ) )
33	27, 29, 30, 31, 32	cbvralf 2941	. . . . . . . 8 |- ( A. z e. A k <_ z <-> A. j e. A k <_ j )
34	26, 33	sylib 196	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> A. j e. A k <_ j )
35	21	simprbi 464	. . . . . . . . 9 |- ( k e. A -> ( 1 / D ) < k )
36	35	ad2antrl 727	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( 1 / D ) < k )
37	22	ad2antrl 727	. . . . . . . . 9 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> k e. NN )
38		1red 9401	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> 1 e. RR )
39		nnre 10329	. . . . . . . . . . 11 |- ( k e. NN -> k e. RR )
40	39	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> k e. RR )
41	5	rpregt0d 11033	. . . . . . . . . . 11 |- ( ph -> ( D e. RR /\ 0 < D ) )
42	41	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( D e. RR /\ 0 < D ) )
43		ltdivmul2 10207	. . . . . . . . . 10 |- ( ( 1 e. RR /\ k e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
44	38, 40, 42, 43	syl3anc 1218	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
45	37, 44	syldan 470	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
46	36, 45	mpbid 210	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> 1 < ( k x. D ) )
47	24, 25, 34, 46	syl12anc 1216	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> 1 < ( k x. D ) )
48		oveq1 6098	. . . . . . . . . . . 12 |- ( k = 1 -> ( k x. D ) = ( 1 x. D ) )
49	48	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( k x. D ) = ( 1 x. D ) )
50	5	rpcnd 11029	. . . . . . . . . . . . 13 |- ( ph -> D e. CC )
51	50	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ k = 1 ) -> D e. CC )
52	51	mulid2d 9404	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( 1 x. D ) = D )
53	49, 52	eqtrd 2475	. . . . . . . . . 10 |- ( ( ph /\ k = 1 ) -> ( k x. D ) = D )
54	53	oveq1d 6106	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) = ( D / 2 ) )
55	5	rpred 11027	. . . . . . . . . . . 12 |- ( ph -> D e. RR )
56	55	rehalfcld 10571	. . . . . . . . . . 11 |- ( ph -> ( D / 2 ) e. RR )
57		halfre 10540	. . . . . . . . . . . 12 |- ( 1 / 2 ) e. RR
58	57	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 1 / 2 ) e. RR )
59		1red 9401	. . . . . . . . . . 11 |- ( ph -> 1 e. RR )
60		stoweidlem14.3	. . . . . . . . . . . 12 |- ( ph -> D < 1 )
61		2re 10391	. . . . . . . . . . . . . 14 |- 2 e. RR
62	61	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. RR )
63		2pos 10413	. . . . . . . . . . . . . 14 |- 0 < 2
64	63	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 0 < 2 )
65		ltdiv1 10193	. . . . . . . . . . . . 13 |- ( ( D e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
66	55, 59, 62, 64, 65	syl112anc 1222	. . . . . . . . . . . 12 |- ( ph -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
67	60, 66	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( D / 2 ) < ( 1 / 2 ) )
68		halflt1 10543	. . . . . . . . . . . 12 |- ( 1 / 2 ) < 1
69	68	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 1 / 2 ) < 1 )
70	56, 58, 59, 67, 69	lttrd 9532	. . . . . . . . . 10 |- ( ph -> ( D / 2 ) < 1 )
71	70	adantr 465	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( D / 2 ) < 1 )
72	54, 71	eqbrtrd 4312	. . . . . . . 8 |- ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
73	72	adantlr 714	. . . . . . 7 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
74		simpll 753	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ph )
75		simplrl 759	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. A )
76	75, 22	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. NN )
77		df-ne 2608	. . . . . . . . . . 11 |- ( k =/= 1 <-> -. k = 1 )
78	77	biimpri 206	. . . . . . . . . 10 |- ( -. k = 1 -> k =/= 1 )
79	78	adantl 466	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k =/= 1 )
80		eluz2b3 10928	. . . . . . . . 9 |- ( k e. ( ZZ>= ` 2 ) <-> ( k e. NN /\ k =/= 1 ) )
81	76, 79, 80	sylanbrc 664	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. ( ZZ>= ` 2 ) )
82		1zzd 10677	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> 1 e. ZZ )
83		df-2 10380	. . . . . . . . . . . . . . 15 |- 2 = ( 1 + 1 )
84	83	fveq2i 5694	. . . . . . . . . . . . . 14 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
85	84	eleq2i 2507	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` 2 ) <-> k e. ( ZZ>= ` ( 1 + 1 ) ) )
86		eluzsub 10890	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
87	85, 86	syl3an3b 1256	. . . . . . . . . . . 12 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
88		nnuz 10896	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
89	87, 88	syl6eleqr 2534	. . . . . . . . . . 11 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. NN )
90	82, 82, 81, 89	syl3anc 1218	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. NN )
91	22, 39	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> k e. RR )
92	91	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> k e. RR )
93		peano2rem 9675	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. RR -> ( k - 1 ) e. RR )
94	92, 93	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> ( k - 1 ) e. RR )
95		simpr 461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> k e. RR )
96	95	ltm1d 10265	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( k - 1 ) < k )
97		ltnle 9454	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( ( k - 1 ) < k <-> -. k <_ ( k - 1 ) ) )
98	96, 97	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> -. k <_ ( k - 1 ) )
99	94, 92, 98	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> -. k <_ ( k - 1 ) )
100		breq2 4296	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( k - 1 ) -> ( k <_ z <-> k <_ ( k - 1 ) ) )
101	100	notbid 294	. . . . . . . . . . . . . . . . . . . 20 |- ( z = ( k - 1 ) -> ( -. k <_ z <-> -. k <_ ( k - 1 ) ) )
102	101	rspcev 3073	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( k - 1 ) e. A /\ -. k <_ ( k - 1 ) ) -> E. z e. A -. k <_ z )
103	99, 102	syldan 470	. . . . . . . . . . . . . . . . . 18 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> E. z e. A -. k <_ z )
104		rexnal 2726	. . . . . . . . . . . . . . . . . 18 |- ( E. z e. A -. k <_ z <-> -. A. z e. A k <_ z )
105	103, 104	sylib 196	. . . . . . . . . . . . . . . . 17 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> -. A. z e. A k <_ z )
106	105	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( k - 1 ) e. A -> ( k e. A -> -. A. z e. A k <_ z ) )
107		imnan 422	. . . . . . . . . . . . . . . 16 |- ( ( k e. A -> -. A. z e. A k <_ z ) <-> -. ( k e. A /\ A. z e. A k <_ z ) )
108	106, 107	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( k - 1 ) e. A -> -. ( k e. A /\ A. z e. A k <_ z ) )
109	108	con2i 120	. . . . . . . . . . . . . 14 |- ( ( k e. A /\ A. z e. A k <_ z ) -> -. ( k - 1 ) e. A )
110	109	ad2antlr 726	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( k - 1 ) e. A )
111		breq2 4296	. . . . . . . . . . . . . 14 |- ( j = ( k - 1 ) -> ( ( 1 / D ) < j <-> ( 1 / D ) < ( k - 1 ) ) )
112	111, 1	elrab2 3119	. . . . . . . . . . . . 13 |- ( ( k - 1 ) e. A <-> ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
113	110, 112	sylnib 304	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
114		ianor 488	. . . . . . . . . . . 12 |- ( -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
115	113, 114	sylib 196	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
116		imor 412	. . . . . . . . . . 11 |- ( ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
117	115, 116	sylibr 212	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) )
118	90, 117	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( 1 / D ) < ( k - 1 ) )
119	75, 22, 39, 93	4syl 21	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
120	55	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D e. RR )
121	5	rpne0d 11032	. . . . . . . . . . . 12 |- ( ph -> D =/= 0 )
122	121	ad2antrr 725	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D =/= 0 )
123	120, 122	rereccld 10158	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( 1 / D ) e. RR )
124	119, 123	lenltd 9520	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k - 1 ) <_ ( 1 / D ) <-> -. ( 1 / D ) < ( k - 1 ) ) )
125	118, 124	mpbird 232	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( 1 / D ) )
126		eluzelre 10871	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` 2 ) -> k e. RR )
127	126	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. RR )
128	55	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. RR )
129	127, 128	remulcld 9414	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. RR )
130	129	rehalfcld 10571	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) / 2 ) e. RR )
131	130	3adant3 1008	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) e. RR )
132	59, 55	readdcld 9413	. . . . . . . . . . . 12 |- ( ph -> ( 1 + D ) e. RR )
133	132	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 + D ) e. RR )
134	133	rehalfcld 10571	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 1 + D ) / 2 ) e. RR )
135	134	3adant3 1008	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) e. RR )
136		1red 9401	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> 1 e. RR )
137		eluzelcn 10872	. . . . . . . . . . . . . . 15 |- ( k e. ( ZZ>= ` 2 ) -> k e. CC )
138	137	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. CC )
139	50	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. CC )
140	138, 139	mulcld 9406	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. CC )
141	140	3adant3 1008	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. CC )
142	50	3ad2ant1 1009	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. CC )
143	141, 142	npcand 9723	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) = ( k x. D ) )
144	129, 128	resubcld 9776	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - D ) e. RR )
145	144	3adant3 1008	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) e. RR )
146	55	3ad2ant1 1009	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. RR )
147		simp3 990	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) <_ ( 1 / D ) )
148		1red 9401	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ZZ>= ` 2 ) -> 1 e. RR )
149	126, 148	resubcld 9776	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` 2 ) -> ( k - 1 ) e. RR )
150	149	3ad2ant2 1010	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) e. RR )
151	6	3ad2ant1 1009	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 / D ) e. RR )
152	41	3ad2ant1 1009	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( D e. RR /\ 0 < D ) )
153		lemul1 10181	. . . . . . . . . . . . . . 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 ) ) )
154	150, 151, 152, 153	syl3anc 1218	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) <_ ( 1 / D ) <-> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) ) )
155	147, 154	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) )
156		1cnd 9402	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 e. CC )
157	138, 156, 139	subdird 9801	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - ( 1 x. D ) ) )
158	139	mulid2d 9404	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 x. D ) = D )
159	158	oveq2d 6107	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - ( 1 x. D ) ) = ( ( k x. D ) - D ) )
160	157, 159	eqtrd 2475	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
161	160	3adant3 1008	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
162		1cnd 9402	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. CC )
163	162, 50, 121	3jca 1168	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
164	163	3ad2ant1 1009	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
165		divcan1 10003	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ D e. CC /\ D =/= 0 ) -> ( ( 1 / D ) x. D ) = 1 )
166	164, 165	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 / D ) x. D ) = 1 )
167	155, 161, 166	3brtr3d 4321	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) <_ 1 )
168	145, 136, 146, 167	leadd1dd 9953	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) <_ ( 1 + D ) )
169	143, 168	eqbrtrrd 4314	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) <_ ( 1 + D ) )
170	129	3adant3 1008	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. RR )
171	132	3ad2ant1 1009	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 + D ) e. RR )
172	61, 63	pm3.2i 455	. . . . . . . . . . . 12 |- ( 2 e. RR /\ 0 < 2 )
173	172	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 2 e. RR /\ 0 < 2 ) )
174		lediv1 10194	. . . . . . . . . . 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 ) ) )
175	170, 171, 173, 174	syl3anc 1218	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) <_ ( 1 + D ) <-> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) ) )
176	169, 175	mpbid 210	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) )
177	55, 59, 59, 60	ltadd2dd 9530	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + D ) < ( 1 + 1 ) )
178		1p1e2 10435	. . . . . . . . . . . . 13 |- ( 1 + 1 ) = 2
179	177, 178	syl6breq 4331	. . . . . . . . . . . 12 |- ( ph -> ( 1 + D ) < 2 )
180		ltdiv1 10193	. . . . . . . . . . . . 13 |- ( ( ( 1 + D ) e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
181	132, 62, 62, 64, 180	syl112anc 1222	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
182	179, 181	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) )
183		2div2e1 10444	. . . . . . . . . . 11 |- ( 2 / 2 ) = 1
184	182, 183	syl6breq 4331	. . . . . . . . . 10 |- ( ph -> ( ( 1 + D ) / 2 ) < 1 )
185	184	3ad2ant1 1009	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) < 1 )
186	131, 135, 136, 176, 185	lelttrd 9529	. . . . . . . 8 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) < 1 )
187	74, 81, 125, 186	syl3anc 1218	. . . . . . 7 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
188	73, 187	pm2.61dan 789	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( ( k x. D ) / 2 ) < 1 )
189	23, 47, 188	jca32 535	. . . . 5 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
190	189	ex 434	. . . 4 |- ( ph -> ( ( k e. A /\ A. z e. A k <_ z ) -> ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) ) )
191	190	eximdv 1676	. . 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 ) ) ) )
192	20, 191	mpd 15	. 2 |- ( ph -> E. k ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
193		df-rex 2721	. 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 ) ) )
194	192, 193	sylibr 212	1 |- ( ph -> E. k e. NN ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 965   = wceq 1369   E.wex 1586   e. wcel 1756   =/= wne 2606   A.wral 2715   E.wrex 2716   {crab 2719   C_ wss 3328   (/)c0 3637   class class class wbr 4292   ` cfv 5418  (class class class)co 6091   CCcc 9280   RRcr 9281   0cc0 9282   1c1 9283   + caddc 9285   x. cmul 9287   < clt 9418   <_ cle 9419   - cmin 9595   / cdiv 9993   NNcn 10322   2c2 10371   ZZcz 10646   ZZ>=cuz 10861   RR+crp 10991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359  ax-pre-sup 9360

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-recs 6832  df-rdg 6866  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-div 9994  df-nn 10323  df-2 10380  df-n0 10580  df-z 10647  df-uz 10862  df-rp 10992

This theorem is referenced by:  stoweidlem49  29844