Theorem poimirlem2 34438

Description: Lemma for poimir 34469- 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 6492	. . . . . . . . . . . . . . . . 17 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ◡𝑈))
3	2	simprbi 497	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ◡𝑈)
4	1, 3	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → Fun ◡𝑈)
5		imadif 6311	. . . . . . . . . . . . . . 15 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
6	4, 5	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})))
7		poimirlem2.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑉 ∈ (1...(𝑁 − 1)))
8		fzp1elp1 12810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
9	7, 8	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑉 + 1) ∈ (1...((𝑁 − 1) + 1)))
10		poimir.0	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑁 ∈ ℕ)
11	10	nncnd 11504	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑁 ∈ ℂ)
12		npcan1 10915	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
13	11, 12	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
14	13	oveq2d 7035	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
15	9, 14	eleqtrd 2884	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑉 + 1) ∈ (1...𝑁))
16		fzsplit 12783	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
17	15, 16	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)))
18	17	difeq1d 4021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}))
19		difundir 4179	. . . . . . . . . . . . . . . . 17 ⊢ (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}))
20		elfzuz 12754	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ (ℤ≥‘1))
21	7, 20	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘1))
22		fzsuc 12804	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (ℤ≥‘1) → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
23	21, 22	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...(𝑉 + 1)) = ((1...𝑉) ∪ {(𝑉 + 1)}))
24	23	difeq1d 4021	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}))
25		difun2 4345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∖ {(𝑉 + 1)})
26		elfzelz 12758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → 𝑉 ∈ ℤ)
27	7, 26	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑉 ∈ ℤ)
28	27	zred 11937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑉 ∈ ℝ)
29	28	ltp1d 11420	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 < (𝑉 + 1))
30	27	peano2zd 11940	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑉 + 1) ∈ ℤ)
31	30	zred 11937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 + 1) ∈ ℝ)
32	28, 31	ltnled 10636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 < (𝑉 + 1) ↔ ¬ (𝑉 + 1) ≤ 𝑉))
33	29, 32	mpbid 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ (𝑉 + 1) ≤ 𝑉)
34		elfzle2 12761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 + 1) ∈ (1...𝑉) → (𝑉 + 1) ≤ 𝑉)
35	33, 34	nsyl 142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (1...𝑉))
36		difsn 4640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑉 + 1) ∈ (1...𝑉) → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
37	35, 36	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑉) ∖ {(𝑉 + 1)}) = (1...𝑉))
38	25, 37	syl5eq 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((1...𝑉) ∪ {(𝑉 + 1)}) ∖ {(𝑉 + 1)}) = (1...𝑉))
39	24, 38	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) = (1...𝑉))
40	31	ltp1d 11420	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑉 + 1) < ((𝑉 + 1) + 1))
41		peano2re 10662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) ∈ ℝ → ((𝑉 + 1) + 1) ∈ ℝ)
42	31, 41	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ ℝ)
43	31, 42	ltnled 10636	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑉 + 1) < ((𝑉 + 1) + 1) ↔ ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1)))
44	40, 43	mpbid 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ¬ ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
45		elfzle1 12760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((𝑉 + 1) + 1) ≤ (𝑉 + 1))
46	44, 45	nsyl 142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁))
47		difsn 4640	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ (𝑉 + 1) ∈ (((𝑉 + 1) + 1)...𝑁) → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
48	46, 47	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)}) = (((𝑉 + 1) + 1)...𝑁))
49	39, 48	uneq12d 4063	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((1...(𝑉 + 1)) ∖ {(𝑉 + 1)}) ∪ ((((𝑉 + 1) + 1)...𝑁) ∖ {(𝑉 + 1)})) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
50	19, 49	syl5eq 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁)) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
51	18, 50	eqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) ∖ {(𝑉 + 1)}) = ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁)))
52	51	imaeq2d 5809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
53	6, 52	eqtr3d 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))))
54		imaundi 5887	. . . . . . . . . . . . 13 ⊢ (𝑈 “ ((1...𝑉) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
55	53, 54	syl6eq 2846	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
56	55	eleq2d 2867	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ 𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
57		eldif 3871	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
58		elun 4048	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
59	56, 57, 58	3bitr3g 314	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
60	59	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))))
61		imassrn 5820	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (1...𝑉)) ⊆ ran 𝑈
62		f1of 6486	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
63	1, 62	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
64	63	frnd 6392	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
65	61, 64	sstrid 3902	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (1...𝑁))
66	65	sselda 3891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (1...𝑁))
67		poimirlem2.2	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
68	67	ffnd 6386	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
69	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑇 Fn (1...𝑁))
70		1ex 10486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1 ∈ V
71		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)))
72	70, 71	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉))
73		c0ex 10484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ V
74		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
75	73, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))
76	72, 75	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)))
77		imain 6312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
78	4, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))))
79		fzdisj 12784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 < (𝑉 + 1) → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
80	29, 79	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑉) ∩ ((𝑉 + 1)...𝑁)) = ∅)
81	80	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = (𝑈 “ ∅))
82		ima0 5824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑈 “ ∅) = ∅
83	81, 82	syl6eq 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∩ ((𝑉 + 1)...𝑁))) = ∅)
84	78, 83	eqtr3d 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅)
85		fnun 6336	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ ((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
86	76, 84, 85	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
87		imaundi 5887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
88	10	nnzd 11936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → 𝑁 ∈ ℤ)
89		peano2zm 11875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
90	88, 89	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
91		uzid 12108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
92	90, 91	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)))
93		peano2uz 12150	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
94	92, 93	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑁 − 1)))
95	13, 94	eqeltrrd 2883	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑁 − 1)))
96		fzss2 12797	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
97	95, 96	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
98	97, 7	sseldd 3892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 ∈ (1...𝑁))
99		fzsplit 12783	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
100	98, 99	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...𝑁) = ((1...𝑉) ∪ ((𝑉 + 1)...𝑁)))
101	100	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))))
102		f1ofo 6493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
103	1, 102	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–onto→(1...𝑁))
104		foima 6466	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
106	101, 105	eqtr3d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...𝑉) ∪ ((𝑉 + 1)...𝑁))) = (1...𝑁))
107	87, 106	syl5eqr 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) = (1...𝑁))
108	107	fneq2d 6320	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...𝑉)) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁)))
109	86, 108	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
110	109	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
111		fzfid 13191	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (1...𝑁) ∈ Fin)
112		inidm 4117	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
113		eqidd 2795	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
114		fvun1 6624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
115	72, 75, 114	mp3an12 1443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
116	84, 115	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...𝑉)) × {1})‘𝑛))
117	70	fvconst2 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (1...𝑉)) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
118	117	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...𝑉)) × {1})‘𝑛) = 1)
119	116, 118	eqtrd 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
120	119	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
121	69, 110, 111, 111, 112, 113, 120	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
122		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))))
123	70, 122	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1)))
124		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
125	73, 124	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁))
126	123, 125	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...(𝑉 + 1))) × {1}) Fn (𝑈 “ (1...(𝑉 + 1))) ∧ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
127		imain 6312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
128	4, 127	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
129		fzdisj 12784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) < ((𝑉 + 1) + 1) → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
130	40, 129	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁)) = ∅)
131	130	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
132	131, 82	syl6eq 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∩ (((𝑉 + 1) + 1)...𝑁))) = ∅)
133	128, 132	eqtr3d 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅)
134		fnun 6336	. . . . . . . . . . . . . . . . . . 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)...𝑁))))
135	126, 133, 134	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))))
136		imaundi 5887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
137	17	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))))
138	137, 105	eqtr3d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 + 1)) ∪ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
139	136, 138	syl5eqr 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = (1...𝑁))
140	139	fneq2d 6320	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 + 1))) ∪ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
141	135, 140	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
142	141	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
143		uzid 12108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ ℤ → 𝑉 ∈ (ℤ≥‘𝑉))
144	27, 143	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘𝑉))
145		peano2uz 12150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (ℤ≥‘𝑉) → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
146	144, 145	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘𝑉))
147		fzss2 12797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → (1...𝑉) ⊆ (1...(𝑉 + 1)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...𝑉) ⊆ (1...(𝑉 + 1)))
149		imass2 5844	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...𝑉) ⊆ (1...(𝑉 + 1)) → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
150	148, 149	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (1...𝑉)) ⊆ (𝑈 “ (1...(𝑉 + 1))))
151	150	sselda 3891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))))
152		fvun1 6624	. . . . . . . . . . . . . . . . . . . . 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})‘𝑛))
153	123, 125, 152	mp3an12 1443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
154	133, 153	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛))
155	70	fvconst2 6836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 + 1))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
156	155	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → (((𝑈 “ (1...(𝑉 + 1))) × {1})‘𝑛) = 1)
157	154, 156	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 + 1)))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
158	151, 157	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
159	158	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
160	69, 142, 111, 111, 112, 113, 159	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
161	121, 160	eqtr4d 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
162	66, 161	mpdan 683	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...𝑉))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
163		imassrn 5820	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ ran 𝑈
164	163, 64	sstrid 3902	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (1...𝑁))
165	164	sselda 3891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
166	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
167	109	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
168		fzfid 13191	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (1...𝑁) ∈ Fin)
169		eqidd 2795	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
170		uzid 12108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 + 1) ∈ ℤ → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
171	30, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)))
172		peano2uz 12150	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘(𝑉 + 1)) → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
173	171, 172	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)))
174		fzss1 12796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 + 1) + 1) ∈ (ℤ≥‘(𝑉 + 1)) → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
175	173, 174	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁))
176		imass2 5844	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑉 + 1) + 1)...𝑁) ⊆ ((𝑉 + 1)...𝑁) → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
177	175, 176	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) ⊆ (𝑈 “ ((𝑉 + 1)...𝑁)))
178	177	sselda 3891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))
179		fvun2 6625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...𝑉)) × {1}) Fn (𝑈 “ (1...𝑉)) ∧ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑉 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
180	72, 75, 179	mp3an12 1443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...𝑉)) ∩ (𝑈 “ ((𝑉 + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
181	84, 180	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛))
182	73	fvconst2 6836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
183	182	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})‘𝑛) = 0)
184	181, 183	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
185	178, 184	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
186	185	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
187	166, 167, 168, 168, 112, 169, 186	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
188	141	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
189		fvun2 6625	. . . . . . . . . . . . . . . . . . . 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})‘𝑛))
190	123, 125, 189	mp3an12 1443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...(𝑉 + 1))) ∩ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
191	133, 190	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛))
192	73	fvconst2 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
193	192	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → (((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})‘𝑛) = 0)
194	191, 193	eqtrd 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
195	194	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 0)
196	166, 188, 168, 168, 112, 169, 195	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
197	187, 196	eqtr4d 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
198	165, 197	mpdan 683	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
199	162, 198	jaodan 952	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
200	199	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
201		poimirlem2.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
202	201	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
203		vex 3439	. . . . . . . . . . . . . . . . 17 ⊢ 𝑦 ∈ V
204		ovex 7051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 + 1) ∈ V
205	203, 204	ifex 4431	. . . . . . . . . . . . . . . 16 ⊢ if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V
206	205	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
207		breq1 4967	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑉 − 1) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
208	207	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 < 𝑀 ↔ (𝑉 − 1) < 𝑀))
209		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → 𝑦 = (𝑉 − 1))
210		oveq1 7026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = (𝑉 − 1) → (𝑦 + 1) = ((𝑉 − 1) + 1))
211	27	zcnd 11938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑉 ∈ ℂ)
212		npcan1 10915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑉 ∈ ℂ → ((𝑉 − 1) + 1) = 𝑉)
213	211, 212	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 − 1) + 1) = 𝑉)
214	210, 213	sylan9eqr 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → (𝑦 + 1) = 𝑉)
215	208, 209, 214	ifbieq12d 4410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
216	215	adantlr 711	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
217		poimirlem2.5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝑀 ∈ ((0...𝑁) ∖ {𝑉}))
218	217	eldifad 3873	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝑀 ∈ (0...𝑁))
219		elfzelz 12758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 ∈ (0...𝑁) → 𝑀 ∈ ℤ)
220	218, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℤ)
221		zltlem1 11885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
222	220, 27, 221	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑀 < 𝑉 ↔ 𝑀 ≤ (𝑉 − 1)))
223	220	zred 11937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℝ)
224		peano2zm 11875	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑉 ∈ ℤ → (𝑉 − 1) ∈ ℤ)
225	27, 224	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑉 − 1) ∈ ℤ)
226	225	zred 11937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 − 1) ∈ ℝ)
227	223, 226	lenltd 10635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑀 ≤ (𝑉 − 1) ↔ ¬ (𝑉 − 1) < 𝑀))
228	222, 227	bitrd 280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑀 < 𝑉 ↔ ¬ (𝑉 − 1) < 𝑀))
229	228	biimpa 477	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ (𝑉 − 1) < 𝑀)
230	229	iffalsed 4394	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
231	230	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = 𝑉)
232	216, 231	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
233	232	eqeq2d 2804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
234	233	biimpa 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
235		oveq2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑉 → (1...𝑗) = (1...𝑉))
236	235	imaeq2d 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑉 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑉)))
237	236	xpeq1d 5475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑉 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑉)) × {1}))
238		oveq1 7026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑉 → (𝑗 + 1) = (𝑉 + 1))
239	238	oveq1d 7034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑉 → ((𝑗 + 1)...𝑁) = ((𝑉 + 1)...𝑁))
240	239	imaeq2d 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑉 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑉 + 1)...𝑁)))
241	240	xpeq1d 5475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑉 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))
242	237, 241	uneq12d 4063	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝑉 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))
243	242	oveq2d 7035	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝑉 → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
244	234, 243	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
245	206, 244	csbied 3846	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
246		elfzm1b 12835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑉 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
247	27, 88, 246	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑉 ∈ (1...𝑁) ↔ (𝑉 − 1) ∈ (0...(𝑁 − 1))))
248	98, 247	mpbid 233	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
249	248	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
250		ovexd 7053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
251	202, 245, 249, 250	fvmptd 6644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
252	251	fveq1d 6543	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
253	252	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
254	205	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
255		breq1 4967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → (𝑦 < 𝑀 ↔ 𝑉 < 𝑀))
256		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → 𝑦 = 𝑉)
257		oveq1 7026	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑉 → (𝑦 + 1) = (𝑉 + 1))
258	255, 256, 257	ifbieq12d 4410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑉 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)))
259		ltnsym 10587	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
260	223, 28, 259	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑀 < 𝑉 → ¬ 𝑉 < 𝑀))
261	260	imp 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ¬ 𝑉 < 𝑀)
262	261	iffalsed 4394	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = (𝑉 + 1))
263	258, 262	sylan9eqr 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 + 1))
264	263	eqeq2d 2804	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = (𝑉 + 1)))
265	264	biimpa 477	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = (𝑉 + 1))
266		oveq2 7027	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 + 1) → (1...𝑗) = (1...(𝑉 + 1)))
267	266	imaeq2d 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 + 1))))
268	267	xpeq1d 5475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 + 1))) × {1}))
269		oveq1 7026	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑉 + 1) → (𝑗 + 1) = ((𝑉 + 1) + 1))
270	269	oveq1d 7034	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 + 1) → ((𝑗 + 1)...𝑁) = (((𝑉 + 1) + 1)...𝑁))
271	270	imaeq2d 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))
272	271	xpeq1d 5475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑉 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))
273	268, 272	uneq12d 4063	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑉 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))
274	273	oveq2d 7035	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑉 + 1) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
275	265, 274	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
276	254, 275	csbied 3846	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
277		fz1ssfz0 12853	. . . . . . . . . . . . . . . 16 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
278	277, 7	sseldi 3889	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑉 ∈ (0...(𝑁 − 1)))
279	278	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → 𝑉 ∈ (0...(𝑁 − 1)))
280		ovexd 7053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))) ∈ V)
281	202, 276, 279, 280	fvmptd 6644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0}))))
282	281	fveq1d 6543	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
283	282	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 + 1))) × {1}) ∪ ((𝑈 “ (((𝑉 + 1) + 1)...𝑁)) × {0})))‘𝑛))
284	200, 253, 283	3eqtr4d 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ (𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
285	284	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑉)) ∨ 𝑛 ∈ (𝑈 “ (((𝑉 + 1) + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
286	60, 285	sylbid 241	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
287	286	expdimp 453	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
288	287	necon1ad 3000	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {(𝑉 + 1)})))
289		elimasni 5835	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → (𝑉 + 1)𝑈𝑛)
290		eqcom 2801	. . . . . . . . 9 ⊢ (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑈‘(𝑉 + 1)) = 𝑛)
291		f1ofn 6487	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
292	1, 291	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
293		fnbrfvb 6589	. . . . . . . . . 10 ⊢ ((𝑈 Fn (1...𝑁) ∧ (𝑉 + 1) ∈ (1...𝑁)) → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
294	292, 15, 293	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘(𝑉 + 1)) = 𝑛 ↔ (𝑉 + 1)𝑈𝑛))
295	290, 294	syl5bb 284	. . . . . . . 8 ⊢ (𝜑 → (𝑛 = (𝑈‘(𝑉 + 1)) ↔ (𝑉 + 1)𝑈𝑛))
296	289, 295	syl5ibr 247	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
297	296	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {(𝑉 + 1)}) → 𝑛 = (𝑈‘(𝑉 + 1))))
298	288, 297	syld 47	. . . . 5 ⊢ (((𝜑 ∧ 𝑀 < 𝑉) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
299	298	ralrimiva 3148	. . . 4 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))))
300		fvex 6554	. . . . 5 ⊢ (𝑈‘(𝑉 + 1)) ∈ V
301		eqeq2 2805	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘(𝑉 + 1))))
302	301	imbi2d 342	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
303	302	ralbidv 3163	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑉 + 1)) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1)))))
304	300, 303	spcev 3547	. . . 4 ⊢ (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘(𝑉 + 1))) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
305	299, 304	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑀 < 𝑉) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
306		imadif 6311	. . . . . . . . . . . . . . 15 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
307	4, 306	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})))
308	100	difeq1d 4021	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}))
309		difundir 4179	. . . . . . . . . . . . . . . . 17 ⊢ (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉}))
310	213, 21	eqeltrd 2882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘1))
311		uzid 12108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑉 − 1) ∈ ℤ → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
312	225, 311	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
313		peano2uz 12150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑉 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
314	312, 313	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑉 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
315	213, 314	eqeltrrd 2883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘(𝑉 − 1)))
316		fzsplit2 12782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑉 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
317	310, 315, 316	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)))
318	213	oveq1d 7034	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = (𝑉...𝑉))
319		fzsn 12799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑉 ∈ ℤ → (𝑉...𝑉) = {𝑉})
320	27, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉...𝑉) = {𝑉})
321	318, 320	eqtrd 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑉) = {𝑉})
322	321	uneq2d 4062	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑉)) = ((1...(𝑉 − 1)) ∪ {𝑉}))
323	317, 322	eqtrd 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...𝑉) = ((1...(𝑉 − 1)) ∪ {𝑉}))
324	323	difeq1d 4021	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}))
325		difun2 4345	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∖ {𝑉})
326	28	ltm1d 11422	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑉 − 1) < 𝑉)
327	226, 28	ltnled 10636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑉 − 1) < 𝑉 ↔ ¬ 𝑉 ≤ (𝑉 − 1)))
328	326, 327	mpbid 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ¬ 𝑉 ≤ (𝑉 − 1))
329		elfzle2 12761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑉 ∈ (1...(𝑉 − 1)) → 𝑉 ≤ (𝑉 − 1))
330	328, 329	nsyl 142	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ¬ 𝑉 ∈ (1...(𝑉 − 1)))
331		difsn 4640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ 𝑉 ∈ (1...(𝑉 − 1)) → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
332	330, 331	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∖ {𝑉}) = (1...(𝑉 − 1)))
333	325, 332	syl5eq 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((1...(𝑉 − 1)) ∪ {𝑉}) ∖ {𝑉}) = (1...(𝑉 − 1)))
334	324, 333	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((1...𝑉) ∖ {𝑉}) = (1...(𝑉 − 1)))
335		elfzle1 12760	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 ∈ ((𝑉 + 1)...𝑁) → (𝑉 + 1) ≤ 𝑉)
336	33, 335	nsyl 142	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ¬ 𝑉 ∈ ((𝑉 + 1)...𝑁))
337		difsn 4640	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ 𝑉 ∈ ((𝑉 + 1)...𝑁) → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
338	336, 337	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑉 + 1)...𝑁) ∖ {𝑉}) = ((𝑉 + 1)...𝑁))
339	334, 338	uneq12d 4063	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((1...𝑉) ∖ {𝑉}) ∪ (((𝑉 + 1)...𝑁) ∖ {𝑉})) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
340	309, 339	syl5eq 2842	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((1...𝑉) ∪ ((𝑉 + 1)...𝑁)) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
341	308, 340	eqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑉}) = ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁)))
342	341	imaeq2d 5809	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
343	307, 342	eqtr3d 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))))
344		imaundi 5887	. . . . . . . . . . . . 13 ⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ ((𝑉 + 1)...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))
345	343, 344	syl6eq 2846	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))))
346	345	eleq2d 2867	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ 𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁)))))
347		eldif 3871	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})))
348		elun 4048	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ ((𝑉 + 1)...𝑁))) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))))
349	346, 347, 348	3bitr3g 314	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
350	349	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) ↔ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))))
351		imassrn 5820	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ (1...(𝑉 − 1))) ⊆ ran 𝑈
352	351, 64	sstrid 3902	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (1...𝑁))
353	352	sselda 3891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (1...𝑁))
354	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑇 Fn (1...𝑁))
355		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))))
356	70, 355	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1)))
357		fnconstg 6438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 ∈ V → ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
358	73, 357	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))
359	356, 358	pm3.2i 471	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)))
360		imain 6312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ◡𝑈 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
361	4, 360	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))))
362		fzdisj 12784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑉 − 1) < 𝑉 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
363	326, 362	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∩ (𝑉...𝑁)) = ∅)
364	363	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = (𝑈 “ ∅))
365	364, 82	syl6eq 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∩ (𝑉...𝑁))) = ∅)
366	361, 365	eqtr3d 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅)
367		fnun 6336	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁))) ∧ ((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
368	359, 366, 367	sylancr 587	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))))
369		imaundi 5887	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁)))
370		uzss 12114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
371	315, 370	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (ℤ≥‘𝑉) ⊆ (ℤ≥‘(𝑉 − 1)))
372		elfzuz3 12755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑉 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
373	7, 372	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘𝑉))
374	371, 373	sseldd 3892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)))
375		peano2uz 12150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑁 − 1) ∈ (ℤ≥‘(𝑉 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
376	374, 375	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ≥‘(𝑉 − 1)))
377	13, 376	eqeltrrd 2883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(𝑉 − 1)))
378		fzsplit2 12782	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑉 − 1) + 1) ∈ (ℤ≥‘1) ∧ 𝑁 ∈ (ℤ≥‘(𝑉 − 1))) → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
379	310, 377, 378	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)))
380	213	oveq1d 7034	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (((𝑉 − 1) + 1)...𝑁) = (𝑉...𝑁))
381	380	uneq2d 4062	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑉 − 1)) ∪ (((𝑉 − 1) + 1)...𝑁)) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
382	379, 381	eqtrd 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑉 − 1)) ∪ (𝑉...𝑁)))
383	382	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))))
384	383, 105	eqtr3d 2832	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑉 − 1)) ∪ (𝑉...𝑁))) = (1...𝑁))
385	369, 384	syl5eqr 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) = (1...𝑁))
386	385	fneq2d 6320	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑉 − 1))) ∪ (𝑈 “ (𝑉...𝑁))) ↔ (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁)))
387	368, 386	mpbid 233	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
388	387	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
389		fzfid 13191	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (1...𝑁) ∈ Fin)
390		eqidd 2795	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
391		fvun1 6624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
392	356, 358, 391	mp3an12 1443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
393	366, 392	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛))
394	70	fvconst2 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
395	394	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...(𝑉 − 1))) × {1})‘𝑛) = 1)
396	393, 395	eqtrd 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
397	396	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 1)
398	354, 388, 389, 389, 112, 390, 397	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
399	109	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
400		fzss2 12797	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑉 ∈ (ℤ≥‘(𝑉 − 1)) → (1...(𝑉 − 1)) ⊆ (1...𝑉))
401	315, 400	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (1...(𝑉 − 1)) ⊆ (1...𝑉))
402		imass2 5844	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1...(𝑉 − 1)) ⊆ (1...𝑉) → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
403	401, 402	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ (1...(𝑉 − 1))) ⊆ (𝑈 “ (1...𝑉)))
404	403	sselda 3891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → 𝑛 ∈ (𝑈 “ (1...𝑉)))
405	404, 119	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
406	405	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 1)
407	354, 399, 389, 389, 112, 390, 406	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
408	398, 407	eqtr4d 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
409	353, 408	mpdan 683	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (1...(𝑉 − 1)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
410		imassrn 5820	. . . . . . . . . . . . . . . 16 ⊢ (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ ran 𝑈
411	410, 64	sstrid 3902	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (1...𝑁))
412	411	sselda 3891	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (1...𝑁))
413	68	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑇 Fn (1...𝑁))
414	387	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})) Fn (1...𝑁))
415		fzfid 13191	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (1...𝑁) ∈ Fin)
416		eqidd 2795	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
417		fzss1 12796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑉 + 1) ∈ (ℤ≥‘𝑉) → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
418	146, 417	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁))
419		imass2 5844	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 + 1)...𝑁) ⊆ (𝑉...𝑁) → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
420	418, 419	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑈 “ ((𝑉 + 1)...𝑁)) ⊆ (𝑈 “ (𝑉...𝑁)))
421	420	sselda 3891	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))
422		fvun2 6625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) × {1}) Fn (𝑈 “ (1...(𝑉 − 1))) ∧ ((𝑈 “ (𝑉...𝑁)) × {0}) Fn (𝑈 “ (𝑉...𝑁)) ∧ (((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁)))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
423	356, 358, 422	mp3an12 1443	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑈 “ (1...(𝑉 − 1))) ∩ (𝑈 “ (𝑉...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
424	366, 423	sylan 580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛))
425	73	fvconst2 6836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ (𝑈 “ (𝑉...𝑁)) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
426	425	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → (((𝑈 “ (𝑉...𝑁)) × {0})‘𝑛) = 0)
427	424, 426	eqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑉...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
428	421, 427	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
429	428	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))‘𝑛) = 0)
430	413, 414, 415, 415, 112, 416, 429	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
431	109	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})) Fn (1...𝑁))
432	184	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))‘𝑛) = 0)
433	413, 431, 415, 415, 112, 416, 432	ofval 7279	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
434	430, 433	eqtr4d 2833	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
435	412, 434	mpdan 683	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
436	409, 435	jaodan 952	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
437	436	adantlr 711	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
438	201	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
439	205	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
440	215	adantlr 711	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉))
441		lttr 10566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 − 1) ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑀 ∈ ℝ) → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
442	226, 28, 223, 441	syl3anc 1364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (((𝑉 − 1) < 𝑉 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀))
443	326, 442	mpand 691	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑉 < 𝑀 → (𝑉 − 1) < 𝑀))
444	443	imp 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) < 𝑀)
445	444	iftrued 4391	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
446	445	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if((𝑉 − 1) < 𝑀, (𝑉 − 1), 𝑉) = (𝑉 − 1))
447	440, 446	eqtrd 2830	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑉 − 1))
448		simpll 763	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → 𝜑)
449		oveq2 7027	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑉 − 1) → (1...𝑗) = (1...(𝑉 − 1)))
450	449	imaeq2d 5809	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑉 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑉 − 1))))
451	450	xpeq1d 5475	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑉 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
452	451	adantl 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑉 − 1))) × {1}))
453		oveq1 7026	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑉 − 1) → (𝑗 + 1) = ((𝑉 − 1) + 1))
454	453, 213	sylan9eqr 2852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑗 + 1) = 𝑉)
455	454	oveq1d 7034	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑗 + 1)...𝑁) = (𝑉...𝑁))
456	455	imaeq2d 5809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑉...𝑁)))
457	456	xpeq1d 5475	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑉...𝑁)) × {0}))
458	452, 457	uneq12d 4063	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))
459	458	oveq2d 7035	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
460	448, 459	sylan 580	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) ∧ 𝑗 = (𝑉 − 1)) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
461	439, 447, 460	csbied2 3847	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = (𝑉 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
462	248	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑉 − 1) ∈ (0...(𝑁 − 1)))
463		ovexd 7053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))) ∈ V)
464	438, 461, 462, 463	fvmptd 6644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘(𝑉 − 1)) = (𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0}))))
465	464	fveq1d 6543	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
466	465	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...(𝑉 − 1))) × {1}) ∪ ((𝑈 “ (𝑉...𝑁)) × {0})))‘𝑛))
467	205	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ∈ V)
468		iftrue 4389	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑉 < 𝑀 → if(𝑉 < 𝑀, 𝑉, (𝑉 + 1)) = 𝑉)
469	258, 468	sylan9eqr 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = 𝑉)
470	469	eqeq2d 2804	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → (𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) ↔ 𝑗 = 𝑉))
471	470	biimpa 477	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → 𝑗 = 𝑉)
472	471, 243	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) ∧ 𝑗 = if(𝑦 < 𝑀, 𝑦, (𝑦 + 1))) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
473	467, 472	csbied 3846	. . . . . . . . . . . . . . 15 ⊢ ((𝑉 < 𝑀 ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
474	473	adantll 710	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑦 = 𝑉) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
475	278	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → 𝑉 ∈ (0...(𝑁 − 1)))
476		ovexd 7053	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))) ∈ V)
477	438, 474, 475, 476	fvmptd 6644	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → (𝐹‘𝑉) = (𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0}))))
478	477	fveq1d 6543	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
479	478	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘𝑉)‘𝑛) = ((𝑇 ∘𝑓 + (((𝑈 “ (1...𝑉)) × {1}) ∪ ((𝑈 “ ((𝑉 + 1)...𝑁)) × {0})))‘𝑛))
480	437, 466, 479	3eqtr4d 2840	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ (𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁)))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛))
481	480	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...(𝑉 − 1))) ∨ 𝑛 ∈ (𝑈 “ ((𝑉 + 1)...𝑁))) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
482	350, 481	sylbid 241	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ((𝑛 ∈ (𝑈 “ (1...𝑁)) ∧ ¬ 𝑛 ∈ (𝑈 “ {𝑉})) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
483	482	expdimp 453	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (¬ 𝑛 ∈ (𝑈 “ {𝑉}) → ((𝐹‘(𝑉 − 1))‘𝑛) = ((𝐹‘𝑉)‘𝑛)))
484	483	necon1ad 3000	. . . . . 6 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 ∈ (𝑈 “ {𝑉})))
485		elimasni 5835	. . . . . . . 8 ⊢ (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑉𝑈𝑛)
486		eqcom 2801	. . . . . . . . 9 ⊢ (𝑛 = (𝑈‘𝑉) ↔ (𝑈‘𝑉) = 𝑛)
487		fnbrfvb 6589	. . . . . . . . . 10 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑉 ∈ (1...𝑁)) → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
488	292, 98, 487	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘𝑉) = 𝑛 ↔ 𝑉𝑈𝑛))
489	486, 488	syl5bb 284	. . . . . . . 8 ⊢ (𝜑 → (𝑛 = (𝑈‘𝑉) ↔ 𝑉𝑈𝑛))
490	485, 489	syl5ibr 247	. . . . . . 7 ⊢ (𝜑 → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
491	490	ad2antrr 722	. . . . . 6 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (𝑛 ∈ (𝑈 “ {𝑉}) → 𝑛 = (𝑈‘𝑉)))
492	484, 491	syld 47	. . . . 5 ⊢ (((𝜑 ∧ 𝑉 < 𝑀) ∧ 𝑛 ∈ (𝑈 “ (1...𝑁))) → (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
493	492	ralrimiva 3148	. . . 4 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)))
494		fvex 6554	. . . . 5 ⊢ (𝑈‘𝑉) ∈ V
495		eqeq2 2805	. . . . . . 7 ⊢ (𝑚 = (𝑈‘𝑉) → (𝑛 = 𝑚 ↔ 𝑛 = (𝑈‘𝑉)))
496	495	imbi2d 342	. . . . . 6 ⊢ (𝑚 = (𝑈‘𝑉) → ((((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ (((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
497	496	ralbidv 3163	. . . . 5 ⊢ (𝑚 = (𝑈‘𝑉) → (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉))))
498	494, 497	spcev 3547	. . . 4 ⊢ (∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = (𝑈‘𝑉)) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
499	493, 498	syl 17	. . 3 ⊢ ((𝜑 ∧ 𝑉 < 𝑀) → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
500		eldifsni 4631	. . . . 5 ⊢ (𝑀 ∈ ((0...𝑁) ∖ {𝑉}) → 𝑀 ≠ 𝑉)
501	217, 500	syl 17	. . . 4 ⊢ (𝜑 → 𝑀 ≠ 𝑉)
502	223, 28	lttri2d 10628	. . . 4 ⊢ (𝜑 → (𝑀 ≠ 𝑉 ↔ (𝑀 < 𝑉 ∨ 𝑉 < 𝑀)))
503	501, 502	mpbid 233	. . 3 ⊢ (𝜑 → (𝑀 < 𝑉 ∨ 𝑉 < 𝑀))
504	305, 499, 503	mpjaodan 953	. 2 ⊢ (𝜑 → ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
505		nfv 1893	. . . 4 ⊢ Ⅎ𝑚((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)
506	505	rmo2 3800	. . 3 ⊢ (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚))
507		rmoeq1 3367	. . . 4 ⊢ ((𝑈 “ (1...𝑁)) = (1...𝑁) → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
508	105, 507	syl 17	. . 3 ⊢ (𝜑 → (∃*𝑛 ∈ (𝑈 “ (1...𝑁))((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
509	506, 508	syl5bbr 286	. 2 ⊢ (𝜑 → (∃𝑚∀𝑛 ∈ (𝑈 “ (1...𝑁))(((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛) → 𝑛 = 𝑚) ↔ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛)))
510	504, 509	mpbid 233	1 ⊢ (𝜑 → ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑉 − 1))‘𝑛) ≠ ((𝐹‘𝑉)‘𝑛))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   = wceq 1522  ∃wex 1762   ∈ wcel 2080   ≠ wne 2983  ∀wral 3104  ∃*wrmo 3107  Vcvv 3436  ⦋csb 3813   ∖ cdif 3858   ∪ cun 3859   ∩ cin 3860   ⊆ wss 3861  ∅c0 4213  ifcif 4383  {csn 4474   class class class wbr 4964   ↦ cmpt 5043   × cxp 5444  ^◡ccnv 5445  ran crn 5447   “ cima 5449  Fun wfun 6222   Fn wfn 6223  ⟶wf 6224  –onto→wfo 6226  –1-1-onto→wf1o 6227  ‘cfv 6228  (class class class)co 7019   ∘_𝑓 cof 7268  Fincfn 8360  ℂcc 10384  ℝcr 10385  0cc0 10386  1c1 10387   + caddc 10389   < clt 10524   ≤ cle 10525   − cmin 10719  ℕcn 11488  ℤcz 11831  ℤ_≥cuz 12093  ...cfz 12742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322  ax-cnex 10442  ax-resscn 10443  ax-1cn 10444  ax-icn 10445  ax-addcl 10446  ax-addrcl 10447  ax-mulcl 10448  ax-mulrcl 10449  ax-mulcom 10450  ax-addass 10451  ax-mulass 10452  ax-distr 10453  ax-i2m1 10454  ax-1ne0 10455  ax-1rid 10456  ax-rnegex 10457  ax-rrecex 10458  ax-cnre 10459  ax-pre-lttri 10460  ax-pre-lttrn 10461  ax-pre-ltadd 10462  ax-pre-mulgt0 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-nel 3090  df-ral 3109  df-rex 3110  df-reu 3111  df-rmo 3112  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-pred 6026  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-riota 6980  df-ov 7022  df-oprab 7023  df-mpo 7024  df-of 7270  df-om 7440  df-1st 7548  df-2nd 7549  df-wrecs 7801  df-recs 7863  df-rdg 7901  df-1o 7956  df-er 8142  df-en 8361  df-dom 8362  df-sdom 8363  df-fin 8364  df-pnf 10526  df-mnf 10527  df-xr 10528  df-ltxr 10529  df-le 10530  df-sub 10721  df-neg 10722  df-nn 11489  df-n0 11748  df-z 11832  df-uz 12094  df-fz 12743

This theorem is referenced by:  poimirlem8  34444  poimirlem18  34454  poimirlem21  34457  poimirlem22  34458