seqf1olem1 - Metamath Proof Explorer

	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**
Step	Hyp	Ref	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
5	3, 4	ifex 4429	. . 3 ⊢ if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ∈ V
6	5	a1i 11	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ∈ V)
7		iftrue 4387	. . . . . . . . 9 ⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
8	7	fveq2d 6542	. . . . . . . 8 ⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
9	8	eqeq2d 2805	. . . . . . 7 ⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
10	9	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
11		simprr 769	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘))
12		elfzelz 12758	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
13	12	zred 11936	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
14	13	ad2antlr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ)
15		simprl 767	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾)
16	14, 15	gtned 10622	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘)
17		seqf1olem.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
18		f1of 6483	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
19	17, 18	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
20	19	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
21		fzssp1 12800	. . . . . . . . . . . . . . . 16 ⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
22		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁))
23	21, 22	sseldi 3887	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
24	20, 23	ffvelrnd 6717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)))
25		seqf1o.4	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
26		elfzp1 12807	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
27	25, 26	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
28	27	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
29	24, 28	mpbid 233	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))
30	29	ord 859	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1)))
31	17	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
32		f1ocnvfv 6900	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
33	31, 23, 32	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
34		seqf1olem.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (^◡𝐹‘(𝑁 + 1))
35	34	eqeq1i 2800	. . . . . . . . . . . . 13 ⊢ (𝐾 = 𝑘 ↔ (^◡𝐹‘(𝑁 + 1)) = 𝑘)
36	33, 35	syl6ibr 253	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
37	30, 36	syld 47	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
38	37	necon1ad 3001	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁)))
39	16, 38	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁))
40	11, 39	eqeltrd 2883	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁))
41	11	eqcomd 2801	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥)
42		f1ocnvfv 6900	. . . . . . . . . . . . 13 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
43	31, 23, 42	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
44	41, 43	mpd 15	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) = 𝑘)
45	44, 15	eqbrtrd 4984	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) < 𝐾)
46		iftrue 4387	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
47	45, 46	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
48	47, 44	eqtr2d 2832	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))
49	40, 48	jca 512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))))
50	49	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
51	10, 50	sylbid 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
52		iffalse 4390	. . . . . . . . 9 ⊢ (¬ 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
53	52	fveq2d 6542	. . . . . . . 8 ⊢ (¬ 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
54	53	eqeq2d 2805	. . . . . . 7 ⊢ (¬ 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
55	54	adantl 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)))
58	17, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
59		f1of1 6482	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
61		f1f 6443	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
62	60, 61	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
63		peano2uz 12150	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
64	25, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
65		eluzfz2 12765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
66	64, 65	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
67	62, 66	ffvelrnd 6717	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (^◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
68	34, 67	syl5eqel 2887	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1)))
69		elfzelz 12758	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ∈ ℤ)
70	68, 69	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 ∈ ℤ)
71	70	zred 11936	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ ℝ)
72	71	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
73	13	ad2antlr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
74		peano2re 10660	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
75	73, 74	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
76		simprl 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
77	72, 73, 76	nltled 10637	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘)
78	73	ltp1d 11418	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
79	72, 73, 75, 77, 78	lelttrd 10645	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
80	72, 79	ltned 10623	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
81	19	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
82		fzp1elp1 12810	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
83	82	ad2antlr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
84	81, 83	ffvelrnd 6717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
85		elfzp1 12807	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
86	25, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
87	86	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
88	84, 87	mpbid 233	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
89	88	ord 859	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
90	17	ad2antrr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
91		f1ocnvfv 6900	. . . . . . . . . . . . . 14 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
92	90, 83, 91	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
93	34	eqeq1i 2800	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑘 + 1) ↔ (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))
94	92, 93	syl6ibr 253	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
95	89, 94	syld 47	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
96	95	necon1ad 3001	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁)))
97	80, 96	mpd 15	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
98	56, 97	eqeltrd 2883	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
99	56	eqcomd 2801	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
100		f1ocnvfv 6900	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (^◡𝐹‘𝑥) = (𝑘 + 1)))
101	90, 83, 100	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (^◡𝐹‘𝑥) = (𝑘 + 1)))
102	99, 101	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (^◡𝐹‘𝑥) = (𝑘 + 1))
103	102	breq1d 4972	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
104		lttr 10564	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
105	73, 75, 72, 104	syl3anc 1364	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
106	78, 105	mpand 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾))
107	103, 106	sylbid 241	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾))
108	76, 107	mtod 199	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
109		iffalse 4390	. . . . . . . . . 10 ⊢ (¬ (^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
110	108, 109	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
111	102	oveq1d 7031	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1))
112	73	recnd 10515	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
113		ax-1cn 10441	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
114		pncan 10739	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
115	112, 113, 114	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
116	110, 111, 115	3eqtrrd 2836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))
117	98, 116	jca 512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))))
118	117	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
119	55, 118	sylbid 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
120	51, 119	pm2.61dan 809	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
121	120	expimpd 454	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
122	46	eqeq2d 2805	. . . . . . 7 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
123	122	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
124		simprr 769	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 = (^◡𝐹‘𝑥))
125	62	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
126		simplr 765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...𝑁))
127	21, 126	sseldi 3887	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
128	125, 127	ffvelrnd 6717	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
129	124, 128	eqeltrd 2883	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
130		elfzle1 12760	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘)
131	129, 130	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘)
132		elfzelz 12758	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑘 ∈ ℤ)
133	129, 132	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℤ)
134	133	zred 11936	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℝ)
135	71	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ∈ ℝ)
136		eluzelz 12103	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
137	25, 136	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
138	137	peano2zd 11939	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
139	138	zred 11936	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
140	139	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ)
141		simprl 767	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) < 𝐾)
142	124, 141	eqbrtrd 4984	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < 𝐾)
143		elfzle2 12761	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
144	68, 143	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1))
145	144	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1))
146	134, 135, 140, 142, 145	ltletrd 10647	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1))
147	137	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑁 ∈ ℤ)
148		zleltp1 11882	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
149	133, 147, 148	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
150	146, 149	mpbird 258	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁)
151		eluzel2 12098	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
152	25, 151	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℤ)
153	152	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ∈ ℤ)
154		elfz 12748	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
155	133, 153, 147, 154	syl3anc 1364	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
156	131, 150, 155	mpbir2and 709	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁))
157	142, 8	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
158	124	fveq2d 6542	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(^◡𝐹‘𝑥)))
159	17	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
160		f1ocnvfv2 6899	. . . . . . . . . 10 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
161	159, 127, 160	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
162	157, 158, 161	3eqtrrd 2836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
163	156, 162	jca 512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
164	163	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = (^◡𝐹‘𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
165	123, 164	sylbid 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
166	109	eqeq2d 2805	. . . . . . 7 ⊢ (¬ (^◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((^◡𝐹‘𝑥) − 1)))
167	166	adantl 482	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((^◡𝐹‘𝑥) − 1)))
168	152	zred 11936	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
169	168	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ)
170	71	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ)
171		simprr 769	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 = ((^◡𝐹‘𝑥) − 1))
172	62	ad2antrr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
173		simplr 765	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
174	21, 173	sseldi 3887	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
175	172, 174	ffvelrnd 6717	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
176		elfzelz 12758	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (^◡𝐹‘𝑥) ∈ ℤ)
177	175, 176	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℤ)
178		peano2zm 11874	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘𝑥) ∈ ℤ → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
179	177, 178	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
180	171, 179	eqeltrd 2883	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ)
181	180	zred 11936	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ)
182		elfzle1 12760	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾)
183	68, 182	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
184	183	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾)
185	177	zred 11936	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℝ)
186		simprl 767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
187	170, 185, 186	nltled 10637	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (^◡𝐹‘𝑥))
188		elfzelz 12758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
189	188	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
190	189	zred 11936	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
191	137	zred 11936	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑁 ∈ ℝ)
192	191	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
193	139	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
194		elfzle2 12761	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁)
195	194	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁)
196	192	ltp1d 11418	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
197	190, 192, 193, 195, 196	lelttrd 10645	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
198	190, 197	gtned 10622	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
199	198	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
200	60	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
201	66	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
202		f1fveq 6885	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
203	200, 201, 174, 202	syl12anc 833	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
204	203	necon3bid 3028	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
205	199, 204	mpbird 258	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
206	34	neeq1i 3048	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ≠ (^◡𝐹‘𝑥) ↔ (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
207	205, 206	sylibr 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (^◡𝐹‘𝑥))
208	207	necomd 3039	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≠ 𝐾)
209	170, 185, 187, 208	leneltd 10641	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 < (^◡𝐹‘𝑥))
210	70	ad2antrr 722	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ)
211		zltlem1 11884	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ (^◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
212	210, 177, 211	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
213	209, 212	mpbid 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((^◡𝐹‘𝑥) − 1))
214	213, 171	breqtrrd 4990	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘)
215	169, 170, 181, 184, 214	letrd 10644	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘)
216		elfzle2 12761	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
217	175, 216	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
218	191	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ)
219		1re 10487	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
220		lesubadd 10960	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
221	219, 220	mp3an2 1441	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
222	185, 218, 221	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
223	217, 222	mpbird 258	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) − 1) ≤ 𝑁)
224	171, 223	eqbrtrd 4984	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁)
225	152	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℤ)
226	137	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℤ)
227	180, 225, 226, 154	syl3anc 1364	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ↔ (𝑀 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
228	215, 224, 227	mpbir2and 709	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
229	170, 181, 214	lensymd 10638	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾)
230	229, 53	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
231	171	oveq1d 7031	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((^◡𝐹‘𝑥) − 1) + 1))
232	177	zcnd 11937	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℂ)
233		npcan 10743	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
234	232, 113, 233	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
235	231, 234	eqtrd 2831	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (^◡𝐹‘𝑥))
236	235	fveq2d 6542	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(^◡𝐹‘𝑥)))
237	17	ad2antrr 722	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
238	237, 174, 160	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
239	230, 236, 238	3eqtrrd 2836	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
240	228, 239	jca 512	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
241	240	expr 457	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = ((^◡𝐹‘𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
242	167, 241	sylbid 241	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
243	165, 242	pm2.61dan 809	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
244	243	expimpd 454	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
245	121, 244	impbid 213	. 2 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
246	1, 2, 6, 245	f1od 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-1→wf1 6222 –1-1-onto→wf1o 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

W3C validator