Theorem pntpbnd1 21233

Description: Lemma for pntpbnd 21235. (Contributed by Mario Carneiro, 11-Apr-2016.)

Hypotheses

Ref	Expression
pntpbnd.r	|- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
pntpbnd1.e	|- ( ph -> E e. ( 0 (,) 1 ) )
pntpbnd1.x	|- X = ( exp ` ( 2 / E ) )
pntpbnd1.y	|- ( ph -> Y e. ( X (,) +oo ) )
pntpbnd1.1	|- ( ph -> A e. RR+ )
pntpbnd1.2	|- ( ph -> A. i e. NN A. j e. ZZ ( abs ` sum_ y e. ( i ... j ) ( ( R ` y ) / ( y x. ( y + 1 ) ) ) ) <_ A )
pntpbnd1.c	|- C = ( A + 2 )
pntpbnd1.k	|- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
pntpbnd1.3	|- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )

Assertion

Ref	Expression
pntpbnd1	|- ( ph -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) <_ A )

Distinct variable groups:   i, j, n, y, K   ph, n   R, i, j, n, y   i, a, j, n, y, A   n, E, y   i, Y, j, n, y

Allowed substitution hints:   ph( y, i, j, a)   C( y, i, j, n, a)   R( a)   E( i, j, a)   K( a)   X( y, i, j, n, a)   Y( a)

Proof of Theorem pntpbnd1

Dummy variables m x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfid 11267	. . . . . 6 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) e. Fin )
2		ioossre 10928	. . . . . . . . . . . . . 14 |- ( X (,) +oo ) C_ RR
3		pntpbnd1.y	. . . . . . . . . . . . . 14 |- ( ph -> Y e. ( X (,) +oo ) )
4	2, 3	sseldi 3306	. . . . . . . . . . . . 13 |- ( ph -> Y e. RR )
5		0re 9047	. . . . . . . . . . . . . . 15 |- 0 e. RR
6	5	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 0 e. RR )
7		pntpbnd1.x	. . . . . . . . . . . . . . . 16 |- X = ( exp ` ( 2 / E ) )
8		2re 10025	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR
9		ioossre 10928	. . . . . . . . . . . . . . . . . . . 20 |- ( 0 (,) 1 ) C_ RR
10		pntpbnd1.e	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> E e. ( 0 (,) 1 ) )
11	9, 10	sseldi 3306	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> E e. RR )
12		eliooord 10926	. . . . . . . . . . . . . . . . . . . . 21 |- ( E e. ( 0 (,) 1 ) -> ( 0 < E /\ E < 1 ) )
13	10, 12	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 < E /\ E < 1 ) )
14	13	simpld 446	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < E )
15	11, 14	elrpd 10602	. . . . . . . . . . . . . . . . . 18 |- ( ph -> E e. RR+ )
16		rerpdivcl 10595	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ E e. RR+ ) -> ( 2 / E ) e. RR )
17	8, 15, 16	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 / E ) e. RR )
18	17	reefcld 12645	. . . . . . . . . . . . . . . 16 |- ( ph -> ( exp ` ( 2 / E ) ) e. RR )
19	7, 18	syl5eqel 2488	. . . . . . . . . . . . . . 15 |- ( ph -> X e. RR )
20		efgt0 12659	. . . . . . . . . . . . . . . . 17 |- ( ( 2 / E ) e. RR -> 0 < ( exp ` ( 2 / E ) ) )
21	17, 20	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 < ( exp ` ( 2 / E ) ) )
22	21, 7	syl6breqr 4212	. . . . . . . . . . . . . . 15 |- ( ph -> 0 < X )
23		eliooord 10926	. . . . . . . . . . . . . . . . 17 |- ( Y e. ( X (,) +oo ) -> ( X < Y /\ Y < +oo ) )
24	3, 23	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X < Y /\ Y < +oo ) )
25	24	simpld 446	. . . . . . . . . . . . . . 15 |- ( ph -> X < Y )
26	6, 19, 4, 22, 25	lttrd 9187	. . . . . . . . . . . . . 14 |- ( ph -> 0 < Y )
27	6, 4, 26	ltled 9177	. . . . . . . . . . . . 13 |- ( ph -> 0 <_ Y )
28		flge0nn0 11180	. . . . . . . . . . . . 13 |- ( ( Y e. RR /\ 0 <_ Y ) -> ( |_ ` Y ) e. NN0 )
29	4, 27, 28	syl2anc 643	. . . . . . . . . . . 12 |- ( ph -> ( |_ ` Y ) e. NN0 )
30		nn0p1nn 10215	. . . . . . . . . . . 12 |- ( ( |_ ` Y ) e. NN0 -> ( ( |_ ` Y ) + 1 ) e. NN )
31	29, 30	syl 16	. . . . . . . . . . 11 |- ( ph -> ( ( |_ ` Y ) + 1 ) e. NN )
32		elfzuz 11011	. . . . . . . . . . 11 |- ( n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
33		nnuz 10477	. . . . . . . . . . . 12 |- NN = ( ZZ>= ` 1 )
34	33	uztrn2 10459	. . . . . . . . . . 11 |- ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) ) -> n e. NN )
35	31, 32, 34	syl2an 464	. . . . . . . . . 10 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. NN )
36	35	nnrpd 10603	. . . . . . . . 9 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> n e. RR+ )
37		pntpbnd.r	. . . . . . . . . . 11 |- R = ( a e. RR+ |-> ( (ψ ` a ) - a ) )
38	37	pntrf 21210	. . . . . . . . . 10 |- R : RR+ --> RR
39	38	ffvelrni 5828	. . . . . . . . 9 |- ( n e. RR+ -> ( R ` n ) e. RR )
40	36, 39	syl 16	. . . . . . . 8 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
41	35	peano2nnd 9973	. . . . . . . . 9 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n + 1 ) e. NN )
42	35, 41	nnmulcld 10003	. . . . . . . 8 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
43	40, 42	nndivred 10004	. . . . . . 7 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
44	43	adantlr 696	. . . . . 6 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
45	1, 44	fsumrecl 12483	. . . . 5 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
46	40	adantlr 696	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
47		fveq2 5687	. . . . . . . . . 10 |- ( i = n -> ( R ` i ) = ( R ` n ) )
48	47	breq2d 4184	. . . . . . . . 9 |- ( i = n -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` n ) ) )
49	48	rspccva 3011	. . . . . . . 8 |- ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( R ` n ) )
50	49	adantll 695	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( R ` n ) )
51	42	adantlr 696	. . . . . . . 8 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
52	51	nnred 9971	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. RR )
53	51	nngt0d 9999	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 < ( n x. ( n + 1 ) ) )
54		divge0 9835	. . . . . . 7 |- ( ( ( ( R ` n ) e. RR /\ 0 <_ ( R ` n ) ) /\ ( ( n x. ( n + 1 ) ) e. RR /\ 0 < ( n x. ( n + 1 ) ) ) ) -> 0 <_ ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
55	46, 50, 52, 53, 54	syl22anc 1185	. . . . . 6 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
56	1, 44, 55	fsumge0 12529	. . . . 5 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> 0 <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
57	45, 56	absidd 12180	. . . 4 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
58	44, 55	absidd 12180	. . . . 5 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
59	58	sumeq2dv 12452	. . . 4 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
60	57, 59	eqtr4d 2439	. . 3 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
61		fzfid 11267	. . . . 5 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) e. Fin )
62	43	adantlr 696	. . . . . 6 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
63	62	recnd 9070	. . . . 5 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. CC )
64	61, 63	fsumneg 12525	. . . 4 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
65	40	adantlr 696	. . . . . . . . . 10 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. RR )
66	65	renegcld 9420	. . . . . . . . 9 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( R ` n ) e. RR )
67	47	breq1d 4182	. . . . . . . . . . . 12 |- ( i = n -> ( ( R ` i ) <_ 0 <-> ( R ` n ) <_ 0 ) )
68	67	rspccva 3011	. . . . . . . . . . 11 |- ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) <_ 0 )
69	68	adantll 695	. . . . . . . . . 10 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) <_ 0 )
70	65	le0neg1d 9554	. . . . . . . . . 10 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) <_ 0 <-> 0 <_ -u ( R ` n ) ) )
71	69, 70	mpbid 202	. . . . . . . . 9 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ -u ( R ` n ) )
72	42	adantlr 696	. . . . . . . . . 10 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. NN )
73	72	nnred 9971	. . . . . . . . 9 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. RR )
74	72	nngt0d 9999	. . . . . . . . 9 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 < ( n x. ( n + 1 ) ) )
75		divge0 9835	. . . . . . . . 9 |- ( ( ( -u ( R ` n ) e. RR /\ 0 <_ -u ( R ` n ) ) /\ ( ( n x. ( n + 1 ) ) e. RR /\ 0 < ( n x. ( n + 1 ) ) ) ) -> 0 <_ ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
76	66, 71, 73, 74, 75	syl22anc 1185	. . . . . . . 8 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
77	40	recnd 9070	. . . . . . . . . 10 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` n ) e. CC )
78	42	nncnd 9972	. . . . . . . . . 10 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) e. CC )
79	42	nnne0d 10000	. . . . . . . . . 10 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( n x. ( n + 1 ) ) =/= 0 )
80	77, 78, 79	divnegd 9759	. . . . . . . . 9 |- ( ( ph /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
81	80	adantlr 696	. . . . . . . 8 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) = ( -u ( R ` n ) / ( n x. ( n + 1 ) ) ) )
82	76, 81	breqtrrd 4198	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> 0 <_ -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
83	62	le0neg1d 9554	. . . . . . 7 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 <-> 0 <_ -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
84	82, 83	mpbird 224	. . . . . 6 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 )
85	62, 84	absnidd 12171	. . . . 5 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
86	85	sumeq2dv 12452	. . . 4 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
87	61, 62	fsumrecl 12483	. . . . 5 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
88	62	renegcld 9420	. . . . . . . 8 |- ( ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) /\ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) e. RR )
89	61, 88, 82	fsumge0 12529	. . . . . . 7 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> 0 <_ sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -u ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
90	89, 64	breqtrd 4196	. . . . . 6 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> 0 <_ -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
91	87	le0neg1d 9554	. . . . . 6 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 <-> 0 <_ -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
92	90, 91	mpbird 224	. . . . 5 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) <_ 0 )
93	87, 92	absnidd 12171	. . . 4 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = -u sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) )
94	64, 86, 93	3eqtr4rd 2447	. . 3 |- ( ( ph /\ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) -> ( abs ` sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) = sum_ n e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( abs ` ( ( R ` n ) / ( n x. ( n + 1 ) ) ) ) )
95		pntpbnd1.c	. . . . . . . . . . . . 13 |- C = ( A + 2 )
96		pntpbnd1.1	. . . . . . . . . . . . . 14 |- ( ph -> A e. RR+ )
97		2rp 10573	. . . . . . . . . . . . . 14 |- 2 e. RR+
98		rpaddcl 10588	. . . . . . . . . . . . . 14 |- ( ( A e. RR+ /\ 2 e. RR+ ) -> ( A + 2 ) e. RR+ )
99	96, 97, 98	sylancl 644	. . . . . . . . . . . . 13 |- ( ph -> ( A + 2 ) e. RR+ )
100	95, 99	syl5eqel 2488	. . . . . . . . . . . 12 |- ( ph -> C e. RR+ )
101	100, 15	rpdivcld 10621	. . . . . . . . . . 11 |- ( ph -> ( C / E ) e. RR+ )
102	101	rpred 10604	. . . . . . . . . 10 |- ( ph -> ( C / E ) e. RR )
103	102	reefcld 12645	. . . . . . . . 9 |- ( ph -> ( exp ` ( C / E ) ) e. RR )
104		pnfxr 10669	. . . . . . . . 9 |- +oo e. RR*
105		icossre 10947	. . . . . . . . 9 |- ( ( ( exp ` ( C / E ) ) e. RR /\ +oo e. RR* ) -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
106	103, 104, 105	sylancl 644	. . . . . . . 8 |- ( ph -> ( ( exp ` ( C / E ) ) [,) +oo ) C_ RR )
107		pntpbnd1.k	. . . . . . . 8 |- ( ph -> K e. ( ( exp ` ( C / E ) ) [,) +oo ) )
108	106, 107	sseldd 3309	. . . . . . 7 |- ( ph -> K e. RR )
109	108, 4	remulcld 9072	. . . . . 6 |- ( ph -> ( K x. Y ) e. RR )
110	4	recnd 9070	. . . . . . . . 9 |- ( ph -> Y e. CC )
111	110	mulid2d 9062	. . . . . . . 8 |- ( ph -> ( 1 x. Y ) = Y )
112		1re 9046	. . . . . . . . . . 11 |- 1 e. RR
113	112	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
114		efgt1 12672	. . . . . . . . . . 11 |- ( ( C / E ) e. RR+ -> 1 < ( exp ` ( C / E ) ) )
115	101, 114	syl 16	. . . . . . . . . 10 |- ( ph -> 1 < ( exp ` ( C / E ) ) )
116		elicopnf 10956	. . . . . . . . . . . . 13 |- ( ( exp ` ( C / E ) ) e. RR -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
117	103, 116	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( K e. ( ( exp ` ( C / E ) ) [,) +oo ) <-> ( K e. RR /\ ( exp ` ( C / E ) ) <_ K ) ) )
118	117	simplbda 608	. . . . . . . . . . 11 |- ( ( ph /\ K e. ( ( exp ` ( C / E ) ) [,) +oo ) ) -> ( exp ` ( C / E ) ) <_ K )
119	107, 118	mpdan 650	. . . . . . . . . 10 |- ( ph -> ( exp ` ( C / E ) ) <_ K )
120	113, 103, 108, 115, 119	ltletrd 9186	. . . . . . . . 9 |- ( ph -> 1 < K )
121		ltmul1 9816	. . . . . . . . . 10 |- ( ( 1 e. RR /\ K e. RR /\ ( Y e. RR /\ 0 < Y ) ) -> ( 1 < K <-> ( 1 x. Y ) < ( K x. Y ) ) )
122	113, 108, 4, 26, 121	syl112anc 1188	. . . . . . . . 9 |- ( ph -> ( 1 < K <-> ( 1 x. Y ) < ( K x. Y ) ) )
123	120, 122	mpbid 202	. . . . . . . 8 |- ( ph -> ( 1 x. Y ) < ( K x. Y ) )
124	111, 123	eqbrtrrd 4194	. . . . . . 7 |- ( ph -> Y < ( K x. Y ) )
125	4, 109, 124	ltled 9177	. . . . . 6 |- ( ph -> Y <_ ( K x. Y ) )
126		flword2 11175	. . . . . 6 |- ( ( Y e. RR /\ ( K x. Y ) e. RR /\ Y <_ ( K x. Y ) ) -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) )
127	4, 109, 125, 126	syl3anc 1184	. . . . 5 |- ( ph -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) )
128	109	flcld 11162	. . . . . 6 |- ( ph -> ( |_ ` ( K x. Y ) ) e. ZZ )
129		uzid 10456	. . . . . 6 |- ( ( |_ ` ( K x. Y ) ) e. ZZ -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) )
130	128, 129	syl 16	. . . . 5 |- ( ph -> ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) )
131		elfzuzb 11009	. . . . 5 |- ( ( |_ ` ( K x. Y ) ) e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) /\ ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` ( K x. Y ) ) ) ) )
132	127, 130, 131	sylanbrc 646	. . . 4 |- ( ph -> ( |_ ` ( K x. Y ) ) e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) )
133		oveq2 6048	. . . . . . . 8 |- ( x = ( |_ ` Y ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) )
134	133	raleqdv 2870	. . . . . . 7 |- ( x = ( |_ ` Y ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) ) )
135	133	raleqdv 2870	. . . . . . 7 |- ( x = ( |_ ` Y ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) )
136	134, 135	orbi12d 691	. . . . . 6 |- ( x = ( |_ ` Y ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) )
137	136	imbi2d 308	. . . . 5 |- ( x = ( |_ ` Y ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) ) )
138		oveq2 6048	. . . . . . . 8 |- ( x = m -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... m ) )
139	138	raleqdv 2870	. . . . . . 7 |- ( x = m -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) ) )
140	138	raleqdv 2870	. . . . . . 7 |- ( x = m -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) )
141	139, 140	orbi12d 691	. . . . . 6 |- ( x = m -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) ) )
142	141	imbi2d 308	. . . . 5 |- ( x = m -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) ) ) )
143		oveq2 6048	. . . . . . . 8 |- ( x = ( m + 1 ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) )
144	143	raleqdv 2870	. . . . . . 7 |- ( x = ( m + 1 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) ) )
145	143	raleqdv 2870	. . . . . . 7 |- ( x = ( m + 1 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) )
146	144, 145	orbi12d 691	. . . . . 6 |- ( x = ( m + 1 ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
147	146	imbi2d 308	. . . . 5 |- ( x = ( m + 1 ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) ) )
148		oveq2 6048	. . . . . . . 8 |- ( x = ( |_ ` ( K x. Y ) ) -> ( ( ( |_ ` Y ) + 1 ) ... x ) = ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) )
149	148	raleqdv 2870	. . . . . . 7 |- ( x = ( |_ ` ( K x. Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) ) )
150	148	raleqdv 2870	. . . . . . 7 |- ( x = ( |_ ` ( K x. Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) )
151	149, 150	orbi12d 691	. . . . . 6 |- ( x = ( |_ ` ( K x. Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) ) )
152	151	imbi2d 308	. . . . 5 |- ( x = ( |_ ` ( K x. Y ) ) -> ( ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... x ) ( R ` i ) <_ 0 ) ) <-> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ( R ` i ) <_ 0 ) ) ) )
153		elfzle3 11019	. . . . . . . . 9 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) )
154		elfzel2 11013	. . . . . . . . . . . 12 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) e. ZZ )
155	154	zred 10331	. . . . . . . . . . 11 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) e. RR )
156	155	ltp1d 9897	. . . . . . . . . 10 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) )
157		peano2re 9195	. . . . . . . . . . . 12 |- ( ( |_ ` Y ) e. RR -> ( ( |_ ` Y ) + 1 ) e. RR )
158	155, 157	syl 16	. . . . . . . . . . 11 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) + 1 ) e. RR )
159	155, 158	ltnled 9176	. . . . . . . . . 10 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( ( |_ ` Y ) < ( ( |_ ` Y ) + 1 ) <-> -. ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) ) )
160	156, 159	mpbid 202	. . . . . . . . 9 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> -. ( ( |_ ` Y ) + 1 ) <_ ( |_ ` Y ) )
161	153, 160	pm2.21dd 101	. . . . . . . 8 |- ( i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) -> ( R ` i ) <_ 0 )
162	161	rgen 2731	. . . . . . 7 |- A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0
163	162	olci 381	. . . . . 6 |- ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 )
164	163	a1ii 25	. . . . 5 |- ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) -> ( ph -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` Y ) ) ( R ` i ) <_ 0 ) ) )
165		elfzofz 11109	. . . . . . . . . 10 |- ( m e. ( ( |_ ` Y )..^ ( |_ ` ( K x. Y ) ) ) -> m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) )
166		elfzp12 11081	. . . . . . . . . . 11 |- ( ( |_ ` ( K x. Y ) ) e. ( ZZ>= ` ( |_ ` Y ) ) -> ( m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
167	127, 166	syl 16	. . . . . . . . . 10 |- ( ph -> ( m e. ( ( |_ ` Y ) ... ( |_ ` ( K x. Y ) ) ) <-> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
168	165, 167	syl5ib 211	. . . . . . . . 9 |- ( ph -> ( m e. ( ( |_ ` Y )..^ ( |_ ` ( K x. Y ) ) ) -> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) ) )
169	168	imp 419	. . . . . . . 8 |- ( ( ph /\ m e. ( ( |_ ` Y )..^ ( |_ ` ( K x. Y ) ) ) ) -> ( m = ( |_ ` Y ) \/ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) )
170	31	nnrpd 10603	. . . . . . . . . . . . . 14 |- ( ph -> ( ( |_ ` Y ) + 1 ) e. RR+ )
171	38	ffvelrni 5828	. . . . . . . . . . . . . 14 |- ( ( ( |_ ` Y ) + 1 ) e. RR+ -> ( R ` ( ( |_ ` Y ) + 1 ) ) e. RR )
172	170, 171	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( R ` ( ( |_ ` Y ) + 1 ) ) e. RR )
173	6, 172	letrid 9179	. . . . . . . . . . . 12 |- ( ph -> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
174	173	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
175		oveq1 6047	. . . . . . . . . . . . . . . 16 |- ( m = ( |_ ` Y ) -> ( m + 1 ) = ( ( |_ ` Y ) + 1 ) )
176	175	oveq2d 6056	. . . . . . . . . . . . . . 15 |- ( m = ( |_ ` Y ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) )
177	4	flcld 11162	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( |_ ` Y ) e. ZZ )
178	177	peano2zd 10334	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( |_ ` Y ) + 1 ) e. ZZ )
179		fzsn 11050	. . . . . . . . . . . . . . . 16 |- ( ( ( |_ ` Y ) + 1 ) e. ZZ -> ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
180	178, 179	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( |_ ` Y ) + 1 ) ... ( ( |_ ` Y ) + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
181	176, 180	sylan9eqr 2458	. . . . . . . . . . . . . 14 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = { ( ( |_ ` Y ) + 1 ) } )
182	181	raleqdv 2870	. . . . . . . . . . . . 13 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> A. i e. { ( ( |_ ` Y ) + 1 ) } 0 <_ ( R ` i ) ) )
183		ovex 6065	. . . . . . . . . . . . . 14 |- ( ( |_ ` Y ) + 1 ) e. _V
184		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( i = ( ( |_ ` Y ) + 1 ) -> ( R ` i ) = ( R ` ( ( |_ ` Y ) + 1 ) ) )
185	184	breq2d 4184	. . . . . . . . . . . . . 14 |- ( i = ( ( |_ ` Y ) + 1 ) -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) ) )
186	183, 185	ralsn 3809	. . . . . . . . . . . . 13 |- ( A. i e. { ( ( |_ ` Y ) + 1 ) } 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) )
187	182, 186	syl6bb 253	. . . . . . . . . . . 12 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) ) )
188	181	raleqdv 2870	. . . . . . . . . . . . 13 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> A. i e. { ( ( |_ ` Y ) + 1 ) } ( R ` i ) <_ 0 ) )
189	184	breq1d 4182	. . . . . . . . . . . . . 14 |- ( i = ( ( |_ ` Y ) + 1 ) -> ( ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
190	183, 189	ralsn 3809	. . . . . . . . . . . . 13 |- ( A. i e. { ( ( |_ ` Y ) + 1 ) } ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 )
191	188, 190	syl6bb 253	. . . . . . . . . . . 12 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) )
192	187, 191	orbi12d 691	. . . . . . . . . . 11 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) <-> ( 0 <_ ( R ` ( ( |_ ` Y ) + 1 ) ) \/ ( R ` ( ( |_ ` Y ) + 1 ) ) <_ 0 ) ) )
193	174, 192	mpbird 224	. . . . . . . . . 10 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) )
194	193	a1d 23	. . . . . . . . 9 |- ( ( ph /\ m = ( |_ ` Y ) ) -> ( ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) \/ A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 ) ) )
195		elfzuz 11011	. . . . . . . . . . . . . . . . 17 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
196	195	adantl 453	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) )
197		eluzfz2 11021	. . . . . . . . . . . . . . . 16 |- ( m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) -> m e. ( ( ( |_ ` Y ) + 1 ) ... m ) )
198	196, 197	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. ( ( ( |_ ` Y ) + 1 ) ... m ) )
199		fveq2 5687	. . . . . . . . . . . . . . . . 17 |- ( i = m -> ( R ` i ) = ( R ` m ) )
200	199	breq2d 4184	. . . . . . . . . . . . . . . 16 |- ( i = m -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` m ) ) )
201	200	rspcv 3008	. . . . . . . . . . . . . . 15 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... m ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` m ) ) )
202	198, 201	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` m ) ) )
203		pntpbnd1.3	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
204	203	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
205	33	uztrn2 10459	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( |_ ` Y ) + 1 ) e. NN /\ m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) ) -> m e. NN )
206	31, 195, 205	syl2an 464	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. NN )
207	206	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> m e. NN )
208		elfzle1 11016	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ m )
209	208	adantl 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) + 1 ) <_ m )
210		elfzelz 11015	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m e. ZZ )
211		zltp1le 10281	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( |_ ` Y ) e. ZZ /\ m e. ZZ ) -> ( ( |_ ` Y ) < m <-> ( ( |_ ` Y ) + 1 ) <_ m ) )
212	177, 210, 211	syl2an 464	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( |_ ` Y ) < m <-> ( ( |_ ` Y ) + 1 ) <_ m ) )
213	209, 212	mpbird 224	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( |_ ` Y ) < m )
214		fllt 11170	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( Y e. RR /\ m e. ZZ ) -> ( Y < m <-> ( |_ ` Y ) < m ) )
215	4, 210, 214	syl2an 464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( Y < m <-> ( |_ ` Y ) < m ) )
216	213, 215	mpbird 224	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> Y < m )
217		elfzle2 11017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) -> m <_ ( |_ ` ( K x. Y ) ) )
218	217	adantl 453	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m <_ ( |_ ` ( K x. Y ) ) )
219		flge 11169	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( K x. Y ) e. RR /\ m e. ZZ ) -> ( m <_ ( K x. Y ) <-> m <_ ( |_ ` ( K x. Y ) ) ) )
220	109, 210, 219	syl2an 464	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m <_ ( K x. Y ) <-> m <_ ( |_ ` ( K x. Y ) ) ) )
221	218, 220	mpbird 224	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m <_ ( K x. Y ) )
222	216, 221	jca 519	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( Y < m /\ m <_ ( K x. Y ) ) )
223	222	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( Y < m /\ m <_ ( K x. Y ) ) )
224	10	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> E e. ( 0 (,) 1 ) )
225	3	ad2antrr 707	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> Y e. ( X (,) +oo ) )
226		simpr 448	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
227	37, 224, 7, 225, 207, 223, 226	pntpbnd1a 21232	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> ( abs ` ( ( R ` m ) / m ) ) <_ E )
228		breq2 4176	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = m -> ( Y < y <-> Y < m ) )
229		breq1 4175	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = m -> ( y <_ ( K x. Y ) <-> m <_ ( K x. Y ) ) )
230	228, 229	anbi12d 692	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = m -> ( ( Y < y /\ y <_ ( K x. Y ) ) <-> ( Y < m /\ m <_ ( K x. Y ) ) ) )
231		fveq2 5687	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = m -> ( R ` y ) = ( R ` m ) )
232		id 20	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = m -> y = m )
233	231, 232	oveq12d 6058	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y = m -> ( ( R ` y ) / y ) = ( ( R ` m ) / m ) )
234	233	fveq2d 5691	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = m -> ( abs ` ( ( R ` y ) / y ) ) = ( abs ` ( ( R ` m ) / m ) ) )
235	234	breq1d 4182	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = m -> ( ( abs ` ( ( R ` y ) / y ) ) <_ E <-> ( abs ` ( ( R ` m ) / m ) ) <_ E ) )
236	230, 235	anbi12d 692	. . . . . . . . . . . . . . . . . . . 20 |- ( y = m -> ( ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) <-> ( ( Y < m /\ m <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` m ) / m ) ) <_ E ) ) )
237	236	rspcev 3012	. . . . . . . . . . . . . . . . . . 19 |- ( ( m e. NN /\ ( ( Y < m /\ m <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` m ) / m ) ) <_ E ) ) -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
238	207, 223, 227, 237	syl12anc 1182	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) -> E. y e. NN ( ( Y < y /\ y <_ ( K x. Y ) ) /\ ( abs ` ( ( R ` y ) / y ) ) <_ E ) )
239	204, 238	mtand 641	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
240	239	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
241	206	nnrpd 10603	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> m e. RR+ )
242	38	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( m e. RR+ -> ( R ` m ) e. RR )
243	241, 242	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` m ) e. RR )
244	243	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) e. RR )
245	244	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) e. CC )
246	245	subid1d 9356	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( ( R ` m ) - 0 ) = ( R ` m ) )
247	206	peano2nnd 9973	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m + 1 ) e. NN )
248	247	nnrpd 10603	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( m + 1 ) e. RR+ )
249	38	ffvelrni 5828	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m + 1 ) e. RR+ -> ( R ` ( m + 1 ) ) e. RR )
250	248, 249	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( R ` ( m + 1 ) ) e. RR )
251	250	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) e. RR )
252	5	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> 0 e. RR )
253		letric 9130	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( 0 e. RR /\ ( R ` ( m + 1 ) ) e. RR ) -> ( 0 <_ ( R ` ( m + 1 ) ) \/ ( R ` ( m + 1 ) ) <_ 0 ) )
254	5, 250, 253	sylancr 645	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 0 <_ ( R ` ( m + 1 ) ) \/ ( R ` ( m + 1 ) ) <_ 0 ) )
255	254	ord 367	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( -. 0 <_ ( R ` ( m + 1 ) ) -> ( R ` ( m + 1 ) ) <_ 0 ) )
256	255	imp 419	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) -> ( R ` ( m + 1 ) ) <_ 0 )
257	256	adantrl 697	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) <_ 0 )
258	251, 252, 244, 257	lesub2dd 9599	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( ( R ` m ) - 0 ) <_ ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
259	246, 258	eqbrtrrd 4194	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` m ) <_ ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
260		simprl 733	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> 0 <_ ( R ` m ) )
261	244, 260	absidd 12180	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( R ` m ) ) = ( R ` m ) )
262	251, 252, 244, 257, 260	letrd 9183	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( R ` ( m + 1 ) ) <_ ( R ` m ) )
263	251, 244, 262	abssuble0d 12190	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) = ( ( R ` m ) - ( R ` ( m + 1 ) ) ) )
264	259, 261, 263	3brtr4d 4202	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( 0 <_ ( R ` m ) /\ -. 0 <_ ( R ` ( m + 1 ) ) ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
265	264	expr 599	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> ( -. 0 <_ ( R ` ( m + 1 ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) )
266	240, 265	mt3d 119	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ 0 <_ ( R ` m ) ) -> 0 <_ ( R ` ( m + 1 ) ) )
267	266	ex 424	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( 0 <_ ( R ` m ) -> 0 <_ ( R ` ( m + 1 ) ) ) )
268	202, 267	syld 42	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> 0 <_ ( R ` ( m + 1 ) ) ) )
269		ovex 6065	. . . . . . . . . . . . . 14 |- ( m + 1 ) e. _V
270		fveq2 5687	. . . . . . . . . . . . . . 15 |- ( i = ( m + 1 ) -> ( R ` i ) = ( R ` ( m + 1 ) ) )
271	270	breq2d 4184	. . . . . . . . . . . . . 14 |- ( i = ( m + 1 ) -> ( 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( m + 1 ) ) ) )
272	269, 271	ralsn 3809	. . . . . . . . . . . . 13 |- ( A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) <-> 0 <_ ( R ` ( m + 1 ) ) )
273	268, 272	syl6ibr 219	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) )
274	273	ancld 537	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) ) )
275		fzsuc 11052	. . . . . . . . . . . . . 14 |- ( m e. ( ZZ>= ` ( ( |_ ` Y ) + 1 ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) )
276	196, 275	syl 16	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) = ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) )
277	276	raleqdv 2870	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) 0 <_ ( R ` i ) ) )
278		ralunb 3488	. . . . . . . . . . . 12 |- ( A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m ) u. { ( m + 1 ) } ) 0 <_ ( R ` i ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) )
279	277, 278	syl6bb 253	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) <-> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) /\ A. i e. { ( m + 1 ) } 0 <_ ( R ` i ) ) ) )
280	274, 279	sylibrd 226	. . . . . . . . . 10 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) 0 <_ ( R ` i ) -> A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) 0 <_ ( R ` i ) ) )
281	199	breq1d 4182	. . . . . . . . . . . . . . . 16 |- ( i = m -> ( ( R ` i ) <_ 0 <-> ( R ` m ) <_ 0 ) )
282	281	rspcv 3008	. . . . . . . . . . . . . . 15 |- ( m e. ( ( ( |_ ` Y ) + 1 ) ... m ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` m ) <_ 0 ) )
283	198, 282	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` m ) <_ 0 ) )
284	239	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> -. ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
285	255	con1d 118	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( -. ( R ` ( m + 1 ) ) <_ 0 -> 0 <_ ( R ` ( m + 1 ) ) ) )
286	285	imp 419	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ -. ( R ` ( m + 1 ) ) <_ 0 ) -> 0 <_ ( R ` ( m + 1 ) ) )
287	286	adantrl 697	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> 0 <_ ( R ` ( m + 1 ) ) )
288	243	adantr 452	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) e. RR )
289	288	renegcld 9420	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) e. RR )
290	250	adantr 452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` ( m + 1 ) ) e. RR )
291	289, 290	addge02d 9571	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( 0 <_ ( R ` ( m + 1 ) ) <-> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) ) )
292	287, 291	mpbid 202	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) )
293	290	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` ( m + 1 ) ) e. CC )
294	288	recnd 9070	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) e. CC )
295	293, 294	negsubd 9373	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( ( R ` ( m + 1 ) ) + -u ( R ` m ) ) = ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
296	292, 295	breqtrd 4196	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> -u ( R ` m ) <_ ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
297		simprl 733	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) <_ 0 )
298	288, 297	absnidd 12171	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( R ` m ) ) = -u ( R ` m ) )
299	5	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> 0 e. RR )
300	288, 299, 290, 297, 287	letrd 9183	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( R ` m ) <_ ( R ` ( m + 1 ) ) )
301	288, 290, 300	abssubge0d 12189	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) = ( ( R ` ( m + 1 ) ) - ( R ` m ) ) )
302	296, 298, 301	3brtr4d 4202	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( ( R ` m ) <_ 0 /\ -. ( R ` ( m + 1 ) ) <_ 0 ) ) -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) )
303	302	expr 599	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> ( -. ( R ` ( m + 1 ) ) <_ 0 -> ( abs ` ( R ` m ) ) <_ ( abs ` ( ( R ` ( m + 1 ) ) - ( R ` m ) ) ) ) )
304	284, 303	mt3d 119	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) /\ ( R ` m ) <_ 0 ) -> ( R ` ( m + 1 ) ) <_ 0 )
305	304	ex 424	. . . . . . . . . . . . . 14 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( ( R ` m ) <_ 0 -> ( R ` ( m + 1 ) ) <_ 0 ) )
306	283, 305	syld 42	. . . . . . . . . . . . 13 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( R ` ( m + 1 ) ) <_ 0 ) )
307	270	breq1d 4182	. . . . . . . . . . . . . 14 |- ( i = ( m + 1 ) -> ( ( R ` i ) <_ 0 <-> ( R ` ( m + 1 ) ) <_ 0 ) )
308	269, 307	ralsn 3809	. . . . . . . . . . . . 13 |- ( A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 <-> ( R ` ( m + 1 ) ) <_ 0 )
309	306, 308	syl6ibr 219	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) )
310	309	ancld 537	. . . . . . . . . . 11 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... m ) ( R ` i ) <_ 0 /\ A. i e. { ( m + 1 ) } ( R ` i ) <_ 0 ) ) )
311	276	raleqdv 2870	. . . . . . . . . . . 12 |- ( ( ph /\ m e. ( ( ( |_ ` Y ) + 1 ) ... ( |_ ` ( K x. Y ) ) ) ) -> ( A. i e. ( ( ( |_ ` Y ) + 1 ) ... ( m + 1 ) ) ( R ` i ) <_ 0 <-> A. i e. ( ( ( ( |_ ` Y ) + 1 ) ... m