poimirlem23 - Mathbox for Brendan Leahy

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

Theorem poimirlem23 38025

Description: Lemma for poimir 38035, two ways of expressing the property that a face is not on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)

**Hypotheses**
Ref	Expression
poimir.0	⊢ (𝜑 → 𝑁 ∈ ℕ)
poimirlem23.1	⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))
poimirlem23.2	⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
poimirlem23.3	⊢ (𝜑 → 𝑉 ∈ (0...𝑁))

**Assertion**
Ref	Expression
poimirlem23	⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))

Distinct variable groups: 𝑗,𝑝,𝑦,𝜑 𝑗,𝑁,𝑦 𝑇,𝑗,𝑦 𝑈,𝑗,𝑦 𝑗,𝑉,𝑦 𝜑,𝑝 𝑗,𝐾,𝑝 𝑁,𝑝 𝑇,𝑝 𝑈,𝑝 𝑦,𝐾 𝑉,𝑝

**Proof of Theorem poimirlem23**
Step	Hyp	Ref	Expression
1		ovex 7393	. . . . . 6 ⊢ (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
2	1	csbex 5236	. . . . 5 ⊢ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
3	2	rgenw 3059	. . . 4 ⊢ ∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4		eqid 2741	. . . . 5 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5		fveq1 6830	. . . . . . 7 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑁) = (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
6	5	neeq1d 2995	. . . . . 6 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7		df-ne 2937	. . . . . 6 ⊢ ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
8	6, 7	bitrdi 289	. . . . 5 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
9	4, 8	rexrnmptw 7040	. . . 4 ⊢ (∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
10	3, 9	ax-mp 5	. . 3 ⊢ (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
11		rexnal 3093	. . 3 ⊢ (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
12	10, 11	bitri 277	. 2 ⊢ (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
13		poimir.0	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
14	13	nnzd 12545	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15		poimirlem23.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))
16		elfzelz 13473	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℤ)
18		zlem1lt 12574	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
19	14, 17, 18	syl2anc 591	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
20		elfzle2 13477	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁)
21	15, 20	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≤ 𝑁)
22	17	zred 12628	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ ℝ)
23	13	nnred 12184	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℝ)
24	22, 23	letri3d 11283	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 = 𝑁 ↔ (𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉)))
25	24	biimprd 250	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉) → 𝑉 = 𝑁))
26	21, 25	mpand 702	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 → 𝑉 = 𝑁))
27	19, 26	sylbird 262	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 − 1) < 𝑉 → 𝑉 = 𝑁))
28	27	necon3ad 2949	. . . . . . 7 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ (𝑁 − 1) < 𝑉))
29		nnm1nn0 12473	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
30	13, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
31		nn0fz0 13574	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℕ₀ ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
32	30, 31	sylib 220	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
33	32	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34		iffalse 4466	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
35	13	nncnd 12185	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36		npcan1 11570	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
37	35, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
38	34, 37	sylan9eqr 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
39	38	csbeq1d 3837	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40		oveq2 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
41	40	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
42	41	xpeq1d 5650	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43		oveq1 7367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
44	43	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
45	44	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
46	45	xpeq1d 5650	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
47	42, 46	uneq12d 4102	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48		poimirlem23.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49		f1ofo 6778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50		foima 6748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
51	48, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
52	51	xpeq1d 5650	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
53	23	ltp1d 12081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
54	14	peano2zd 12631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
55		fzn 13489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
56	54, 14, 55	syl2anc 591	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
57	53, 56	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
58	57	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
59	58	xpeq1d 5650	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60		ima0 6036	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 “ ∅) = ∅
61	60	xpeq1i 5647	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 “ ∅) × {0}) = (∅ × {0})
62		0xp 5720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ × {0}) = ∅
63	61, 62	eqtri 2764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 “ ∅) × {0}) = ∅
64	59, 63	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
65	52, 64	uneq12d 4102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66		un0 4325	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
67	65, 66	eqtrdi 2792	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
68	47, 67	sylan9eqr 2798	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
69	68	oveq2d 7376	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
70	13, 69	csbied 3869	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
71	70	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
72	39, 71	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
73	72	fveq1d 6833	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁))
74		elfzonn0 13657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ₀)
75		nn0p1nn 12471	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77		elsni 4575	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
78	77	oveq2d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
79	78	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
80	76, 79	syl5ibrcom 249	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
81	80	imp 408	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
82	81	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83		poimirlem23.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))
84		1ex 11135	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
85	84	fconst 6717	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) × {1}):(1...𝑁)⟶{1}
86	85	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87		ovexd 7395	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) ∈ V)
88		inidm 4158	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
89	82, 83, 86, 87, 87, 88	off 7642	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∘_f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90		elfz1end 13503	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
91	13, 90	sylib 220	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92	89, 91	ffvelcdmd 7030	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
93	92	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
94	73, 93	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
95	94	nnne0d 12222	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96		breq1 5078	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98		oveq1 7367	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
99	96, 97, 98	ifbieq12d 4486	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
100	99	csbeq1d 3837	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑁 − 1) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101	100	fveq1d 6833	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑁 − 1) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102	101	neeq1d 2995	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑁 − 1) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
103	7, 102	bitr3id 287	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑁 − 1) → (¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104	103	rspcev 3562	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
105	33, 95, 104	syl2anc 591	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106	105, 11	sylib 220	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107	106	ex 414	. . . . . . 7 ⊢ (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
108	28, 107	syld 47	. . . . . 6 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
109	108	necon4ad 2955	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110	109	pm4.71rd 568	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
111	30	nn0zd 12544	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
112		uzid 12798	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
113		peano2uz 12846	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
114	111, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
115	37, 114	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
116		fzss2 13513	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118	117	sselda 3917	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
119	91	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
120	83	ffnd 6660	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
121	120	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
122	84	fconst 6717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123		c0ex 11133	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
124	123	fconst 6717	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125	122, 124	pm3.2i 472	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126		dff1o3 6777	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
127	126	simprbi 499	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
128		imain 6574	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
129	48, 127, 128	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130		elfzelz 13473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131	130	zred 12628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132	131	ltp1d 12081	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133		fzdisj 13500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135	134	imaeq2d 6019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136	135, 60	eqtrdi 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137	129, 136	sylan9req 2797	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138		fun 6693	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139	125, 137, 138	sylancr 594	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140		elfznn0 13569	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
141	140, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142		nnuz 12822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
143	141, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
144		elfzuz3 13470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
145		fzsplit2 13498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146	143, 144, 145	syl2anc 591	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147	146	imaeq2d 6019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148		imaundi 6104	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149	147, 148	eqtr2di 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150	149, 51	sylan9eqr 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151	150	feq2d 6643	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152	139, 151	mpbid 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153	152	ffnd 6660	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154		ovexd 7395	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155		eqidd 2742	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇‘𝑁) = (𝑇‘𝑁))
156		eqidd 2742	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157	121, 153, 154, 154, 88, 155, 156	ofval 7635	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158	119, 157	mpdan 694	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159	158	eqeq1d 2743	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
160	83, 91	ffvelcdmd 7030	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇‘𝑁) ∈ (0..^𝐾))
161		elfzonn0 13657	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑁) ∈ (0..^𝐾) → (𝑇‘𝑁) ∈ ℕ₀)
162	160, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℕ₀)
163	162	nn0red 12494	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℝ)
164	163	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇‘𝑁) ∈ ℝ)
165	162	nn0ge0d 12496	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑇‘𝑁))
166	165	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇‘𝑁))
167		1re 11139	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
168		snssi 4720	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → {1} ⊆ ℝ)
169	167, 168	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {1} ⊆ ℝ
170		0re 11141	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171		snssi 4720	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
172	170, 171	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {0} ⊆ ℝ
173	169, 172	unssi 4123	. . . . . . . . . . . 12 ⊢ ({1} ∪ {0}) ⊆ ℝ
174	152, 119	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175	173, 174	sselid 3915	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176		elun 4086	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177		0le1 11668	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
178		elsni 4575	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179	177, 178	breqtrrid 5113	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180		0le0 12277	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 0
181		elsni 4575	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182	180, 181	breqtrrid 5113	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183	179, 182	jaoi 864	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184	176, 183	sylbi 219	. . . . . . . . . . . 12 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
185	174, 184	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
186		add20 11657	. . . . . . . . . . 11 ⊢ ((((𝑇‘𝑁) ∈ ℝ ∧ 0 ≤ (𝑇‘𝑁)) ∧ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ ∧ 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
187	164, 166, 175, 185, 186	syl22anc 845	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
188	159, 187	bitrd 281	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189	118, 188	syldan 598	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190	189	ralbidva 3162	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191	190	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192		breq2 5079	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝑁 → (𝑦 < 𝑉 ↔ 𝑦 < 𝑁))
193	192	ifbid 4481	. . . . . . . . . . . . 13 ⊢ (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194		elfzelz 13473	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195	194	zred 12628	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196	195	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
197	30	nn0red 12494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
198	197	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
199	23	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200		elfzle2 13477	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201	200	adantl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
202	23	ltm1d 12083	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
203	202	adantr 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204	196, 198, 199, 201, 203	lelttrd 11299	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205	204	iftrued 4465	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206	193, 205	sylan9eqr 2798	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207	206	an32s 659	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208	207	csbeq1d 3837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209	208	fveq1d 6833	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210	209	eqeq1d 2743	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211	210	ralbidva 3162	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212		nfv 1922	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213		nfcsb1v 3857	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214		nfcv 2903	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑁
215	213, 214	nffv 6841	. . . . . . . . 9 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216	215	nfeq1 2918	. . . . . . . 8 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217		csbeq1a 3847	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218	217	fveq1d 6833	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219	218	eqeq1d 2743	. . . . . . . 8 ⊢ (𝑗 = 𝑦 → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220	212, 216, 219	cbvralw 3283	. . . . . . 7 ⊢ (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
221	211, 220	bitr4di 291	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222		ne0i 4272	. . . . . . . . . 10 ⊢ ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223		r19.3rzv 4434	. . . . . . . . . 10 ⊢ ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
224	32, 222, 223	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
225		elfzelz 13473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226	225	zred 12628	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227	226	ltp1d 12081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228	227, 133	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229	228	imaeq2d 6019	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230	229, 60	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231	129, 230	sylan9req 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232	231	adantlr 722	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233		simplr 775	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) = 𝑁)
234		f1ofn 6772	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
235	48, 234	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
236	235	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237		elfznn0 13569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ₀)
238	237, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239	238, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ_≥‘1))
240		fzss1 13512	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242	241	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
243	37	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244		elfzuz3 13470	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑗))
245		eluzp1p1 12811	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
247	246	adantl 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
248	243, 247	eqeltrrd 2842	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑗 + 1)))
249		eluzfz2 13481	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251		fnfvima 7181	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252	236, 242, 250, 251	syl3anc 1380	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253	252	adantlr 722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254	233, 253	eqeltrrd 2842	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255		fnconstg 6719	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
256	84, 255	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257		fnconstg 6719	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258	123, 257	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259		fvun2 6923	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260	256, 258, 259	mp3an12 1460	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261	232, 254, 260	syl2anc 591	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262	123	fvconst2 7152	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263	254, 262	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264	261, 263	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265	264	ralrimiva 3133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑈‘𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266	265	ex 414	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
267	32	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268		ax-1ne0 11102	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
269		imain 6574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
270	48, 127, 269	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))))
271	202, 37	breqtrrd 5103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272		fzdisj 13500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273	271, 272	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274	273	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275	274, 60	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276	270, 275	eqtr3d 2778	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277	276	adantr 482	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
278	91	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279		elimasni 6050	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280		fnbrfvb 6881	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
281	235, 91, 280	syl2anc 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
282	279, 281	imbitrrid 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈‘𝑁) = 𝑁))
283	282	necon3ad 2949	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284	283	imp 408	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285	278, 284	eldifd 3896	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286		imadif 6573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
287	48, 127, 286	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288		difun2 4412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289		elun 4086	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
290		velsn 4574	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
291	290	orbi2i 919	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
292	289, 291	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
293	13, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
294		fzm1 13556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
296	292, 295	bitr4id 292	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297	296	eqrdv 2739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298	297	difeq1d 4059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299	197, 23	ltnled 11288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300	202, 299	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301		elfzle2 13477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302	300, 301	nsyl 140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303		difsn 4734	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305	288, 298, 304	3eqtr3a 2800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306	305	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
307	51	difeq1d 4059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308	287, 306, 307	3eqtr3rd 2785	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309	308	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310	285, 309	eleqtrd 2843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311		fnconstg 6719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
312	84, 311	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313		fnconstg 6719	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314	123, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315		fvun1 6922	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑈 “ (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})‘𝑁))
316	312, 314, 315	mp3an12 1460	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317	277, 310, 316	syl2anc 591	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
318	84	fvconst2 7152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319	310, 318	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320	317, 319	eqtrd 2776	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321	320	neeq1d 2995	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322	268, 321	mpbiri 260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323		df-ne 2937	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324		oveq2 7368	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325	324	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326	325	xpeq1d 5650	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327		oveq1 7367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328	327	oveq1d 7375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329	328	imaeq2d 6019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330	329	xpeq1d 5650	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331	326, 330	uneq12d 4102	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332	331	fveq1d 6833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333	332	neeq1d 2995	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334	323, 333	bitr3id 287	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335	334	rspcev 3562	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336	267, 322, 335	syl2anc 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337	336	ex 414	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338		rexnal 3093	. . . . . . . . . . . 12 ⊢ (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339	337, 338	imbitrdi 253	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340	339	necon4ad 2955	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈‘𝑁) = 𝑁))
341	266, 340	impbid 214	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342	224, 341	anbi12d 639	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343		r19.26 3101	. . . . . . . 8 ⊢ (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344	342, 343	bitr4di 291	. . . . . . 7 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345	344	adantr 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346	191, 221, 345	3bitr4d 313	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))
347	346	pm5.32da 585	. . . 4 ⊢ (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
348	110, 347	bitrd 281	. . 3 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
349	348	notbid 320	. 2 ⊢ (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
350	12, 349	bitrid 285	1 ⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∨ wo 854 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 Vcvv 3433 ⦋csb 3833 ∖ cdif 3882 ∪ cun 3883 ∩ cin 3884 ⊆ wss 3885 ∅c0 4264 ifcif 4457 {csn 4558 class class class wbr 5075 ↦ cmpt 5156 × cxp 5619 ^◡ccnv 5620 ran crn 5622 “ cima 5624 Fun wfun 6483 Fn wfn 6484 ⟶wf 6485 –onto→wfo 6487 –1-1-onto→wf1o 6488 ‘cfv 6489 (class class class)co 7360 ∘_f cof 7622 ℂcc 11031 ℝcr 11032 0cc0 11033 1c1 11034 + caddc 11036 < clt 11174 ≤ cle 11175 − cmin 11372 ℕcn 12169 ℕ₀cn0 12432 ℤcz 12519 ℤ_≥cuz 12783 ...cfz 13456 ..^cfzo 13603

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-of 7624 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-n0 12433 df-z 12520 df-uz 12784 df-fz 13457 df-fzo 13604

This theorem is referenced by: poimirlem24 38026

W3C validator