Metamath Proof Explorer

Theorem seqf1olem1

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

Ref Expression
Hypotheses 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 seqf1olem1 
|- ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )

Proof

Step Hyp Ref Expression
1 seqf1o.1 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x .+ y ) e. S )
2 seqf1o.2 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x .+ y ) = ( y .+ x ) )
3 seqf1o.3 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ z e. S ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
4 seqf1o.4 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
5 seqf1o.5 
 |-  ( ph -> C C_ S )
6 seqf1olem.5 
 |-  ( ph -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
7 seqf1olem.6 
 |-  ( ph -> G : ( M ... ( N + 1 ) ) --> C )
8 seqf1olem.7 
 |-  J = ( k e. ( M ... N ) |-> ( F ` if ( k < K , k , ( k + 1 ) ) ) )
9 seqf1olem.8 
 |-  K = ( `' F ` ( N + 1 ) )
10 fvexd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) e. _V )
11 fvex 
 |-  ( `' F ` x ) e. _V
12 ovex 
 |-  ( ( `' F ` x ) - 1 ) e. _V
13 11 12 ifex 
 |-  if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V
14 13 a1i 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) e. _V )
15 iftrue 
 |-  ( k < K -> if ( k < K , k , ( k + 1 ) ) = k )
16 15 fveq2d 
 |-  ( k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
17 16 eqeq2d 
 |-  ( k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
18 17 adantl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` k ) ) )
19 simprr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x = ( F ` k ) )
20 elfzelz 
 |-  ( k e. ( M ... N ) -> k e. ZZ )
21 20 zred 
 |-  ( k e. ( M ... N ) -> k e. RR )
22 21 ad2antlr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. RR )
23 simprl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k < K )
24 22 23 gtned 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> K =/= k )
25 f1of 
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
26 6 25 syl 
 |-  ( ph -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
27 26 ad2antrr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
28 fzssp1 
 |-  ( M ... N ) C_ ( M ... ( N + 1 ) )
29 simplr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... N ) )
30 28 29 sseldi 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k e. ( M ... ( N + 1 ) ) )
31 27 30 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... ( N + 1 ) ) )
32 elfzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
33 4 32 syl 
 |-  ( ph -> ( ( F ` k ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) ) )
34 33 ad2antrr 
 |-  ( ( ( 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 ) ) ) )
35 31 34 mpbid 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) e. ( M ... N ) \/ ( F ` k ) = ( N + 1 ) ) )
36 35 ord 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> ( F ` k ) = ( N + 1 ) ) )
37 6 ad2antrr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
38 f1ocnvfv 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
39 37 30 38 syl2anc 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = k ) )
40 9 eqeq1i 
 |-  ( K = k <-> ( `' F ` ( N + 1 ) ) = k )
41 39 40 syl6ibr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = ( N + 1 ) -> K = k ) )
42 36 41 syld 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( -. ( F ` k ) e. ( M ... N ) -> K = k ) )
43 42 necon1ad 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( K =/= k -> ( F ` k ) e. ( M ... N ) ) )
44 24 43 mpd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) e. ( M ... N ) )
45 19 44 eqeltrd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> x e. ( M ... N ) )
46 19 eqcomd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( F ` k ) = x )
47 f1ocnvfv 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ k e. ( M ... ( N + 1 ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
48 37 30 47 syl2anc 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( ( F ` k ) = x -> ( `' F ` x ) = k ) )
49 46 48 mpd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) = k )
50 49 23 eqbrtrd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( `' F ` x ) < K )
51 iftrue 
 |-  ( ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
52 50 51 syl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( `' F ` x ) )
53 52 49 eqtr2d 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
54 45 53 jca 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( k < K /\ x = ( F ` k ) ) ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) )
55 54 expr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ k < K ) -> ( x = ( F ` k ) -> ( x e. ( M ... N ) /\ k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) ) ) )
56 18 55 sylbid 
 |-  ( ( ( 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 ) ) ) ) )
57 iffalse 
 |-  ( -. k < K -> if ( k < K , k , ( k + 1 ) ) = ( k + 1 ) )
