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

Theorem seqf1olem1 13408
 Description: Lemma for seqf1o 13410. (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 6661 . 2 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ V)
3 fvex 6659 . . . 4 (𝐹𝑥) ∈ V
4 ovex 7169 . . . 4 ((𝐹𝑥) − 1) ∈ V
53, 4ifex 4473 . . 3 if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V
65a1i 11 . 2 ((𝜑𝑥 ∈ (𝑀...𝑁)) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ∈ V)
7 iftrue 4431 . . . . . . . . 9 (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
87fveq2d 6650 . . . . . . . 8 (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
98eqeq2d 2809 . . . . . . 7 (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
109adantl 485 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹𝑘)))
11 simprr 772 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 = (𝐹𝑘))
12 elfzelz 12905 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
1312zred 12078 . . . . . . . . . . . 12 (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
1413ad2antlr 726 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ ℝ)
15 simprl 770 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 < 𝐾)
1614, 15gtned 10767 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐾𝑘)
17 seqf1olem.5 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18 f1of 6591 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
1917, 18syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
2019ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
21 fzssp1 12948 . . . . . . . . . . . . . . . 16 (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
22 simplr 768 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...𝑁))
2321, 22sseldi 3913 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
2420, 23ffvelrnd 6830 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...(𝑁 + 1)))
25 seqf1o.4 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝑀))
26 elfzp1 12955 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2827ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1))))
2924, 28mpbid 235 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) ∈ (𝑀...𝑁) ∨ (𝐹𝑘) = (𝑁 + 1)))
3029ord 861 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → (𝐹𝑘) = (𝑁 + 1)))
3117ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
32 f1ocnvfv 7014 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
3331, 23, 32syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = 𝑘))
34 seqf1olem.8 . . . . . . . . . . . . . 14 𝐾 = (𝐹‘(𝑁 + 1))
3534eqeq1i 2803 . . . . . . . . . . . . 13 (𝐾 = 𝑘 ↔ (𝐹‘(𝑁 + 1)) = 𝑘)
3633, 35syl6ibr 255 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
3730, 36syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (¬ (𝐹𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
3837necon1ad 3004 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐾𝑘 → (𝐹𝑘) ∈ (𝑀...𝑁)))
3916, 38mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) ∈ (𝑀...𝑁))
4011, 39eqeltrd 2890 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑥 ∈ (𝑀...𝑁))
4111eqcomd 2804 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑘) = 𝑥)
42 f1ocnvfv 7014 . . . . . . . . . . . . 13 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4331, 23, 42syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → ((𝐹𝑘) = 𝑥 → (𝐹𝑥) = 𝑘))
4441, 43mpd 15 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) = 𝑘)
4544, 15eqbrtrd 5053 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝐹𝑥) < 𝐾)
46 iftrue 4431 . . . . . . . . . 10 ((𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4745, 46syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = (𝐹𝑥))
4847, 44eqtr2d 2834 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
4940, 48jca 515 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾𝑥 = (𝐹𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
5049expr 460 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
5110, 50sylbid 243 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
52 iffalse 4434 . . . . . . . . 9 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
5352fveq2d 6650 . . . . . . . 8 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
5453eqeq2d 2809 . . . . . . 7 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
5554adantl 485 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
56 simprr 772 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
57 f1ocnv 6603 . . . . . . . . . . . . . . . . . . 19 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
5817, 57syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
59 f1of1 6590 . . . . . . . . . . . . . . . . . 18 (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
6058, 59syl 17 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
61 f1f 6550 . . . . . . . . . . . . . . . . 17 (𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6260, 61syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
63 peano2uz 12292 . . . . . . . . . . . . . . . . . 18 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ𝑀))
6425, 63syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑁 + 1) ∈ (ℤ𝑀))
65 eluzfz2 12913 . . . . . . . . . . . . . . . . 17 ((𝑁 + 1) ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6664, 65syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
6762, 66ffvelrnd 6830 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
6834, 67eqeltrid 2894 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ (𝑀...(𝑁 + 1)))
69 elfzelz 12905 . . . . . . . . . . . . . 14 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
7068, 69syl 17 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℤ)
7170zred 12078 . . . . . . . . . . . 12 (𝜑𝐾 ∈ ℝ)
7271ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
7313ad2antlr 726 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
74 peano2re 10805 . . . . . . . . . . . . 13 (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
7573, 74syl 17 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
76 simprl 770 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
7772, 73, 76nltled 10782 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾𝑘)
7873ltp1d 11562 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
7972, 73, 75, 77, 78lelttrd 10790 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
8072, 79ltned 10768 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
8119ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
82 fzp1elp1 12958 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8382ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
8481, 83ffvelrnd 6830 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
85 elfzp1 12955 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8625, 85syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8786ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
8884, 87mpbid 235 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
8988ord 861 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
9017ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
91 f1ocnvfv 7014 . . . . . . . . . . . . . 14 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9290, 83, 91syl2anc 587 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
9334eqeq1i 2803 . . . . . . . . . . . . 13 (𝐾 = (𝑘 + 1) ↔ (𝐹‘(𝑁 + 1)) = (𝑘 + 1))
9492, 93syl6ibr 255 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
9589, 94syld 47 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
9695necon1ad 3004 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)))
9780, 96mpd 15 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
9856, 97eqeltrd 2890 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
9956eqcomd 2804 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
100 f1ocnvfv 7014 . . . . . . . . . . . . . . 15 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10190, 83, 100syl2anc 587 . . . . . . . . . . . . . 14 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (𝐹𝑥) = (𝑘 + 1)))
10299, 101mpd 15 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹𝑥) = (𝑘 + 1))
103102breq1d 5041 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
104 lttr 10709 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10573, 75, 72, 104syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
10678, 105mpand 694 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾𝑘 < 𝐾))
107103, 106sylbid 243 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) < 𝐾𝑘 < 𝐾))
10876, 107mtod 201 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (𝐹𝑥) < 𝐾)
109 iffalse 4434 . . . . . . . . . 10 (¬ (𝐹𝑥) < 𝐾 → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
110108, 109syl 17 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) = ((𝐹𝑥) − 1))
111102oveq1d 7151 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹𝑥) − 1) = ((𝑘 + 1) − 1))
11273recnd 10661 . . . . . . . . . 10 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
113 ax-1cn 10587 . . . . . . . . . 10 1 ∈ ℂ
114 pncan 10884 . . . . . . . . . 10 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
115112, 113, 114sylancl 589 . . . . . . . . 9 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
116110, 111, 1153eqtrrd 2838 . . . . . . . 8 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))
11798, 116jca 515 . . . . . . 7 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))))
118117expr 460 . . . . . 6 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
11955, 118sylbid 243 . . . . 5 (((𝜑𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12051, 119pm2.61dan 812 . . . 4 ((𝜑𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
121120expimpd 457 . . 3 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
12246eqeq2d 2809 . . . . . . 7 ((𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
123122adantl 485 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = (𝐹𝑥)))
124 simprr 772 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 = (𝐹𝑥))
12562ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
126 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...𝑁))
12721, 126sseldi 3913 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
128125, 127ffvelrnd 6830 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
129124, 128eqeltrd 2890 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
130 elfzle1 12908 . . . . . . . . . 10 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝑘)
131129, 130syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀𝑘)
132 elfzelz 12905 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ)
133129, 132syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℤ)
134133zred 12078 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ ℝ)
13571ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ∈ ℝ)
136 eluzelz 12244 . . . . . . . . . . . . . . 15 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
13725, 136syl 17 . . . . . . . . . . . . . 14 (𝜑𝑁 ∈ ℤ)
138137peano2zd 12081 . . . . . . . . . . . . 13 (𝜑 → (𝑁 + 1) ∈ ℤ)
139138zred 12078 . . . . . . . . . . . 12 (𝜑 → (𝑁 + 1) ∈ ℝ)
140139ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑁 + 1) ∈ ℝ)
141 simprl 770 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑥) < 𝐾)
142124, 141eqbrtrd 5053 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < 𝐾)
143 elfzle2 12909 . . . . . . . . . . . . 13 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
14468, 143syl 17 . . . . . . . . . . . 12 (𝜑𝐾 ≤ (𝑁 + 1))
145144ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐾 ≤ (𝑁 + 1))
146134, 135, 140, 142, 145ltletrd 10792 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 < (𝑁 + 1))
147137ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑁 ∈ ℤ)
148 zleltp1 12024 . . . . . . . . . . 11 ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘𝑁𝑘 < (𝑁 + 1)))
149133, 147, 148syl2anc 587 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘𝑁𝑘 < (𝑁 + 1)))
150146, 149mpbird 260 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘𝑁)
151 eluzel2 12239 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
15225, 151syl 17 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℤ)
153152ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑀 ∈ ℤ)
154 elfz 12894 . . . . . . . . . 10 ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
155133, 153, 147, 154syl3anc 1368 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
156131, 150, 155mpbir2and 712 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑘 ∈ (𝑀...𝑁))
157142, 8syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹𝑘))
158124fveq2d 6650 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹𝑘) = (𝐹‘(𝐹𝑥)))
15917ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
160 f1ocnvfv2 7013 . . . . . . . . . 10 ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
161159, 127, 160syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝐹‘(𝐹𝑥)) = 𝑥)
162157, 158, 1613eqtrrd 2838 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
163156, 162jca 515 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ((𝐹𝑥) < 𝐾𝑘 = (𝐹𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
164163expr 460 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = (𝐹𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
165123, 164sylbid 243 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
166109eqeq2d 2809 . . . . . . 7 (¬ (𝐹𝑥) < 𝐾 → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
167166adantl 485 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) ↔ 𝑘 = ((𝐹𝑥) − 1)))
168152zred 12078 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
169168ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℝ)
17071ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℝ)
171 simprr 772 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 = ((𝐹𝑥) − 1))
17262ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
173 simplr 768 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
17421, 173sseldi 3913 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
175172, 174ffvelrnd 6830 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ (𝑀...(𝑁 + 1)))
176 elfzelz 12905 . . . . . . . . . . . . . 14 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ∈ ℤ)
177175, 176syl 17 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℤ)
178 peano2zm 12016 . . . . . . . . . . . . 13 ((𝐹𝑥) ∈ ℤ → ((𝐹𝑥) − 1) ∈ ℤ)
179177, 178syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ∈ ℤ)
180171, 179eqeltrd 2890 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℤ)
181180zred 12078 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ ℝ)
182 elfzle1 12908 . . . . . . . . . . . 12 (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀𝐾)
18368, 182syl 17 . . . . . . . . . . 11 (𝜑𝑀𝐾)
184183ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝐾)
185177zred 12078 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℝ)
186 simprl 770 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ (𝐹𝑥) < 𝐾)
187170, 185, 186nltled 10782 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ (𝐹𝑥))
188 elfzelz 12905 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
189188adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
190189zred 12078 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
191137zred 12078 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑁 ∈ ℝ)
192191adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
193139adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
194 elfzle2 12909 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑀...𝑁) → 𝑥𝑁)
195194adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥𝑁)
196192ltp1d 11562 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
197190, 192, 193, 195, 196lelttrd 10790 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
198190, 197gtned 10767 . . . . . . . . . . . . . . . . 17 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
199198adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
20060ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
20166ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
202 f1fveq 6999 . . . . . . . . . . . . . . . . . 18 ((𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
203200, 201, 174, 202syl12anc 835 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) = (𝐹𝑥) ↔ (𝑁 + 1) = 𝑥))
204203necon3bid 3031 . . . . . . . . . . . . . . . 16 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
205199, 204mpbird 260 . . . . . . . . . . . . . . 15 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
20634neeq1i 3051 . . . . . . . . . . . . . . 15 (𝐾 ≠ (𝐹𝑥) ↔ (𝐹‘(𝑁 + 1)) ≠ (𝐹𝑥))
207205, 206sylibr 237 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≠ (𝐹𝑥))
208207necomd 3042 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≠ 𝐾)
209170, 185, 187, 208leneltd 10786 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 < (𝐹𝑥))
21070ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ∈ ℤ)
211 zltlem1 12026 . . . . . . . . . . . . 13 ((𝐾 ∈ ℤ ∧ (𝐹𝑥) ∈ ℤ) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
212210, 177, 211syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐾 < (𝐹𝑥) ↔ 𝐾 ≤ ((𝐹𝑥) − 1)))
213209, 212mpbid 235 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾 ≤ ((𝐹𝑥) − 1))
214213, 171breqtrrd 5059 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐾𝑘)
215169, 170, 181, 184, 214letrd 10789 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀𝑘)
216 elfzle2 12909 . . . . . . . . . . . 12 ((𝐹𝑥) ∈ (𝑀...(𝑁 + 1)) → (𝐹𝑥) ≤ (𝑁 + 1))
217175, 216syl 17 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ≤ (𝑁 + 1))
218191ad2antrr 725 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℝ)
219 1re 10633 . . . . . . . . . . . . 13 1 ∈ ℝ
220 lesubadd 11104 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
221219, 220mp3an2 1446 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
222185, 218, 221syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) ≤ 𝑁 ↔ (𝐹𝑥) ≤ (𝑁 + 1)))
223217, 222mpbird 260 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ((𝐹𝑥) − 1) ≤ 𝑁)
224171, 223eqbrtrd 5053 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘𝑁)
225152ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑀 ∈ ℤ)
226137ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑁 ∈ ℤ)
227180, 225, 226, 154syl3anc 1368 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀𝑘𝑘𝑁)))
228215, 224, 227mpbir2and 712 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
229170, 181, 214lensymd 10783 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → ¬ 𝑘 < 𝐾)
230229, 53syl 17 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
231171oveq1d 7151 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (((𝐹𝑥) − 1) + 1))
232177zcnd 12079 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹𝑥) ∈ ℂ)
233 npcan 10887 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
234232, 113, 233sylancl 589 . . . . . . . . . . 11 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (((𝐹𝑥) − 1) + 1) = (𝐹𝑥))
235231, 234eqtrd 2833 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 + 1) = (𝐹𝑥))
236235fveq2d 6650 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(𝐹𝑥)))
23717ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
238237, 174, 160syl2anc 587 . . . . . . . . 9 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝐹‘(𝐹𝑥)) = 𝑥)
239230, 236, 2383eqtrrd 2838 . . . . . . . 8 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
240228, 239jca 515 . . . . . . 7 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (𝐹𝑥) < 𝐾𝑘 = ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
241240expr 460 . . . . . 6 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = ((𝐹𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
242167, 241sylbid 243 . . . . 5 (((𝜑𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (𝐹𝑥) < 𝐾) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
243165, 242pm2.61dan 812 . . . 4 ((𝜑𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
244243expimpd 457 . . 3 (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
245121, 244impbid 215 . 2 (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((𝐹𝑥) < 𝐾, (𝐹𝑥), ((𝐹𝑥) − 1)))))
2461, 2, 6, 245f1od 7379 1 (𝜑𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441   ⊆ wss 3881  ifcif 4425   class class class wbr 5031   ↦ cmpt 5111  ◡ccnv 5519  ⟶wf 6321  –1-1→wf1 6322  –1-1-onto→wf1o 6324  ‘cfv 6325  (class class class)co 7136  ℂcc 10527  ℝcr 10528  1c1 10530   + caddc 10532   < clt 10667   ≤ cle 10668   − cmin 10862  ℤcz 11972  ℤ≥cuz 12234  ...cfz 12888 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11629  df-n0 11889  df-z 11973  df-uz 12235  df-fz 12889 This theorem is referenced by:  seqf1olem2  13409
 Copyright terms: Public domain W3C validator