MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  seqf1olem1 Structured version   Visualization version   GIF version

Theorem seqf1olem1 14079
Description: Lemma for seqf1o 14081. (Contributed by Mario Carneiro, 26-Feb-2014.) (Revised by Mario Carneiro, 27-May-2014.)
Hypotheses
Ref Expression
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
Ref Expression
seqf1olem1 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
Distinct variable groups:   𝑥,𝑘,𝑦,𝑧,𝐹   𝑘,𝐺,𝑥,𝑦,𝑧   𝑘,𝑀,𝑥,𝑦,𝑧   + ,𝑘,𝑥,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝑘,𝑁,𝑥,𝑦,𝑧   𝑘,𝐾,𝑥,𝑦,𝑧   𝜑,𝑘,𝑥,𝑦,𝑧   𝑆,𝑘,𝑥,𝑦,𝑧   𝐶,𝑘,𝑥,𝑦,𝑧
Allowed substitution hint:   𝐽(𝑘)

Proof of Theorem seqf1olem1
StepHypRef Expression
1 seqf1olem.7 . 2 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
2 fvexd 6922 . 2 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V)
3 fvex 6920 . . . 4 (𝐹𝑥) ∈ V
4 ovex 7464 . . . 4 ((𝐹𝑥) − 1) ∈ V
53, 4ifex 4581 . . 3 if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V
65a1i 11 . 2 ((𝜑𝑥 ∈ (𝑀...𝑁)) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V)
7 iftrue 4537 . . . . . . . . 9 (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
87fveq2d 6911 . . . . . . . 8 (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
98eqeq2d 2746 . . . . . . 7 (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
109adantl 481 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
11 simprr 773 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 = (𝐹𝑘))
12 elfzelz 13561 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
1312zred 12720 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
1413ad2antlr 727 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ ℝ)
15 simprl 771 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 < 𝐾)
1614, 15gtned 11394 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐾𝑘)
17 seqf1olem.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18 f1of 6849 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
2019ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
21 fzssp1 13604 . . . . . . . . . . . . . . . 16 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
22 simplr 769 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...𝑁))
2321, 22sselid 3993 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
2420, 23ffvelcdmd 7105 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...(𝑁 + 1)))
25 seqf1o.4 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
26 elfzp1 13611 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2827ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2924, 28mpbid 232 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1)))
3029ord 864 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → (𝐹𝑘) = (𝑁 + 1)))
3117ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
32 f1ocnvfv 7298 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
3331, 23, 32syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
34 seqf1olem.8 . . . . . . . . . . . . . 14 𝐾 = (𝐹‘(𝑁 + 1))
3534eqeq1i 2740 . . . . . . . . . . . . 13 (𝐾 = 𝑘 ↔ (𝐹‘(𝑁 + 1)) = 𝑘)
3633, 35imbitrrdi 252 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
3730, 36syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
3837necon1ad 2955 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐾𝑘 → (𝐹𝑘) ∈ (𝑀...𝑁)))
3916, 38mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...𝑁))
4011, 39eqeltrd 2839 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 ∈ (𝑀...𝑁))
4111eqcomd 2741 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) = 𝑥)
42 f1ocnvfv 7298 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4331, 23, 42syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4441, 43mpd 15 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) = 𝑘)
4544, 15eqbrtrd 5170 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) < 𝐾)
46 iftrue 4537 . . . . . . . . . 10 ((𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4745, 46syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4847, 44eqtr2d 2776 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
4940, 48jca 511 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
5049expr 456 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
5110, 50sylbid 240 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
52 iffalse 4540 . . . . . . . . 9 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
5352fveq2d 6911 . . . . . . . 8 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
5453eqeq2d 2746 . . . . . . 7 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
5554adantl 481 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
56 simprr 773 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
57 f1ocnv 6861 . . . . . . . . . . . . . . . . . . 19 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
5817, 57syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
59 f1of1 6848 . . . . . . . . . . . . . . . . . 18 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
61 f1f 6805 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
63 peano2uz 12941 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
6425, 63syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + 1) ∈ (ℤ𝑀))
65 eluzfz2 13569 . . . . . . . . . . . . . . . . 17 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6664, 65syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6762, 66ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
6834, 67eqeltrid 2843 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
6968elfzelzd 13562 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℤ)
7069zred 12720 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
7170ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
7213ad2antlr 727 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
73 peano2re 11432 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
7472, 73syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
75 simprl 771 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
7671, 72, 75nltled 11409 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾𝑘)
7772ltp1d 12196 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
7871, 72, 74, 76, 77lelttrd 11417 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
7971, 78ltned 11395 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
8019ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
81 fzp1elp1 13614 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8281ad2antlr 727 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8380, 82ffvelcdmd 7105 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
84 elfzp1 13611 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8525, 84syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8685ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8783, 86mpbid 232 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
8887ord 864 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
8917ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
90 f1ocnvfv 7298 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9189, 82, 90syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9234eqeq1i 2740 . . . . . . . . . . . . 13 (𝐾 = (𝑘 + 1) ↔ (𝐹‘(𝑁 + 1)) = (𝑘 + 1))
9391, 92imbitrrdi 252 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
9488, 93syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
9594necon1ad 2955 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)))
9679, 95mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
9756, 96eqeltrd 2839 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
9856eqcomd 2741 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
99 f1ocnvfv 7298 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10089, 82, 99syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10198, 100mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹𝑥) = (𝑘 + 1))
102101breq1d 5158 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
103 lttr 11335 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10472, 74, 71, 103syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10577, 104mpand 695 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾𝑘 < 𝐾))
106102, 105sylbid 240 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾𝑘 < 𝐾))
10775, 106mtod 198 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (𝐹𝑥) < 𝐾)
108 iffalse 4540 . . . . . . . . . 10 (¬ (𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
109107, 108syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
110101oveq1d 7446 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) − 1) = ((𝑘 + 1) − 1))
11172recnd 11287 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
112 ax-1cn 11211 . . . . . . . . . 10 1 ∈ ℂ
113 pncan 11512 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
114111, 112, 113sylancl 586 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
115109, 110, 1143eqtrrd 2780 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
11697, 115jca 511 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
117116expr 456 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
11855, 117sylbid 240 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
11951, 118pm2.61dan 813 . . . 4 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
120119expimpd 453 . . 3 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12146eqeq2d 2746 . . . . . . 7 ((𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
122121adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
123 eluzel2 12881 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
12425, 123syl 17 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
125124ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀 ∈ ℤ)
126 eluzelz 12886 . . . . . . . . . . 11 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
12725, 126syl 17 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
128127ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑁 ∈ ℤ)
129 simprr 773 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 = (𝐹𝑥))
13062ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
131 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...𝑁))
13221, 131sselid 3993 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
133130, 132ffvelcdmd 7105 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
134129, 133eqeltrd 2839 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
135134elfzelzd 13562 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℤ)
136 elfzle1 13564 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝑘)
137134, 136syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀𝑘)
138135zred 12720 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℝ)
13970ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ∈ ℝ)
140127peano2zd 12723 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
141140zred 12720 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ ℝ)
142141ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑁 + 1) ∈ ℝ)
143 simprl 771 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) < 𝐾)
144129, 143eqbrtrd 5170 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < 𝐾)
145 elfzle2 13565 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
14668, 145syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≤ (𝑁 + 1))
147146ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ≤ (𝑁 + 1))
148138, 139, 142, 144, 147ltletrd 11419 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < (𝑁 + 1))
149 zleltp1 12666 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 < (𝑁 + 1)))
150135, 128, 149syl2anc 584 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘𝑁𝑘 < (𝑁 + 1)))
151148, 150mpbird 257 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘𝑁)
152125, 128, 135, 137, 151elfzd 13552 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...𝑁))
153144, 8syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
154129fveq2d 6911 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑘) = (𝐹‘(𝐹𝑥)))
15517ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
156 f1ocnvfv2 7297 . . . . . . . . . 10 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
157155, 132, 156syl2anc 584 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘(𝐹𝑥)) = 𝑥)
158153, 154, 1573eqtrrd 2780 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
159152, 158jca 511 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
160159expr 456 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = (𝐹𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
161122, 160sylbid 240 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
162108eqeq2d 2746 . . . . . . 7 (¬ (𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
163162adantl 481 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
164124ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℤ)
165127ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℤ)
166 simprr 773 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 = ((𝐹𝑥) − 1))
16762ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
168 simplr 769 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
16921, 168sselid 3993 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
170167, 169ffvelcdmd 7105 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
171170elfzelzd 13562 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℤ)
172 peano2zm 12658 . . . . . . . . . . 11 ((𝐹𝑥) ∈ ℤ → ((𝐹𝑥) − 1) ∈ ℤ)
173171, 172syl 17 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ∈ ℤ)
174166, 173eqeltrd 2839 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℤ)
175124zred 12720 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
176175ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℝ)
17770ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℝ)
178174zred 12720 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℝ)
179 elfzle1 13564 . . . . . . . . . . . 12 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝐾)
18068, 179syl 17 . . . . . . . . . . 11 (𝜑𝑀𝐾)
181180ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝐾)
182171zred 12720 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℝ)
183 simprl 771 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ (𝐹𝑥) < 𝐾)
184177, 182, 183nltled 11409 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ (𝐹𝑥))
185 elfzelz 13561 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
186185adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
187186zred 12720 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
188127zred 12720 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℝ)
189188adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
190141adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
191 elfzle2 13565 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
192191adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
193189ltp1d 12196 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
194187, 189, 190, 192, 193lelttrd 11417 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
195187, 194gtned 11394 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
196195adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
19760ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
19866ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
199 f1fveq 7282 . . . . . . . . . . . . . . . . . 18 ((𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
200197, 198, 169, 199syl12anc 837 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
201200necon3bid 2983 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
202196, 201mpbird 257 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
20334neeq1i 3003 . . . . . . . . . . . . . . 15 (𝐾 ≠ (𝐹𝑥) ↔ (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
204202, 203sylibr 234 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≠ (𝐹𝑥))
205204necomd 2994 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≠ 𝐾)
206177, 182, 184, 205leneltd 11413 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 < (𝐹𝑥))
20769ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℤ)
208 zltlem1 12668 . . . . . . . . . . . . 13 ((𝐾 ∈ ℤ ∧ (𝐹𝑥) ∈ ℤ) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
209207, 171, 208syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
210206, 209mpbid 232 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ ((𝐹𝑥) − 1))
211210, 166breqtrrd 5176 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾𝑘)
212176, 177, 178, 181, 211letrd 11416 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝑘)
213 elfzle2 13565 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ≤ (𝑁 + 1))
214170, 213syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≤ (𝑁 + 1))
215188ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℝ)
216 1re 11259 . . . . . . . . . . . . 13 1 ∈ ℝ
217 lesubadd 11733 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
218216, 217mp3an2 1448 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
219182, 215, 218syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
220214, 219mpbird 257 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ≤ 𝑁)
221166, 220eqbrtrd 5170 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘𝑁)
222164, 165, 174, 212, 221elfzd 13552 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
223177, 178, 211lensymd 11410 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ 𝑘 < 𝐾)
224223, 53syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
225166oveq1d 7446 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (((𝐹𝑥) − 1) + 1))
226171zcnd 12721 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℂ)
227 npcan 11515 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
228226, 112, 227sylancl 586 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
229225, 228eqtrd 2775 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (𝐹𝑥))
230229fveq2d 6911 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐹𝑥)))
23117ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
232231, 169, 156syl2anc 584 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
233224, 230, 2323eqtrrd 2780 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
234222, 233jca 511 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
235234expr 456 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = ((𝐹𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
236163, 235sylbid 240 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
237161, 236pm2.61dan 813 . . . 4 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
238237expimpd 453 . . 3 (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
239120, 238impbid 212 . 2 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
2401, 2, 6, 239f1od 7685 1 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wne 2938  Vcvv 3478  wss 3963  ifcif 4531   class class class wbr 5148  cmpt 5231  ccnv 5688  wf 6559  1-1wf1 6560  1-1-ontowf1o 6562  cfv 6563  (class class class)co 7431  cc 11151  cr 11152  1c1 11154   + caddc 11156   < clt 11293  cle 11294  cmin 11490  cz 12611  cuz 12876  ...cfz 13544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545
This theorem is referenced by:  seqf1olem2  14080
  Copyright terms: Public domain W3C validator