58 57 fveq2d 
 |-  ( -. k < K -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
59 58 eqeq2d 
 |-  ( -. k < K -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
60 59 adantl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ -. k < K ) -> ( x = ( F ` if ( k < K , k , ( k + 1 ) ) ) <-> x = ( F ` ( k + 1 ) ) ) )
61 simprr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x = ( F ` ( k + 1 ) ) )
62 f1ocnv 
 |-  ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
63 6 62 syl 
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
64 f1of1 
 |-  ( `' F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
65 63 64 syl 
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
66 f1f 
 |-  ( `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
67 65 66 syl 
 |-  ( ph -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
68 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
69 4 68 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
70 eluzfz2 
 |-  ( ( N + 1 ) e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
71 69 70 syl 
 |-  ( ph -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
72 67 71 ffvelrnd 
 |-  ( ph -> ( `' F ` ( N + 1 ) ) e. ( M ... ( N + 1 ) ) )
73 9 72 eqeltrid 
 |-  ( ph -> K e. ( M ... ( N + 1 ) ) )
74 elfzelz 
 |-  ( K e. ( M ... ( N + 1 ) ) -> K e. ZZ )
75 73 74 syl 
 |-  ( ph -> K e. ZZ )
76 75 zred 
 |-  ( ph -> K e. RR )
77 76 ad2antrr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K e. RR )
78 21 ad2antlr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. RR )
79 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
80 78 79 syl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. RR )
81 simprl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. k < K )
82 77 78 81 nltled 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K <_ k )
83 78 ltp1d 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k < ( k + 1 ) )
84 77 78 80 82 83 lelttrd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K < ( k + 1 ) )
85 77 84 ltned 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> K =/= ( k + 1 ) )
86 26 ad2antrr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
87 fzp1elp1 
 |-  ( k e. ( M ... N ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
88 87 ad2antlr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( k + 1 ) e. ( M ... ( N + 1 ) ) )
89 86 88 ffvelrnd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) )
90 elfzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
91 4 90 syl 
 |-  ( ph -> ( ( F ` ( k + 1 ) ) e. ( M ... ( N + 1 ) ) <-> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) ) )
92 91 ad2antrr 
 |-  ( ( ( 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 ) ) ) )
93 89 92 mpbid 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) e. ( M ... N ) \/ ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
94 93 ord 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> ( F ` ( k + 1 ) ) = ( N + 1 ) ) )
95 6 ad2antrr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
96 f1ocnvfv 
 |-  ( ( 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 ) ) )
97 95 88 96 syl2anc 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> ( `' F ` ( N + 1 ) ) = ( k + 1 ) ) )
98 9 eqeq1i 
 |-  ( K = ( k + 1 ) <-> ( `' F ` ( N + 1 ) ) = ( k + 1 ) )
99 97 98 syl6ibr 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = ( N + 1 ) -> K = ( k + 1 ) ) )
100 94 99 syld 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( -. ( F ` ( k + 1 ) ) e. ( M ... N ) -> K = ( k + 1 ) ) )
101 100 necon1ad 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( K =/= ( k + 1 ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) ) )
102 85 101 mpd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) e. ( M ... N ) )
103 61 102 eqeltrd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> x e. ( M ... N ) )
104 61 eqcomd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( F ` ( k + 1 ) ) = x )
105 f1ocnvfv 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ ( k + 1 ) e. ( M ... ( N + 1 ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
106 95 88 105 syl2anc 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( F ` ( k + 1 ) ) = x -> ( `' F ` x ) = ( k + 1 ) ) )
107 104 106 mpd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( `' F ` x ) = ( k + 1 ) )
108 107 breq1d 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K <-> ( k + 1 ) < K ) )
109 lttr 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR /\ K e. RR ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
110 78 80 77 109 syl3anc 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k < ( k + 1 ) /\ ( k + 1 ) < K ) -> k < K ) )
111 83 110 mpand 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) < K -> k < K ) )
112 108 111 sylbid 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) < K -> k < K ) )
113 81 112 mtod 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> -. ( `' F ` x ) < K )
114 iffalse 
 |-  ( -. ( `' F ` x ) < K -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
115 113 114 syl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) = ( ( `' F ` x ) - 1 ) )
116 107 oveq1d 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( `' F ` x ) - 1 ) = ( ( k + 1 ) - 1 ) )
117 78 recnd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k e. CC )
118 ax-1cn 
 |-  1 e. CC
119 pncan 
 |-  ( ( k e. CC /\ 1 e. CC ) -> ( ( k + 1 ) - 1 ) = k )
