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

Theorem seqf1olem1 13259
Description: Lemma for seqf1o 13261. (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 6553 . 2 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V)
3 fvex 6551 . . . 4 (𝐹𝑥) ∈ V
4 ovex 7048 . . . 4 ((𝐹𝑥) − 1) ∈ V
53, 4ifex 4429 . . 3 if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V
65a1i 11 . 2 ((𝜑𝑥 ∈ (𝑀...𝑁)) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V)
7 iftrue 4387 . . . . . . . . 9 (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
87fveq2d 6542 . . . . . . . 8 (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
98eqeq2d 2805 . . . . . . 7 (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
109adantl 482 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
11 simprr 769 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 = (𝐹𝑘))
12 elfzelz 12758 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
1312zred 11936 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
1413ad2antlr 723 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ ℝ)
15 simprl 767 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 < 𝐾)
1614, 15gtned 10622 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐾𝑘)
17 seqf1olem.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18 f1of 6483 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
2019ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
21 fzssp1 12800 . . . . . . . . . . . . . . . 16 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
22 simplr 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...𝑁))
2321, 22sseldi 3887 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
2420, 23ffvelrnd 6717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...(𝑁 + 1)))
25 seqf1o.4 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
26 elfzp1 12807 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2827ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2924, 28mpbid 233 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1)))
3029ord 859 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → (𝐹𝑘) = (𝑁 + 1)))
3117ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
32 f1ocnvfv 6900 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
3331, 23, 32syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
34 seqf1olem.8 . . . . . . . . . . . . . 14 𝐾 = (𝐹‘(𝑁 + 1))
3534eqeq1i 2800 . . . . . . . . . . . . 13 (𝐾 = 𝑘 ↔ (𝐹‘(𝑁 + 1)) = 𝑘)
3633, 35syl6ibr 253 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
3730, 36syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
3837necon1ad 3001 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐾𝑘 → (𝐹𝑘) ∈ (𝑀...𝑁)))
3916, 38mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...𝑁))
4011, 39eqeltrd 2883 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 ∈ (𝑀...𝑁))
4111eqcomd 2801 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) = 𝑥)
42 f1ocnvfv 6900 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4331, 23, 42syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4441, 43mpd 15 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) = 𝑘)
4544, 15eqbrtrd 4984 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) < 𝐾)
46 iftrue 4387 . . . . . . . . . 10 ((𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4745, 46syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4847, 44eqtr2d 2832 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
4940, 48jca 512 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
5049expr 457 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
5110, 50sylbid 241 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
52 iffalse 4390 . . . . . . . . 9 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
5352fveq2d 6542 . . . . . . . 8 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
5453eqeq2d 2805 . . . . . . 7 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
5554adantl 482 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
56 simprr 769 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
57 f1ocnv 6495 . . . . . . . . . . . . . . . . . . 19 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
5817, 57syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
59 f1of1 6482 . . . . . . . . . . . . . . . . . 18 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
61 f1f 6443 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
63 peano2uz 12150 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
6425, 63syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + 1) ∈ (ℤ𝑀))
65 eluzfz2 12765 . . . . . . . . . . . . . . . . 17 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6664, 65syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6762, 66ffvelrnd 6717 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
6834, 67syl5eqel 2887 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
69 elfzelz 12758 . . . . . . . . . . . . . 14 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
7068, 69syl 17 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℤ)
7170zred 11936 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
7271ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
7313ad2antlr 723 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
74 peano2re 10660 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
7573, 74syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
76 simprl 767 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
7772, 73, 76nltled 10637 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾𝑘)
7873ltp1d 11418 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
7972, 73, 75, 77, 78lelttrd 10645 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
8072, 79ltned 10623 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
8119ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
82 fzp1elp1 12810 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8382ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8481, 83ffvelrnd 6717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
85 elfzp1 12807 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8625, 85syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8786ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8884, 87mpbid 233 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
8988ord 859 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
9017ad2antrr 722 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
91 f1ocnvfv 6900 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9290, 83, 91syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9334eqeq1i 2800 . . . . . . . . . . . . 13 (𝐾 = (𝑘 + 1) ↔ (𝐹‘(𝑁 + 1)) = (𝑘 + 1))
9492, 93syl6ibr 253 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
9589, 94syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
9695necon1ad 3001 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)))
9780, 96mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
9856, 97eqeltrd 2883 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
9956eqcomd 2801 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
100 f1ocnvfv 6900 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10190, 83, 100syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10299, 101mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹𝑥) = (𝑘 + 1))
103102breq1d 4972 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
104 lttr 10564 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10573, 75, 72, 104syl3anc 1364 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10678, 105mpand 691 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾𝑘 < 𝐾))
107103, 106sylbid 241 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾𝑘 < 𝐾))
10876, 107mtod 199 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (𝐹𝑥) < 𝐾)
109 iffalse 4390 . . . . . . . . . 10 (¬ (𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
110108, 109syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
111102oveq1d 7031 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) − 1) = ((𝑘 + 1) − 1))
11273recnd 10515 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
113 ax-1cn 10441 . . . . . . . . . 10 1 ∈ ℂ
114 pncan 10739 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
115112, 113, 114sylancl 586 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
116110, 111, 1153eqtrrd 2836 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
11798, 116jca 512 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
118117expr 457 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
11955, 118sylbid 241 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12051, 119pm2.61dan 809 . . . 4 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
121120expimpd 454 . . 3 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12246eqeq2d 2805 . . . . . . 7 ((𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
123122adantl 482 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
124 simprr 769 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 = (𝐹𝑥))
12562ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
126 simplr 765 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...𝑁))
12721, 126sseldi 3887 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
128125, 127ffvelrnd 6717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
129124, 128eqeltrd 2883 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
130 elfzle1 12760 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝑘)
131129, 130syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀𝑘)
132 elfzelz 12758 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ)
133129, 132syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℤ)
134133zred 11936 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℝ)
13571ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ∈ ℝ)
136 eluzelz 12103 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
13725, 136syl 17 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
138137peano2zd 11939 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
139138zred 11936 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ ℝ)
140139ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑁 + 1) ∈ ℝ)
141 simprl 767 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) < 𝐾)
142124, 141eqbrtrd 4984 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < 𝐾)
143 elfzle2 12761 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
14468, 143syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≤ (𝑁 + 1))
145144ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ≤ (𝑁 + 1))
146134, 135, 140, 142, 145ltletrd 10647 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < (𝑁 + 1))
147137ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑁 ∈ ℤ)
148 zleltp1 11882 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 < (𝑁 + 1)))
149133, 147, 148syl2anc 584 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘𝑁𝑘 < (𝑁 + 1)))
150146, 149mpbird 258 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘𝑁)
151 eluzel2 12098 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
15225, 151syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
153152ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀 ∈ ℤ)
154 elfz 12748 . . . . . . . . . 10 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
155133, 153, 147, 154syl3anc 1364 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
156131, 150, 155mpbir2and 709 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...𝑁))
157142, 8syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
158124fveq2d 6542 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑘) = (𝐹‘(𝐹𝑥)))
15917ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
160 f1ocnvfv2 6899 . . . . . . . . . 10 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
161159, 127, 160syl2anc 584 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘(𝐹𝑥)) = 𝑥)
162157, 158, 1613eqtrrd 2836 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
163156, 162jca 512 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
164163expr 457 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = (𝐹𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
165123, 164sylbid 241 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
166109eqeq2d 2805 . . . . . . 7 (¬ (𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
167166adantl 482 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
168152zred 11936 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
169168ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℝ)
17071ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℝ)
171 simprr 769 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 = ((𝐹𝑥) − 1))
17262ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
173 simplr 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
17421, 173sseldi 3887 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
175172, 174ffvelrnd 6717 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
176 elfzelz 12758 . . . . . . . . . . . . . 14 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ∈ ℤ)
177175, 176syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℤ)
178 peano2zm 11874 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ ℤ → ((𝐹𝑥) − 1) ∈ ℤ)
179177, 178syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ∈ ℤ)
180171, 179eqeltrd 2883 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℤ)
181180zred 11936 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℝ)
182 elfzle1 12760 . . . . . . . . . . . 12 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝐾)
18368, 182syl 17 . . . . . . . . . . 11 (𝜑𝑀𝐾)
184183ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝐾)
185177zred 11936 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℝ)
186 simprl 767 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ (𝐹𝑥) < 𝐾)
187170, 185, 186nltled 10637 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ (𝐹𝑥))
188 elfzelz 12758 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
189188adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
190189zred 11936 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
191137zred 11936 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℝ)
192191adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
193139adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
194 elfzle2 12761 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
195194adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
196192ltp1d 11418 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
197190, 192, 193, 195, 196lelttrd 10645 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
198190, 197gtned 10622 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
199198adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
20060ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
20166ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
202 f1fveq 6885 . . . . . . . . . . . . . . . . . 18 ((𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
203200, 201, 174, 202syl12anc 833 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
204203necon3bid 3028 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
205199, 204mpbird 258 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
20634neeq1i 3048 . . . . . . . . . . . . . . 15 (𝐾 ≠ (𝐹𝑥) ↔ (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
207205, 206sylibr 235 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≠ (𝐹𝑥))
208207necomd 3039 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≠ 𝐾)
209170, 185, 187, 208leneltd 10641 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 < (𝐹𝑥))
21070ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℤ)
211 zltlem1 11884 . . . . . . . . . . . . 13 ((𝐾 ∈ ℤ ∧ (𝐹𝑥) ∈ ℤ) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
212210, 177, 211syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
213209, 212mpbid 233 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ ((𝐹𝑥) − 1))
214213, 171breqtrrd 4990 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾𝑘)
215169, 170, 181, 184, 214letrd 10644 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝑘)
216 elfzle2 12761 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ≤ (𝑁 + 1))
217175, 216syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≤ (𝑁 + 1))
218191ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℝ)
219 1re 10487 . . . . . . . . . . . . 13 1 ∈ ℝ
220 lesubadd 10960 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
221219, 220mp3an2 1441 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
222185, 218, 221syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
223217, 222mpbird 258 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ≤ 𝑁)
224171, 223eqbrtrd 4984 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘𝑁)
225152ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℤ)
226137ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℤ)
227180, 225, 226, 154syl3anc 1364 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
228215, 224, 227mpbir2and 709 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
229170, 181, 214lensymd 10638 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ 𝑘 < 𝐾)
230229, 53syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
231171oveq1d 7031 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (((𝐹𝑥) − 1) + 1))
232177zcnd 11937 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℂ)
233 npcan 10743 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
234232, 113, 233sylancl 586 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
235231, 234eqtrd 2831 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (𝐹𝑥))
236235fveq2d 6542 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐹𝑥)))
23717ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
238237, 174, 160syl2anc 584 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
239230, 236, 2383eqtrrd 2836 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
240228, 239jca 512 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
241240expr 457 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = ((𝐹𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
242167, 241sylbid 241 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
243165, 242pm2.61dan 809 . . . 4 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
244243expimpd 454 . . 3 (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
245121, 244impbid 213 . 2 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
2461, 2, 6, 245f1od 7255 1 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3a 1080   = wceq 1522  wcel 2081  wne 2984  Vcvv 3437  wss 3859  ifcif 4381   class class class wbr 4962  cmpt 5041  ccnv 5442  wf 6221  1-1wf1 6222  1-1-ontowf1o 6224  cfv 6225  (class class class)co 7016  cc 10381  cr 10382  1c1 10384   + caddc 10386   < clt 10521  cle 10522  cmin 10717  cz 11829  cuz 12093  ...cfz 12742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-cnex 10439  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459  ax-pre-mulgt0 10460
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-tp 4477  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-mpt 5042  df-tr 5064  df-id 5348  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-pred 6023  df-ord 6069  df-on 6070  df-lim 6071  df-suc 6072  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-riota 6977  df-ov 7019  df-oprab 7020  df-mpo 7021  df-om 7437  df-1st 7545  df-2nd 7546  df-wrecs 7798  df-recs 7860  df-rdg 7898  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527  df-sub 10719  df-neg 10720  df-nn 11487  df-n0 11746  df-z 11830  df-uz 12094  df-fz 12743
This theorem is referenced by:  seqf1olem2  13260
  Copyright terms: Public domain W3C validator