Theorem stoweidlem14 29657

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 3427	. . . . . . 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 3390	. . . . 5 |- ( ph -> A C_ NN )
5		stoweidlem14.2	. . . . . . 7 |- ( ph -> D e. RR+ )
6	5	rprecred 11028	. . . . . 6 |- ( ph -> ( 1 / D ) e. RR )
7		arch 10566	. . . . . 6 |- ( ( 1 / D ) e. RR -> E. k e. NN ( 1 / D ) < k )
8		breq2 4286	. . . . . . . . . . 11 |- ( j = k -> ( ( 1 / D ) < j <-> ( 1 / D ) < k ) )
9	8	elrab 3108	. . . . . . . . . 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 2526	. . . . . . . 8 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> k e. A )
12		simpr 458	. . . . . . . 8 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> ( 1 / D ) < k )
13	11, 12	jca 529	. . . . . . 7 |- ( ( k e. NN /\ ( 1 / D ) < k ) -> ( k e. A /\ ( 1 / D ) < k ) )
14	13	reximi2 2814	. . . . . 6 |- ( E. k e. NN ( 1 / D ) < k -> E. k e. A ( 1 / D ) < k )
15		rexn0 3772	. . . . . 6 |- ( E. k e. A ( 1 / D ) < k -> A =/= (/) )
16	6, 7, 14, 15	4syl 21	. . . . 5 |- ( ph -> A =/= (/) )
17		nnwo 10910	. . . . 5 |- ( ( A C_ NN /\ A =/= (/) ) -> E. k e. A A. z e. A k <_ z )
18	4, 16, 17	syl2anc 656	. . . 4 |- ( ph -> E. k e. A A. z e. A k <_ z )
19		df-rex 2713	. . . 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 3110	. . . . . . . 8 |- ( k e. A <-> ( k e. NN /\ ( 1 / D ) < k ) )
22	21	simplbi 457	. . . . . . 7 |- ( k e. A -> k e. NN )
23	22	ad2antrl 722	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. NN )
24		simpl 454	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ph )
25		simprl 750	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> k e. A )
26		simprr 751	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> A. z e. A k <_ z )
27		nfcv 2571	. . . . . . . . 9 |- F/_ z A
28		nfrab1 2893	. . . . . . . . . 10 |- F/_ j { j e. NN | ( 1 / D ) < j }
29	1, 28	nfcxfr 2568	. . . . . . . . 9 |- F/_ j A
30		nfv 1674	. . . . . . . . 9 |- F/ j k <_ z
31		nfv 1674	. . . . . . . . 9 |- F/ z k <_ j
32		breq2 4286	. . . . . . . . 9 |- ( z = j -> ( k <_ z <-> k <_ j ) )
33	27, 29, 30, 31, 32	cbvralf 2933	. . . . . . . 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 461	. . . . . . . . 9 |- ( k e. A -> ( 1 / D ) < k )
36	35	ad2antrl 722	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( 1 / D ) < k )
37	22	ad2antrl 722	. . . . . . . . 9 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> k e. NN )
38		1re 9375	. . . . . . . . . . 11 |- 1 e. RR
39	38	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> 1 e. RR )
40		nnre 10319	. . . . . . . . . . 11 |- ( k e. NN -> k e. RR )
41	40	adantl 463	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> k e. RR )
42	5	rpregt0d 11023	. . . . . . . . . . 11 |- ( ph -> ( D e. RR /\ 0 < D ) )
43	42	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( D e. RR /\ 0 < D ) )
44		ltdivmul2 10197	. . . . . . . . . 10 |- ( ( 1 e. RR /\ k e. RR /\ ( D e. RR /\ 0 < D ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
45	39, 41, 43, 44	syl3anc 1213	. . . . . . . . 9 |- ( ( ph /\ k e. NN ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
46	37, 45	syldan 467	. . . . . . . 8 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> ( ( 1 / D ) < k <-> 1 < ( k x. D ) ) )
47	36, 46	mpbid 210	. . . . . . 7 |- ( ( ph /\ ( k e. A /\ A. j e. A k <_ j ) ) -> 1 < ( k x. D ) )
48	24, 25, 34, 47	syl12anc 1211	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> 1 < ( k x. D ) )
49		oveq1 6089	. . . . . . . . . . . 12 |- ( k = 1 -> ( k x. D ) = ( 1 x. D ) )
50	49	adantl 463	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( k x. D ) = ( 1 x. D ) )
51	5	rpcnd 11019	. . . . . . . . . . . . 13 |- ( ph -> D e. CC )
52	51	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ k = 1 ) -> D e. CC )
53	52	mulid2d 9394	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( 1 x. D ) = D )
54	50, 53	eqtrd 2467	. . . . . . . . . 10 |- ( ( ph /\ k = 1 ) -> ( k x. D ) = D )
55	54	oveq1d 6097	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) = ( D / 2 ) )
56	5	rpred 11017	. . . . . . . . . . . 12 |- ( ph -> D e. RR )
57	56	rehalfcld 10561	. . . . . . . . . . 11 |- ( ph -> ( D / 2 ) e. RR )
58		halfre 10530	. . . . . . . . . . . 12 |- ( 1 / 2 ) e. RR
59	58	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 1 / 2 ) e. RR )
60	38	a1i 11	. . . . . . . . . . 11 |- ( ph -> 1 e. RR )
61		stoweidlem14.3	. . . . . . . . . . . 12 |- ( ph -> D < 1 )
62		2re 10381	. . . . . . . . . . . . . 14 |- 2 e. RR
63	62	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. RR )
64		2pos 10403	. . . . . . . . . . . . . 14 |- 0 < 2
65	64	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 0 < 2 )
66		ltdiv1 10183	. . . . . . . . . . . . 13 |- ( ( D e. RR /\ 1 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
67	56, 60, 63, 65, 66	syl112anc 1217	. . . . . . . . . . . 12 |- ( ph -> ( D < 1 <-> ( D / 2 ) < ( 1 / 2 ) ) )
68	61, 67	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( D / 2 ) < ( 1 / 2 ) )
69		halflt1 10533	. . . . . . . . . . . 12 |- ( 1 / 2 ) < 1
70	69	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( 1 / 2 ) < 1 )
71	57, 59, 60, 68, 70	lttrd 9522	. . . . . . . . . 10 |- ( ph -> ( D / 2 ) < 1 )
72	71	adantr 462	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( D / 2 ) < 1 )
73	55, 72	eqbrtrd 4302	. . . . . . . 8 |- ( ( ph /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
74	73	adantlr 709	. . . . . . 7 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
75		simpll 748	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ph )
76		simplrl 754	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. A )
77	76, 22	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. NN )
78		df-ne 2600	. . . . . . . . . . 11 |- ( k =/= 1 <-> -. k = 1 )
79	78	biimpri 206	. . . . . . . . . 10 |- ( -. k = 1 -> k =/= 1 )
80	79	adantl 463	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k =/= 1 )
81		eluz2b3 10918	. . . . . . . . 9 |- ( k e. ( ZZ>= ` 2 ) <-> ( k e. NN /\ k =/= 1 ) )
82	77, 80, 81	sylanbrc 659	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> k e. ( ZZ>= ` 2 ) )
83		1z 10666	. . . . . . . . . . . 12 |- 1 e. ZZ
84	83	a1i 11	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> 1 e. ZZ )
85		df-2 10370	. . . . . . . . . . . . . . 15 |- 2 = ( 1 + 1 )
86	85	fveq2i 5684	. . . . . . . . . . . . . 14 |- ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
87	86	eleq2i 2499	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` 2 ) <-> k e. ( ZZ>= ` ( 1 + 1 ) ) )
88		eluzsub 10880	. . . . . . . . . . . . 13 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` ( 1 + 1 ) ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
89	87, 88	syl3an3b 1251	. . . . . . . . . . . 12 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. ( ZZ>= ` 1 ) )
90		nnuz 10886	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
91	89, 90	syl6eleqr 2526	. . . . . . . . . . 11 |- ( ( 1 e. ZZ /\ 1 e. ZZ /\ k e. ( ZZ>= ` 2 ) ) -> ( k - 1 ) e. NN )
92	84, 84, 82, 91	syl3anc 1213	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. NN )
93	22, 40	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. A -> k e. RR )
94	93	adantl 463	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> k e. RR )
95		peano2rem 9665	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. RR -> ( k - 1 ) e. RR )
96	94, 95	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> ( k - 1 ) e. RR )
97		simpr 458	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> k e. RR )
98	97	ltm1d 10255	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( k - 1 ) < k )
99		ltnle 9444	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> ( ( k - 1 ) < k <-> -. k <_ ( k - 1 ) ) )
100	98, 99	mpbid 210	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( k - 1 ) e. RR /\ k e. RR ) -> -. k <_ ( k - 1 ) )
101	96, 94, 100	syl2anc 656	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> -. k <_ ( k - 1 ) )
102		breq2 4286	. . . . . . . . . . . . . . . . . . . . 21 |- ( z = ( k - 1 ) -> ( k <_ z <-> k <_ ( k - 1 ) ) )
103	102	notbid 294	. . . . . . . . . . . . . . . . . . . 20 |- ( z = ( k - 1 ) -> ( -. k <_ z <-> -. k <_ ( k - 1 ) ) )
104	103	rspcev 3064	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( k - 1 ) e. A /\ -. k <_ ( k - 1 ) ) -> E. z e. A -. k <_ z )
105	101, 104	syldan 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> E. z e. A -. k <_ z )
106		rexnal 2718	. . . . . . . . . . . . . . . . . 18 |- ( E. z e. A -. k <_ z <-> -. A. z e. A k <_ z )
107	105, 106	sylib 196	. . . . . . . . . . . . . . . . 17 |- ( ( ( k - 1 ) e. A /\ k e. A ) -> -. A. z e. A k <_ z )
108	107	ex 434	. . . . . . . . . . . . . . . 16 |- ( ( k - 1 ) e. A -> ( k e. A -> -. A. z e. A k <_ z ) )
109		imnan 422	. . . . . . . . . . . . . . . 16 |- ( ( k e. A -> -. A. z e. A k <_ z ) <-> -. ( k e. A /\ A. z e. A k <_ z ) )
110	108, 109	sylib 196	. . . . . . . . . . . . . . 15 |- ( ( k - 1 ) e. A -> -. ( k e. A /\ A. z e. A k <_ z ) )
111	110	con2i 120	. . . . . . . . . . . . . 14 |- ( ( k e. A /\ A. z e. A k <_ z ) -> -. ( k - 1 ) e. A )
112	111	ad2antlr 721	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( k - 1 ) e. A )
113		breq2 4286	. . . . . . . . . . . . . 14 |- ( j = ( k - 1 ) -> ( ( 1 / D ) < j <-> ( 1 / D ) < ( k - 1 ) ) )
114	113, 1	elrab2 3110	. . . . . . . . . . . . 13 |- ( ( k - 1 ) e. A <-> ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
115	112, 114	sylnib 304	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) )
116		ianor 485	. . . . . . . . . . . 12 |- ( -. ( ( k - 1 ) e. NN /\ ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
117	115, 116	sylib 196	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
118		imor 412	. . . . . . . . . . 11 |- ( ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) <-> ( -. ( k - 1 ) e. NN \/ -. ( 1 / D ) < ( k - 1 ) ) )
119	117, 118	sylibr 212	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k - 1 ) e. NN -> -. ( 1 / D ) < ( k - 1 ) ) )
120	92, 119	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> -. ( 1 / D ) < ( k - 1 ) )
121	76, 22, 40, 95	4syl 21	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) e. RR )
122	56	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D e. RR )
123	5	rpne0d 11022	. . . . . . . . . . . 12 |- ( ph -> D =/= 0 )
124	123	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> D =/= 0 )
125	122, 124	rereccld 10148	. . . . . . . . . 10 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( 1 / D ) e. RR )
126	121, 125	lenltd 9510	. . . . . . . . 9 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k - 1 ) <_ ( 1 / D ) <-> -. ( 1 / D ) < ( k - 1 ) ) )
127	120, 126	mpbird 232	. . . . . . . 8 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( k - 1 ) <_ ( 1 / D ) )
128		eluzelre 10861	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` 2 ) -> k e. RR )
129	128	adantl 463	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. RR )
130	56	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. RR )
131	129, 130	remulcld 9404	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. RR )
132	131	rehalfcld 10561	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) / 2 ) e. RR )
133	132	3adant3 1003	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) e. RR )
134	60, 56	readdcld 9403	. . . . . . . . . . . 12 |- ( ph -> ( 1 + D ) e. RR )
135	134	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 + D ) e. RR )
136	135	rehalfcld 10561	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 1 + D ) / 2 ) e. RR )
137	136	3adant3 1003	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) e. RR )
138	38	a1i 11	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> 1 e. RR )
139		eluzelcn 10862	. . . . . . . . . . . . . . 15 |- ( k e. ( ZZ>= ` 2 ) -> k e. CC )
140	139	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. CC )
141	51	adantr 462	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> D e. CC )
142	140, 141	mulcld 9396	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( k x. D ) e. CC )
143	142	3adant3 1003	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. CC )
144	51	3ad2ant1 1004	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. CC )
145	143, 144	npcand 9713	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) = ( k x. D ) )
146	131, 130	resubcld 9766	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - D ) e. RR )
147	146	3adant3 1003	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) e. RR )
148	56	3ad2ant1 1004	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> D e. RR )
149		simp3 985	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) <_ ( 1 / D ) )
150	38	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( k e. ( ZZ>= ` 2 ) -> 1 e. RR )
151	128, 150	resubcld 9766	. . . . . . . . . . . . . . . 16 |- ( k e. ( ZZ>= ` 2 ) -> ( k - 1 ) e. RR )
152	151	3ad2ant2 1005	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k - 1 ) e. RR )
153	6	3ad2ant1 1004	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 / D ) e. RR )
154	42	3ad2ant1 1004	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( D e. RR /\ 0 < D ) )
155		lemul1 10171	. . . . . . . . . . . . . . 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 ) ) )
156	152, 153, 154, 155	syl3anc 1213	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) <_ ( 1 / D ) <-> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) ) )
157	149, 156	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) <_ ( ( 1 / D ) x. D ) )
158		ax-1cn 9330	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
159	158	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 e. CC )
160	140, 159, 141	subdird 9791	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - ( 1 x. D ) ) )
161	141	mulid2d 9394	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 1 x. D ) = D )
162	161	oveq2d 6098	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k x. D ) - ( 1 x. D ) ) = ( ( k x. D ) - D ) )
163	160, 162	eqtrd 2467	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
164	163	3adant3 1003	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k - 1 ) x. D ) = ( ( k x. D ) - D ) )
165	158	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. CC )
166	165, 51, 123	3jca 1163	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
167	166	3ad2ant1 1004	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 e. CC /\ D e. CC /\ D =/= 0 ) )
168		divcan1 9993	. . . . . . . . . . . . . 14 |- ( ( 1 e. CC /\ D e. CC /\ D =/= 0 ) -> ( ( 1 / D ) x. D ) = 1 )
169	167, 168	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 / D ) x. D ) = 1 )
170	157, 164, 169	3brtr3d 4311	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) - D ) <_ 1 )
171	147, 138, 148, 170	leadd1dd 9943	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( ( k x. D ) - D ) + D ) <_ ( 1 + D ) )
172	145, 171	eqbrtrrd 4304	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) <_ ( 1 + D ) )
173	131	3adant3 1003	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( k x. D ) e. RR )
174	134	3ad2ant1 1004	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 1 + D ) e. RR )
175	62, 64	pm3.2i 452	. . . . . . . . . . . 12 |- ( 2 e. RR /\ 0 < 2 )
176	175	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( 2 e. RR /\ 0 < 2 ) )
177		lediv1 10184	. . . . . . . . . . 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 ) ) )
178	173, 174, 176, 177	syl3anc 1213	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) <_ ( 1 + D ) <-> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) ) )
179	172, 178	mpbid 210	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) <_ ( ( 1 + D ) / 2 ) )
180	56, 60, 60, 61	ltadd2dd 9520	. . . . . . . . . . . . 13 |- ( ph -> ( 1 + D ) < ( 1 + 1 ) )
181		1p1e2 10425	. . . . . . . . . . . . 13 |- ( 1 + 1 ) = 2
182	180, 181	syl6breq 4321	. . . . . . . . . . . 12 |- ( ph -> ( 1 + D ) < 2 )
183		ltdiv1 10183	. . . . . . . . . . . . 13 |- ( ( ( 1 + D ) e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
184	134, 63, 63, 65, 183	syl112anc 1217	. . . . . . . . . . . 12 |- ( ph -> ( ( 1 + D ) < 2 <-> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) ) )
185	182, 184	mpbid 210	. . . . . . . . . . 11 |- ( ph -> ( ( 1 + D ) / 2 ) < ( 2 / 2 ) )
186		2div2e1 10434	. . . . . . . . . . 11 |- ( 2 / 2 ) = 1
187	185, 186	syl6breq 4321	. . . . . . . . . 10 |- ( ph -> ( ( 1 + D ) / 2 ) < 1 )
188	187	3ad2ant1 1004	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( 1 + D ) / 2 ) < 1 )
189	133, 137, 138, 179, 188	lelttrd 9519	. . . . . . . 8 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) /\ ( k - 1 ) <_ ( 1 / D ) ) -> ( ( k x. D ) / 2 ) < 1 )
190	75, 82, 127, 189	syl3anc 1213	. . . . . . 7 |- ( ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) /\ -. k = 1 ) -> ( ( k x. D ) / 2 ) < 1 )
191	74, 190	pm2.61dan 784	. . . . . 6 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( ( k x. D ) / 2 ) < 1 )
192	23, 48, 191	jca32 532	. . . . 5 |- ( ( ph /\ ( k e. A /\ A. z e. A k <_ z ) ) -> ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
193	192	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 ) ) ) )
194	193	eximdv 1677	. . 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 ) ) ) )
195	20, 194	mpd 15	. 2 |- ( ph -> E. k ( k e. NN /\ ( 1 < ( k x. D ) /\ ( ( k x. D ) / 2 ) < 1 ) ) )
196		df-rex 2713	. 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 ) ) )
197	195, 196	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 960   = wceq 1364   E.wex 1591   e. wcel 1757   =/= wne 2598   A.wral 2707   E.wrex 2708   {crab 2711   C_ wss 3318   (/)c0 3627   class class class wbr 4282   ` cfv 5408  (class class class)co 6082   CCcc 9270   RRcr 9271   0cc0 9272   1c1 9273   + caddc 9275   x. cmul 9277   < clt 9408   <_ cle 9409   - cmin 9585   / cdiv 9983   NNcn 10312   2c2 10361   ZZcz 10636   ZZ>=cuz 10851   RR+crp 10981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-cnex 9328  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349  ax-pre-sup 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-div 9984  df-nn 10313  df-2 10370  df-n0 10570  df-z 10637  df-uz 10852  df-rp 10982

This theorem is referenced by:  stoweidlem49  29692