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 38147

Description: Lemma for poimir 38157, 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 7431	. . . . . 6 ⊢ (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
2	1	csbex 5263	. . . . 5 ⊢ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
3	2	rgenw 3082	. . . 4 ⊢ ∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4		eqid 2764	. . . . 5 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5		fveq1 6868	. . . . . . 7 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑁) = (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
6	5	neeq1d 3018	. . . . . 6 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7		df-ne 2960	. . . . . 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 7078	. . . 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 3116	. . 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 12596	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15		poimirlem23.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))
16		elfzelz 13531	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℤ)
18		zlem1lt 12625	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
19	14, 17, 18	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
20		elfzle2 13535	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁)
21	15, 20	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≤ 𝑁)
22	17	zred 12679	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ ℝ)
23	13	nnred 12227	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℝ)
24	22, 23	letri3d 11327	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 = 𝑁 ↔ (𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉)))
25	24	biimprd 250	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉) → 𝑉 = 𝑁))
26	21, 25	mpand 705	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 → 𝑉 = 𝑁))
27	19, 26	sylbird 262	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 − 1) < 𝑉 → 𝑉 = 𝑁))
28	27	necon3ad 2972	. . . . . . 7 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ (𝑁 − 1) < 𝑉))
29		nnm1nn0 12524	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
30	13, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
31		nn0fz0 13632	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℕ₀ ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
32	30, 31	sylib 220	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
33	32	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34		iffalse 4491	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
35	13	nncnd 12228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36		npcan1 11614	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
37	35, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
38	34, 37	sylan9eqr 2821	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
39	38	csbeq1d 3858	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40		oveq2 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
41	40	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
42	41	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43		oveq1 7405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
44	43	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
45	44	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
46	45	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
47	42, 46	uneq12d 4124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48		poimirlem23.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49		f1ofo 6816	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50		foima 6785	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
51	48, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
52	51	xpeq1d 5678	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
53	23	ltp1d 12124	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
54	14	peano2zd 12682	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
55		fzn 13547	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
56	54, 14, 55	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
57	53, 56	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
58	57	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
59	58	xpeq1d 5678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60		ima0 6068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 “ ∅) = ∅
61	60	xpeq1i 5675	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 “ ∅) × {0}) = (∅ × {0})
62		0xp 5748	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ × {0}) = ∅
63	61, 62	eqtri 2787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 “ ∅) × {0}) = ∅
64	59, 63	eqtrdi 2815	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
65	52, 64	uneq12d 4124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66		un0 4350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
67	65, 66	eqtrdi 2815	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
68	47, 67	sylan9eqr 2821	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
69	68	oveq2d 7414	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
70	13, 69	csbied 3890	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
71	70	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
72	39, 71	eqtrd 2799	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
73	72	fveq1d 6871	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁))
74		elfzonn0 13715	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ₀)
75		nn0p1nn 12522	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77		elsni 4601	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
78	77	oveq2d 7414	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
79	78	eleq1d 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
80	76, 79	syl5ibrcom 249	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
81	80	imp 410	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
82	81	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83		poimirlem23.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))
84		1ex 11178	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
85	84	fconst 6752	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) × {1}):(1...𝑁)⟶{1}
86	85	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87		ovexd 7433	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) ∈ V)
88		inidm 4180	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
89	82, 83, 86, 87, 87, 88	off 7680	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∘_f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90		elfz1end 13561	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
91	13, 90	sylib 220	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92	89, 91	ffvelcdmd 7068	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
93	92	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
94	73, 93	eqeltrd 2864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
95	94	nnne0d 12265	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96		breq1 5105	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98		oveq1 7405	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
99	96, 97, 98	ifbieq12d 4511	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
100	99	csbeq1d 3858	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑁 − 1) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101	100	fveq1d 6871	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑁 − 1) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102	101	neeq1d 3018	. . . . . . . . . . . 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 3583	. . . . . . . . . 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 593	. . . . . . . . 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 416	. . . . . . 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 2978	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110	109	pm4.71rd 570	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
111	30	nn0zd 12595	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
112		uzid 12856	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
113		peano2uz 12904	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
114	111, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
115	37, 114	eqeltrrd 2865	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
116		fzss2 13571	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118	117	sselda 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
119	91	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
120	83	ffnd 6694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
121	120	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
122	84	fconst 6752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123		c0ex 11175	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
124	123	fconst 6752	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125	122, 124	pm3.2i 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126		dff1o3 6815	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
127	126	simprbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
128		imain 6608	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
129	48, 127, 128	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130		elfzelz 13531	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131	130	zred 12679	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132	131	ltp1d 12124	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133		fzdisj 13558	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135	134	imaeq2d 6051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136	135, 60	eqtrdi 2815	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137	129, 136	sylan9req 2820	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138		fun 6728	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139	125, 137, 138	sylancr 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140		elfznn0 13627	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
141	140, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142		nnuz 12880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
143	141, 142	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
144		elfzuz3 13528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
145		fzsplit2 13556	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146	143, 144, 145	syl2anc 593	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147	146	imaeq2d 6051	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148		imaundi 6136	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149	147, 148	eqtr2di 2816	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150	149, 51	sylan9eqr 2821	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151	150	feq2d 6677	. . . . . . . . . . . . . . 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 6694	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154		ovexd 7433	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155		eqidd 2765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇‘𝑁) = (𝑇‘𝑁))
156		eqidd 2765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157	121, 153, 154, 154, 88, 155, 156	ofval 7673	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158	119, 157	mpdan 697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159	158	eqeq1d 2766	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
160	83, 91	ffvelcdmd 7068	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇‘𝑁) ∈ (0..^𝐾))
161		elfzonn0 13715	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑁) ∈ (0..^𝐾) → (𝑇‘𝑁) ∈ ℕ₀)
162	160, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℕ₀)
163	162	nn0red 12545	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℝ)
164	163	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇‘𝑁) ∈ ℝ)
165	162	nn0ge0d 12547	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑇‘𝑁))
166	165	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇‘𝑁))
167		1re 11183	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
168		snssi 4746	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → {1} ⊆ ℝ)
169	167, 168	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {1} ⊆ ℝ
170		0re 11185	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171		snssi 4746	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
172	170, 171	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {0} ⊆ ℝ
173	169, 172	unssi 4145	. . . . . . . . . . . 12 ⊢ ({1} ∪ {0}) ⊆ ℝ
174	152, 119	ffvelcdmd 7068	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175	173, 174	sselid 3936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176		elun 4108	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177		0le1 11712	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
178		elsni 4601	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179	177, 178	breqtrrid 5140	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180		0le0 12321	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 0
181		elsni 4601	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182	180, 181	breqtrrid 5140	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183	179, 182	jaoi 868	. . . . . . . . . . . . 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 11701	. . . . . . . . . . 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 849	. . . . . . . . . 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 600	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190	189	ralbidva 3185	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191	190	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192		breq2 5106	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝑁 → (𝑦 < 𝑉 ↔ 𝑦 < 𝑁))
193	192	ifbid 4506	. . . . . . . . . . . . 13 ⊢ (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194		elfzelz 13531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195	194	zred 12679	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196	195	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
197	30	nn0red 12545	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
198	197	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
199	23	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200		elfzle2 13535	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201	200	adantl 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
202	23	ltm1d 12126	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
203	202	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204	196, 198, 199, 201, 203	lelttrd 11343	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205	204	iftrued 4490	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206	193, 205	sylan9eqr 2821	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207	206	an32s 662	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208	207	csbeq1d 3858	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209	208	fveq1d 6871	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210	209	eqeq1d 2766	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211	210	ralbidva 3185	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213		nfcsb1v 3878	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑁
215	213, 214	nffv 6879	. . . . . . . . 9 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216	215	nfeq1 2941	. . . . . . . 8 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217		csbeq1a 3868	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218	217	fveq1d 6871	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219	218	eqeq1d 2766	. . . . . . . 8 ⊢ (𝑗 = 𝑦 → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
220	212, 216, 219	cbvralw 3306	. . . . . . 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 4295	. . . . . . . . . 10 ⊢ ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223		r19.3rzv 4459	. . . . . . . . . 10 ⊢ ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
224	32, 222, 223	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
225		elfzelz 13531	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226	225	zred 12679	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227	226	ltp1d 12124	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228	227, 133	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229	228	imaeq2d 6051	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230	229, 60	eqtrdi 2815	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231	129, 230	sylan9req 2820	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232	231	adantlr 725	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233		simplr 778	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) = 𝑁)
234		f1ofn 6809	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
235	48, 234	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
236	235	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237		elfznn0 13627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ₀)
238	237, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239	238, 142	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ_≥‘1))
240		fzss1 13570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242	241	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
243	37	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244		elfzuz3 13528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑗))
245		eluzp1p1 12869	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
247	246	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
248	243, 247	eqeltrrd 2865	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑗 + 1)))
249		eluzfz2 13539	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251		fnfvima 7219	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252	236, 242, 250, 251	syl3anc 1392	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253	252	adantlr 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254	233, 253	eqeltrrd 2865	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255		fnconstg 6754	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
256	84, 255	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257		fnconstg 6754	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258	123, 257	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259		fvun2 6961	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260	256, 258, 259	mp3an12 1474	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261	232, 254, 260	syl2anc 593	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262	123	fvconst2 7190	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263	254, 262	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264	261, 263	eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265	264	ralrimiva 3156	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑈‘𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266	265	ex 416	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
267	32	adantr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268		ax-1ne0 11144	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
269		imain 6608	. . . . . . . . . . . . . . . . . . . . 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 5130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272		fzdisj 13558	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273	271, 272	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274	273	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275	274, 60	eqtrdi 2815	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276	270, 275	eqtr3d 2801	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277	276	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
278	91	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279		elimasni 6082	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280		fnbrfvb 6919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
281	235, 91, 280	syl2anc 593	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
282	279, 281	imbitrrid 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈‘𝑁) = 𝑁))
283	282	necon3ad 2972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284	283	imp 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285	278, 284	eldifd 3917	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286		imadif 6607	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
287	48, 127, 286	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288		difun2 4437	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289		elun 4108	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
290		velsn 4600	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
291	290	orbi2i 923	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
292	289, 291	bitri 277	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
293	13, 142	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
294		fzm1 13614	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298	297	difeq1d 4081	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299	197, 23	ltnled 11332	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300	202, 299	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301		elfzle2 13535	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302	300, 301	nsyl 140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303		difsn 4760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305	288, 298, 304	3eqtr3a 2823	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306	305	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
307	51	difeq1d 4081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308	287, 306, 307	3eqtr3rd 2808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309	308	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310	285, 309	eleqtrd 2866	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311		fnconstg 6754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
312	84, 311	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313		fnconstg 6754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314	123, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315		fvun1 6960	. . . . . . . . . . . . . . . . . . 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 1474	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317	277, 310, 316	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
318	84	fvconst2 7190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319	310, 318	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320	317, 319	eqtrd 2799	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321	320	neeq1d 3018	. . . . . . . . . . . . . . 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 2960	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324		oveq2 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325	324	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326	325	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327		oveq1 7405	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328	327	oveq1d 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329	328	imaeq2d 6051	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330	329	xpeq1d 5678	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331	326, 330	uneq12d 4124	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332	331	fveq1d 6871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333	332	neeq1d 3018	. . . . . . . . . . . . . . . 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 3583	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336	267, 322, 335	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337	336	ex 416	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338		rexnal 3116	. . . . . . . . . . . 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 2978	. . . . . . . . . 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 641	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343		r19.26 3124	. . . . . . . 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 484	. . . . . 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 587	. . . 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 399 ∨ wo 858 = wceq 1562 ∈ wcel 2144 ≠ wne 2959 ∀wral 3078 ∃wrex 3088 Vcvv 3456 ⦋csb 3854 ∖ cdif 3903 ∪ cun 3904 ∩ cin 3905 ⊆ wss 3906 ∅c0 4287 ifcif 4482 {csn 4584 class class class wbr 5102 ↦ cmpt 5183 × cxp 5647 ^◡ccnv 5648 ran crn 5650 “ cima 5652 Fun wfun 6517 Fn wfn 6518 ⟶wf 6519 –onto→wfo 6521 –1-1-onto→wf1o 6522 ‘cfv 6523 (class class class)co 7398 ∘_f cof 7660 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 < clt 11218 ≤ cle 11219 − cmin 11416 ℕcn 12212 ℕ₀cn0 12483 ℤcz 12570 ℤ_≥cuz 12841 ...cfz 13514 ..^cfzo 13661

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-rep 5229 ax-sep 5248 ax-nul 5258 ax-pow 5324 ax-pr 5392 ax-un 7720 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3064 df-ral 3079 df-rex 3089 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-riota 7355 df-ov 7401 df-oprab 7402 df-mpo 7403 df-of 7662 df-om 7849 df-1st 7972 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-er 8680 df-en 8930 df-dom 8931 df-sdom 8932 df-pnf 11220 df-mnf 11221 df-xr 11222 df-ltxr 11223 df-le 11224 df-sub 11418 df-neg 11419 df-nn 12213 df-n0 12484 df-z 12571 df-uz 12842 df-fz 13515 df-fzo 13662

This theorem is referenced by: poimirlem24 38148

W3C validator