seqf1oglem1 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > seqf1oglem1		GIF version

Theorem seqf1oglem1 10580

Description: Lemma for seqf1og 10582. (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	⊢ (𝜑 → 𝐶 ⊆ 𝑆)
seqf1og.p	⊢ (𝜑 → + ∈ 𝑉)
seqf1olem.5	⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
seqf1olem.6	⊢ (𝜑 → 𝐺:(𝑀...(𝑁 + 1))⟶𝐶)
seqf1olem.7	⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
seqf1olem.8	⊢ 𝐾 = (^◡𝐹‘(𝑁 + 1))

**Assertion**
Ref	Expression
seqf1oglem1	⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))

Distinct variable groups: 𝑥,𝑘,𝑦,𝑧,𝐹 𝑘,𝐺,𝑥,𝑦,𝑧 𝑘,𝑀,𝑥,𝑦,𝑧 + ,𝑘,𝑥,𝑦,𝑧 𝑥,𝐽,𝑦,𝑧 𝑘,𝑁,𝑥,𝑦,𝑧 𝑘,𝐾,𝑥,𝑦,𝑧 𝜑,𝑘,𝑥,𝑦,𝑧 𝑆,𝑘,𝑥,𝑦,𝑧 𝐶,𝑘,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐽(𝑘) 𝑉(𝑥,𝑦,𝑧,𝑘)

