Theorem seqf1olem1 11841

Description: Lemma for seqf1o 11843. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)

Hypotheses

Ref	Expression
seqf1o.1	|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
seqf1o.2	|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
seqf1o.3	|- ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
seqf1o.4	|- ( ph -> N e. ( ZZ>= ` M ) )
seqf1o.5	|- ( ph -> C C_ S )
seqf1olem.5	|- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
seqf1olem.6	|- ( ph -> G : ( M ... ( N + 1 ) ) --> C )
seqf1olem.7	|- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
seqf1olem.8	|- K = ( `' F ` ( N + 1 ) )

Assertion

Ref	Expression
seqf1olem1	|- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )

Distinct variable groups:   x, k, y, z, F   k, G, x, y, z   k, M, x, y, z   .+ , k, x, y, z   x, J, y, z   k, N, x, y, z   k, K, x, y, z   ph, k, x, y, z   S, k, x, y, z   C, k, x, y, z

Allowed substitution hint:   J( k)

Proof of Theorem seqf1olem1

Step	Hyp	Ref	Expression
1		seqf1olem.7	. 2 |- J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
2		fvex 5698	. . 3 |- ( F ` if ( k < K , k , ( k + 1 ) ) ) e. _V
3	2	a1i 11	. 2 |- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) e. _V )
4		fvex 5698	. . . 4 |- ( `' F ` x ) e. _V
5		ovex 6115	. . . 4 |- ( ( `' F ` x ) - 1 ) e. _V
6	4, 5	ifex 3855	. . 3 |- if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V
7	6	a1i 11	. 2 |- ( ( ph /\ x e. ( M ... N ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V )
8		iftrue 3794	. . . . . . . . 9 |- ( k < K -> if ( k < K , k , ( k + 1 ) ) = k )
9	8	fveq2d 5692	. . . . . . . 8 |- ( k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
10	9	eqeq2d 2452	. . . . . . 7 |- ( k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
11	10	adantl 463	. . . . . 6 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
12		simprr 751	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x = ( F ` k ) )
13		elfzelz 11449	. . . . . . . . . . . . 13 |- ( k e. ( M ... N ) -> k e. ZZ )
14	13	zred 10743	. . . . . . . . . . . 12 |- ( k e. ( M ... N ) -> k e. RR )
15	14	ad2antlr 721	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. RR )
16		simprl 750	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k < K )
17	15, 16	gtned 9505	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> K =/= k )
18		seqf1olem.5	. . . . . . . . . . . . . . . . 17 |- ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
19		f1of 5638	. . . . . . . . . . . . . . . . 17 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
20	18, 19	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
21	20	ad2antrr 720	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
22		fzssp1 11497	. . . . . . . . . . . . . . . 16 |- ( M ... N ) C_ ( M ... ( N + 1 ) )
23		simplr 749	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... N ) )
24	22, 23	sseldi 3351	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... ( N + 1 ) ) )
25	21, 24	ffvelrnd 5841	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... ( N + 1 ) ) )
26		seqf1o.4	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. ( ZZ>= ` M ) )
27		elfzp1 11501	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` M ) -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
28	26, 27	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
29	28	ad2antrr 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
30	25, 29	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) )
31	30	ord 377	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> ( F ` k ) = ( N + 1 ) ) )
32	18	ad2antrr 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
33		f1ocnvfv 5982	. . . . . . . . . . . . . 14 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
34	32, 24, 33	syl2anc 656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
35		seqf1olem.8	. . . . . . . . . . . . . 14 |- K = ( `' F ` ( N + 1 ) )
36	35	eqeq1i 2448	. . . . . . . . . . . . 13 |- ( K = k <-> ( `' F ` ( N + 1 ) ) = k )
37	34, 36	syl6ibr 227	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> K = k ) )
38	31, 37	syld 44	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> K = k ) )
39	38	necon1ad 2676	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( K =/= k -> ( F ` k ) e. ( M ... N ) ) )
40	17, 39	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... N ) )
41	12, 40	eqeltrd 2515	. . . . . . . 8 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x e. ( M ... N ) )
42	12	eqcomd 2446	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) = x )
43		f1ocnvfv 5982	. . . . . . . . . . . . 13 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
44	32, 24, 43	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
45	42, 44	mpd 15	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) = k )
46	45, 16	eqbrtrd 4309	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) < K )
47		iftrue 3794	. . . . . . . . . 10 |- ( ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
48	46, 47	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
49	48, 45	eqtr2d 2474	. . . . . . . 8 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
50	41, 49	jca 529	. . . . . . 7 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) )
51	50	expr 612	. . . . . 6 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` k ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
52	11, 51	sylbid 215	. . . . 5 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
53		iffalse 3796	. . . . . . . . 9 |- ( -. k < K -> if ( k < K , k , ( k + 1 ) ) = ( k + 1 ) )
54	53	fveq2d 5692	. . . . . . . 8 |- ( -. k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
55	54	eqeq2d 2452	. . . . . . 7 |- ( -. k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
56	55	adantl 463	. . . . . 6 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
57		simprr 751	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x = ( F ` ( k + 1 ) ) )
58		f1ocnv 5650	. . . . . . . . . . . . . . . . . . 19 |- ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
59	18, 58	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
60		f1of1 5637	. . . . . . . . . . . . . . . . . 18 |- ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
61	59, 60	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
62		f1f 5603	. . . . . . . . . . . . . . . . 17 |- ( `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
63	61, 62	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
64		peano2uz 10904	. . . . . . . . . . . . . . . . . 18 |- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
65	26, 64	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
66		eluzfz2 11455	. . . . . . . . . . . . . . . . 17 |- ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
67	65, 66	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
68	63, 67	ffvelrnd 5841	. . . . . . . . . . . . . . 15 |- ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
69	35, 68	syl5eqel 2525	. . . . . . . . . . . . . 14 |- ( ph -> K e. ( M ... ( N + 1 ) ) )
70		elfzelz 11449	. . . . . . . . . . . . . 14 |- ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
71	69, 70	syl 16	. . . . . . . . . . . . 13 |- ( ph -> K e. ZZ )
72	71	zred 10743	. . . . . . . . . . . 12 |- ( ph -> K e. RR )
73	72	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K e. RR )
74	14	ad2antlr 721	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. RR )
75		peano2re 9538	. . . . . . . . . . . . 13 |- ( k e. RR -> ( k + 1 ) e. RR )
76	74, 75	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. RR )
77		simprl 750	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. k < K )
78	73, 74	lenltd 9516	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( K <_ k <-> -. k < K ) )
79	77, 78	mpbird 232	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K <_ k )
80	74	ltp1d 10259	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k < ( k + 1 ) )
81	73, 74, 76, 79, 80	lelttrd 9525	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K < ( k + 1 ) )
82	73, 81	ltned 9506	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K =/= ( k + 1 ) )
83	20	ad2antrr 720	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
84		fzp1elp1 11505	. . . . . . . . . . . . . . . 16 |- ( k e. ( M ... N ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
85	84	ad2antlr 721	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
86	83, 85	ffvelrnd 5841	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) )
87		elfzp1 11501	. . . . . . . . . . . . . . . 16 |- ( N e. ( ZZ>= ` M ) -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
88	26, 87	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
89	88	ad2antrr 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
90	86, 89	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
91	90	ord 377	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
92	18	ad2antrr 720	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
93		f1ocnvfv 5982	. . . . . . . . . . . . . 14 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( k + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = ( k + 1 ) ) )
94	92, 85, 93	syl2anc 656	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = ( k + 1 ) ) )
95	35	eqeq1i 2448	. . . . . . . . . . . . 13 |- ( K = ( k + 1 ) <-> ( `' F ` ( N + 1 ) ) = ( k + 1 ) )
96	94, 95	syl6ibr 227	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> K = ( k + 1 ) ) )
97	91, 96	syld 44	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> K = ( k + 1 ) ) )
98	97	necon1ad 2676	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( K =/= ( k + 1 ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) ) )
99	82, 98	mpd 15	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) )
100	57, 99	eqeltrd 2515	. . . . . . . 8 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x e. ( M ... N ) )
101	57	eqcomd 2446	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) = x )
102		f1ocnvfv 5982	. . . . . . . . . . . . . . 15 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( k + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
103	92, 85, 102	syl2anc 656	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
104	101, 103	mpd 15	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( `' F ` x ) = ( k + 1 ) )
105	104	breq1d 4299	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K <-> ( k + 1 ) < K ) )
106		lttr 9447	. . . . . . . . . . . . . 14 |- ( ( k e. RR /\ ( k + 1 ) e. RR /\ K e. RR ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
107	74, 76, 73, 106	syl3anc 1213	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
108	80, 107	mpand 670	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) < K -> k < K ) )
109	105, 108	sylbid 215	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K -> k < K ) )
110	77, 109	mtod 177	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. ( `' F ` x ) < K )
111		iffalse 3796	. . . . . . . . . 10 |- ( -. ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
112	110, 111	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
113	104	oveq1d 6105	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) - 1 ) = ( ( k + 1 ) - 1 ) )
114	74	recnd 9408	. . . . . . . . . 10 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. CC )
115		ax-1cn 9336	. . . . . . . . . 10 |- 1 e. CC
116		pncan 9612	. . . . . . . . . 10 |- ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
117	114, 115, 116	sylancl 657	. . . . . . . . 9 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) - 1 ) = k )
118	112, 113, 117	3eqtrrd 2478	. . . . . . . 8 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
119	100, 118	jca 529	. . . . . . 7 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) )
120	119	expr 612	. . . . . 6 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` ( k + 1 ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
121	56, 120	sylbid 215	. . . . 5 |- ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
122	52, 121	pm2.61dan 784	. . . 4 |- ( ( ph /\ k e. ( M ... N ) ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
123	122	expimpd 600	. . 3 |- ( ph -> ( ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
124	47	eqeq2d 2452	. . . . . . 7 |- ( ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
125	124	adantl 463	. . . . . 6 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
126		simprr 751	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k = ( `' F ` x ) )
127	63	ad2antrr 720	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
128		simplr 749	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... N ) )
129	22, 128	sseldi 3351	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... ( N + 1 ) ) )
130	127, 129	ffvelrnd 5841	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
131	126, 130	eqeltrd 2515	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... ( N + 1 ) ) )
132		elfzle1 11450	. . . . . . . . . 10 |- ( k e. ( M ... ( N + 1 ) ) -> M <_ k )
133	131, 132	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M <_ k )
134		elfzelz 11449	. . . . . . . . . . . . 13 |- ( k e. ( M ... ( N + 1 ) ) -> k e. ZZ )
135	131, 134	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ZZ )
136	135	zred 10743	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. RR )
137	72	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K e. RR )
138		eluzelz 10866	. . . . . . . . . . . . . . 15 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
139	26, 138	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> N e. ZZ )
140	139	peano2zd 10746	. . . . . . . . . . . . 13 |- ( ph -> ( N + 1 ) e. ZZ )
141	140	zred 10743	. . . . . . . . . . . 12 |- ( ph -> ( N + 1 ) e. RR )
142	141	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( N + 1 ) e. RR )
143		simprl 750	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) < K )
144	126, 143	eqbrtrd 4309	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < K )
145		elfzle2 11451	. . . . . . . . . . . . 13 |- ( K e. ( M ... ( N + 1 ) ) -> K <_ ( N + 1 ) )
146	69, 145	syl 16	. . . . . . . . . . . 12 |- ( ph -> K <_ ( N + 1 ) )
147	146	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K <_ ( N + 1 ) )
148	136, 137, 142, 144, 147	ltletrd 9527	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < ( N + 1 ) )
149	139	ad2antrr 720	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> N e. ZZ )
150		zleltp1 10691	. . . . . . . . . . 11 |- ( ( k e. ZZ /\ N e. ZZ ) -> ( k <_ N <-> k < ( N + 1 ) ) )
151	135, 149, 150	syl2anc 656	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k <_ N <-> k < ( N + 1 ) ) )
152	148, 151	mpbird 232	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k <_ N )
153		eluzel2 10862	. . . . . . . . . . . 12 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
154	26, 153	syl 16	. . . . . . . . . . 11 |- ( ph -> M e. ZZ )
155	154	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M e. ZZ )
156		elfz 11439	. . . . . . . . . 10 |- ( ( k e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
157	135, 155, 149, 156	syl3anc 1213	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
158	133, 152, 157	mpbir2and 908	. . . . . . . 8 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... N ) )
159	144, 9	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
160	126	fveq2d 5692	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` k ) = ( F ` ( `' F ` x ) ) )
161	18	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
162		f1ocnvfv2 5981	. . . . . . . . . 10 |- ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
163	161, 129, 162	syl2anc 656	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` ( `' F ` x ) ) = x )
164	159, 160, 163	3eqtrrd 2478	. . . . . . . 8 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
165	158, 164	jca 529	. . . . . . 7 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) )
166	165	expr 612	. . . . . 6 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = ( `' F ` x ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
167	125, 166	sylbid 215	. . . . 5 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
168	111	eqeq2d 2452	. . . . . . 7 |- ( -. ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
169	168	adantl 463	. . . . . 6 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
170	154	zred 10743	. . . . . . . . . . 11 |- ( ph -> M e. RR )
171	170	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. RR )
172	72	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. RR )
173		simprr 751	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k = ( ( `' F ` x ) - 1 ) )
174	63	ad2antrr 720	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
175		simplr 749	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... N ) )
176	22, 175	sseldi 3351	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
177	174, 176	ffvelrnd 5841	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
178		elfzelz 11449	. . . . . . . . . . . . . 14 |- ( ( `' F ` x ) e. ( M ... ( N + 1 ) ) -> ( `' F ` x ) e. ZZ )
179	177, 178	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ZZ )
180		peano2zm 10684	. . . . . . . . . . . . 13 |- ( ( `' F ` x ) e. ZZ -> ( ( `' F ` x ) - 1 ) e. ZZ )
181	179, 180	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) e. ZZ )
182	173, 181	eqeltrd 2515	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ZZ )
183	182	zred 10743	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. RR )
184		elfzle1 11450	. . . . . . . . . . . 12 |- ( K e. ( M ... ( N + 1 ) ) -> M <_ K )
185	69, 184	syl 16	. . . . . . . . . . 11 |- ( ph -> M <_ K )
186	185	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ K )
187		simprl 750	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. ( `' F ` x ) < K )
188	179	zred 10743	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. RR )
189	172, 188	lenltd 9516	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K <_ ( `' F ` x ) <-> -. ( `' F ` x ) < K ) )
190	187, 189	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( `' F ` x ) )
191		elfzelz 11449	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( M ... N ) -> x e. ZZ )
192	191	adantl 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. ZZ )
193	192	zred 10743	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
194	139	zred 10743	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> N e. RR )
195	194	adantr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
196	141	adantr 462	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
197		elfzle2 11451	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( M ... N ) -> x <_ N )
198	197	adantl 463	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
199	195	ltp1d 10259	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
200	193, 195, 196, 198, 199	lelttrd 9525	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
201	193, 200	gtned 9505	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) =/= x )
202	201	adantr 462	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) =/= x )
203	61	ad2antrr 720	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
204	67	ad2antrr 720	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
205		f1fveq 5972	. . . . . . . . . . . . . . . . . 18 |- ( ( `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) /\ ( ( N + 1 ) e. ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) ) -> ( ( `' F ` ( N + 1 ) ) = ( `' F ` x ) <-> ( N + 1 ) = x ) )
206	203, 204, 176, 205	syl12anc 1211	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) = ( `' F ` x ) <-> ( N + 1 ) = x ) )
207	206	necon3bid 2641	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) <-> ( N + 1 ) =/= x ) )
208	202, 207	mpbird 232	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
209	35	neeq1i 2616	. . . . . . . . . . . . . . 15 |- ( K =/= ( `' F ` x ) <-> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
210	208, 209	sylibr 212	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K =/= ( `' F ` x ) )
211	210	necomd 2693	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) =/= K )
212	172, 188	ltlend 9515	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K < ( `' F ` x ) <-> ( K <_ ( `' F ` x ) /\ ( `' F ` x ) =/= K ) ) )
213	190, 211, 212	mpbir2and 908	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K < ( `' F ` x ) )
214	71	ad2antrr 720	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. ZZ )
215		zltlem1 10693	. . . . . . . . . . . . 13 |- ( ( K e. ZZ /\ ( `' F ` x ) e. ZZ ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
216	214, 179, 215	syl2anc 656	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
217	213, 216	mpbid 210	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( ( `' F ` x ) - 1 ) )
218	217, 173	breqtrrd 4315	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ k )
219	171, 172, 183, 186, 218	letrd 9524	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ k )
220		elfzle2 11451	. . . . . . . . . . . 12 |- ( ( `' F ` x ) e. ( M ... ( N + 1 ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
221	177, 220	syl 16	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
222	194	ad2antrr 720	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. RR )
223		1re 9381	. . . . . . . . . . . . 13 |- 1 e. RR
224		lesubadd 9807	. . . . . . . . . . . . 13 |- ( ( ( `' F ` x ) e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
225	223, 224	mp3an2 1297	. . . . . . . . . . . 12 |- ( ( ( `' F ` x ) e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
226	188, 222, 225	syl2anc 656	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
227	221, 226	mpbird 232	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) <_ N )
228	173, 227	eqbrtrd 4309	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k <_ N )
229	154	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. ZZ )
230	139	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. ZZ )
231	182, 229, 230, 156	syl3anc 1213	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
232	219, 228, 231	mpbir2and 908	. . . . . . . 8 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ( M ... N ) )
233	172, 183	lenltd 9516	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K <_ k <-> -. k < K ) )
234	218, 233	mpbid 210	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. k < K )
235	234, 54	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
236	173	oveq1d 6105	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( ( ( `' F ` x ) - 1 ) + 1 ) )
237	179	zcnd 10744	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. CC )
238		npcan 9615	. . . . . . . . . . . 12 |- ( ( ( `' F ` x ) e. CC /\ 1 e. CC ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
239	237, 115, 238	sylancl 657	. . . . . . . . . . 11 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
240	236, 239	eqtrd 2473	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( `' F ` x ) )
241	240	fveq2d 5692	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( k + 1 ) ) = ( F ` ( `' F ` x ) ) )
242	18	ad2antrr 720	. . . . . . . . . 10 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
243	242, 176, 162	syl2anc 656	. . . . . . . . 9 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
244	235, 241, 243	3eqtrrd 2478	. . . . . . . 8 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
245	232, 244	jca 529	. . . . . . 7 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) )
246	245	expr 612	. . . . . 6 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = ( ( `' F ` x ) - 1 ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
247	169, 246	sylbid 215	. . . . 5 |- ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
248	167, 247	pm2.61dan 784	. . . 4 |- ( ( ph /\ x e. ( M ... N ) ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
249	248	expimpd 600	. . 3 |- ( ph -> ( ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
250	123, 249	impbid 191	. 2 |- ( ph -> ( ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) <-> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
251	1, 3, 7, 250	f1od 6309	1 |- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1761   =/= wne 2604   _Vcvv 2970   C_ wss 3325   ifcif 3788   class class class wbr 4289   e. cmpt 4347   `'ccnv 4835   -->wf 5411   -1-1->wf1 5412   -1-1-onto->wf1o 5414   ` cfv 5415  (class class class)co 6090   CCcc 9276   RRcr 9277   1c1 9279   + caddc 9281   < clt 9414   <_ cle 9415   - cmin 9591   ZZcz 10642   ZZ>=cuz 10857   ...cfz 11433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-n0 10576  df-z 10643  df-uz 10858  df-fz 11434

This theorem is referenced by:  seqf1olem2  11842