120 117 118 119 sylancl 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> ( ( k + 1 ) - 1 ) = k )
121 115 116 120 3eqtrrd 
 |-  ( ( ( ph /\ k e. ( M ... N ) ) /\ ( -. k < K /\ x = ( F ` ( k + 1 ) ) ) ) -> k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) )
122 103 121 jca 
 |-  ( ( ( 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 ) ) ) )
123 122 expr 
 |-  ( ( ( 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 ) ) ) ) )
124 60 123 sylbid 
 |-  ( ( ( 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 ) ) ) ) )
125 56 124 pm2.61dan 
 |-  ( ( 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 ) ) ) ) )
126 125 expimpd 
 |-  ( 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 ) ) ) ) )
127 51 eqeq2d 
 |-  ( ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
128 127 adantl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( `' F ` x ) ) )
129 simprr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k = ( `' F ` x ) )
130 67 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
131 simplr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... N ) )
132 28 131 sseldi 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x e. ( M ... ( N + 1 ) ) )
133 130 132 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
134 129 133 eqeltrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... ( N + 1 ) ) )
135 elfzle1 
 |-  ( k e. ( M ... ( N + 1 ) ) -> M <_ k )
136 134 135 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M <_ k )
137 elfzelz 
 |-  ( k e. ( M ... ( N + 1 ) ) -> k e. ZZ )
138 134 137 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ZZ )
139 138 zred 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. RR )
140 76 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K e. RR )
141 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
142 4 141 syl 
 |-  ( ph -> N e. ZZ )
143 142 peano2zd 
 |-  ( ph -> ( N + 1 ) e. ZZ )
144 143 zred 
 |-  ( ph -> ( N + 1 ) e. RR )
145 144 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( N + 1 ) e. RR )
146 simprl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( `' F ` x ) < K )
147 129 146 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < K )
148 elfzle2 
 |-  ( K e. ( M ... ( N + 1 ) ) -> K <_ ( N + 1 ) )
149 73 148 syl 
 |-  ( ph -> K <_ ( N + 1 ) )
150 149 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> K <_ ( N + 1 ) )
151 139 140 145 147 150 ltletrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k < ( N + 1 ) )
152 142 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> N e. ZZ )
153 zleltp1 
 |-  ( ( k e. ZZ /\ N e. ZZ ) -> ( k <_ N <-> k < ( N + 1 ) ) )
154 138 152 153 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k <_ N <-> k < ( N + 1 ) ) )
155 151 154 mpbird 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k <_ N )
156 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
157 4 156 syl 
 |-  ( ph -> M e. ZZ )
158 157 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> M e. ZZ )
159 elfz 
 |-  ( ( k e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
160 138 158 152 159 syl3anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
161 136 155 160 mpbir2and 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> k e. ( M ... N ) )
162 147 16 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` k ) )
163 129 fveq2d 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` k ) = ( F ` ( `' F ` x ) ) )
164 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
165 f1ocnvfv2 
 |-  ( ( F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) /\ x e. ( M ... ( N + 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
166 164 132 165 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( F ` ( `' F ` x ) ) = x )
167 162 163 166 3eqtrrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
168 161 167 jca 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( ( `' F ` x ) < K /\ k = ( `' F ` x ) ) ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) )
169 168 expr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( `' F ` x ) < K ) -> ( k = ( `' F ` x ) -> ( k e. ( M ... N ) /\ x = ( F ` if ( k < K , k , ( k + 1 ) ) ) ) ) )
170 128 169 sylbid 
 |-  ( ( ( 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 ) ) ) ) ) )
171 114 eqeq2d 
 |-  ( -. ( `' F ` x ) < K -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
172 171 adantl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ -. ( `' F ` x ) < K ) -> ( k = if ( ( `' F ` x ) < K , ( `' F ` x ) , ( ( `' F ` x ) - 1 ) ) <-> k = ( ( `' F ` x ) - 1 ) ) )
173 157 zred 
 |-  ( ph -> M e. RR )
174 173 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. RR )
175 76 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. RR )
176 simprr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k = ( ( `' F ` x ) - 1 ) )
177 67 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) --> ( M ... ( N + 1 ) ) )
178 simplr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... N ) )
179 28 178 sseldi 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x e. ( M ... ( N + 1 ) ) )
180 177 179 ffvelrnd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ( M ... ( N + 1 ) ) )
181 elfzelz 
 |-  ( ( `' F ` x ) e. ( M ... ( N + 1 ) ) -> ( `' F ` x ) e. ZZ )
182 180 181 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. ZZ )
183 peano2zm 
 |-  ( ( `' F ` x ) e. ZZ -> ( ( `' F ` x ) - 1 ) e. ZZ )
184 182 183 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) e. ZZ )
185 176 184 eqeltrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ZZ )
186 185 zred 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. RR )
187 elfzle1 
 |-  ( K e. ( M ... ( N + 1 ) ) -> M <_ K )
188 73 187 syl 
 |-  ( ph -> M <_ K )