**Proof of Theorem seqf1oglem1**
Step	Hyp	Ref	Expression
1		seqf1olem.7	. 2 ⊢ 𝐽 = (𝑘 ∈ (𝑀...𝑁) ↦ (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
2		seqf1olem.5	. . . . 5 ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
3		f1of 5492	. . . . 5 ⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
4	2, 3	syl 14	. . . 4 ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
5	4	adantr 276	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
6		fzelp1 10130	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
7	6	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
8		fzp1elp1 10131	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
9	8	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
10		elfzelz 10081	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
11		seqf1olem.8	. . . . . . 7 ⊢ 𝐾 = (^◡𝐹‘(𝑁 + 1))
12		f1ocnv 5505	. . . . . . . . . . 11 ⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
13	2, 12	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
14		f1of1 5491	. . . . . . . . . 10 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
15	13, 14	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
16		f1f 5451	. . . . . . . . 9 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
17	15, 16	syl 14	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
18		seqf1o.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
19		peano2uz 9638	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
20	18, 19	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
21		eluzfz2 10088	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
22	20, 21	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
23	17, 22	ffvelcdmd 5686	. . . . . . 7 ⊢ (𝜑 → (^◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
24	11, 23	eqeltrid 2280	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1)))
25	24	elfzelzd 10082	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
26		zdclt 9384	. . . . 5 ⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝑘 < 𝐾)
27	10, 25, 26	syl2anr 290	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID 𝑘 < 𝐾)
28	7, 9, 27	ifcldcd 3593	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
29	5, 28	ffvelcdmd 5686	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ (𝑀...(𝑁 + 1)))
30	17	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
31		fzelp1 10130	. . . . . 6 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
32	31	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
33	30, 32	ffvelcdmd 5686	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
34	33	elfzelzd 10082	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (^◡𝐹‘𝑥) ∈ ℤ)
35		peano2zm 9345	. . . 4 ⊢ ((^◡𝐹‘𝑥) ∈ ℤ → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
36	34, 35	syl 14	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
37	25	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
38		zdclt 9384	. . . 4 ⊢ (((^◡𝐹‘𝑥) ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID (^◡𝐹‘𝑥) < 𝐾)
39	34, 37, 38	syl2anc 411	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → DECID (^◡𝐹‘𝑥) < 𝐾)
40	34, 36, 39	ifcldcd 3593	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ∈ ℤ)
41		iftrue 3562	. . . . . . . . 9 ⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
42	41	fveq2d 5550	. . . . . . . 8 ⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
43	42	eqeq2d 2205	. . . . . . 7 ⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
44	43	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
45		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘))
46	5, 7	ffvelcdmd 5686	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)))
47	46	elfzelzd 10082	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℤ)
48		eluzel2 9587	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
49	18, 48	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
50	49	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
51		uzssz 9602	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
52	51, 18	sselid 3177	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
53	52	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ)
54		fzdcel 10096	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
55	47, 50, 53, 54	syl3anc 1249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
56	55	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
57	10	zred 9429	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
58	57	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ)
59		simprl 529	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾)
60	58, 59	gtned 8122	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘)
61	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
62		fzssp1 10123	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
63		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁))
64	62, 63	sselid 3177	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
65	61, 64	ffvelcdmd 5686	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)))
66		elfzp1 10128	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
67	18, 66	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
68	67	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1))))
69	65, 68	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) ∈ (𝑀...𝑁) ∨ (𝐹‘𝑘) = (𝑁 + 1)))
70	69	ord 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1)))
71	2	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
72		f1ocnvfv 5814	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
73	71, 64, 72	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
74	11	eqeq1i 2201	. . . . . . . . . . . . . 14 ⊢ (𝐾 = 𝑘 ↔ (^◡𝐹‘(𝑁 + 1)) = 𝑘)
75	73, 74	imbitrrdi 162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
76	70, 75	syld 45	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
77	76	a1d 22	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (DECID (𝐹‘𝑘) ∈ (𝑀...𝑁) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘)))
78	77	necon1addc 2440	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (DECID (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁))))
79	56, 60, 78	mp2d 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁))
80	45, 79	eqeltrd 2270	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁))
81	45	eqcomd 2199	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥)
82		f1ocnvfv 5814	. . . . . . . . . . . . 13 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
83	71, 64, 82	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
84	81, 83	mpd 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) = 𝑘)
85	84, 59	eqbrtrd 4051	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) < 𝐾)
86		iftrue 3562	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
87	85, 86	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
88	87, 84	eqtr2d 2227	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))
89	80, 88	jca 306	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))))
90	89	expr 375	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘𝑘) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
91	44, 90	sylbid 150	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
92		iffalse 3565	. . . . . . . . 9 ⊢ (¬ 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
93	92	fveq2d 5550	. . . . . . . 8 ⊢ (¬ 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
94	93	eqeq2d 2205	. . . . . . 7 ⊢ (¬ 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
95	94	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
96		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
97	5, 9	ffvelcdmd 5686	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
98	97	elfzelzd 10082	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
99		fzdcel 10096	. . . . . . . . . . . 12 ⊢ (((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
100	98, 50, 53, 99	syl3anc 1249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
101	100	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
102	25	zred 9429	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ ℝ)
103	102	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
104	57	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
105		peano2re 8145	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
106	104, 105	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
107		simprl 529	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
108	103, 104, 107	nltled 8130	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘)
109	104	ltp1d 8939	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
110	103, 104, 106, 108, 109	lelttrd 8134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
111	103, 110	ltned 8123	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
112	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
113	8	ad2antlr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
114	112, 113	ffvelcdmd 5686	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
115		elfzp1 10128	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
116	18, 115	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
117	116	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)) ↔ ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1))))
118	114, 117	mpbid 147	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) ∨ (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
119	118	ord 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
120	2	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
121		f1ocnvfv 5814	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
122	120, 113, 121	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1)))
123	11	eqeq1i 2201	. . . . . . . . . . . . . 14 ⊢ (𝐾 = (𝑘 + 1) ↔ (^◡𝐹‘(𝑁 + 1)) = (𝑘 + 1))
124	122, 123	imbitrrdi 162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = (𝑁 + 1) → 𝐾 = (𝑘 + 1)))
125	119, 124	syld 45	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1)))
126	125	a1d 22	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → 𝐾 = (𝑘 + 1))))
127	126	necon1addc 2440	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))))
128	101, 111, 127	mp2d 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
129	96, 128	eqeltrd 2270	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
130	96	eqcomd 2199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
131		f1ocnvfv 5814	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ (𝑘 + 1) ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (^◡𝐹‘𝑥) = (𝑘 + 1)))
132	120, 113, 131	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝐹‘(𝑘 + 1)) = 𝑥 → (^◡𝐹‘𝑥) = (𝑘 + 1)))
133	130, 132	mpd 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (^◡𝐹‘𝑥) = (𝑘 + 1))
134	133	breq1d 4039	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
135		lttr 8083	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
136	104, 106, 103, 135	syl3anc 1249	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
137	109, 136	mpand 429	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾))
138	134, 137	sylbid 150	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾))
139	107, 138	mtod 664	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
140		iffalse 3565	. . . . . . . . . 10 ⊢ (¬ (^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
141	139, 140	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
142	133	oveq1d 5925	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1))
143	104	recnd 8038	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
144		ax-1cn 7955	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
145		pncan 8215	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
147	141, 142, 146	3eqtrrd 2231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))
148	129, 147	jca 306	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))))
149	148	expr 375	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘(𝑘 + 1)) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
150	95, 149	sylbid 150	. . . . 5 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
151		exmiddc 837	. . . . . 6 ⊢ (DECID 𝑘 < 𝐾 → (𝑘 < 𝐾 ∨ ¬ 𝑘 < 𝐾))
152	27, 151	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 < 𝐾 ∨ ¬ 𝑘 < 𝐾))
153	91, 150, 152	mpjaodan 799	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
154	153	expimpd 363	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
155	86	eqeq2d 2205	. . . . . . 7 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
156	155	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
157	49	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ∈ ℤ)
158		eluzelz 9591	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑁 ∈ ℤ)
159	18, 158	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
160	159	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑁 ∈ ℤ)
161		simprr 531	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 = (^◡𝐹‘𝑥))
162	17	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
163		simplr 528	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...𝑁))
164	62, 163	sselid 3177	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
165	162, 164	ffvelcdmd 5686	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
166	161, 165	eqeltrd 2270	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
167	166	elfzelzd 10082	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℤ)
168		elfzle1 10083	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘)
169	166, 168	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘)
170	167	zred 9429	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℝ)
171	102	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ∈ ℝ)
172	159	peano2zd 9432	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
173	172	zred 9429	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
174	173	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ)
175		simprl 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) < 𝐾)
176	161, 175	eqbrtrd 4051	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < 𝐾)
177		elfzle2 10084	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
178	24, 177	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1))
179	178	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1))
180	170, 171, 174, 176, 179	ltletrd 8432	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1))
181		zleltp1 9362	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
182	167, 160, 181	syl2anc 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
183	180, 182	mpbird 167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁)
184	157, 160, 167, 169, 183	elfzd 10072	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁))
185	176, 42	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
186	161	fveq2d 5550	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(^◡𝐹‘𝑥)))
187	2	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
188		f1ocnvfv2 5813	. . . . . . . . . 10 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
189	187, 164, 188	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
190	185, 186, 189	3eqtrrd 2231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
191	184, 190	jca 306	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
192	191	expr 375	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = (^◡𝐹‘𝑥) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
193	156, 192	sylbid 150	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
194	140	eqeq2d 2205	. . . . . . 7 ⊢ (¬ (^◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((^◡𝐹‘𝑥) − 1)))
195	194	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = ((^◡𝐹‘𝑥) − 1)))
196	49	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℤ)
197	159	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℤ)
198		simprr 531	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 = ((^◡𝐹‘𝑥) − 1))
199	17	ad2antrr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
200		simplr 528	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...𝑁))
201	62, 200	sselid 3177	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
202	199, 201	ffvelcdmd 5686	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
203	202	elfzelzd 10082	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℤ)
204	203, 35	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
205	198, 204	eqeltrd 2270	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ)
206	49	zred 9429	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
207	206	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ)
208	102	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ)
209	205	zred 9429	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ)
210		elfzle1 10083	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾)
211	24, 210	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
212	211	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾)
213		elfzelz 10081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
214	213	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
215	214	zred 9429	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
216	159	zred 9429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
217	216	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
218	173	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
219		elfzle2 10084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁)
220	219	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁)
221	217	ltp1d 8939	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
222	215, 217, 218, 220, 221	lelttrd 8134	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
223	215, 222	gtned 8122	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ≠ 𝑥)
224	223	adantr 276	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ≠ 𝑥)
225	15	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
226	22	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
227		f1fveq 5807	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
228	225, 226, 201, 227	syl12anc 1247	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
229	228	necon3bid 2405	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
230	224, 229	mpbird 167	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
231	11	neeq1i 2379	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ≠ (^◡𝐹‘𝑥) ↔ (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
232	230, 231	sylibr 134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (^◡𝐹‘𝑥))
233	232	necomd 2450	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≠ 𝐾)
234	25	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ)
235		zapne 9381	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝐹‘𝑥) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((^◡𝐹‘𝑥) # 𝐾 ↔ (^◡𝐹‘𝑥) ≠ 𝐾))
236	203, 234, 235	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) # 𝐾 ↔ (^◡𝐹‘𝑥) ≠ 𝐾))
237	233, 236	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) # 𝐾)
238	203	zred 9429	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℝ)
239		simprl 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
240	208, 238, 239	nltled 8130	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (^◡𝐹‘𝑥))
241	208, 238, 240	leltapd 8648	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐾 < (^◡𝐹‘𝑥) ↔ (^◡𝐹‘𝑥) # 𝐾))
242	237, 241	mpbird 167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 < (^◡𝐹‘𝑥))
243		zltlem1 9364	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ (^◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
244	234, 203, 243	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
245	242, 244	mpbid 147	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((^◡𝐹‘𝑥) − 1))
246	245, 198	breqtrrd 4057	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘)
247	207, 208, 209, 212, 246	letrd 8133	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘)
248		elfzle2 10084	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
249	202, 248	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
250	216	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ)
251		1re 8008	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
252		lesubadd 8443	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
253	251, 252	mp3an2 1336	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
254	238, 250, 253	syl2anc 411	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
255	249, 254	mpbird 167	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) − 1) ≤ 𝑁)
256	198, 255	eqbrtrd 4051	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁)
257	196, 197, 205, 247, 256	elfzd 10072	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
258	208, 209, 246	lensymd 8131	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾)
259	258, 93	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
260	198	oveq1d 5925	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((^◡𝐹‘𝑥) − 1) + 1))
261	203	zcnd 9430	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℂ)
262		npcan 8218	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
263	261, 144, 262	sylancl 413	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
264	260, 263	eqtrd 2226	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (^◡𝐹‘𝑥))
265	264	fveq2d 5550	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘(𝑘 + 1)) = (𝐹‘(^◡𝐹‘𝑥)))
266	2	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
267	266, 201, 188	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
268	259, 265, 267	3eqtrrd 2231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))
269	257, 268	jca 306	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))))
270	269	expr 375	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = ((^◡𝐹‘𝑥) − 1) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
271	195, 270	sylbid 150	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ¬ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
272		exmiddc 837	. . . . . 6 ⊢ (DECID (^◡𝐹‘𝑥) < 𝐾 → ((^◡𝐹‘𝑥) < 𝐾 ∨ ¬ (^◡𝐹‘𝑥) < 𝐾))
273	39, 272	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((^◡𝐹‘𝑥) < 𝐾 ∨ ¬ (^◡𝐹‘𝑥) < 𝐾))
274	193, 271, 273	mpjaodan 799	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
275	274	expimpd 363	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1))) → (𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))))))
276	154, 275	impbid 129	. 2 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) ↔ (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
277	1, 29, 40, 276	f1od 6113	1 ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 DECID wdc 835 ∧ w3a 980 = wceq 1364 ∈ wcel 2164 ≠ wne 2364 ⊆ wss 3153 ifcif 3557 class class class wbr 4029 ↦ cmpt 4090 ^◡ccnv 4654 ⟶wf 5242 –1-1→wf1 5243 –1-1-onto→wf1o 5245 ‘cfv 5246 (class class class)co 5910 ℂcc 7860 ℝcr 7861 1c1 7863 + caddc 7865 < clt 8044 ≤ cle 8045 − cmin 8180 # cap 8590 ℤcz 9307 ℤ_≥cuz 9582 ...cfz 10064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4462 ax-setind 4565 ax-cnex 7953 ax-resscn 7954 ax-1cn 7955 ax-1re 7956 ax-icn 7957 ax-addcl 7958 ax-addrcl 7959 ax-mulcl 7960 ax-mulrcl 7961 ax-addcom 7962 ax-mulcom 7963 ax-addass 7964 ax-mulass 7965 ax-distr 7966 ax-i2m1 7967 ax-0lt1 7968 ax-1rid 7969 ax-0id 7970 ax-rnegex 7971 ax-precex 7972 ax-cnre 7973 ax-pre-ltirr 7974 ax-pre-ltwlin 7975 ax-pre-lttrn 7976 ax-pre-apti 7977 ax-pre-ltadd 7978 ax-pre-mulgt0 7979

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-reu 2479 df-rab 2481 df-v 2762 df-sbc 2986 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-if 3558 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-br 4030 df-opab 4091 df-mpt 4092 df-id 4322 df-xp 4661 df-rel 4662 df-cnv 4663 df-co 4664 df-dm 4665 df-rn 4666 df-res 4667 df-ima 4668 df-iota 5207 df-fun 5248 df-fn 5249 df-f 5250 df-f1 5251 df-fo 5252 df-f1o 5253 df-fv 5254 df-riota 5865 df-ov 5913 df-oprab 5914 df-mpo 5915 df-pnf 8046 df-mnf 8047 df-xr 8048 df-ltxr 8049 df-le 8050 df-sub 8182 df-neg 8183 df-reap 8584 df-ap 8591 df-inn 8973 df-n0 9231 df-z 9308 df-uz 9583 df-fz 10065

This theorem is referenced by: seqf1oglem2 10581

W3C validator