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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqf1o.5 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑆 )
seqf1olem.5 ⊢ ( 𝜑 → 𝐹 : ( 𝑀 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 𝑀 ... ( 𝑁 + 1 ) ) )
seqf1olem.6 ⊢ ( 𝜑 → 𝐺 : ( 𝑀 ... ( 𝑁 + 1 ) ) ⟶ 𝐶 )
seqf1olem.7 ⊢ 𝐽 = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝐹 ‘ if ( 𝑘 < 𝐾 , 𝑘 , ( 𝑘 + 1 ) ) ) )
seqf1olem.8 ⊢ 𝐾 = ( ◡ 𝐹 ‘ ( 𝑁 + 1 ) )
Assertion seqf1olem1 ( 𝜑 → 𝐽 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )

Proof

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