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 37608

Description: Lemma for poimir 37640- 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 6849	. . . . 5 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
4		poimir.0	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5	4	nncnd 12280	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
6		npcan1 11686	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
8	4	nnzd 12638	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		peano2zm 12658	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10		uzid 12891	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
11		peano2uz 12941	. . . . . . . 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 13601	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
15	13, 14	syl 17	. . . . 5 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
16		poimirlem1.4	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))
17	15, 16	sseldd 3996	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
18	3, 17	ffvelcdmd 7105	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁))
19		fzp1elp1 13614	. . . . . 6 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
20	16, 19	syl 17	. . . . 5 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...((𝑁 − 1) + 1)))
21	7	oveq2d 7447	. . . . 5 ⊢ (𝜑 → (1...((𝑁 − 1) + 1)) = (1...𝑁))
22	20, 21	eleqtrd 2841	. . . 4 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
23	3, 22	ffvelcdmd 7105	. . 3 ⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁))
24		imassrn 6091	. . . . . . . . . 10 ⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈
25		frn 6744	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
26	1, 2, 25	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
27	24, 26	sstrid 4007	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁))
28	27	sselda 3995	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁))
29		poimirlem2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
30	29	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ)
31	30	zred 12720	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ)
32	31	ltp1d 12196	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1))
33	31, 32	ltned 11395	. . . . . . . 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 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀))
37		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1))
38	36, 37	ifbieq1d 4555	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)))
39		elfzelz 13561	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ)
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41	40	zred 12720	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
42	41	ltm1d 12198	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
43	42	iftrued 4539	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1))
44	38, 43	sylan9eqr 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1))
45	44	csbeq1d 3912	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
47		elfzm1b 13639	. . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...((𝑁 − 1) − 1)))
50		oveq2 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑀 − 1) → (1...𝑗) = (1...(𝑀 − 1)))
51	50	imaeq2d 6080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1))))
52	51	xpeq1d 5718	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
53	52	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 − 1))) × {1}))
54		oveq1 7438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑀 − 1) → (𝑗 + 1) = ((𝑀 − 1) + 1))
55	40	zcnd 12721	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℂ)
56		npcan1 11686	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
58	54, 57	sylan9eqr 2797	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
59	58	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
60	59	imaeq2d 6080	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁)))
61	60	xpeq1d 5718	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0}))
62	53, 61	uneq12d 4179	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))
63	62	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
64	49, 63	csbied 3946	. . . . . . . . . . . . 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 2775	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
67	46	zcnd 12721	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
68		npcan1 11686	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
69	67, 68	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
70		peano2zm 12658	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ ℤ)
71		uzid 12891	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 1) − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
72		peano2uz 12941	. . . . . . . . . . . . . . 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 13601	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
76	74, 75	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
77	76, 49	sseldd 3996	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑀 − 1) ∈ (0...(𝑁 − 1)))
78		ovexd 7466	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))) ∈ V)
79	35, 66, 77, 78	fvmptd 7023	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘(𝑀 − 1)) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
80	79	fveq1d 6909	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
81	80	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
82	29	ffnd 6738	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
83	82	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁))
84		1ex 11255	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
85		fnconstg 6797	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))))
86	84, 85	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1)))
87		c0ex 11253	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
88		fnconstg 6797	. . . . . . . . . . . . . . 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 6855	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
92	91	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
93		imain 6653	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
94	1, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
95		fzdisj 13588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
96	42, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
97	96	imaeq2d 6080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅))
98		ima0 6097	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ∅) = ∅
99	97, 98	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
100	94, 99	eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
101		fnun 6683	. . . . . . . . . . . . 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 13557	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (ℤ_≥‘1))
104	16, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
105	57, 104	eqeltrd 2839	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘1))
106		peano2zm 12658	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
107		uzid 12891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
108		peano2uz 12941	. . . . . . . . . . . . . . . . . . . . . 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 12941	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑀 − 1)) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
112		uzss 12899	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)) → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
113	110, 111, 112	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
114		elfzuz3 13558	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
115		eluzp1p1 12904	. . . . . . . . . . . . . . . . . . . . 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 3996	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 − 1)))
119		fzsplit2 13586	. . . . . . . . . . . . . . . . . 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 7446	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑀 − 1) + 1)...𝑁) = (𝑀...𝑁))
122	121	uneq2d 4178	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
123	120, 122	eqtrd 2775	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
124	123	imaeq2d 6080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
125		imaundi 6172	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))
126	124, 125	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
127		f1ofo 6856	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
128		foima 6826	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
129	1, 127, 128	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
130	126, 129	eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁))
131	130	fneq2d 6663	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) ↔ (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁)))
132	102, 131	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
133	132	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})) Fn (1...𝑁))
134		ovexd 7466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (1...𝑁) ∈ V)
135		inidm 4235	. . . . . . . . . 10 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136		eqidd 2736	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
137	100	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
138		fzss2 13601	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁))
139		imass2 6123	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
140	117, 138, 139	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
141	140	sselda 3995	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))
142		fvun2 7001	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))) ∧ ((𝑈 “ (𝑀...𝑁)) × {0}) Fn (𝑈 “ (𝑀...𝑁)) ∧ (((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
143	86, 89, 142	mp3an12 1450	. . . . . . . . . . . . 13 ⊢ ((((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅ ∧ 𝑛 ∈ (𝑈 “ (𝑀...𝑁))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
144	137, 141, 143	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))‘𝑛) = (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛))
145	87	fvconst2 7224	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (𝑀...𝑁)) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
146	141, 145	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (𝑀...𝑁)) × {0})‘𝑛) = 0)
147	144, 146	eqtrd 2775	. . . . . . . . . . 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 7708	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
150	28, 149	mpdan 687	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 0))
151	30	zcnd 12721	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ)
152	151	addridd 11459	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
153	28, 152	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
154	81, 150, 153	3eqtrd 2779	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛))
155		breq1 5151	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀))
156		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1))
157	155, 156	ifbieq2d 4557	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)))
158	41	ltnrd 11393	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝑀 < 𝑀)
159	158	iffalsed 4542	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1))
160	157, 159	sylan9eqr 2797	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1))
161	160	csbeq1d 3912	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
162		ovex 7464	. . . . . . . . . . . . 13 ⊢ (𝑀 + 1) ∈ V
163		oveq2 7439	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → (1...𝑗) = (1...(𝑀 + 1)))
164	163	imaeq2d 6080	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1))))
165	164	xpeq1d 5718	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑀 + 1))) × {1}))
166		oveq1 7438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 + 1) = ((𝑀 + 1) + 1))
167	166	oveq1d 7446	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑀 + 1) → ((𝑗 + 1)...𝑁) = (((𝑀 + 1) + 1)...𝑁))
168	167	imaeq2d 6080	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
169	168	xpeq1d 5718	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))
170	165, 169	uneq12d 4179	. . . . . . . . . . . . . 14 ⊢ (𝑗 = (𝑀 + 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
171	170	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑗 = (𝑀 + 1) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
172	162, 171	csbie 3944	. . . . . . . . . . . 12 ⊢ ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
173	161, 172	eqtrdi 2791	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
174		fz1ssfz0 13660	. . . . . . . . . . . 12 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
175	174, 16	sselid 3993	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑀 ∈ (0...(𝑁 − 1)))
176		ovexd 7466	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))) ∈ V)
177	35, 173, 175, 176	fvmptd 7023	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝑀) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
178	177	fveq1d 6909	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
179	178	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
180		fnconstg 6797	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))))
181	84, 180	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1)))
182		fnconstg 6797	. . . . . . . . . . . . . . 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 6653	. . . . . . . . . . . . . . . 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 11432	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
188	41, 187	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
189	188	ltp1d 12196	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1))
190		fzdisj 13588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
192	191	imaeq2d 6080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
193	186, 192	eqtr3d 2777	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
194	193, 98	eqtrdi 2791	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
195		fnun 6683	. . . . . . . . . . . . 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 13587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
198	22, 197	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
199	198	imaeq2d 6080	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))))
200		imaundi 6172	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
201	199, 200	eqtrdi 2791	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
202	201, 129	eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁))
203	202	fneq2d 6663	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) ↔ (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})) Fn (1...𝑁)))
204	196, 203	mpbid 232	. . . . . . . . . . 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 13600	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)))
208		imass2 6123	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
209	104, 207, 208	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
210	209	sselda 3995	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))))
211		fvun1 7000	. . . . . . . . . . . . . 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 1450	. . . . . . . . . . . . 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 7224	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ (𝑈 “ (1...(𝑀 + 1))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
215	210, 214	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → (((𝑈 “ (1...(𝑀 + 1))) × {1})‘𝑛) = 1)
216	213, 215	eqtrd 2775	. . . . . . . . . . 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 7708	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
219	28, 218	mpdan 687	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛) = ((𝑇‘𝑛) + 1))
220	179, 219	eqtrd 2775	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1))
221	34, 154, 220	3netr4d 3016	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
222	221	ralrimiva 3144	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
223		fzpr 13616	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
224	16, 39, 223	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
225	224	imaeq2d 6080	. . . . . 6 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)}))
226		f1ofn 6850	. . . . . . . 8 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
227	1, 226	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
228		fnimapr 6992	. . . . . . 7 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁)) → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
229	227, 17, 22, 228	syl3anc 1370	. . . . . 6 ⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
230	225, 229	eqtrd 2775	. . . . 5 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
231	222, 230	raleqtrdv 3326	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
232		fvex 6920	. . . . 5 ⊢ (𝑈‘𝑀) ∈ V
233		fvex 6920	. . . . 5 ⊢ (𝑈‘(𝑀 + 1)) ∈ V
234		fveq2 6907	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)))
235		fveq2 6907	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀)))
236	234, 235	neeq12d 3000	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀))))
237		fveq2 6907	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
238		fveq2 6907	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
239	237, 238	neeq12d 3000	. . . . 5 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
240	232, 233, 236, 239	ralpr 4705	. . . 4 ⊢ (∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
241	231, 240	sylib 218	. . 3 ⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
242	41	ltp1d 12196	. . . . 5 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
243	41, 242	ltned 11395	. . . 4 ⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1))
244		f1of1 6848	. . . . . . 7 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–1-1→(1...𝑁))
245	1, 244	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1→(1...𝑁))
246		f1veqaeq 7277	. . . . . 6 ⊢ ((𝑈:(1...𝑁)–1-1→(1...𝑁) ∧ (𝑀 ∈ (1...𝑁) ∧ (𝑀 + 1) ∈ (1...𝑁))) → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
247	245, 17, 22, 246	syl12anc 837	. . . . 5 ⊢ (𝜑 → ((𝑈‘𝑀) = (𝑈‘(𝑀 + 1)) → 𝑀 = (𝑀 + 1)))
248	247	necon3d 2959	. . . 4 ⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
249	243, 248	mpd 15	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))
250	236	anbi1d 631	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))))
251		neeq1 3001	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚))
252	250, 251	anbi12d 632	. . . 4 ⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚)))
253		fveq2 6907	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
254		fveq2 6907	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
255	253, 254	neeq12d 3000	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
256	255	anbi2d 630	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))))
257		neeq2 3002	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝑈‘𝑀) ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
258	256, 257	anbi12d 632	. . . 4 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))))
259	252, 258	rspc2ev 3635	. . 3 ⊢ (((𝑈‘𝑀) ∈ (1...𝑁) ∧ (𝑈‘(𝑀 + 1)) ∈ (1...𝑁) ∧ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))) ∧ (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))) → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
260	18, 23, 241, 249, 259	syl112anc 1373	. 2 ⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
261		dfrex2 3071	. . 3 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
262		fveq2 6907	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚))
263		fveq2 6907	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚))
264	262, 263	neeq12d 3000	. . . . 5 ⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))
265	264	rmo4 3739	. . . 4 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
266		dfral2 3097	. . . . . 6 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
267		df-ne 2939	. . . . . . . . 9 ⊢ (𝑛 ≠ 𝑚 ↔ ¬ 𝑛 = 𝑚)
268	267	anbi2i 623	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚))
269		annim 403	. . . . . . . 8 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ ¬ 𝑛 = 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
270	268, 269	bitri 275	. . . . . . 7 ⊢ (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
271	270	rexbii 3092	. . . . . 6 ⊢ (∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
272	266, 271	xchbinxr 335	. . . . 5 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
273	272	ralbii 3091	. . . 4 ⊢ (∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
274	265, 273	bitri 275	. . 3 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
275	261, 274	xchbinxr 335	. 2 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
276	260, 275	sylib 218	1 ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ≠ wne 2938 ∀wral 3059 ∃wrex 3068 ∃*wrmo 3377 Vcvv 3478 ⦋csb 3908 ∪ cun 3961 ∩ cin 3962 ⊆ wss 3963 ∅c0 4339 ifcif 4531 {csn 4631 {cpr 4633 class class class wbr 5148 ↦ cmpt 5231 × cxp 5687 ^◡ccnv 5688 ran crn 5690 “ cima 5692 Fun wfun 6557 Fn wfn 6558 ⟶wf 6559 –1-1→wf1 6560 –onto→wfo 6561 –1-1-onto→wf1o 6562 ‘cfv 6563 (class class class)co 7431 ∘_f cof 7695 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 < clt 11293 − cmin 11490 ℕcn 12264 ℤcz 12611 ℤ_≥cuz 12876 ...cfz 13544

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-nn 12265 df-n0 12525 df-z 12612 df-uz 12877 df-fz 13545

This theorem is referenced by: poimirlem8 37615 poimirlem18 37625 poimirlem21 37628 poimirlem22 37629

W3C validator