poimirlem1 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem1		Structured version Visualization version GIF version

Theorem poimirlem1 35705

Description: Lemma for poimir 35737- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)

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

**Assertion**
Ref	Expression
poimirlem1	⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))

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

Proof of Theorem poimirlem1 Dummy variable 𝑚 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		poimirlem2.3	. . . . 5 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
2		f1of 6700	. . . . 5 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
4		poimir.0	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5	4	nncnd 11919	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
6		npcan1 11330	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
8	4	nnzd 12354	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		peano2zm 12293	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10		uzid 12526	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
11		peano2uz 12570	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
12	8, 9, 10, 11	4syl 19	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
13	7, 12	eqeltrrd 2840	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
14		fzss2 13225	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
15	13, 14	syl 17	. . . . 5 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
16		poimirlem1.4	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))
17	15, 16	sseldd 3918	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
18	3, 17	ffvelrnd 6944	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁))
19		fzp1elp1 13238	. . . . . 6 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
20	16, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
21	7	oveq2d 7271	. . . . 5 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
22	20, 21	eleqtrd 2841	. . . 4 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
23	3, 22	ffvelrnd 6944	. . 3 ⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁))
24		imassrn 5969	. . . . . . . . . 10 ⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈
25		frn 6591	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
26	1, 2, 25	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
27	24, 26	sstrid 3928	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁))
28	27	sselda 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁))
29		poimirlem2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
30	29	ffvelrnda 6943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ)
31	30	zred 12355	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ)
32	31	ltp1d 11835	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1))
33	31, 32	ltned 11041	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1))
34	28, 33	syldan 590	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1))
35		poimirlem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
36		breq1 5073	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀))
37		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1))
38	36, 37	ifbieq1d 4480	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)))
39		elfzelz 13185	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ)
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41	40	zred 12355	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
42	41	ltm1d 11837	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
43	42	iftrued 4464	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1))
44	38, 43	sylan9eqr 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1))
45	44	csbeq1d 3832	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
47		elfzm1b 13263	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
48	40, 46, 47	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
49	16, 48	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))
50		oveq2 7263	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
51	50	imaeq2d 5958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1))))
52	51	xpeq1d 5609	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
53	52	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
54		oveq1 7262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
55	40	zcnd 12356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℂ)
56		npcan1 11330	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
58	54, 57	sylan9eqr 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
59	58	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
60	59	imaeq2d 5958	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁)))
61	60	xpeq1d 5609	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0}))
62	53, 61	uneq12d 4094	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))
63	62	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
64	49, 63	csbied 3866	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
66	45, 65	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
67	46	zcnd 12356	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
68		npcan1 11330	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
69	67, 68	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
70		peano2zm 12293	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ ℤ)
71		uzid 12526	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 1) − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
72		peano2uz 12570	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 1) − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)) → (((𝑁 − 1) − 1) + 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
73	46, 70, 71, 72	4syl 19	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
74	69, 73	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
75		fzss2 13225	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
76	74, 75	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
77	76, 49	sseldd 3918	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
78		ovexd 7290	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V)
79	35, 66, 77, 78	fvmptd 6864	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
80	79	fveq1d 6758	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
81	80	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
82	29	ffnd 6585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
83	82	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁))
84		1ex 10902	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
85		fnconstg 6646	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))))
86	84, 85	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1)))
87		c0ex 10900	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
88		fnconstg 6646	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ V → ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
89	87, 88	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))
90	86, 89	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
91		dff1o3 6706	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
92	91	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
93		imain 6503	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
94	1, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
95		fzdisj 13212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
96	42, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
97	96	imaeq2d 5958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅))
98		ima0 5974	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ∅) = ∅
99	97, 98	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
100	94, 99	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
101		fnun 6529	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) ∧ ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
102	90, 100, 101	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
103		elfzuz 13181	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (ℤ_≥‘1))
104	16, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
105	57, 104	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘1))
106		peano2zm 12293	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
107		uzid 12526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
108		peano2uz 12570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
109	40, 106, 107, 108	4syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
110	57, 109	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑀 − 1)))
111		peano2uz 12570	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑀 − 1)) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
112		uzss 12534	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)) → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
113	110, 111, 112	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
114		elfzuz3 13182	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
115		eluzp1p1 12539	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
116	16, 114, 115	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
117	7, 116	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
118	113, 117	sseldd 3918	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 − 1)))
119		fzsplit2 13210	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑀 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
120	105, 118, 119	syl2anc 583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
121	57	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
122	121	uneq2d 4093	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
123	120, 122	eqtrd 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
124	123	imaeq2d 5958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
125		imaundi 6042	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))
126	124, 125	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
127		f1ofo 6707	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
128		foima 6677	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
129	1, 127, 128	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
130	126, 129	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁))
131	130	fneq2d 6511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) ↔ (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)))
132	102, 131	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
133	132	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
134		ovexd 7290	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V)
135		inidm 4149	. . . . . . . . . 10 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136		eqidd 2739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
137	100	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
138		fzss2 13225	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁))
139		imass2 5999	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
140	117, 138, 139	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
141	140	sselda 3917	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))
142		fvun2 6842	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
143	86, 89, 142	mp3an12 1449	. . . . . . . . . . . . 13 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
144	137, 141, 143	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
145	87	fvconst2 7061	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
146	141, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
147	144, 146	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
148	147	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
149	83, 133, 134, 134, 135, 136, 148	ofval 7522	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
150	28, 149	mpdan 683	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
151	30	zcnd 12356	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ)
152	151	addid1d 11105	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
153	28, 152	syldan 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
154	81, 150, 153	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛))
155		breq1 5073	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀))
156		oveq1 7262	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1))
157	155, 156	ifbieq2d 4482	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)))
158	41	ltnrd 11039	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝑀 < 𝑀)
159	158	iffalsed 4467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1))
160	157, 159	sylan9eqr 2801	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1))
161	160	csbeq1d 3832	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
162		ovex 7288	. . . . . . . . . . . . 13 ⊢ (𝑀 + 1) ∈ V
163		oveq2 7263	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1)))
164	163	imaeq2d 5958	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1))))
165	164	xpeq1d 5609	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1}))
166		oveq1 7262	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1))
167	166	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁))
168	167	imaeq2d 5958	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
169	168	xpeq1d 5609	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))
170	165, 169	uneq12d 4094	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
171	170	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑀 + 1) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
172	162, 171	csbie 3864	. . . . . . . . . . . 12 ⊢ ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
173	161, 172	eqtrdi 2795	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
174		fz1ssfz0 13281	. . . . . . . . . . . 12 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
175	174, 16	sselid 3915	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
176		ovexd 7290	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V)
177	35, 173, 175, 176	fvmptd 6864	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑀) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
178	177	fveq1d 6758	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
179	178	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
180		fnconstg 6646	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))))
181	84, 180	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1)))
182		fnconstg 6646	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ V → ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
183	87, 182	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁))
184	181, 183	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ (((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) ∧ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
185		imain 6503	. . . . . . . . . . . . . . . 16 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
186	1, 92, 185	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
187		peano2re 11078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
188	41, 187	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
189	188	ltp1d 11835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1))
190		fzdisj 13212	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
192	191	imaeq2d 5958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
193	186, 192	eqtr3d 2780	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
194	193, 98	eqtrdi 2795	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
195		fnun 6529	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (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)...𝑁))))
196	184, 194, 195	sylancr 586	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
197		fzsplit 13211	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
198	22, 197	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
199	198	imaeq2d 5958	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))))
200		imaundi 6042	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
201	199, 200	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
202	201, 129	eqtr3d 2780	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁))
203	202	fneq2d 6511	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
204	196, 203	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
205	204	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
206	194	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
207		fzss1 13224	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)))
208		imass2 5999	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
209	104, 207, 208	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
210	209	sselda 3917	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))))
211		fvun1 6841	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (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})‘𝑛))
212	181, 183, 211	mp3an12 1449	. . . . . . . . . . . . 13 ⊢ ((((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
213	206, 210, 212	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
214	84	fvconst2 7061	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
215	210, 214	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
216	213, 215	eqtrd 2778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
217	216	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
218	83, 205, 134, 134, 135, 136, 217	ofval 7522	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
219	28, 218	mpdan 683	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
220	179, 219	eqtrd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1))
221	34, 154, 220	3netr4d 3020	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
222	221	ralrimiva 3107	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
223		fzpr 13240	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
224	16, 39, 223	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
225	224	imaeq2d 5958	. . . . . . 7 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)}))
226		f1ofn 6701	. . . . . . . . 9 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
227	1, 226	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
228		fnimapr 6834	. . . . . . . 8 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
229	227, 17, 22, 228	syl3anc 1369	. . . . . . 7 ⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
230	225, 229	eqtrd 2778	. . . . . 6 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
231	230	raleqdv 3339	. . . . 5 ⊢ (𝜑 → (∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)))
232	222, 231	mpbid 231	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
233		fvex 6769	. . . . 5 ⊢ (𝑈‘𝑀) ∈ V
234		fvex 6769	. . . . 5 ⊢ (𝑈‘(𝑀 + 1)) ∈ V
235		fveq2 6756	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)))
236		fveq2 6756	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀)))
237	235, 236	neeq12d 3004	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀))))
238		fveq2 6756	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
239		fveq2 6756	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
240	238, 239	neeq12d 3004	. . . . 5 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
241	233, 234, 237, 240	ralpr 4633	. . . 4 ⊢ (∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
242	232, 241	sylib 217	. . 3 ⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
243	41	ltp1d 11835	. . . . 5 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
244	41, 243	ltned 11041	. . . 4 ⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1))
245		f1of1 6699	. . . . . . 7 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁))
246	1, 245	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1→(1...𝑁))
247		f1veqaeq 7111	. . . . . 6 ⊢ ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
248	246, 17, 22, 247	syl12anc 833	. . . . 5 ⊢ (𝜑 → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
249	248	necon3d 2963	. . . 4 ⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
250	244, 249	mpd 15	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))
251	237	anbi1d 629	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))))
252		neeq1 3005	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚))
253	251, 252	anbi12d 630	. . . 4 ⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚)))
254		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
255		fveq2 6756	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
256	254, 255	neeq12d 3004	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
257	256	anbi2d 628	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))))
258		neeq2 3006	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈‘𝑀) ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
259	257, 258	anbi12d 630	. . . 4 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))))
260	253, 259	rspc2ev 3564	. . 3 ⊢ (((𝑈‘𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
261	18, 23, 242, 250, 260	syl112anc 1372	. 2 ⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
262		dfrex2 3166	. . 3 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
263		fveq2 6756	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚))
264		fveq2 6756	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚))
265	263, 264	neeq12d 3004	. . . . 5 ⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))
266	265	rmo4 3660	. . . 4 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
267		dfral2 3164	. . . . . 6 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
268		df-ne 2943	. . . . . . . . 9 ⊢ (𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚)
269	268	anbi2i 622	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚))
270		annim 403	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
271	269, 270	bitri 274	. . . . . . 7 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
272	271	rexbii 3177	. . . . . 6 ⊢ (∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
273	267, 272	xchbinxr 334	. . . . 5 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
274	273	ralbii 3090	. . . 4 ⊢ (∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
275	266, 274	bitri 274	. . 3 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
276	262, 275	xchbinxr 334	. 2 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
277	261, 276	sylib 217	1 ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 ∃*wrmo 3066 Vcvv 3422 ⦋csb 3828 ∪ cun 3881 ∩ cin 3882 ⊆ wss 3883 ∅c0 4253 ifcif 4456 {csn 4558 {cpr 4560 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 ran crn 5581 “ cima 5583 Fun wfun 6412 Fn wfn 6413 ⟶wf 6414 –1-1→wf1 6415 –onto→wfo 6416 –1-1-onto→wf1o 6417 ‘cfv 6418 (class class class)co 7255 ∘_f cof 7509 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 < clt 10940 − cmin 11135 ℕcn 11903 ℤcz 12249 ℤ_≥cuz 12511 ...cfz 13168

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-er 8456 df-en 8692 df-dom 8693 df-sdom 8694 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-nn 11904 df-n0 12164 df-z 12250 df-uz 12512 df-fz 13169

This theorem is referenced by: poimirlem8 35712 poimirlem18 35722 poimirlem21 35725 poimirlem22 35726

W3C validator