seqf1oglem1 - Intuitionistic Logic Explorer

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

Theorem seqf1oglem1 10681

Description: Lemma for seqf1og 10683. (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 5533	. . . . 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 10211	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
7	6	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
8		fzp1elp1 10212	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
9	8	adantl 277	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
10		elfzelz 10162	. . . . 5 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℤ)
11		seqf1olem.8	. . . . . . 7 ⊢ 𝐾 = (^◡𝐹‘(𝑁 + 1))
12		f1ocnv 5546	. . . . . . . . . . 11 ⊢ (𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
13	2, 12	syl 14	. . . . . . . . . 10 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
14		f1of1 5532	. . . . . . . . . 10 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
15	13, 14	syl 14	. . . . . . . . 9 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)))
16		f1f 5492	. . . . . . . . 9 ⊢ (^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
17	15, 16	syl 14	. . . . . . . 8 ⊢ (𝜑 → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
18		seqf1o.4	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘𝑀))
19		peano2uz 9719	. . . . . . . . . 10 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
20	18, 19	syl 14	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 + 1) ∈ (ℤ_≥‘𝑀))
21		eluzfz2 10169	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘𝑀) → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
22	20, 21	syl 14	. . . . . . . 8 ⊢ (𝜑 → (𝑁 + 1) ∈ (𝑀...(𝑁 + 1)))
23	17, 22	ffvelcdmd 5728	. . . . . . 7 ⊢ (𝜑 → (^◡𝐹‘(𝑁 + 1)) ∈ (𝑀...(𝑁 + 1)))
24	11, 23	eqeltrid 2293	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ (𝑀...(𝑁 + 1)))
25	24	elfzelzd 10163	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℤ)
26		zdclt 9465	. . . . 5 ⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID 𝑘 < 𝐾)
27	10, 25, 26	syl2anr 290	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID 𝑘 < 𝐾)
28	7, 9, 27	ifcldcd 3612	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
29	5, 28	ffvelcdmd 5728	. 2 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ∈ (𝑀...(𝑁 + 1)))
30	17	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ^◡𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
31		fzelp1 10211	. . . . . 6 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
32	31	adantl 277	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
33	30, 32	ffvelcdmd 5728	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
34	33	elfzelzd 10163	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (^◡𝐹‘𝑥) ∈ ℤ)
35		peano2zm 9425	. . . 4 ⊢ ((^◡𝐹‘𝑥) ∈ ℤ → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
36	34, 35	syl 14	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
37	25	adantr 276	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
38		zdclt 9465	. . . 4 ⊢ (((^◡𝐹‘𝑥) ∈ ℤ ∧ 𝐾 ∈ ℤ) → DECID (^◡𝐹‘𝑥) < 𝐾)
39	34, 37, 38	syl2anc 411	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → DECID (^◡𝐹‘𝑥) < 𝐾)
40	34, 36, 39	ifcldcd 3612	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ∈ ℤ)
41		iftrue 3580	. . . . . . . . 9 ⊢ (𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = 𝑘)
42	41	fveq2d 5592	. . . . . . . 8 ⊢ (𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
43	42	eqeq2d 2218	. . . . . . 7 ⊢ (𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
44	43	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘𝑘)))
45		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 = (𝐹‘𝑘))
46	5, 7	ffvelcdmd 5728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)))
47	46	elfzelzd 10163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) ∈ ℤ)
48		eluzel2 9668	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (ℤ_≥‘𝑀) → 𝑀 ∈ ℤ)
49	18, 48	syl 14	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℤ)
50	49	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
51		uzssz 9683	. . . . . . . . . . . . . 14 ⊢ (ℤ_≥‘𝑀) ⊆ ℤ
52	51, 18	sselid 3195	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑁 ∈ ℤ)
53	52	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ)
54		fzdcel 10177	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
55	47, 50, 53, 54	syl3anc 1250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
56	55	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → DECID (𝐹‘𝑘) ∈ (𝑀...𝑁))
57	10	zred 9510	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑀...𝑁) → 𝑘 ∈ ℝ)
58	57	ad2antlr 489	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ ℝ)
59		simprl 529	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 < 𝐾)
60	58, 59	gtned 8200	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐾 ≠ 𝑘)
61	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
62		fzssp1 10204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀...𝑁) ⊆ (𝑀...(𝑁 + 1))
63		simplr 528	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...𝑁))
64	62, 63	sselid 3195	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
65	61, 64	ffvelcdmd 5728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...(𝑁 + 1)))
66		elfzp1 10209	. . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐹‘𝑘) = (𝑁 + 1)))
71	2	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
72		f1ocnvfv 5860	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
73	71, 64, 72	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → (^◡𝐹‘(𝑁 + 1)) = 𝑘))
74	11	eqeq1i 2214	. . . . . . . . . . . . . 14 ⊢ (𝐾 = 𝑘 ↔ (^◡𝐹‘(𝑁 + 1)) = 𝑘)
75	73, 74	imbitrrdi 162	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = (𝑁 + 1) → 𝐾 = 𝑘))
76	70, 75	syld 45	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘))
77	76	a1d 22	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (DECID (𝐹‘𝑘) ∈ (𝑀...𝑁) → (¬ (𝐹‘𝑘) ∈ (𝑀...𝑁) → 𝐾 = 𝑘)))
78	77	necon1addc 2453	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (DECID (𝐹‘𝑘) ∈ (𝑀...𝑁) → (𝐾 ≠ 𝑘 → (𝐹‘𝑘) ∈ (𝑀...𝑁))))
79	56, 60, 78	mp2d 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) ∈ (𝑀...𝑁))
80	45, 79	eqeltrd 2283	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → 𝑥 ∈ (𝑀...𝑁))
81	45	eqcomd 2212	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (𝐹‘𝑘) = 𝑥)
82		f1ocnvfv 5860	. . . . . . . . . . . . 13 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑘 ∈ (𝑀...(𝑁 + 1))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
83	71, 64, 82	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → ((𝐹‘𝑘) = 𝑥 → (^◡𝐹‘𝑥) = 𝑘))
84	81, 83	mpd 13	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) = 𝑘)
85	84, 59	eqbrtrd 4072	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → (^◡𝐹‘𝑥) < 𝐾)
86		iftrue 3580	. . . . . . . . . 10 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
87	85, 86	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘𝑘))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = (^◡𝐹‘𝑥))
88	87, 84	eqtr2d 2240	. . . . . . . 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 3583	. . . . . . . . 9 ⊢ (¬ 𝑘 < 𝐾 → if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)) = (𝑘 + 1))
93	92	fveq2d 5592	. . . . . . . 8 ⊢ (¬ 𝑘 < 𝐾 → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
94	93	eqeq2d 2218	. . . . . . 7 ⊢ (¬ 𝑘 < 𝐾 → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
95	94	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ ¬ 𝑘 < 𝐾) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) ↔ 𝑥 = (𝐹‘(𝑘 + 1))))
96		simprr 531	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 = (𝐹‘(𝑘 + 1)))
97	5, 9	ffvelcdmd 5728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
98	97	elfzelzd 10163	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘(𝑘 + 1)) ∈ ℤ)
99		fzdcel 10177	. . . . . . . . . . . 12 ⊢ (((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
100	98, 50, 53, 99	syl3anc 1250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
101	100	adantr 276	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
102	25	zred 9510	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ∈ ℝ)
103	102	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ∈ ℝ)
104	57	ad2antlr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℝ)
105		peano2re 8223	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℝ → (𝑘 + 1) ∈ ℝ)
106	104, 105	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ ℝ)
107		simprl 529	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ 𝑘 < 𝐾)
108	103, 104, 107	nltled 8208	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≤ 𝑘)
109	104	ltp1d 9018	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 < (𝑘 + 1))
110	103, 104, 106, 108, 109	lelttrd 8212	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 < (𝑘 + 1))
111	103, 110	ltned 8201	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐾 ≠ (𝑘 + 1))
112	4	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))⟶(𝑀...(𝑁 + 1)))
113	8	ad2antlr 489	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝑘 + 1) ∈ (𝑀...(𝑁 + 1)))
114	112, 113	ffvelcdmd 5728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...(𝑁 + 1)))
115		elfzp1 10209	. . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (¬ (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐹‘(𝑘 + 1)) = (𝑁 + 1)))
120	2	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
121		f1ocnvfv 5860	. . . . . . . . . . . . . . 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 2214	. . . . . . . . . . . . . 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 2453	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (DECID (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁) → (𝐾 ≠ (𝑘 + 1) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))))
128	101, 111, 127	mp2d 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) ∈ (𝑀...𝑁))
129	96, 128	eqeltrd 2283	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑥 ∈ (𝑀...𝑁))
130	96	eqcomd 2212	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → (𝐹‘(𝑘 + 1)) = 𝑥)
131		f1ocnvfv 5860	. . . . . . . . . . . . . . 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 4060	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 ↔ (𝑘 + 1) < 𝐾))
135		lttr 8161	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℝ ∧ (𝑘 + 1) ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
136	104, 106, 103, 135	syl3anc 1250	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 < (𝑘 + 1) ∧ (𝑘 + 1) < 𝐾) → 𝑘 < 𝐾))
137	109, 136	mpand 429	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) < 𝐾 → 𝑘 < 𝐾))
138	134, 137	sylbid 150	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) < 𝐾 → 𝑘 < 𝐾))
139	107, 138	mtod 665	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
140		iffalse 3583	. . . . . . . . . 10 ⊢ (¬ (^◡𝐹‘𝑥) < 𝐾 → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
141	139, 140	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) = ((^◡𝐹‘𝑥) − 1))
142	133	oveq1d 5971	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((^◡𝐹‘𝑥) − 1) = ((𝑘 + 1) − 1))
143	104	recnd 8116	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → 𝑘 ∈ ℂ)
144		ax-1cn 8033	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
145		pncan 8293	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) ∧ (¬ 𝑘 < 𝐾 ∧ 𝑥 = (𝐹‘(𝑘 + 1)))) → ((𝑘 + 1) − 1) = 𝑘)
147	141, 142, 146	3eqtrrd 2244	. . . . . . . 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 838	. . . . . 6 ⊢ (DECID 𝑘 < 𝐾 → (𝑘 < 𝐾 ∨ ¬ 𝑘 < 𝐾))
152	27, 151	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑘 < 𝐾 ∨ ¬ 𝑘 < 𝐾))
153	91, 150, 152	mpjaodan 800	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
154	153	expimpd 363	. . 3 ⊢ (𝜑 → ((𝑘 ∈ (𝑀...𝑁) ∧ 𝑥 = (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1)))) → (𝑥 ∈ (𝑀...𝑁) ∧ 𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)))))
155	86	eqeq2d 2218	. . . . . . 7 ⊢ ((^◡𝐹‘𝑥) < 𝐾 → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
156	155	adantl 277	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (^◡𝐹‘𝑥) < 𝐾) → (𝑘 = if((^◡𝐹‘𝑥) < 𝐾, (^◡𝐹‘𝑥), ((^◡𝐹‘𝑥) − 1)) ↔ 𝑘 = (^◡𝐹‘𝑥)))
157	49	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ∈ ℤ)
158		eluzelz 9672	. . . . . . . . . . 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 3195	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
165	162, 164	ffvelcdmd 5728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
166	161, 165	eqeltrd 2283	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...(𝑁 + 1)))
167	166	elfzelzd 10163	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℤ)
168		elfzle1 10164	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝑘)
169	166, 168	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑀 ≤ 𝑘)
170	167	zred 9510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ ℝ)
171	102	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ∈ ℝ)
172	159	peano2zd 9513	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
173	172	zred 9510	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 + 1) ∈ ℝ)
174	173	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑁 + 1) ∈ ℝ)
175		simprl 529	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (^◡𝐹‘𝑥) < 𝐾)
176	161, 175	eqbrtrd 4072	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < 𝐾)
177		elfzle2 10165	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝐾 ≤ (𝑁 + 1))
178	24, 177	syl 14	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐾 ≤ (𝑁 + 1))
179	178	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐾 ≤ (𝑁 + 1))
180	170, 171, 174, 176, 179	ltletrd 8511	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 < (𝑁 + 1))
181		zleltp1 9443	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
182	167, 160, 181	syl2anc 411	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝑘 ≤ 𝑁 ↔ 𝑘 < (𝑁 + 1)))
183	180, 182	mpbird 167	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ≤ 𝑁)
184	157, 160, 167, 169, 183	elfzd 10153	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝑘 ∈ (𝑀...𝑁))
185	176, 42	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘𝑘))
186	161	fveq2d 5592	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘𝑘) = (𝐹‘(^◡𝐹‘𝑥)))
187	2	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → 𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)))
188		f1ocnvfv2 5859	. . . . . . . . . 10 ⊢ ((𝐹:(𝑀...(𝑁 + 1))–1-1-onto→(𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
189	187, 164, 188	syl2anc 411	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ ((^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = (^◡𝐹‘𝑥))) → (𝐹‘(^◡𝐹‘𝑥)) = 𝑥)
190	185, 186, 189	3eqtrrd 2244	. . . . . . . 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 2218	. . . . . . 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 3195	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑥 ∈ (𝑀...(𝑁 + 1)))
202	199, 201	ffvelcdmd 5728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)))
203	202	elfzelzd 10163	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℤ)
204	203, 35	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) − 1) ∈ ℤ)
205	198, 204	eqeltrd 2283	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℤ)
206	49	zred 9510	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ ℝ)
207	206	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ∈ ℝ)
208	102	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℝ)
209	205	zred 9510	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ ℝ)
210		elfzle1 10164	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (𝑀...(𝑁 + 1)) → 𝑀 ≤ 𝐾)
211	24, 210	syl 14	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ≤ 𝐾)
212	211	ad2antrr 488	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝐾)
213		elfzelz 10162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
214	213	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℤ)
215	214	zred 9510	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
216	159	zred 9510	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℝ)
217	216	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℝ)
218	173	adantr 276	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → (𝑁 + 1) ∈ ℝ)
219		elfzle2 10165	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ≤ 𝑁)
220	219	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝑁)
221	217	ltp1d 9018	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑁 < (𝑁 + 1))
222	215, 217, 218, 220, 221	lelttrd 8212	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 < (𝑁 + 1))
223	215, 222	gtned 8200	. . . . . . . . . . . . . . . . . 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 5853	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝐹:(𝑀...(𝑁 + 1))–1-1→(𝑀...(𝑁 + 1)) ∧ ((𝑁 + 1) ∈ (𝑀...(𝑁 + 1)) ∧ 𝑥 ∈ (𝑀...(𝑁 + 1)))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
228	225, 226, 201, 227	syl12anc 1248	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) = (^◡𝐹‘𝑥) ↔ (𝑁 + 1) = 𝑥))
229	228	necon3bid 2418	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥) ↔ (𝑁 + 1) ≠ 𝑥))
230	224, 229	mpbird 167	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
231	11	neeq1i 2392	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ≠ (^◡𝐹‘𝑥) ↔ (^◡𝐹‘(𝑁 + 1)) ≠ (^◡𝐹‘𝑥))
232	230, 231	sylibr 134	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≠ (^◡𝐹‘𝑥))
233	232	necomd 2463	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≠ 𝐾)
234	25	ad2antrr 488	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ∈ ℤ)
235		zapne 9462	. . . . . . . . . . . . . . 15 ⊢ (((^◡𝐹‘𝑥) ∈ ℤ ∧ 𝐾 ∈ ℤ) → ((^◡𝐹‘𝑥) # 𝐾 ↔ (^◡𝐹‘𝑥) ≠ 𝐾))
236	203, 234, 235	syl2anc 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ((^◡𝐹‘𝑥) # 𝐾 ↔ (^◡𝐹‘𝑥) ≠ 𝐾))
237	233, 236	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) # 𝐾)
238	203	zred 9510	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℝ)
239		simprl 529	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ (^◡𝐹‘𝑥) < 𝐾)
240	208, 238, 239	nltled 8208	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ (^◡𝐹‘𝑥))
241	208, 238, 240	leltapd 8727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐾 < (^◡𝐹‘𝑥) ↔ (^◡𝐹‘𝑥) # 𝐾))
242	237, 241	mpbird 167	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 < (^◡𝐹‘𝑥))
243		zltlem1 9445	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ ℤ ∧ (^◡𝐹‘𝑥) ∈ ℤ) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
244	234, 203, 243	syl2anc 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐾 < (^◡𝐹‘𝑥) ↔ 𝐾 ≤ ((^◡𝐹‘𝑥) − 1)))
245	242, 244	mpbid 147	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ ((^◡𝐹‘𝑥) − 1))
246	245, 198	breqtrrd 4078	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝐾 ≤ 𝑘)
247	207, 208, 209, 212, 246	letrd 8211	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑀 ≤ 𝑘)
248		elfzle2 10165	. . . . . . . . . . . 12 ⊢ ((^◡𝐹‘𝑥) ∈ (𝑀...(𝑁 + 1)) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
249	202, 248	syl 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ≤ (𝑁 + 1))
250	216	ad2antrr 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑁 ∈ ℝ)
251		1re 8086	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
252		lesubadd 8522	. . . . . . . . . . . . 13 ⊢ (((^◡𝐹‘𝑥) ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (((^◡𝐹‘𝑥) − 1) ≤ 𝑁 ↔ (^◡𝐹‘𝑥) ≤ (𝑁 + 1)))
253	251, 252	mp3an2 1338	. . . . . . . . . . . 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 4072	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ≤ 𝑁)
257	196, 197, 205, 247, 256	elfzd 10153	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → 𝑘 ∈ (𝑀...𝑁))
258	208, 209, 246	lensymd 8209	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → ¬ 𝑘 < 𝐾)
259	258, 93	syl 14	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝐹‘if(𝑘 < 𝐾, 𝑘, (𝑘 + 1))) = (𝐹‘(𝑘 + 1)))
260	198	oveq1d 5971	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (((^◡𝐹‘𝑥) − 1) + 1))
261	203	zcnd 9511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (^◡𝐹‘𝑥) ∈ ℂ)
262		npcan 8296	. . . . . . . . . . . 12 ⊢ (((^◡𝐹‘𝑥) ∈ ℂ ∧ 1 ∈ ℂ) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
263	261, 144, 262	sylancl 413	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (((^◡𝐹‘𝑥) − 1) + 1) = (^◡𝐹‘𝑥))
264	260, 263	eqtrd 2239	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) ∧ (¬ (^◡𝐹‘𝑥) < 𝐾 ∧ 𝑘 = ((^◡𝐹‘𝑥) − 1))) → (𝑘 + 1) = (^◡𝐹‘𝑥))
265	264	fveq2d 5592	. . . . . . . . 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 2244	. . . . . . . 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 838	. . . . . 6 ⊢ (DECID (^◡𝐹‘𝑥) < 𝐾 → ((^◡𝐹‘𝑥) < 𝐾 ∨ ¬ (^◡𝐹‘𝑥) < 𝐾))
273	39, 272	syl 14	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝑀...𝑁)) → ((^◡𝐹‘𝑥) < 𝐾 ∨ ¬ (^◡𝐹‘𝑥) < 𝐾))
274	193, 271, 273	mpjaodan 800	. . . 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 6161	1 ⊢ (𝜑 → 𝐽:(𝑀...𝑁)–1-1-onto→(𝑀...𝑁))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 710 DECID wdc 836 ∧ w3a 981 = wceq 1373 ∈ wcel 2177 ≠ wne 2377 ⊆ wss 3170 ifcif 3575 class class class wbr 4050 ↦ cmpt 4112 ^◡ccnv 4681 ⟶wf 5275 –1-1→wf1 5276 –1-1-onto→wf1o 5278 ‘cfv 5279 (class class class)co 5956 ℂcc 7938 ℝcr 7939 1c1 7941 + caddc 7943 < clt 8122 ≤ cle 8123 − cmin 8258 # cap 8669 ℤcz 9387 ℤ_≥cuz 9663 ...cfz 10145

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4169 ax-pow 4225 ax-pr 4260 ax-un 4487 ax-setind 4592 ax-cnex 8031 ax-resscn 8032 ax-1cn 8033 ax-1re 8034 ax-icn 8035 ax-addcl 8036 ax-addrcl 8037 ax-mulcl 8038 ax-mulrcl 8039 ax-addcom 8040 ax-mulcom 8041 ax-addass 8042 ax-mulass 8043 ax-distr 8044 ax-i2m1 8045 ax-0lt1 8046 ax-1rid 8047 ax-0id 8048 ax-rnegex 8049 ax-precex 8050 ax-cnre 8051 ax-pre-ltirr 8052 ax-pre-ltwlin 8053 ax-pre-lttrn 8054 ax-pre-apti 8055 ax-pre-ltadd 8056 ax-pre-mulgt0 8057

This theorem depends on definitions: df-bi 117 df-stab 833 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3003 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-if 3576 df-pw 3622 df-sn 3643 df-pr 3644 df-op 3646 df-uni 3856 df-int 3891 df-br 4051 df-opab 4113 df-mpt 4114 df-id 4347 df-xp 4688 df-rel 4689 df-cnv 4690 df-co 4691 df-dm 4692 df-rn 4693 df-res 4694 df-ima 4695 df-iota 5240 df-fun 5281 df-fn 5282 df-f 5283 df-f1 5284 df-fo 5285 df-f1o 5286 df-fv 5287 df-riota 5911 df-ov 5959 df-oprab 5960 df-mpo 5961 df-pnf 8124 df-mnf 8125 df-xr 8126 df-ltxr 8127 df-le 8128 df-sub 8260 df-neg 8261 df-reap 8663 df-ap 8670 df-inn 9052 df-n0 9311 df-z 9388 df-uz 9664 df-fz 10146

This theorem is referenced by: seqf1oglem2 10682

W3C validator