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 34304

Description: Lemma for poimir 34314, 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)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))

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

**Proof of Theorem poimirlem23**
Step	Hyp	Ref	Expression
1		ovex 7002	. . . . . 6 ⊢ (𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
2	1	csbex 5066	. . . . 5 ⊢ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
3	2	rgenw 3094	. . . 4 ⊢ ∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4		eqid 2772	. . . . 5 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5		fveq1 6492	. . . . . . 7 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑁) = (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
6	5	neeq1d 3020	. . . . . 6 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7		df-ne 2962	. . . . . 6 ⊢ ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
8	6, 7	syl6bb 279	. . . . 5 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
9	4, 8	rexrnmpt 6680	. . . 4 ⊢ (∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
10	3, 9	ax-mp 5	. . 3 ⊢ (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
11		rexnal 3179	. . 3 ⊢ (∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
12	10, 11	bitri 267	. 2 ⊢ (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
13		poimir.0	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ ℕ)
14	13	nnzd 11892	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15		poimirlem23.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))
16		elfzelz 12717	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℤ)
18		zlem1lt 11840	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
19	14, 17, 18	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
20		elfzle2 12720	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁)
21	15, 20	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≤ 𝑁)
22	17	zred 11893	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ ℝ)
23	13	nnred 11448	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℝ)
24	22, 23	letri3d 10574	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 = 𝑁 ↔ (𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉)))
25	24	biimprd 240	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉) → 𝑉 = 𝑁))
26	21, 25	mpand 682	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 → 𝑉 = 𝑁))
27	19, 26	sylbird 252	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 − 1) < 𝑉 → 𝑉 = 𝑁))
28	27	necon3ad 2974	. . . . . . 7 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ (𝑁 − 1) < 𝑉))
29		nnm1nn0 11743	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
30	13, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
31		nn0fz0 12814	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℕ₀ ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
32	30, 31	sylib 210	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
33	32	adantr 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34		iffalse 4353	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
35	13	nncnd 11449	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36		npcan1 10858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
37	35, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
38	34, 37	sylan9eqr 2830	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
39	38	csbeq1d 3789	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40		oveq2 6978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
41	40	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
42	41	xpeq1d 5429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43		oveq1 6977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
44	43	oveq1d 6985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
45	44	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
46	45	xpeq1d 5429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
47	42, 46	uneq12d 4025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48		poimirlem23.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49		f1ofo 6445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50		foima 6418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
51	48, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
52	51	xpeq1d 5429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
53	23	ltp1d 11363	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
54	14	peano2zd 11896	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
55		fzn 12732	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
56	54, 14, 55	syl2anc 576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
57	53, 56	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
58	57	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
59	58	xpeq1d 5429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60		ima0 5779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 “ ∅) = ∅
61	60	xpeq1i 5426	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 “ ∅) × {0}) = (∅ × {0})
62		0xp 5492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ × {0}) = ∅
63	61, 62	eqtri 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 “ ∅) × {0}) = ∅
64	59, 63	syl6eq 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
65	52, 64	uneq12d 4025	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66		un0 4225	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
67	65, 66	syl6eq 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
68	47, 67	sylan9eqr 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
69	68	oveq2d 6986	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_𝑓 + ((1...𝑁) × {1})))
70	13, 69	csbied 3811	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⦋𝑁 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_𝑓 + ((1...𝑁) × {1})))
71	70	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋𝑁 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_𝑓 + ((1...𝑁) × {1})))
72	39, 71	eqtrd 2808	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_𝑓 + ((1...𝑁) × {1})))
73	72	fveq1d 6495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇 ∘_𝑓 + ((1...𝑁) × {1}))‘𝑁))
74		elfzonn0 12890	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ₀)
75		nn0p1nn 11741	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77		elsni 4452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
78	77	oveq2d 6986	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
79	78	eleq1d 2844	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
80	76, 79	syl5ibrcom 239	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
81	80	imp 398	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
82	81	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83		poimirlem23.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))
84		1ex 10427	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
85	84	fconst 6388	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) × {1}):(1...𝑁)⟶{1}
86	85	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87		ovexd 7004	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) ∈ V)
88		inidm 4077	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
89	82, 83, 86, 87, 87, 88	off 7236	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∘_𝑓 + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90		elfz1end 12746	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
91	13, 90	sylib 210	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92	89, 91	ffvelrnd 6671	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑇 ∘_𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
93	92	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇 ∘_𝑓 + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
94	73, 93	eqeltrd 2860	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
95	94	nnne0d 11483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96		breq1 4926	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98		oveq1 6977	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
99	96, 97, 98	ifbieq12d 4371	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
100	99	csbeq1d 3789	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑁 − 1) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101	100	fveq1d 6495	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑁 − 1) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102	101	neeq1d 3020	. . . . . . . . . . . 12 ⊢ (𝑦 = (𝑁 − 1) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
103	7, 102	syl5bbr 277	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑁 − 1) → (¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104	103	rspcev 3529	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
105	33, 95, 104	syl2anc 576	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106	105, 11	sylib 210	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107	106	ex 405	. . . . . . 7 ⊢ (𝜑 → (¬ (𝑁 − 1) < 𝑉 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
108	28, 107	syld 47	. . . . . 6 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
109	108	necon4ad 2980	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110	109	pm4.71rd 555	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
111	30	nn0zd 11891	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
112		uzid 12066	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
113		peano2uz 12108	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
114	111, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
115	37, 114	eqeltrrd 2861	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
116		fzss2 12756	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118	117	sselda 3854	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
119	91	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
120	83	ffnd 6339	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
121	120	adantr 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
122	84	fconst 6388	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123		c0ex 10425	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
124	123	fconst 6388	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125	122, 124	pm3.2i 463	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126		dff1o3 6444	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
127	126	simprbi 489	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
128		imain 6266	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
129	48, 127, 128	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130		elfzelz 12717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131	130	zred 11893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132	131	ltp1d 11363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133		fzdisj 12743	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135	134	imaeq2d 5764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136	135, 60	syl6eq 2824	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137	129, 136	sylan9req 2829	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138		fun 6363	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139	125, 137, 138	sylancr 578	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140		elfznn0 12809	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
141	140, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142		nnuz 12088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
143	141, 142	syl6eleq 2870	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
144		elfzuz3 12714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
145		fzsplit2 12741	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146	143, 144, 145	syl2anc 576	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147	146	imaeq2d 5764	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148		imaundi 5842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149	147, 148	syl6req 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150	149, 51	sylan9eqr 2830	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151	150	feq2d 6324	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152	139, 151	mpbid 224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153	152	ffnd 6339	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154		ovexd 7004	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155		eqidd 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇‘𝑁) = (𝑇‘𝑁))
156		eqidd 2773	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157	121, 153, 154, 154, 88, 155, 156	ofval 7230	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158	119, 157	mpdan 674	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159	158	eqeq1d 2774	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
160	83, 91	ffvelrnd 6671	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇‘𝑁) ∈ (0..^𝐾))
161		elfzonn0 12890	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑁) ∈ (0..^𝐾) → (𝑇‘𝑁) ∈ ℕ₀)
162	160, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℕ₀)
163	162	nn0red 11761	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℝ)
164	163	adantr 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇‘𝑁) ∈ ℝ)
165	162	nn0ge0d 11763	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑇‘𝑁))
166	165	adantr 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇‘𝑁))
167		1re 10431	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
168		snssi 4609	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → {1} ⊆ ℝ)
169	167, 168	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {1} ⊆ ℝ
170		0re 10433	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171		snssi 4609	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
172	170, 171	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {0} ⊆ ℝ
173	169, 172	unssi 4045	. . . . . . . . . . . 12 ⊢ ({1} ∪ {0}) ⊆ ℝ
174	152, 119	ffvelrnd 6671	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175	173, 174	sseldi 3852	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176		elun 4010	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177		0le1 10956	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
178		elsni 4452	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179	177, 178	syl5breqr 4961	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180		0le0 11541	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 0
181		elsni 4452	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182	180, 181	syl5breqr 4961	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183	179, 182	jaoi 843	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184	176, 183	sylbi 209	. . . . . . . . . . . 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 10945	. . . . . . . . . . 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 826	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
188	159, 187	bitrd 271	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189	118, 188	syldan 582	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190	189	ralbidva 3140	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191	190	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192		breq2 4927	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝑁 → (𝑦 < 𝑉 ↔ 𝑦 < 𝑁))
193	192	ifbid 4366	. . . . . . . . . . . . 13 ⊢ (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194		elfzelz 12717	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195	194	zred 11893	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196	195	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
197	30	nn0red 11761	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
198	197	adantr 473	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
199	23	adantr 473	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200		elfzle2 12720	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201	200	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
202	23	ltm1d 11365	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
203	202	adantr 473	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204	196, 198, 199, 201, 203	lelttrd 10590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205	204	iftrued 4352	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206	193, 205	sylan9eqr 2830	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207	206	an32s 639	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208	207	csbeq1d 3789	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209	208	fveq1d 6495	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210	209	eqeq1d 2774	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211	210	ralbidva 3140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212		nfv 1873	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213		nfcsb1v 3800	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑁
215	213, 214	nffv 6503	. . . . . . . . 9 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216	215	nfeq1 2939	. . . . . . . 8 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217		csbeq1a 3791	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218	217	fveq1d 6495	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219	218	eqeq1d 2774	. . . . . . . 8 ⊢ (𝑗 = 𝑦 → (((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220	212, 216, 219	cbvral 3373	. . . . . . 7 ⊢ (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
221	211, 220	syl6bbr 281	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222		ne0i 4181	. . . . . . . . . 10 ⊢ ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223		r19.3rzv 4321	. . . . . . . . . 10 ⊢ ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
224	32, 222, 223	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
225		elfzelz 12717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226	225	zred 11893	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227	226	ltp1d 11363	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228	227, 133	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229	228	imaeq2d 5764	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230	229, 60	syl6eq 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231	129, 230	sylan9req 2829	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232	231	adantlr 702	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233		simplr 756	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) = 𝑁)
234		f1ofn 6439	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
235	48, 234	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
236	235	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237		elfznn0 12809	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ₀)
238	237, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239	238, 142	syl6eleq 2870	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ_≥‘1))
240		fzss1 12755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242	241	adantl 474	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
243	37	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244		elfzuz3 12714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑗))
245		eluzp1p1 12077	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
247	246	adantl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
248	243, 247	eqeltrrd 2861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑗 + 1)))
249		eluzfz2 12724	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251		fnfvima 6814	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252	236, 242, 250, 251	syl3anc 1351	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253	252	adantlr 702	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254	233, 253	eqeltrrd 2861	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255		fnconstg 6390	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
256	84, 255	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257		fnconstg 6390	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258	123, 257	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259		fvun2 6577	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260	256, 258, 259	mp3an12 1430	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261	232, 254, 260	syl2anc 576	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262	123	fvconst2 6787	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263	254, 262	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264	261, 263	eqtrd 2808	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265	264	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑈‘𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266	265	ex 405	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
267	32	adantr 473	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268		ax-1ne0 10396	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
269		imain 6266	. . . . . . . . . . . . . . . . . . . . 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 4951	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272		fzdisj 12743	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273	271, 272	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274	273	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275	274, 60	syl6eq 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276	270, 275	eqtr3d 2810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277	276	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
278	91	adantr 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279		elimasni 5790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280		fnbrfvb 6542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
281	235, 91, 280	syl2anc 576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
282	279, 281	syl5ibr 238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈‘𝑁) = 𝑁))
283	282	necon3ad 2974	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284	283	imp 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285	278, 284	eldifd 3836	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286		imadif 6265	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
287	48, 127, 286	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288		difun2 4306	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289	13, 142	syl6eleq 2870	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
290		fzm1 12796	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
291	289, 290	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
292		elun 4010	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
293		velsn 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
294	293	orbi2i 896	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
295	292, 294	bitri 267	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
296	291, 295	syl6rbbr 282	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297	296	eqrdv 2770	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298	297	difeq1d 3984	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299	197, 23	ltnled 10579	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300	202, 299	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301		elfzle2 12720	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302	300, 301	nsyl 138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303		difsn 4599	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305	288, 298, 304	3eqtr3a 2832	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306	305	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
307	51	difeq1d 3984	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308	287, 306, 307	3eqtr3rd 2817	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309	308	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310	285, 309	eleqtrd 2862	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311		fnconstg 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
312	84, 311	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313		fnconstg 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314	123, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315		fvun1 6576	. . . . . . . . . . . . . . . . . . 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 1430	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317	277, 310, 316	syl2anc 576	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
318	84	fvconst2 6787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319	310, 318	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320	317, 319	eqtrd 2808	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321	320	neeq1d 3020	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322	268, 321	mpbiri 250	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323		df-ne 2962	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324		oveq2 6978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325	324	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326	325	xpeq1d 5429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327		oveq1 6977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328	327	oveq1d 6985	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329	328	imaeq2d 5764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330	329	xpeq1d 5429	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331	326, 330	uneq12d 4025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332	331	fveq1d 6495	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333	332	neeq1d 3020	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334	323, 333	syl5bbr 277	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335	334	rspcev 3529	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336	267, 322, 335	syl2anc 576	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337	336	ex 405	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338		rexnal 3179	. . . . . . . . . . . 12 ⊢ (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339	337, 338	syl6ib 243	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340	339	necon4ad 2980	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈‘𝑁) = 𝑁))
341	266, 340	impbid 204	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342	224, 341	anbi12d 621	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343		r19.26 3114	. . . . . . . 8 ⊢ (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344	342, 343	syl6bbr 281	. . . . . . 7 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345	344	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346	191, 221, 345	3bitr4d 303	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))
347	346	pm5.32da 571	. . . 4 ⊢ (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
348	110, 347	bitrd 271	. . 3 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
349	348	notbid 310	. 2 ⊢ (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
350	12, 349	syl5bb 275	1 ⊢ (𝜑 → (∃𝑝 ∈ ran (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_𝑓 + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))(𝑝‘𝑁) ≠ 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 387 ∨ wo 833 = wceq 1507 ∈ wcel 2048 ≠ wne 2961 ∀wral 3082 ∃wrex 3083 Vcvv 3409 ⦋csb 3782 ∖ cdif 3822 ∪ cun 3823 ∩ cin 3824 ⊆ wss 3825 ∅c0 4173 ifcif 4344 {csn 4435 class class class wbr 4923 ↦ cmpt 5002 × cxp 5398 ^◡ccnv 5399 ran crn 5401 “ cima 5403 Fun wfun 6176 Fn wfn 6177 ⟶wf 6178 –onto→wfo 6180 –1-1-onto→wf1o 6181 ‘cfv 6182 (class class class)co 6970 ∘_𝑓 cof 7219 ℂcc 10325 ℝcr 10326 0cc0 10327 1c1 10328 + caddc 10330 < clt 10466 ≤ cle 10467 − cmin 10662 ℕcn 11431 ℕ₀cn0 11700 ℤcz 11786 ℤ_≥cuz 12051 ...cfz 12701 ..^cfzo 12842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-of 7221 df-om 7391 df-1st 7494 df-2nd 7495 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-er 8081 df-en 8299 df-dom 8300 df-sdom 8301 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-nn 11432 df-n0 11701 df-z 11787 df-uz 12052 df-fz 12702 df-fzo 12843

This theorem is referenced by: poimirlem24 34305

W3C validator