Theorem cvg1nlemres 9871

Description: Lemma for cvg1n 9872. The original sequence F has a limit (turns out it is the same as the limit of the modified sequence G). (Contributed by Jim Kingdon, 1-Aug-2021.)

Hypotheses

Ref	Expression
cvg1n.f	|- ( ph -> F : NN --> RR )
cvg1n.c	|- ( ph -> C e. RR+ )
cvg1n.cau	|- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )
cvg1nlem.g	|- G = ( j e. NN |-> ( F ` ( j x. Z ) ) )
cvg1nlem.z	|- ( ph -> Z e. NN )
cvg1nlem.start	|- ( ph -> C < Z )

Assertion

Ref	Expression
cvg1nlemres	|- ( ph -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )

Distinct variable groups:   C, i, k   C, n, k   j, F, k, n   i, G, y, k   n, G   x, G, i, y   i, Z, j, k   n, Z   ph, i, x, y, j   ph, k, n   x, j, y

Allowed substitution hints:   C( x, y, j)   F( x, y, i)   G( j)   Z( x, y)

Proof of Theorem cvg1nlemres

Dummy variables e a b c w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvg1n.f	. . . 4 |- ( ph -> F : NN --> RR )
2		cvg1n.c	. . . 4 |- ( ph -> C e. RR+ )
3		cvg1n.cau	. . . 4 |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )
4		cvg1nlem.g	. . . 4 |- G = ( j e. NN |-> ( F ` ( j x. Z ) ) )
5		cvg1nlem.z	. . . 4 |- ( ph -> Z e. NN )
6		cvg1nlem.start	. . . 4 |- ( ph -> C < Z )
7	1, 2, 3, 4, 5, 6	cvg1nlemf 9869	. . 3 |- ( ph -> G : NN --> RR )
8	1, 2, 3, 4, 5, 6	cvg1nlemcau 9870	. . 3 |- ( ph -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( G ` n ) < ( ( G ` k ) + ( 1 / n ) ) /\ ( G ` k ) < ( ( G ` n ) + ( 1 / n ) ) ) )
9	7, 8	caucvgre 9867	. 2 |- ( ph -> E. y e. RR A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) )
10		fveq2 5198	. . . . . . . . . . 11 |- ( a = w -> ( ZZ>= ` a ) = ( ZZ>= ` w ) )
11	10	raleqdv 2555	. . . . . . . . . 10 |- ( a = w -> ( A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) <-> A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) )
12	11	cbvrexv 2578	. . . . . . . . 9 |- ( E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) <-> E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) )
13	12	ralbii 2372	. . . . . . . 8 |- ( A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) <-> A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) )
14	13	anbi2i 444	. . . . . . 7 |- ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) <-> ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) )
15	14	anbi1i 445	. . . . . 6 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) <-> ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) )
16		simpr 108	. . . . . . . . . 10 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> x e. RR+ )
17	16	rphalfcld 8786	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> ( x / 2 ) e. RR+ )
18		simplr 496	. . . . . . . . 9 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) )
19		oveq2 5540	. . . . . . . . . . . . 13 |- ( c = ( x / 2 ) -> ( y + c ) = ( y + ( x / 2 ) ) )
20	19	breq2d 3797	. . . . . . . . . . . 12 |- ( c = ( x / 2 ) -> ( ( G ` b ) < ( y + c ) <-> ( G ` b ) < ( y + ( x / 2 ) ) ) )
21		oveq2 5540	. . . . . . . . . . . . 13 |- ( c = ( x / 2 ) -> ( ( G ` b ) + c ) = ( ( G ` b ) + ( x / 2 ) ) )
22	21	breq2d 3797	. . . . . . . . . . . 12 |- ( c = ( x / 2 ) -> ( y < ( ( G ` b ) + c ) <-> y < ( ( G ` b ) + ( x / 2 ) ) ) )
23	20, 22	anbi12d 456	. . . . . . . . . . 11 |- ( c = ( x / 2 ) -> ( ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) <-> ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) )
24	23	rexralbidv 2392	. . . . . . . . . 10 |- ( c = ( x / 2 ) -> ( E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) <-> E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) )
25	24	rspcv 2697	. . . . . . . . 9 |- ( ( x / 2 ) e. RR+ -> ( A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) -> E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) )
26	17, 18, 25	sylc 61	. . . . . . . 8 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) )
27	15, 26	sylbir 133	. . . . . . 7 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) )
28	2	rpred 8773	. . . . . . . . . . . . . 14 |- ( ph -> C e. RR )
29	28	ad4antr 477	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> C e. RR )
30		2re 8109	. . . . . . . . . . . . . 14 |- 2 e. RR
31	30	a1i 9	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> 2 e. RR )
32	29, 31	remulcld 7149	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> ( C x. 2 ) e. RR )
33		simplr 496	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> x e. RR+ )
34	32, 33	rerpdivcld 8805	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> ( ( C x. 2 ) / x ) e. RR )
35	5	ad4antr 477	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> Z e. NN )
36	34, 35	nndivred 8088	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> ( ( ( C x. 2 ) / x ) / Z ) e. RR )
37		simprl 497	. . . . . . . . . . 11 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> a e. NN )
38	37	nnred 8052	. . . . . . . . . 10 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> a e. RR )
39	36, 38	readdcld 7148	. . . . . . . . 9 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> ( ( ( ( C x. 2 ) / x ) / Z ) + a ) e. RR )
40		arch 8285	. . . . . . . . 9 |- ( ( ( ( ( C x. 2 ) / x ) / Z ) + a ) e. RR -> E. e e. NN ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e )
41	39, 40	syl 14	. . . . . . . 8 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> E. e e. NN ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e )
42		simprl 497	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) -> e e. NN )
43	35	adantr 270	. . . . . . . . . 10 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) -> Z e. NN )
44	42, 43	nnmulcld 8087	. . . . . . . . 9 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) -> ( e x. Z ) e. NN )
45	1	ad6antr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> F : NN --> RR )
46		simplrl 501	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> e e. NN )
47	5	ad6antr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> Z e. NN )
48	46, 47	nnmulcld 8087	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( e x. Z ) e. NN )
49		eluznn 8687	. . . . . . . . . . . . . . . 16 |- ( ( ( e x. Z ) e. NN /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> i e. NN )
50	48, 49	sylancom 411	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> i e. NN )
51	45, 50	ffvelrnd 5324	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) e. RR )
52	45, 48	ffvelrnd 5324	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` ( e x. Z ) ) e. RR )
53	33	ad2antrr 471	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> x e. RR+ )
54	53	rpred 8773	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> x e. RR )
55	54	rehalfcld 8277	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( x / 2 ) e. RR )
56	52, 55	readdcld 7148	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) e. RR )
57		simpllr 500	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> y e. RR )
58	57	ad3antrrr 475	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y e. RR )
59	58, 55	readdcld 7148	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( y + ( x / 2 ) ) e. RR )
60	59, 55	readdcld 7148	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( y + ( x / 2 ) ) + ( x / 2 ) ) e. RR )
61	28	ad6antr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> C e. RR )
62	61, 48	nndivred 8088	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( C / ( e x. Z ) ) e. RR )
63	52, 62	readdcld 7148	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) e. RR )
64		simpr 108	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> i e. ( ZZ>= ` ( e x. Z ) ) )
65	3	ad6antr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) )
66		fveq2 5198	. . . . . . . . . . . . . . . . . . . 20 |- ( n = ( e x. Z ) -> ( ZZ>= ` n ) = ( ZZ>= ` ( e x. Z ) ) )
67		fveq2 5198	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( e x. Z ) -> ( F ` n ) = ( F ` ( e x. Z ) ) )
68		oveq2 5540	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n = ( e x. Z ) -> ( C / n ) = ( C / ( e x. Z ) ) )
69	68	oveq2d 5548	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( e x. Z ) -> ( ( F ` k ) + ( C / n ) ) = ( ( F ` k ) + ( C / ( e x. Z ) ) ) )
70	67, 69	breq12d 3798	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = ( e x. Z ) -> ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) <-> ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) ) )
71	67, 68	oveq12d 5550	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n = ( e x. Z ) -> ( ( F ` n ) + ( C / n ) ) = ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) )
72	71	breq2d 3797	. . . . . . . . . . . . . . . . . . . . 21 |- ( n = ( e x. Z ) -> ( ( F ` k ) < ( ( F ` n ) + ( C / n ) ) <-> ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) )
73	70, 72	anbi12d 456	. . . . . . . . . . . . . . . . . . . 20 |- ( n = ( e x. Z ) -> ( ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) <-> ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) ) )
74	66, 73	raleqbidv 2561	. . . . . . . . . . . . . . . . . . 19 |- ( n = ( e x. Z ) -> ( A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) <-> A. k e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) ) )
75	74	rspcv 2697	. . . . . . . . . . . . . . . . . 18 |- ( ( e x. Z ) e. NN -> ( A. n e. NN A. k e. ( ZZ>= ` n ) ( ( F ` n ) < ( ( F ` k ) + ( C / n ) ) /\ ( F ` k ) < ( ( F ` n ) + ( C / n ) ) ) -> A. k e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) ) )
76	48, 65, 75	sylc 61	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> A. k e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) )
77		fveq2 5198	. . . . . . . . . . . . . . . . . . . . 21 |- ( k = i -> ( F ` k ) = ( F ` i ) )
78	77	oveq1d 5547	. . . . . . . . . . . . . . . . . . . 20 |- ( k = i -> ( ( F ` k ) + ( C / ( e x. Z ) ) ) = ( ( F ` i ) + ( C / ( e x. Z ) ) ) )
79	78	breq2d 3797	. . . . . . . . . . . . . . . . . . 19 |- ( k = i -> ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) <-> ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( C / ( e x. Z ) ) ) ) )
80	77	breq1d 3795	. . . . . . . . . . . . . . . . . . 19 |- ( k = i -> ( ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) <-> ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) )
81	79, 80	anbi12d 456	. . . . . . . . . . . . . . . . . 18 |- ( k = i -> ( ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) <-> ( ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( C / ( e x. Z ) ) ) /\ ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) ) )
82	81	rspcv 2697	. . . . . . . . . . . . . . . . 17 |- ( i e. ( ZZ>= ` ( e x. Z ) ) -> ( A. k e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` ( e x. Z ) ) < ( ( F ` k ) + ( C / ( e x. Z ) ) ) /\ ( F ` k ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) -> ( ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( C / ( e x. Z ) ) ) /\ ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) ) )
83	64, 76, 82	sylc 61	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( C / ( e x. Z ) ) ) /\ ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) ) )
84	83	simprd 112	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) )
85		simpr 108	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> x e. RR+ )
86	85	ad3antrrr 475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> x e. RR+ )
87	86	rpred 8773	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> x e. RR )
88	87	rehalfcld 8277	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( x / 2 ) e. RR )
89	2	ad6antr 481	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> C e. RR+ )
90	37	ad2antrr 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a e. NN )
91		simplrr 502	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e )
92	89, 86, 47, 46, 90, 91	cvg1nlemcxze 9868	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( C / ( e x. Z ) ) < ( x / 2 ) )
93	62, 88, 92	ltled 7228	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( C / ( e x. Z ) ) <_ ( x / 2 ) )
94	62, 55, 52, 93	leadd2dd 7660	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) + ( C / ( e x. Z ) ) ) <_ ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) )
95	51, 63, 56, 84, 94	ltletrd 7527	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) < ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) )
96	90	nnred 8052	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a e. RR )
97	46	nnred 8052	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> e e. RR )
98		2rp 8739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 2 e. RR+
99	98	a1i 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> 2 e. RR+ )
100	89, 99	rpmulcld 8790	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( C x. 2 ) e. RR+ )
101	100, 86	rpdivcld 8791	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( C x. 2 ) / x ) e. RR+ )
102	47	nnrpd 8772	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> Z e. RR+ )
103	101, 102	rpdivcld 8791	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( C x. 2 ) / x ) / Z ) e. RR+ )
104	103	rpred 8773	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( C x. 2 ) / x ) / Z ) e. RR )
105	104, 96	readdcld 7148	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( ( C x. 2 ) / x ) / Z ) + a ) e. RR )
106	96, 103	ltaddrp2d 8808	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a < ( ( ( ( C x. 2 ) / x ) / Z ) + a ) )
107	96, 105, 97, 106, 91	lttrd 7235	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a < e )
108	96, 97, 107	ltled 7228	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a <_ e )
109	90	nnzd 8468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> a e. ZZ )
110	46	nnzd 8468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> e e. ZZ )
111		eluz 8632	. . . . . . . . . . . . . . . . . . . 20 |- ( ( a e. ZZ /\ e e. ZZ ) -> ( e e. ( ZZ>= ` a ) <-> a <_ e ) )
112	109, 110, 111	syl2anc 403	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( e e. ( ZZ>= ` a ) <-> a <_ e ) )
113	108, 112	mpbird 165	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> e e. ( ZZ>= ` a ) )
114		simprr 498	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) )
115	114	ad2antrr 471	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) )
116		fveq2 5198	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = e -> ( G ` b ) = ( G ` e ) )
117	116	breq1d 3795	. . . . . . . . . . . . . . . . . . . 20 |- ( b = e -> ( ( G ` b ) < ( y + ( x / 2 ) ) <-> ( G ` e ) < ( y + ( x / 2 ) ) ) )
118	116	oveq1d 5547	. . . . . . . . . . . . . . . . . . . . 21 |- ( b = e -> ( ( G ` b ) + ( x / 2 ) ) = ( ( G ` e ) + ( x / 2 ) ) )
119	118	breq2d 3797	. . . . . . . . . . . . . . . . . . . 20 |- ( b = e -> ( y < ( ( G ` b ) + ( x / 2 ) ) <-> y < ( ( G ` e ) + ( x / 2 ) ) ) )
120	117, 119	anbi12d 456	. . . . . . . . . . . . . . . . . . 19 |- ( b = e -> ( ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) <-> ( ( G ` e ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` e ) + ( x / 2 ) ) ) ) )
121	120	rspcv 2697	. . . . . . . . . . . . . . . . . 18 |- ( e e. ( ZZ>= ` a ) -> ( A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) -> ( ( G ` e ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` e ) + ( x / 2 ) ) ) ) )
122	113, 115, 121	sylc 61	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( G ` e ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` e ) + ( x / 2 ) ) ) )
123		oveq1 5539	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = e -> ( j x. Z ) = ( e x. Z ) )
124	123	fveq2d 5202	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = e -> ( F ` ( j x. Z ) ) = ( F ` ( e x. Z ) ) )
125	124, 4	fvmptg 5269	. . . . . . . . . . . . . . . . . . . 20 |- ( ( e e. NN /\ ( F ` ( e x. Z ) ) e. RR ) -> ( G ` e ) = ( F ` ( e x. Z ) ) )
126	46, 52, 125	syl2anc 403	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( G ` e ) = ( F ` ( e x. Z ) ) )
127	126	breq1d 3795	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( G ` e ) < ( y + ( x / 2 ) ) <-> ( F ` ( e x. Z ) ) < ( y + ( x / 2 ) ) ) )
128	126	oveq1d 5547	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( G ` e ) + ( x / 2 ) ) = ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) )
129	128	breq2d 3797	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( y < ( ( G ` e ) + ( x / 2 ) ) <-> y < ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) ) )
130	127, 129	anbi12d 456	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( G ` e ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` e ) + ( x / 2 ) ) ) <-> ( ( F ` ( e x. Z ) ) < ( y + ( x / 2 ) ) /\ y < ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) ) ) )
131	122, 130	mpbid 145	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) < ( y + ( x / 2 ) ) /\ y < ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) ) )
132	131	simpld 110	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` ( e x. Z ) ) < ( y + ( x / 2 ) ) )
133	52, 59, 55, 132	ltadd1dd 7656	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) < ( ( y + ( x / 2 ) ) + ( x / 2 ) ) )
134	51, 56, 60, 95, 133	lttrd 7235	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) < ( ( y + ( x / 2 ) ) + ( x / 2 ) ) )
135	58	recnd 7147	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y e. CC )
136	55	recnd 7147	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( x / 2 ) e. CC )
137	135, 136, 136	addassd 7141	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( y + ( x / 2 ) ) + ( x / 2 ) ) = ( y + ( ( x / 2 ) + ( x / 2 ) ) ) )
138	134, 137	breqtrd 3809	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) < ( y + ( ( x / 2 ) + ( x / 2 ) ) ) )
139	53	rpcnd 8775	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> x e. CC )
140	139	2halvesd 8276	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( x / 2 ) + ( x / 2 ) ) = x )
141	140	oveq2d 5548	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( y + ( ( x / 2 ) + ( x / 2 ) ) ) = ( y + x ) )
142	138, 141	breqtrd 3809	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) < ( y + x ) )
143	51, 55	readdcld 7148	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` i ) + ( x / 2 ) ) e. RR )
144	143, 55	readdcld 7148	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( F ` i ) + ( x / 2 ) ) + ( x / 2 ) ) e. RR )
145	131	simprd 112	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y < ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) )
146	51, 62	readdcld 7148	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` i ) + ( C / ( e x. Z ) ) ) e. RR )
147	83	simpld 110	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( C / ( e x. Z ) ) ) )
148	62, 55, 51, 93	leadd2dd 7660	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` i ) + ( C / ( e x. Z ) ) ) <_ ( ( F ` i ) + ( x / 2 ) ) )
149	52, 146, 143, 147, 148	ltletrd 7527	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` ( e x. Z ) ) < ( ( F ` i ) + ( x / 2 ) ) )
150	52, 143, 55, 149	ltadd1dd 7656	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` ( e x. Z ) ) + ( x / 2 ) ) < ( ( ( F ` i ) + ( x / 2 ) ) + ( x / 2 ) ) )
151	58, 56, 144, 145, 150	lttrd 7235	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y < ( ( ( F ` i ) + ( x / 2 ) ) + ( x / 2 ) ) )
152	51	recnd 7147	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( F ` i ) e. CC )
153	152, 136, 136	addassd 7141	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( ( F ` i ) + ( x / 2 ) ) + ( x / 2 ) ) = ( ( F ` i ) + ( ( x / 2 ) + ( x / 2 ) ) ) )
154	151, 153	breqtrd 3809	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y < ( ( F ` i ) + ( ( x / 2 ) + ( x / 2 ) ) ) )
155	140	oveq2d 5548	. . . . . . . . . . . 12 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` i ) + ( ( x / 2 ) + ( x / 2 ) ) ) = ( ( F ` i ) + x ) )
156	154, 155	breqtrd 3809	. . . . . . . . . . 11 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> y < ( ( F ` i ) + x ) )
157	142, 156	jca 300	. . . . . . . . . 10 |- ( ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) /\ i e. ( ZZ>= ` ( e x. Z ) ) ) -> ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
158	157	ralrimiva 2434	. . . . . . . . 9 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) -> A. i e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
159		fveq2 5198	. . . . . . . . . . 11 |- ( j = ( e x. Z ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( e x. Z ) ) )
160	159	raleqdv 2555	. . . . . . . . . 10 |- ( j = ( e x. Z ) -> ( A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) <-> A. i e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) ) )
161	160	rspcev 2701	. . . . . . . . 9 |- ( ( ( e x. Z ) e. NN /\ A. i e. ( ZZ>= ` ( e x. Z ) ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) ) -> E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
162	44, 158, 161	syl2anc 403	. . . . . . . 8 |- ( ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) /\ ( e e. NN /\ ( ( ( ( C x. 2 ) / x ) / Z ) + a ) < e ) ) -> E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
163	41, 162	rexlimddv 2481	. . . . . . 7 |- ( ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) /\ ( a e. NN /\ A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + ( x / 2 ) ) /\ y < ( ( G ` b ) + ( x / 2 ) ) ) ) ) -> E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
164	27, 163	rexlimddv 2481	. . . . . 6 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. w e. NN A. b e. ( ZZ>= ` w ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
165	15, 164	sylbi 119	. . . . 5 |- ( ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) /\ x e. RR+ ) -> E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
166	165	ralrimiva 2434	. . . 4 |- ( ( ( ph /\ y e. RR ) /\ A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) ) -> A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )
167	166	ex 113	. . 3 |- ( ( ph /\ y e. RR ) -> ( A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) -> A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) ) )
168	167	reximdva 2463	. 2 |- ( ph -> ( E. y e. RR A. c e. RR+ E. a e. NN A. b e. ( ZZ>= ` a ) ( ( G ` b ) < ( y + c ) /\ y < ( ( G ` b ) + c ) ) -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) ) )
169	9, 168	mpd 13	1 |- ( ph -> E. y e. RR A. x e. RR+ E. j e. NN A. i e. ( ZZ>= ` j ) ( ( F ` i ) < ( y + x ) /\ y < ( ( F ` i ) + x ) ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   e. wcel 1433   A.wral 2348   E.wrex 2349   class class class wbr 3785   |-> cmpt 3839   -->wf 4918   ` cfv 4922  (class class class)co 5532   RRcr 6980   + caddc 6984   x. cmul 6986   < clt 7153   <_ cle 7154   / cdiv 7760   NNcn 8039   2c2 8089   ZZcz 8351   ZZ>=cuz 8619   RR+crp 8734

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-1re 7070  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-mulrcl 7075  ax-addcom 7076  ax-mulcom 7077  ax-addass 7078  ax-mulass 7079  ax-distr 7080  ax-i2m1 7081  ax-0lt1 7082  ax-1rid 7083  ax-0id 7084  ax-rnegex 7085  ax-precex 7086  ax-cnre 7087  ax-pre-ltirr 7088  ax-pre-ltwlin 7089  ax-pre-lttrn 7090  ax-pre-apti 7091  ax-pre-ltadd 7092  ax-pre-mulgt0 7093  ax-pre-mulext 7094  ax-arch 7095  ax-caucvg 7096

This theorem depends on definitions:  df-bi 115  df-3or 920  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-nel 2340  df-ral 2353  df-rex 2354  df-reu 2355  df-rmo 2356  df-rab 2357  df-v 2603  df-sbc 2816  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-int 3637  df-br 3786  df-opab 3840  df-mpt 3841  df-id 4048  df-po 4051  df-iso 4052  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-pnf 7155  df-mnf 7156  df-xr 7157  df-ltxr 7158  df-le 7159  df-sub 7281  df-neg 7282  df-reap 7675  df-ap 7682  df-div 7761  df-inn 8040  df-2 8098  df-n0 8289  df-z 8352  df-uz 8620  df-rp 8735

This theorem is referenced by:  cvg1n  9872