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 36079

Description: Lemma for poimir 36111- 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 6784	. . . . 5 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
4		poimir.0	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5	4	nncnd 12169	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
6		npcan1 11580	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
8	4	nnzd 12526	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		peano2zm 12546	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10		uzid 12778	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
11		peano2uz 12826	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
12	8, 9, 10, 11	4syl 19	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
13	7, 12	eqeltrrd 2839	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
14		fzss2 13481	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
15	13, 14	syl 17	. . . . 5 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
16		poimirlem1.4	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))
17	15, 16	sseldd 3945	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
18	3, 17	ffvelcdmd 7036	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁))
19		fzp1elp1 13494	. . . . . 6 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
20	16, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
21	7	oveq2d 7373	. . . . 5 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
22	20, 21	eleqtrd 2840	. . . 4 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
23	3, 22	ffvelcdmd 7036	. . 3 ⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁))
24		imassrn 6024	. . . . . . . . . 10 ⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈
25		frn 6675	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
26	1, 2, 25	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
27	24, 26	sstrid 3955	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁))
28	27	sselda 3944	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁))
29		poimirlem2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
30	29	ffvelcdmda 7035	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ)
31	30	zred 12607	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ)
32	31	ltp1d 12085	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1))
33	31, 32	ltned 11291	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1))
34	28, 33	syldan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (𝑇‘𝑛) ≠ ((𝑇‘𝑛) + 1))
35		poimirlem2.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))
36		breq1 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀))
37		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1))
38	36, 37	ifbieq1d 4510	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)))
39		elfzelz 13441	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ)
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41	40	zred 12607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
42	41	ltm1d 12087	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
43	42	iftrued 4494	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1))
44	38, 43	sylan9eqr 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1))
45	44	csbeq1d 3859	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
47		elfzm1b 13519	. . . . . . . . . . . . . . . 16 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
48	40, 46, 47	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 ∈ (1...(𝑁 − 1)) ↔ (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1))))
49	16, 48	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))
50		oveq2 7365	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
51	50	imaeq2d 6013	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1))))
52	51	xpeq1d 5662	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
53	52	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
54		oveq1 7364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
55	40	zcnd 12608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℂ)
56		npcan1 11580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
58	54, 57	sylan9eqr 2798	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
59	58	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
60	59	imaeq2d 6013	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁)))
61	60	xpeq1d 5662	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0}))
62	53, 61	uneq12d 4124	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))
63	62	oveq2d 7373	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
64	49, 63	csbied 3893	. . . . . . . . . . . . 13 ⊢ (𝜑 → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
65	64	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
66	45, 65	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
67	46	zcnd 12608	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
68		npcan1 11580	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
69	67, 68	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
70		peano2zm 12546	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ ℤ)
71		uzid 12778	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 1) − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
72		peano2uz 12826	. . . . . . . . . . . . . . 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 2839	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
75		fzss2 13481	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
76	74, 75	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
77	76, 49	sseldd 3945	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
78		ovexd 7392	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V)
79	35, 66, 77, 78	fvmptd 6955	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
80	79	fveq1d 6844	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
81	80	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
82	29	ffnd 6669	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
83	82	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁))
84		1ex 11151	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
85		fnconstg 6730	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))))
86	84, 85	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1)))
87		c0ex 11149	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
88		fnconstg 6730	. . . . . . . . . . . . . . 15 ⊢ (0 ∈ V → ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
89	87, 88	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))
90	86, 89	pm3.2i 471	. . . . . . . . . . . . 13 ⊢ (((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)))
91		dff1o3 6790	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
92	91	simprbi 497	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
93		imain 6586	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
94	1, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
95		fzdisj 13468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
96	42, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
97	96	imaeq2d 6013	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅))
98		ima0 6029	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ∅) = ∅
99	97, 98	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
100	94, 99	eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
101		fnun 6614	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁))) ∧ ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
102	90, 100, 101	sylancr 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
103		elfzuz 13437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (ℤ_≥‘1))
104	16, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
105	57, 104	eqeltrd 2838	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘1))
106		peano2zm 12546	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
107		uzid 12778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
108		peano2uz 12826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
109	40, 106, 107, 108	4syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
110	57, 109	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑀 − 1)))
111		peano2uz 12826	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑀 − 1)) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
112		uzss 12786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)) → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
113	110, 111, 112	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
114		elfzuz3 13438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
115		eluzp1p1 12791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
116	16, 114, 115	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
117	7, 116	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
118	113, 117	sseldd 3945	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 − 1)))
119		fzsplit2 13466	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑀 − 1) + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘(𝑀 − 1))) → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
120	105, 118, 119	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)))
121	57	oveq1d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
122	121	uneq2d 4123	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
123	120, 122	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
124	123	imaeq2d 6013	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
125		imaundi 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))
126	124, 125	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
127		f1ofo 6791	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
128		foima 6761	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
129	1, 127, 128	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
130	126, 129	eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁))
131	130	fneq2d 6596	. . . . . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
134		ovexd 7392	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V)
135		inidm 4178	. . . . . . . . . 10 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136		eqidd 2737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
137	100	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
138		fzss2 13481	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁))
139		imass2 6054	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
140	117, 138, 139	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
141	140	sselda 3944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))
142		fvun2 6933	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
143	86, 89, 142	mp3an12 1451	. . . . . . . . . . . . 13 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
144	137, 141, 143	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
145	87	fvconst2 7153	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
146	141, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
147	144, 146	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
148	147	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = 0)
149	83, 133, 134, 134, 135, 136, 148	ofval 7628	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
150	28, 149	mpdan 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
151	30	zcnd 12608	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ)
152	151	addid1d 11355	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
153	28, 152	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
154	81, 150, 153	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛))
155		breq1 5108	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀))
156		oveq1 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1))
157	155, 156	ifbieq2d 4512	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)))
158	41	ltnrd 11289	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝑀 < 𝑀)
159	158	iffalsed 4497	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1))
160	157, 159	sylan9eqr 2798	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1))
161	160	csbeq1d 3859	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
162		ovex 7390	. . . . . . . . . . . . 13 ⊢ (𝑀 + 1) ∈ V
163		oveq2 7365	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1)))
164	163	imaeq2d 6013	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1))))
165	164	xpeq1d 5662	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1}))
166		oveq1 7364	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1))
167	166	oveq1d 7372	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁))
168	167	imaeq2d 6013	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
169	168	xpeq1d 5662	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))
170	165, 169	uneq12d 4124	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
171	170	oveq2d 7373	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑀 + 1) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
172	162, 171	csbie 3891	. . . . . . . . . . . 12 ⊢ ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
173	161, 172	eqtrdi 2792	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
174		fz1ssfz0 13537	. . . . . . . . . . . 12 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
175	174, 16	sselid 3942	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
176		ovexd 7392	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V)
177	35, 173, 175, 176	fvmptd 6955	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑀) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
178	177	fveq1d 6844	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
179	178	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
180		fnconstg 6730	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))))
181	84, 180	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1)))
182		fnconstg 6730	. . . . . . . . . . . . . . 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 471	. . . . . . . . . . . . 13 ⊢ (((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))) ∧ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
185		imain 6586	. . . . . . . . . . . . . . . 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 11328	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
188	41, 187	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
189	188	ltp1d 12085	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1))
190		fzdisj 13468	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
192	191	imaeq2d 6013	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
193	186, 192	eqtr3d 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
194	193, 98	eqtrdi 2792	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
195		fnun 6614	. . . . . . . . . . . . 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 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
197		fzsplit 13467	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
198	22, 197	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
199	198	imaeq2d 6013	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))))
200		imaundi 6102	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
201	199, 200	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
202	201, 129	eqtr3d 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁))
203	202	fneq2d 6596	. . . . . . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁))
206	194	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
207		fzss1 13480	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)))
208		imass2 6054	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
209	104, 207, 208	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
210	209	sselda 3944	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))))
211		fvun1 6932	. . . . . . . . . . . . . 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 1451	. . . . . . . . . . . . 13 ⊢ ((((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
213	206, 210, 212	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛))
214	84	fvconst2 7153	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
215	210, 214	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
216	213, 215	eqtrd 2776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
217	216	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))‘𝑛) = 1)
218	83, 205, 134, 134, 135, 136, 217	ofval 7628	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
219	28, 218	mpdan 685	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
220	179, 219	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1))
221	34, 154, 220	3netr4d 3021	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
222	221	ralrimiva 3143	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
223		fzpr 13496	. . . . . . . . 9 ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
224	16, 39, 223	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
225	224	imaeq2d 6013	. . . . . . 7 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)}))
226		f1ofn 6785	. . . . . . . . 9 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
227	1, 226	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
228		fnimapr 6925	. . . . . . . 8 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
229	227, 17, 22, 228	syl3anc 1371	. . . . . . 7 ⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
230	225, 229	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
231	230	raleqdv 3313	. . . . 5 ⊢ (𝜑 → (∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛)))
232	222, 231	mpbid 231	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
233		fvex 6855	. . . . 5 ⊢ (𝑈‘𝑀) ∈ V
234		fvex 6855	. . . . 5 ⊢ (𝑈‘(𝑀 + 1)) ∈ V
235		fveq2 6842	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)))
236		fveq2 6842	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀)))
237	235, 236	neeq12d 3005	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀))))
238		fveq2 6842	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
239		fveq2 6842	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
240	238, 239	neeq12d 3005	. . . . 5 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
241	233, 234, 237, 240	ralpr 4661	. . . 4 ⊢ (∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
242	232, 241	sylib 217	. . 3 ⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
243	41	ltp1d 12085	. . . . 5 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
244	41, 243	ltned 11291	. . . 4 ⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1))
245		f1of1 6783	. . . . . . 7 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁))
246	1, 245	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1→(1...𝑁))
247		f1veqaeq 7204	. . . . . 6 ⊢ ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
248	246, 17, 22, 247	syl12anc 835	. . . . 5 ⊢ (𝜑 → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
249	248	necon3d 2964	. . . 4 ⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
250	244, 249	mpd 15	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))
251	237	anbi1d 630	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))))
252		neeq1 3006	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚))
253	251, 252	anbi12d 631	. . . 4 ⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚)))
254		fveq2 6842	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
255		fveq2 6842	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
256	254, 255	neeq12d 3005	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
257	256	anbi2d 629	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))))
258		neeq2 3007	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈‘𝑀) ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
259	257, 258	anbi12d 631	. . . 4 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))))
260	253, 259	rspc2ev 3592	. . 3 ⊢ (((𝑈‘𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
261	18, 23, 242, 250, 260	syl112anc 1374	. 2 ⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
262		dfrex2 3076	. . 3 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
263		fveq2 6842	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚))
264		fveq2 6842	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚))
265	263, 264	neeq12d 3005	. . . . 5 ⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))
266	265	rmo4 3688	. . . 4 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
267		dfral2 3102	. . . . . 6 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
268		df-ne 2944	. . . . . . . . 9 ⊢ (𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚)
269	268	anbi2i 623	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚))
270		annim 404	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
271	269, 270	bitri 274	. . . . . . 7 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
272	271	rexbii 3097	. . . . . 6 ⊢ (∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
273	267, 272	xchbinxr 334	. . . . 5 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
274	273	ralbii 3096	. . . 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 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 ∃*wrmo 3352 Vcvv 3445 ⦋csb 3855 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 {csn 4586 {cpr 4588 class class class wbr 5105 ↦ cmpt 5188 × cxp 5631 ^◡ccnv 5632 ran crn 5634 “ cima 5636 Fun wfun 6490 Fn wfn 6491 ⟶wf 6492 –1-1→wf1 6493 –onto→wfo 6494 –1-1-onto→wf1o 6495 ‘cfv 6496 (class class class)co 7357 ∘_f cof 7615 ℂcc 11049 ℝcr 11050 0cc0 11051 1c1 11052 + caddc 11054 < clt 11189 − cmin 11385 ℕcn 12153 ℤcz 12499 ℤ_≥cuz 12763 ...cfz 13424

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-er 8648 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-nn 12154 df-n0 12414 df-z 12500 df-uz 12764 df-fz 13425

This theorem is referenced by: poimirlem8 36086 poimirlem18 36096 poimirlem21 36099 poimirlem22 36100

W3C validator