Theorem poimirlem2 32581

Description: Lemma for poimir 32612- consecutive vertices differ in at most one dimension. (Contributed by Brendan Leahy, 21-Aug-2020.)

Hypotheses

Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimirlem2.1	⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
poimirlem2.2	⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
poimirlem2.3	⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem2.4	⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))
poimirlem2.5	⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))

Assertion

Ref	Expression
poimirlem2	⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))

Distinct variable groups:   𝑗,𝑛,𝑦,𝜑   𝑗,𝐹,𝑛,𝑦   𝑗,𝑀,𝑛,𝑦   𝑗,𝑁,𝑛,𝑦   𝑇,𝑗,𝑛,𝑦   𝑈,𝑗,𝑛,𝑦   𝑗,𝑉,𝑛,𝑦

Proof of Theorem poimirlem2

Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimirlem2.3	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
2		dff1o3 6056	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈))
3	2	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈)
4	1, 3	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun ◡𝑈)
5		imadif 5887	. . . . . . . . . . . . . . 15 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
6	4, 5	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
7		poimirlem2.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))
8		fzp1elp1 12264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
9	7, 8	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
10		poimir.0	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nncnd 10913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
12		npcan1 10334	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
14	13	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
15	9, 14	eleqtrd 2690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 + 1) ∈ (1...𝑁))
16		fzsplit 12238	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
17	15, 16	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
18	17	difeq1d 3689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}))
19		difundir 3839	. . . . . . . . . . . . . . . . 17 ⊢ (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}))
20		elfzuz 12209	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ (ℤ≥‘1))
21	7, 20	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘1))
22		fzsuc 12258	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
24	23	difeq1d 3689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}))
25		difun2 4000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)})
26		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ ℤ)
27	7, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑉 ∈ ℤ)
28	27	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℝ)
29	28	ltp1d 10833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 < (𝑉 + 1))
30	27	peano2zd 11361	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑉 + 1) ∈ ℤ)
31	30	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 + 1) ∈ ℝ)
32	28, 31	ltnled 10063	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉))
33	29, 32	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉)
34		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉)
35	33, 34	nsyl 134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉))
36		difsn 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
38	25, 37	syl5eq 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉))
39	24, 38	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉))
40	31	ltp1d 10833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1))
41		peano2re 10088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) ∈ ℝ → ((𝑉 + 1) + 1) ∈ ℝ)
42	31, 41	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ)
43	31, 42	ltnled 10063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)))
44	40, 43	mpbid 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
45		elfzle1 12215	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
46	44, 45	nsyl 134	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
47		difsn 4269	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
48	46, 47	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
49	39, 48	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
50	19, 49	syl5eq 2656	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
51	18, 50	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
52	51	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
53	6, 52	eqtr3d 2646	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
54		imaundi 5464	. . . . . . . . . . . . 13 ⊢ (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
55	53, 54	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
56	55	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
57		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
58		elun 3715	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
59	56, 57, 58	3bitr3g 301	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
60	59	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
61		imassrn 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (1...𝑉)) ⊆ ran 𝑈
62		f1of 6050	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
63	1, 62	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
64		frn 5966	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
65	63, 64	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
66	61, 65	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁))
67	66	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁))
68		poimirlem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
69		ffn 5958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑇:(1...𝑁)⟶ℤ → 𝑇 Fn (1...𝑁))
70	68, 69	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
71	70	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁))
72		1ex 9914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ V
73		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)))
74	72, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉))
75		c0ex 9913	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
76		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
77	75, 76	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))
78	74, 77	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
79		imain 5888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
80	4, 79	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
81		fzdisj 12239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
82	29, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
83	82	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅))
84		ima0 5400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 “ ∅) = ∅
85	83, 84	syl6eq 2660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅)
86	80, 85	eqtr3d 2646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅)
87		fnun 5911	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
88	78, 86, 87	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
89		imaundi 5464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
90	10	nnzd 11357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℤ)
91		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
93		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
95		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
96	94, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
97	13, 96	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1)))
98		fzss2 12252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
100	99, 7	sseldd 3569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 ∈ (1...𝑁))
101		fzsplit 12238	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
103	102	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))))
104		f1ofo 6057	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
105	1, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁))
106		foima 6033	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
107	105, 106	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
108	103, 107	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁))
109	89, 108	syl5eqr 2658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁))
110	109	fneq2d 5896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
111	88, 110	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
112	111	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
113		fzfid 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin)
114		inidm 3784	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
115		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
116		fvun1 6179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
117	74, 77, 116	mp3an12 1406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
118	86, 117	sylan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
119	72	fvconst2 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
120	119	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
121	118, 120	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
122	121	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
123	71, 112, 113, 113, 114, 115, 122	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
124		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))))
125	72, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1)))
126		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
127	75, 126	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))
128	125, 127	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
129		imain 5888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
130	4, 129	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
131		fzdisj 12239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
132	40, 131	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
133	132	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
134	133, 84	syl6eq 2660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅)
135	130, 134	eqtr3d 2646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅)
136		fnun 5911	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
137	128, 135, 136	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
138		imaundi 5464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
139	17	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))))
140	139, 107	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
141	138, 140	syl5eqr 2658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
142	141	fneq2d 5896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
143	137, 142	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
144	143	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
145		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ ℤ → 𝑉 ∈ (ℤ≥‘𝑉))
146	27, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉))
147		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (ℤ≥‘𝑉) → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
149		fzss2 12252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1)))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...𝑉) ⊆ (1...(𝑉 + 1)))
151		imass2 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...𝑉) ⊆ (1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
152	150, 151	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
153	152	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))
154		fvun1 6179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
155	125, 127, 154	mp3an12 1406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
156	135, 155	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
157	72	fvconst2 6374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
158	157	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
159	156, 158	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
160	153, 159	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
161	160	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
162	71, 144, 113, 113, 114, 115, 161	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
163	123, 162	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
164	67, 163	mpdan 699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
165		imassrn 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈
166	165, 65	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁))
167	166	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
168	70	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
169	111	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
170		fzfid 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin)
171		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
172		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) ∈ ℤ → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
173	30, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
174		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
175	173, 174	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
176		fzss1 12251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
178		imass2 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
179	177, 178	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
180	179	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))
181		fvun2 6180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
182	74, 77, 181	mp3an12 1406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
183	86, 182	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
184	75	fvconst2 6374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
185	184	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
186	183, 185	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
187	180, 186	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
188	187	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
189	168, 169, 170, 170, 114, 171, 188	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
190	143	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
191		fvun2 6180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ∧ (((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
192	125, 127, 191	mp3an12 1406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
193	135, 192	sylan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
194	75	fvconst2 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
195	194	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
196	193, 195	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
197	196	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
198	168, 190, 170, 170, 114, 171, 197	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
199	189, 198	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
200	167, 199	mpdan 699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
201	164, 200	jaodan 822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
202	201	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
203		poimirlem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
204	203	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
205		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
206		ovex 6577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 + 1) ∈ V
207	205, 206	ifex 4106	. . . . . . . . . . . . . . . 16 ⊢ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
208	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
209		breq1 4586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
210	209	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
211		simpr 476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1))
212		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1))
213	27	zcnd 11359	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 ∈ ℂ)
214		npcan1 10334	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉)
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 − 1) + 1) = 𝑉)
216	212, 215	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉)
217	210, 211, 216	ifbieq12d 4063	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
218	217	adantlr 747	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
219		poimirlem2.5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
220	219	eldifad 3552	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
221		elfzelz 12213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ)
222	220, 221	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℤ)
223		zltlem1 11307	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
224	222, 27, 223	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
225	222	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℝ)
226		peano2zm 11297	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑉 ∈ ℤ → (𝑉 − 1) ∈ ℤ)
227	27, 226	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑉 − 1) ∈ ℤ)
228	227	zred 11358	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 − 1) ∈ ℝ)
229	225, 228	lenltd 10062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀))
230	224, 229	bitrd 267	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀))
231	230	biimpa 500	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀)
232	231	iffalsed 4047	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
233	232	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
234	218, 233	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
235	234	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
236	235	biimpa 500	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
237		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉))
238	237	imaeq2d 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉)))
239	238	xpeq1d 5062	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1}))
240		oveq1 6556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1))
241	240	oveq1d 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
242	241	imaeq2d 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁)))
243	242	xpeq1d 5062	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))
244	239, 243	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))
245	244	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑉 → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
246	236, 245	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
247	208, 246	csbied 3526	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
248		elfzm1b 12287	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
249	27, 90, 248	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
250	100, 249	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
251	250	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
252		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V
253	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
254	204, 247, 251, 253	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
255	254	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
256	255	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
257	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
258		breq1 4586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
259		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → 𝑦 = 𝑉)
260		oveq1 6556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1))
261	258, 259, 260	ifbieq12d 4063	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
262		ltnsym 10014	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
263	225, 28, 262	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
264	263	imp 444	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀)
265	264	iffalsed 4047	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
266	261, 265	sylan9eqr 2666	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
267	266	eqeq2d 2620	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
268	267	biimpa 500	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1))
269		oveq2 6557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1)))
270	269	imaeq2d 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1))))
271	270	xpeq1d 5062	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1}))
272		oveq1 6556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1))
273	272	oveq1d 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
274	273	imaeq2d 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
275	274	xpeq1d 5062	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))
276	271, 275	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))
277	276	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑉 + 1) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
278	268, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
279	257, 278	csbied 3526	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
280		1eluzge0 11608	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ (ℤ≥‘0)
281		fzss1 12251	. . . . . . . . . . . . . . . . 17 ⊢ (1 ∈ (ℤ≥‘0) → (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1)))
282	280, 281	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
283	282, 7	sseldi 3566	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (0...(𝑁 − 1)))
284	283	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1)))
285		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V
286	285	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V)
287	204, 279, 284, 286	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
288	287	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
289	288	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
290	202, 256, 289	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
291	290	ex 449	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
292	60, 291	sylbid 229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
293	292	expdimp 452	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
294	293	necon1ad 2799	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
295		elimasni 5411	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛)
296		eqcom 2617	. . . . . . . . 9 ⊢ (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛)
297		f1ofn 6051	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
298	1, 297	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
299		fnbrfvb 6146	. . . . . . . . . 10 ⊢ ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
300	298, 15, 299	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
301	296, 300	syl5bb 271	. . . . . . . 8 ⊢ (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛))
302	295, 301	syl5ibr 235	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
303	302	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
304	294, 303	syld 46	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
305	304	ralrimiva 2949	. . . 4 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
306		fvex 6113	. . . . 5 ⊢ (𝑈‘(𝑉 + 1)) ∈ V
307		eqeq2 2621	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1))))
308	307	imbi2d 329	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
309	308	ralbidv 2969	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
310	306, 309	spcev 3273	. . . 4 ⊢ (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
311	305, 310	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
312		imadif 5887	. . . . . . . . . . . . . . 15 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
313	4, 312	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
314	102	difeq1d 3689	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}))
315		difundir 3839	. . . . . . . . . . . . . . . . 17 ⊢ (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉}))
316	215, 21	eqeltrd 2688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘1))
317		uzid 11578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 − 1) ∈ ℤ → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
318	227, 317	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
319		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
320	318, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
321	215, 320	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1)))
322		fzsplit2 12237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
323	316, 321, 322	syl2anc 691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
324	215	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉))
325		fzsn 12254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉})
326	27, 325	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉...𝑉) = {𝑉})
327	324, 326	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉})
328	327	uneq2d 3729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉}))
329	323, 328	eqtrd 2644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉}))
330	329	difeq1d 3689	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}))
331		difun2 4000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉})
332	28	ltm1d 10835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 1) < 𝑉)
333	228, 28	ltnled 10063	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1)))
334	332, 333	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1))
335		elfzle2 12216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1))
336	334, 335	nsyl 134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1)))
337		difsn 4269	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
338	336, 337	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
339	331, 338	syl5eq 2656	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1)))
340	330, 339	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1)))
341		elfzle1 12215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉)
342	33, 341	nsyl 134	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
343		difsn 4269	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
344	342, 343	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
345	340, 344	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
346	315, 345	syl5eq 2656	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
347	314, 346	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
348	347	imaeq2d 5385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
349	313, 348	eqtr3d 2646	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
350		imaundi 5464	. . . . . . . . . . . . 13 ⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
351	349, 350	syl6eq 2660	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
352	351	eleq2d 2673	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))))
353		eldif 3550	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})))
354		elun 3715	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))
355	352, 353, 354	3bitr3g 301	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
356	355	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
357		imassrn 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈
358	357, 65	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁))
359	358	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁))
360	70	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁))
361		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))))
362	72, 361	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1)))
363		fnconstg 6006	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
364	75, 363	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))
365	362, 364	pm3.2i 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
366		imain 5888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
367	4, 366	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
368		fzdisj 12239	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
369	332, 368	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
370	369	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅))
371	370, 84	syl6eq 2660	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅)
372	367, 371	eqtr3d 2646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅)
373		fnun 5911	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
374	365, 372, 373	sylancr 694	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
375		imaundi 5464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))
376		uzss 11584	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
377	321, 376	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
378		elfzuz3 12210	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
379	7, 378	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
380	377, 379	sseldd 3569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
381		peano2uz 11617	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
382	380, 381	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
383	13, 382	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1)))
384		fzsplit2 12237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
385	316, 383, 384	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
386	215	oveq1d 6564	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁))
387	386	uneq2d 3729	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
388	385, 387	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
389	388	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))))
390	389, 107	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁))
391	375, 390	syl5eqr 2658	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁))
392	391	fneq2d 5896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)))
393	374, 392	mpbid 221	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
394	393	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
395		fzfid 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin)
396		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
397		fvun1 6179	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
398	362, 364, 397	mp3an12 1406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
399	372, 398	sylan 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
400	72	fvconst2 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
401	400	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
402	399, 401	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
403	402	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
404	360, 394, 395, 395, 114, 396, 403	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
405	111	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
406		fzss2 12252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉))
407	321, 406	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉))
408		imass2 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...(𝑉 − 1)) ⊆ (1...𝑉) → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
409	407, 408	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
410	409	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉)))
411	410, 121	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
412	411	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
413	360, 405, 395, 395, 114, 396, 412	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
414	404, 413	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
415	359, 414	mpdan 699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
416		imassrn 5396	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈
417	416, 65	syl5ss 3579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁))
418	417	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
419	70	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
420	393	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
421		fzfid 12634	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin)
422		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
423		fzss1 12251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
424	148, 423	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
425		imass2 5420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
426	424, 425	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
427	426	sselda 3568	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))
428		fvun2 6180	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
429	362, 364, 428	mp3an12 1406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
430	372, 429	sylan 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
431	75	fvconst2 6374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
432	431	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
433	430, 432	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
434	427, 433	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
435	434	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
436	419, 420, 421, 421, 114, 422, 435	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
437	111	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
438	186	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
439	419, 437, 421, 421, 114, 422, 438	ofval 6804	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
440	436, 439	eqtr4d 2647	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
441	418, 440	mpdan 699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
442	415, 441	jaodan 822	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
443	442	adantlr 747	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
444	203	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
445	207	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
446	217	adantlr 747	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
447		lttr 9993	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 − 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
448	228, 28, 225, 447	syl3anc 1318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
449	332, 448	mpand 707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀))
450	449	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)
451	450	iftrued 4044	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
452	451	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
453	446, 452	eqtrd 2644	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1))
454		simpll 786	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑)
455		oveq2 6557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1)))
456	455	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1))))
457	456	xpeq1d 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
458	457	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
459		oveq1 6556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1))
460	459, 215	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉)
461	460	oveq1d 6564	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
462	461	imaeq2d 5385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁)))
463	462	xpeq1d 5062	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0}))
464	458, 463	uneq12d 3730	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))
465	464	oveq2d 6565	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
466	454, 465	sylan 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
467	445, 453, 466	csbied2 3527	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
468	250	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
469		ovex 6577	. . . . . . . . . . . . . . 15 ⊢ (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V
470	469	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V)
471	444, 467, 468, 470	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
472	471	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
473	472	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
474	207	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
475		iftrue 4042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
476	261, 475	sylan9eqr 2666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
477	476	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
478	477	biimpa 500	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
479	478, 245	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
480	474, 479	csbied 3526	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
481	480	adantll 746	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
482	283	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1)))
483	252	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
484	444, 481, 482, 483	fvmptd 6197	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
485	484	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
486	485	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
487	443, 473, 486	3eqtr4d 2654	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
488	487	ex 449	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
489	356, 488	sylbid 229	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
490	489	expdimp 452	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
491	490	necon1ad 2799	. . . . . 6 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉})))
492		elimasni 5411	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛)
493		eqcom 2617	. . . . . . . . 9 ⊢ (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛)
494		fnbrfvb 6146	. . . . . . . . . 10 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
495	298, 100, 494	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
496	493, 495	syl5bb 271	. . . . . . . 8 ⊢ (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛))
497	492, 496	syl5ibr 235	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
498	497	ad2antrr 758	. . . . . 6 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
499	491, 498	syld 46	. . . . 5 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
500	499	ralrimiva 2949	. . . 4 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
501		fvex 6113	. . . . 5 ⊢ (𝑈‘𝑉) ∈ V
502		eqeq2 2621	. . . . . . 7 ⊢ (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉)))
503	502	imbi2d 329	. . . . . 6 ⊢ (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
504	503	ralbidv 2969	. . . . 5 ⊢ (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
505	501, 504	spcev 3273	. . . 4 ⊢ (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
506	500, 505	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
507		eldifsni 4261	. . . . 5 ⊢ (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉)
508	219, 507	syl 17	. . . 4 ⊢ (𝜑 → 𝑀 ≠ 𝑉)
509	225, 28	lttri2d 10055	. . . 4 ⊢ (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
510	508, 509	mpbid 221	. . 3 ⊢ (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
511	311, 506, 510	mpjaodan 823	. 2 ⊢ (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
512		nfv 1830	. . . 4 ⊢ Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)
513	512	rmo2 3492	. . 3 ⊢ (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
514		rmoeq1 3118	. . . 4 ⊢ ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
515	107, 514	syl 17	. . 3 ⊢ (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
516	513, 515	syl5bbr 273	. 2 ⊢ (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
517	511, 516	mpbid 221	1 ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃*wrmo 2899  Vcvv 3173  ⦋csb 3499   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   × cxp 5036  ^◡ccnv 5037  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549   ∘_𝑓 cof 6793  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℤcz 11254  ℤ_≥cuz 11563  ...cfz 12197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198

This theorem is referenced by:  poimirlem8  32587  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601