189 188 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ K )
190 182 zred 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. RR )
191 simprl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. ( `' F ` x ) < K )
192 175 190 191 nltled 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( `' F ` x ) )
193 elfzelz 
 |-  ( x e. ( M ... N ) -> x e. ZZ )
194 193 adantl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. ZZ )
195 194 zred 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. RR )
196 142 zred 
 |-  ( ph -> N e. RR )
197 196 adantr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N e. RR )
198 144 adantr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) e. RR )
199 elfzle2 
 |-  ( x e. ( M ... N ) -> x <_ N )
200 199 adantl 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x <_ N )
201 197 ltp1d 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> N < ( N + 1 ) )
202 195 197 198 200 201 lelttrd 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x < ( N + 1 ) )
203 195 202 gtned 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( N + 1 ) =/= x )
204 203 adantr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) =/= x )
205 65 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> `' F : ( M ... ( N + 1 ) ) -1-1-> ( M ... ( N + 1 ) ) )
206 71 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( N + 1 ) e. ( M ... ( N + 1 ) ) )
207 f1fveq 
 |-  ( ( `' 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 ) )
208 205 206 179 207 syl12anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) = ( `' F ` x ) <-> ( N + 1 ) = x ) )
209 208 necon3bid 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) <-> ( N + 1 ) =/= x ) )
210 204 209 mpbird 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
211 9 neeq1i 
 |-  ( K =/= ( `' F ` x ) <-> ( `' F ` ( N + 1 ) ) =/= ( `' F ` x ) )
212 210 211 sylibr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K =/= ( `' F ` x ) )
213 212 necomd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) =/= K )
214 175 190 192 213 leneltd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K < ( `' F ` x ) )
215 75 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K e. ZZ )
216 zltlem1 
 |-  ( ( K e. ZZ /\ ( `' F ` x ) e. ZZ ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
217 215 182 216 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( K < ( `' F ` x ) <-> K <_ ( ( `' F ` x ) - 1 ) ) )
218 214 217 mpbid 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ ( ( `' F ` x ) - 1 ) )
219 218 176 breqtrrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> K <_ k )
220 174 175 186 189 219 letrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M <_ k )
221 elfzle2 
 |-  ( ( `' F ` x ) e. ( M ... ( N + 1 ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
222 180 221 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) <_ ( N + 1 ) )
223 196 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. RR )
224 1re 
 |-  1 e. RR
225 lesubadd 
 |-  ( ( ( `' F ` x ) e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
226 224 225 mp3an2 
 |-  ( ( ( `' F ` x ) e. RR /\ N e. RR ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
227 190 223 226 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) <_ N <-> ( `' F ` x ) <_ ( N + 1 ) ) )
228 222 227 mpbird 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( `' F ` x ) - 1 ) <_ N )
229 176 228 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k <_ N )
230 157 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> M e. ZZ )
231 142 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> N e. ZZ )
232 185 230 231 159 syl3anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k e. ( M ... N ) <-> ( M <_ k /\ k <_ N ) ) )
233 220 229 232 mpbir2and 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> k e. ( M ... N ) )
234 175 186 219 lensymd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> -. k < K )
235 234 58 syl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` if ( k < K , k , ( k + 1 ) ) ) = ( F ` ( k + 1 ) ) )
236 176 oveq1d 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( ( ( `' F ` x ) - 1 ) + 1 ) )
237 182 zcnd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( `' F ` x ) e. CC )
238 npcan 
 |-  ( ( ( `' F ` x ) e. CC /\ 1 e. CC ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
239 237 118 238 sylancl 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( ( ( `' F ` x ) - 1 ) + 1 ) = ( `' F ` x ) )
240 236 239 eqtrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( k + 1 ) = ( `' F ` x ) )
241 240 fveq2d 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( k + 1 ) ) = ( F ` ( `' F ` x ) ) )
242 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> F : ( M ... ( N + 1 ) ) -1-1-onto-> ( M ... ( N + 1 ) ) )
243 242 179 165 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> ( F ` ( `' F ` x ) ) = x )
244 235 241 243 3eqtrrd 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ ( -. ( `' F ` x ) < K /\ k = ( ( `' F ` x ) - 1 ) ) ) -> x = ( F ` if ( k < K , k , ( k + 1 ) ) ) )
245 233 244 jca 
 |-  ( ( ( 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 
 |-  ( ( ( 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 172 246 sylbid 
 |-  ( ( ( 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 170 247 pm2.61dan 
 |-  ( ( 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 
 |-  ( 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 126 249 impbid 
 |-  ( 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 8 10 14 250 f1od 
 |-  ( ph -> J : ( M ... N ) -1-1-onto-> ( M ... N ) )