# 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
seqf1o.2
seqf1o.3
seqf1o.4 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
seqf1o.5 ${⊢}{\phi }\to {C}\subseteq {S}$
seqf1olem.5 ${⊢}{\phi }\to {F}:\left({M}\dots {N}+1\right)\underset{1-1 onto}{⟶}\left({M}\dots {N}+1\right)$
seqf1olem.6 ${⊢}{\phi }\to {G}:\left({M}\dots {N}+1\right)⟶{C}$
seqf1olem.7 ${⊢}{J}=\left({k}\in \left({M}\dots {N}\right)⟼{F}\left(if\left({k}<{K},{k},{k}+1\right)\right)\right)$
seqf1olem.8 ${⊢}{K}={{F}}^{-1}\left({N}+1\right)$
Assertion seqf1olem1 ${⊢}{\phi }\to {J}:\left({M}\dots {N}\right)\underset{1-1 onto}{⟶}\left({M}\dots {N}\right)$

### Proof

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