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 37628

Description: Lemma for poimir 37660- 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 6848	. . . . 5 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)⟶(1...𝑁))
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝑈:(1...𝑁)⟶(1...𝑁))
4		poimir.0	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ)
5	4	nncnd 12282	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
6		npcan1 11688	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
7	5, 6	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
8	4	nnzd 12640	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
9		peano2zm 12660	. . . . . . . 8 ⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈ ℤ)
10		uzid 12893	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
11		peano2uz 12943	. . . . . . . 8 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
12	8, 9, 10, 11	4syl 19	. . . . . . 7 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
13	7, 12	eqeltrrd 2842	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
14		fzss2 13604	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (1...(𝑁 − 1)) ⊆ (1...𝑁))
15	13, 14	syl 17	. . . . 5 ⊢ (𝜑 → (1...(𝑁 − 1)) ⊆ (1...𝑁))
16		poimirlem1.4	. . . . 5 ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))
17	15, 16	sseldd 3984	. . . 4 ⊢ (𝜑 → 𝑀 ∈ (1...𝑁))
18	3, 17	ffvelcdmd 7105	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ∈ (1...𝑁))
19		fzp1elp1 13617	. . . . . 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 2843	. . . 4 ⊢ (𝜑 → (𝑀 + 1) ∈ (1...𝑁))
23	3, 22	ffvelcdmd 7105	. . 3 ⊢ (𝜑 → (𝑈‘(𝑀 + 1)) ∈ (1...𝑁))
24		imassrn 6089	. . . . . . . . . 10 ⊢ (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ ran 𝑈
25		frn 6743	. . . . . . . . . . 11 ⊢ (𝑈:(1...𝑁)⟶(1...𝑁) → ran 𝑈 ⊆ (1...𝑁))
26	1, 2, 25	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ran 𝑈 ⊆ (1...𝑁))
27	24, 26	sstrid 3995	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (1...𝑁))
28	27	sselda 3983	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑛 ∈ (1...𝑁))
29		poimirlem2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)
30	29	ffvelcdmda 7104	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℤ)
31	30	zred 12722	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℝ)
32	31	ltp1d 12198	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) < ((𝑇‘𝑛) + 1))
33	31, 32	ltned 11397	. . . . . . . 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 5146	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → (𝑦 < 𝑀 ↔ (𝑀 − 1) < 𝑀))
37		id 22	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑀 − 1) → 𝑦 = (𝑀 − 1))
38	36, 37	ifbieq1d 4550	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑀 − 1) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)))
39		elfzelz 13564	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ ℤ)
40	16, 39	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑀 ∈ ℤ)
41	40	zred 12722	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑀 ∈ ℝ)
42	41	ltm1d 12200	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑀 − 1) < 𝑀)
43	42	iftrued 4533	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if((𝑀 − 1) < 𝑀, (𝑀 − 1), (𝑦 + 1)) = (𝑀 − 1))
44	38, 43	sylan9eqr 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 − 1))
45	44	csbeq1d 3903	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋(𝑀 − 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
46	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
47		elfzm1b 13642	. . . . . . . . . . . . . . . 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 6078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑀 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 − 1))))
52	51	xpeq1d 5714	. . . . . . . . . . . . . . . . 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 12723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑀 ∈ ℂ)
56		npcan1 11688	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℂ → ((𝑀 − 1) + 1) = 𝑀)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑀 − 1) + 1) = 𝑀)
58	54, 57	sylan9eqr 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑗 + 1) = 𝑀)
59	58	oveq1d 7446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑗 + 1)...𝑁) = (𝑀...𝑁))
60	59	imaeq2d 6078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (𝑀...𝑁)))
61	60	xpeq1d 5714	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = (𝑀 − 1)) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (𝑀...𝑁)) × {0}))
62	53, 61	uneq12d 4169	. . . . . . . . . . . . . . 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 3935	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = (𝑀 − 1)) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0}))))
67	46	zcnd 12723	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 − 1) ∈ ℂ)
68		npcan1 11688	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℂ → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
69	67, 68	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑁 − 1) − 1) + 1) = (𝑁 − 1))
70		peano2zm 12660	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ ℤ)
71		uzid 12893	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 − 1) − 1) ∈ ℤ → ((𝑁 − 1) − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
72		peano2uz 12943	. . . . . . . . . . . . . . 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 2842	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)))
75		fzss2 13604	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘((𝑁 − 1) − 1)) → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
76	74, 75	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (0...((𝑁 − 1) − 1)) ⊆ (0...(𝑁 − 1)))
77	76, 49	sseldd 3984	. . . . . . . . . . 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 6908	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
81	80	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 − 1))) × {1}) ∪ ((𝑈 “ (𝑀...𝑁)) × {0})))‘𝑛))
82	29	ffnd 6737	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
83	82	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → 𝑇 Fn (1...𝑁))
84		1ex 11257	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ V
85		fnconstg 6796	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1))))
86	84, 85	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 − 1))) × {1}) Fn (𝑈 “ (1...(𝑀 − 1)))
87		c0ex 11255	. . . . . . . . . . . . . . 15 ⊢ 0 ∈ V
88		fnconstg 6796	. . . . . . . . . . . . . . 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 6854	. . . . . . . . . . . . . . . 16 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
92	91	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
93		imain 6651	. . . . . . . . . . . . . . 15 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
94	1, 92, 93	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))))
95		fzdisj 13591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 − 1) < 𝑀 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
96	42, 95	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∩ (𝑀...𝑁)) = ∅)
97	96	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = (𝑈 “ ∅))
98		ima0 6095	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ∅) = ∅
99	97, 98	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 − 1)) ∩ (𝑀...𝑁))) = ∅)
100	94, 99	eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
101		fnun 6682	. . . . . . . . . . . . 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 13560	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → 𝑀 ∈ (ℤ_≥‘1))
104	16, 103	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘1))
105	57, 104	eqeltrd 2841	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘1))
106		peano2zm 12660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
107		uzid 12893	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ ℤ → (𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)))
108		peano2uz 12943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑀 − 1) ∈ (ℤ_≥‘(𝑀 − 1)) → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
109	40, 106, 107, 108	4syl 19	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑀 − 1) + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
110	57, 109	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘(𝑀 − 1)))
111		peano2uz 12943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ (ℤ_≥‘(𝑀 − 1)) → (𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)))
112		uzss 12901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 + 1) ∈ (ℤ_≥‘(𝑀 − 1)) → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
113	110, 111, 112	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (ℤ_≥‘(𝑀 + 1)) ⊆ (ℤ_≥‘(𝑀 − 1)))
114		elfzuz3 13561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ (1...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑀))
115		eluzp1p1 12906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑀) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
116	16, 114, 115	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑀 + 1)))
117	7, 116	eqeltrrd 2842	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 + 1)))
118	113, 117	sseldd 3984	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑀 − 1)))
119		fzsplit2 13589	. . . . . . . . . . . . . . . . . 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 4168	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((1...(𝑀 − 1)) ∪ (((𝑀 − 1) + 1)...𝑁)) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
123	120, 122	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 − 1)) ∪ (𝑀...𝑁)))
124	123	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))))
125		imaundi 6169	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 − 1)) ∪ (𝑀...𝑁))) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁)))
126	124, 125	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))))
127		f1ofo 6855	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
128		foima 6825	. . . . . . . . . . . . . . 15 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
129	1, 127, 128	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
130	126, 129	eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 − 1))) ∪ (𝑈 “ (𝑀...𝑁))) = (1...𝑁))
131	130	fneq2d 6662	. . . . . . . . . . . 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 4227	. . . . . . . . . 10 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
136		eqidd 2738	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) = (𝑇‘𝑛))
137	100	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑈 “ (1...(𝑀 − 1))) ∩ (𝑈 “ (𝑀...𝑁))) = ∅)
138		fzss2 13604	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑀 + 1)) → (𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁))
139		imass2 6120	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (𝑀...𝑁) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
140	117, 138, 139	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (𝑀...𝑁)))
141	140	sselda 3983	. . . . . . . . . . . . 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 1453	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 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 12723	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → (𝑇‘𝑛) ∈ ℂ)
152	151	addridd 11461	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (1...𝑁)) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
153	28, 152	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝑇‘𝑛) + 0) = (𝑇‘𝑛))
154	81, 150, 153	3eqtrd 2781	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) = (𝑇‘𝑛))
155		breq1 5146	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 < 𝑀 ↔ 𝑀 < 𝑀))
156		oveq1 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑀 → (𝑦 + 1) = (𝑀 + 1))
157	155, 156	ifbieq2d 4552	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑀 → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)))
158	41	ltnrd 11395	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝑀 < 𝑀)
159	158	iffalsed 4536	. . . . . . . . . . . . . 14 ⊢ (𝜑 → if(𝑀 < 𝑀, 𝑦, (𝑀 + 1)) = (𝑀 + 1))
160	157, 159	sylan9eqr 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) = (𝑀 + 1))
161	160	csbeq1d 3903	. . . . . . . . . . . 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 6078	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑀 + 1))))
165	164	xpeq1d 5714	. . . . . . . . . . . . . . 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 6078	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑀 + 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
169	168	xpeq1d 5714	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑀 + 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))
170	165, 169	uneq12d 4169	. . . . . . . . . . . . . 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 3934	. . . . . . . . . . . 12 ⊢ ⦋(𝑀 + 1) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))
173	161, 172	eqtrdi 2793	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 = 𝑀) → ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0}))))
174		fz1ssfz0 13663	. . . . . . . . . . . 12 ⊢ (1...(𝑁 − 1)) ⊆ (0...(𝑁 − 1))
175	174, 16	sselid 3981	. . . . . . . . . . 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 6908	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
179	178	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇 ∘_f + (((𝑈 “ (1...(𝑀 + 1))) × {1}) ∪ ((𝑈 “ (((𝑀 + 1) + 1)...𝑁)) × {0})))‘𝑛))
180		fnconstg 6796	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1))))
181	84, 180	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑈 “ (1...(𝑀 + 1))) × {1}) Fn (𝑈 “ (1...(𝑀 + 1)))
182		fnconstg 6796	. . . . . . . . . . . . . . 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 6651	. . . . . . . . . . . . . . . 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 11434	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
188	41, 187	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑀 + 1) ∈ ℝ)
189	188	ltp1d 12198	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑀 + 1) < ((𝑀 + 1) + 1))
190		fzdisj 13591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) < ((𝑀 + 1) + 1) → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
191	189, 190	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁)) = ∅)
192	191	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ ((1...(𝑀 + 1)) ∩ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
193	186, 192	eqtr3d 2779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (𝑈 “ ∅))
194	193, 98	eqtrdi 2793	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∩ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = ∅)
195		fnun 6682	. . . . . . . . . . . . 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 13590	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 + 1) ∈ (1...𝑁) → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
198	22, 197	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (1...𝑁) = ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁)))
199	198	imaeq2d 6078	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))))
200		imaundi 6169	. . . . . . . . . . . . . . 15 ⊢ (𝑈 “ ((1...(𝑀 + 1)) ∪ (((𝑀 + 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁)))
201	199, 200	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))))
202	201, 129	eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑈 “ (1...(𝑀 + 1))) ∪ (𝑈 “ (((𝑀 + 1) + 1)...𝑁))) = (1...𝑁))
203	202	fneq2d 6662	. . . . . . . . . . . 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 13603	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘1) → (𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)))
208		imass2 6120	. . . . . . . . . . . . . . 15 ⊢ ((𝑀...(𝑀 + 1)) ⊆ (1...(𝑀 + 1)) → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
209	104, 207, 208	3syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) ⊆ (𝑈 “ (1...(𝑀 + 1))))
210	209	sselda 3983	. . . . . . . . . . . . 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 1453	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 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 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘𝑀)‘𝑛) = ((𝑇‘𝑛) + 1))
221	34, 154, 220	3netr4d 3018	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))) → ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
222	221	ralrimiva 3146	. . . . 5 ⊢ (𝜑 → ∀𝑛 ∈ (𝑈 “ (𝑀...(𝑀 + 1)))((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
223		fzpr 13619	. . . . . . . 8 ⊢ (𝑀 ∈ ℤ → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
224	16, 39, 223	3syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑀...(𝑀 + 1)) = {𝑀, (𝑀 + 1)})
225	224	imaeq2d 6078	. . . . . 6 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = (𝑈 “ {𝑀, (𝑀 + 1)}))
226		f1ofn 6849	. . . . . . . 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 1373	. . . . . 6 ⊢ (𝜑 → (𝑈 “ {𝑀, (𝑀 + 1)}) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
230	225, 229	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (𝑈 “ (𝑀...(𝑀 + 1))) = {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))})
231	222, 230	raleqtrdv 3328	. . . 4 ⊢ (𝜑 → ∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))
232		fvex 6919	. . . . 5 ⊢ (𝑈‘𝑀) ∈ V
233		fvex 6919	. . . . 5 ⊢ (𝑈‘(𝑀 + 1)) ∈ V
234		fveq2 6906	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)))
235		fveq2 6906	. . . . . 6 ⊢ (𝑛 = (𝑈‘𝑀) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘𝑀)))
236	234, 235	neeq12d 3002	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀))))
237		fveq2 6906	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
238		fveq2 6906	. . . . . 6 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
239	237, 238	neeq12d 3002	. . . . 5 ⊢ (𝑛 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
240	232, 233, 236, 239	ralpr 4700	. . . 4 ⊢ (∀𝑛 ∈ {(𝑈‘𝑀), (𝑈‘(𝑀 + 1))} ((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
241	231, 240	sylib 218	. . 3 ⊢ (𝜑 → (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
242	41	ltp1d 12198	. . . . 5 ⊢ (𝜑 → 𝑀 < (𝑀 + 1))
243	41, 242	ltned 11397	. . . 4 ⊢ (𝜑 → 𝑀 ≠ (𝑀 + 1))
244		f1of1 6847	. . . . . . 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 2961	. . . 4 ⊢ (𝜑 → (𝑀 ≠ (𝑀 + 1) → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1))))
249	243, 248	mpd 15	. . 3 ⊢ (𝜑 → (𝑈‘𝑀) ≠ (𝑈‘(𝑀 + 1)))
250	236	anbi1d 631	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚))))
251		neeq1 3003	. . . . 5 ⊢ (𝑛 = (𝑈‘𝑀) → (𝑛 ≠ 𝑚 ↔ (𝑈‘𝑀) ≠ 𝑚))
252	250, 251	anbi12d 632	. . . 4 ⊢ (𝑛 = (𝑈‘𝑀) → (((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ (𝑈‘𝑀) ≠ 𝑚)))
253		fveq2 6906	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘(𝑀 − 1))‘𝑚) = ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))))
254		fveq2 6906	. . . . . . 7 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((𝐹‘𝑀)‘𝑚) = ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))
255	253, 254	neeq12d 3002	. . . . . 6 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → (((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚) ↔ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1)))))
256	255	anbi2d 630	. . . . 5 ⊢ (𝑚 = (𝑈‘(𝑀 + 1)) → ((((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ↔ (((𝐹‘(𝑀 − 1))‘(𝑈‘𝑀)) ≠ ((𝐹‘𝑀)‘(𝑈‘𝑀)) ∧ ((𝐹‘(𝑀 − 1))‘(𝑈‘(𝑀 + 1))) ≠ ((𝐹‘𝑀)‘(𝑈‘(𝑀 + 1))))))
257		neeq2 3004	. . . . 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 1376	. 2 ⊢ (𝜑 → ∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
261		dfrex2 3073	. . 3 ⊢ (∃𝑛 ∈ (1...𝑁)∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ¬ ∀𝑛 ∈ (1...𝑁) ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
262		fveq2 6906	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘(𝑀 − 1))‘𝑛) = ((𝐹‘(𝑀 − 1))‘𝑚))
263		fveq2 6906	. . . . . 6 ⊢ (𝑛 = 𝑚 → ((𝐹‘𝑀)‘𝑛) = ((𝐹‘𝑀)‘𝑚))
264	262, 263	neeq12d 3002	. . . . 5 ⊢ (𝑛 = 𝑚 → (((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)))
265	264	rmo4 3736	. . . 4 ⊢ (∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
266		dfral2 3099	. . . . . 6 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
267		df-ne 2941	. . . . . . . . 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 3094	. . . . . 6 ⊢ (∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚) ↔ ∃𝑚 ∈ (1...𝑁) ¬ ((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚))
272	266, 271	xchbinxr 335	. . . . 5 ⊢ (∀𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) → 𝑛 = 𝑚) ↔ ¬ ∃𝑚 ∈ (1...𝑁)((((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛) ∧ ((𝐹‘(𝑀 − 1))‘𝑚) ≠ ((𝐹‘𝑀)‘𝑚)) ∧ 𝑛 ≠ 𝑚))
273	272	ralbii 3093	. . . 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 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 ∃*wrmo 3379 Vcvv 3480 ⦋csb 3899 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 ifcif 4525 {csn 4626 {cpr 4628 class class class wbr 5143 ↦ cmpt 5225 × cxp 5683 ^◡ccnv 5684 ran crn 5686 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –1-1→wf1 6558 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 < clt 11295 − cmin 11492 ℕcn 12266 ℤcz 12613 ℤ_≥cuz 12878 ...cfz 13547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-er 8745 df-en 8986 df-dom 8987 df-sdom 8988 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-n0 12527 df-z 12614 df-uz 12879 df-fz 13548

This theorem is referenced by: poimirlem8 37635 poimirlem18 37645 poimirlem21 37648 poimirlem22 37649

W3C validator