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

Theorem seqf1olem1 13047
Description: Lemma for seqf1o 13049. (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 6390 . 2 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V)
3 fvex 6388 . . . 4 (𝐹𝑥) ∈ V
4 ovex 6874 . . . 4 ((𝐹𝑥) − 1) ∈ V
53, 4ifex 4291 . . 3 if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V
65a1i 11 . 2 ((𝜑𝑥 ∈ (𝑀...𝑁)) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V)
7 iftrue 4249 . . . . . . . . 9 (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
87fveq2d 6379 . . . . . . . 8 (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
98eqeq2d 2775 . . . . . . 7 (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
109adantl 473 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
11 simprr 789 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 = (𝐹𝑘))
12 elfzelz 12549 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
1312zred 11729 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
1413ad2antlr 718 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ ℝ)
15 simprl 787 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 < 𝐾)
1614, 15gtned 10426 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐾𝑘)
17 seqf1olem.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18 f1of 6320 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
2019ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
21 fzssp1 12591 . . . . . . . . . . . . . . . 16 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
22 simplr 785 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...𝑁))
2321, 22sseldi 3759 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
2420, 23ffvelrnd 6550 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...(𝑁 + 1)))
25 seqf1o.4 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
26 elfzp1 12598 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2827ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2924, 28mpbid 223 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1)))
3029ord 890 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → (𝐹𝑘) = (𝑁 + 1)))
3117ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
32 f1ocnvfv 6726 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
3331, 23, 32syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
34 seqf1olem.8 . . . . . . . . . . . . . 14 𝐾 = (𝐹‘(𝑁 + 1))
3534eqeq1i 2770 . . . . . . . . . . . . 13 (𝐾 = 𝑘 ↔ (𝐹‘(𝑁 + 1)) = 𝑘)
3633, 35syl6ibr 243 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
3730, 36syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
3837necon1ad 2954 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐾𝑘 → (𝐹𝑘) ∈ (𝑀...𝑁)))
3916, 38mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...𝑁))
4011, 39eqeltrd 2844 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 ∈ (𝑀...𝑁))
4111eqcomd 2771 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) = 𝑥)
42 f1ocnvfv 6726 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4331, 23, 42syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4441, 43mpd 15 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) = 𝑘)
4544, 15eqbrtrd 4831 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) < 𝐾)
46 iftrue 4249 . . . . . . . . . 10 ((𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4745, 46syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4847, 44eqtr2d 2800 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
4940, 48jca 507 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
5049expr 448 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
5110, 50sylbid 231 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
52 iffalse 4252 . . . . . . . . 9 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
5352fveq2d 6379 . . . . . . . 8 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
5453eqeq2d 2775 . . . . . . 7 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
5554adantl 473 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
56 simprr 789 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
57 f1ocnv 6332 . . . . . . . . . . . . . . . . . . 19 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
5817, 57syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
59 f1of1 6319 . . . . . . . . . . . . . . . . . 18 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
61 f1f 6283 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
63 peano2uz 11941 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
6425, 63syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + 1) ∈ (ℤ𝑀))
65 eluzfz2 12556 . . . . . . . . . . . . . . . . 17 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6664, 65syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6762, 66ffvelrnd 6550 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
6834, 67syl5eqel 2848 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
69 elfzelz 12549 . . . . . . . . . . . . . 14 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
7068, 69syl 17 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℤ)
7170zred 11729 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
7271ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
7313ad2antlr 718 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
74 peano2re 10463 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
7573, 74syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
76 simprl 787 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
7772, 73lenltd 10437 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾𝑘 ↔ ¬ 𝑘 < 𝐾))
7876, 77mpbird 248 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾𝑘)
7973ltp1d 11208 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
8072, 73, 75, 78, 79lelttrd 10449 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
8172, 80ltned 10427 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
8219ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
83 fzp1elp1 12601 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8483ad2antlr 718 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8582, 84ffvelrnd 6550 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
86 elfzp1 12598 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8725, 86syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8887ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8985, 88mpbid 223 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
9089ord 890 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
9117ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
92 f1ocnvfv 6726 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9391, 84, 92syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9434eqeq1i 2770 . . . . . . . . . . . . 13 (𝐾 = (𝑘 + 1) ↔ (𝐹‘(𝑁 + 1)) = (𝑘 + 1))
9593, 94syl6ibr 243 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
9690, 95syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
9796necon1ad 2954 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)))
9881, 97mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
9956, 98eqeltrd 2844 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
10056eqcomd 2771 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
101 f1ocnvfv 6726 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10291, 84, 101syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
103100, 102mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹𝑥) = (𝑘 + 1))
104103breq1d 4819 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
105 lttr 10368 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10673, 75, 72, 105syl3anc 1490 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10779, 106mpand 686 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾𝑘 < 𝐾))
108104, 107sylbid 231 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾𝑘 < 𝐾))
10976, 108mtod 189 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (𝐹𝑥) < 𝐾)
110 iffalse 4252 . . . . . . . . . 10 (¬ (𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
111109, 110syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
112103oveq1d 6857 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) − 1) = ((𝑘 + 1) − 1))
11373recnd 10322 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
114 ax-1cn 10247 . . . . . . . . . 10 1 ∈ ℂ
115 pncan 10541 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
116113, 114, 115sylancl 580 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
117111, 112, 1163eqtrrd 2804 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
11899, 117jca 507 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
119118expr 448 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12055, 119sylbid 231 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12151, 120pm2.61dan 847 . . . 4 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
122121expimpd 445 . . 3 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12346eqeq2d 2775 . . . . . . 7 ((𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
124123adantl 473 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
125 simprr 789 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 = (𝐹𝑥))
12662ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
127 simplr 785 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...𝑁))
12821, 127sseldi 3759 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
129126, 128ffvelrnd 6550 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
130125, 129eqeltrd 2844 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
131 elfzle1 12551 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝑘)
132130, 131syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀𝑘)
133 elfzelz 12549 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ)
134130, 133syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℤ)
135134zred 11729 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℝ)
13671ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ∈ ℝ)
137 eluzelz 11896 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
13825, 137syl 17 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
139138peano2zd 11732 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
140139zred 11729 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ ℝ)
141140ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑁 + 1) ∈ ℝ)
142 simprl 787 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) < 𝐾)
143125, 142eqbrtrd 4831 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < 𝐾)
144 elfzle2 12552 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
14568, 144syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≤ (𝑁 + 1))
146145ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ≤ (𝑁 + 1))
147135, 136, 141, 143, 146ltletrd 10451 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < (𝑁 + 1))
148138ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑁 ∈ ℤ)
149 zleltp1 11675 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 < (𝑁 + 1)))
150134, 148, 149syl2anc 579 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘𝑁𝑘 < (𝑁 + 1)))
151147, 150mpbird 248 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘𝑁)
152 eluzel2 11891 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
15325, 152syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
154153ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀 ∈ ℤ)
155 elfz 12539 . . . . . . . . . 10 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
156134, 154, 148, 155syl3anc 1490 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
157132, 151, 156mpbir2and 704 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...𝑁))
158143, 8syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
159125fveq2d 6379 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑘) = (𝐹‘(𝐹𝑥)))
16017ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
161 f1ocnvfv2 6725 . . . . . . . . . 10 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
162160, 128, 161syl2anc 579 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘(𝐹𝑥)) = 𝑥)
163158, 159, 1623eqtrrd 2804 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
164157, 163jca 507 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
165164expr 448 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = (𝐹𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
166124, 165sylbid 231 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
167110eqeq2d 2775 . . . . . . 7 (¬ (𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
168167adantl 473 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
169153zred 11729 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
170169ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℝ)
17171ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℝ)
172 simprr 789 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 = ((𝐹𝑥) − 1))
17362ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
174 simplr 785 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
17521, 174sseldi 3759 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
176173, 175ffvelrnd 6550 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
177 elfzelz 12549 . . . . . . . . . . . . . 14 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ∈ ℤ)
178176, 177syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℤ)
179 peano2zm 11667 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ ℤ → ((𝐹𝑥) − 1) ∈ ℤ)
180178, 179syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ∈ ℤ)
181172, 180eqeltrd 2844 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℤ)
182181zred 11729 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℝ)
183 elfzle1 12551 . . . . . . . . . . . 12 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝐾)
18468, 183syl 17 . . . . . . . . . . 11 (𝜑𝑀𝐾)
185184ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝐾)
186 simprl 787 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ (𝐹𝑥) < 𝐾)
187178zred 11729 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℝ)
188171, 187lenltd 10437 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 ≤ (𝐹𝑥) ↔ ¬ (𝐹𝑥) < 𝐾))
189186, 188mpbird 248 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ (𝐹𝑥))
190 elfzelz 12549 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
191190adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
192191zred 11729 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
193138zred 11729 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℝ)
194193adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
195140adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
196 elfzle2 12552 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
197196adantl 473 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
198194ltp1d 11208 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
199192, 194, 195, 197, 198lelttrd 10449 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
200192, 199gtned 10426 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
201200adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
20260ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
20366ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
204 f1fveq 6711 . . . . . . . . . . . . . . . . . 18 ((𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
205202, 203, 175, 204syl12anc 865 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
206205necon3bid 2981 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
207201, 206mpbird 248 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
20834neeq1i 3001 . . . . . . . . . . . . . . 15 (𝐾 ≠ (𝐹𝑥) ↔ (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
209207, 208sylibr 225 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≠ (𝐹𝑥))
210209necomd 2992 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≠ 𝐾)
211171, 187ltlend 10436 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 < (𝐹𝑥) ↔ (𝐾 ≤ (𝐹𝑥) ∧ (𝐹𝑥) ≠ 𝐾)))
212189, 210, 211mpbir2and 704 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 < (𝐹𝑥))
21370ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℤ)
214 zltlem1 11677 . . . . . . . . . . . . 13 ((𝐾 ∈ ℤ ∧ (𝐹𝑥) ∈ ℤ) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
215213, 178, 214syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
216212, 215mpbid 223 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ ((𝐹𝑥) − 1))
217216, 172breqtrrd 4837 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾𝑘)
218170, 171, 182, 185, 217letrd 10448 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝑘)
219 elfzle2 12552 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ≤ (𝑁 + 1))
220176, 219syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≤ (𝑁 + 1))
221193ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℝ)
222 1re 10293 . . . . . . . . . . . . 13 1 ∈ ℝ
223 lesubadd 10754 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
224222, 223mp3an2 1573 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
225187, 221, 224syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
226220, 225mpbird 248 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ≤ 𝑁)
227172, 226eqbrtrd 4831 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘𝑁)
228153ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℤ)
229138ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℤ)
230181, 228, 229, 155syl3anc 1490 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
231218, 227, 230mpbir2and 704 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
232171, 182lenltd 10437 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾𝑘 ↔ ¬ 𝑘 < 𝐾))
233217, 232mpbid 223 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ 𝑘 < 𝐾)
234233, 53syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
235172oveq1d 6857 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (((𝐹𝑥) − 1) + 1))
236178zcnd 11730 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℂ)
237 npcan 10544 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
238236, 114, 237sylancl 580 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
239235, 238eqtrd 2799 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (𝐹𝑥))
240239fveq2d 6379 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐹𝑥)))
24117ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
242241, 175, 161syl2anc 579 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
243234, 240, 2423eqtrrd 2804 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
244231, 243jca 507 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
245244expr 448 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = ((𝐹𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
246168, 245sylbid 231 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
247166, 246pm2.61dan 847 . . . 4 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
248247expimpd 445 . . 3 (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
249122, 248impbid 203 . 2 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
2501, 2, 6, 249f1od 7083 1 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wne 2937  Vcvv 3350  wss 3732  ifcif 4243   class class class wbr 4809  cmpt 4888  ccnv 5276  wf 6064  1-1wf1 6065  1-1-ontowf1o 6067  cfv 6068  (class class class)co 6842  cc 10187  cr 10188  1c1 10190   + caddc 10192   < clt 10328  cle 10329  cmin 10520  cz 11624  cuz 11886  ...cfz 12533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-er 7947  df-en 8161  df-dom 8162  df-sdom 8163  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-nn 11275  df-n0 11539  df-z 11625  df-uz 11887  df-fz 12534
This theorem is referenced by:  seqf1olem2  13048
  Copyright terms: Public domain W3C validator