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 37650

Description: Lemma for poimir 37660, 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 7464	. . . . . 6 ⊢ (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
2	1	csbex 5311	. . . . 5 ⊢ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
3	2	rgenw 3065	. . . 4 ⊢ ∀𝑦 ∈ (0...(𝑁 − 1))⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) ∈ V
4		eqid 2737	. . . . 5 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))) = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
5		fveq1 6905	. . . . . . 7 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → (𝑝‘𝑁) = (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
6	5	neeq1d 3000	. . . . . 6 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
7		df-ne 2941	. . . . . 6 ⊢ ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
8	6, 7	bitrdi 287	. . . . 5 ⊢ (𝑝 = ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) → ((𝑝‘𝑁) ≠ 0 ↔ ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
9	4, 8	rexrnmptw 7115	. . . 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 3100	. . 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 275	. 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 12640	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℤ)
15		poimirlem23.3	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑉 ∈ (0...𝑁))
16		elfzelz 13564	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ∈ ℤ)
17	15, 16	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℤ)
18		zlem1lt 12669	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝑉 ∈ ℤ) → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
19	14, 17, 18	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 ↔ (𝑁 − 1) < 𝑉))
20		elfzle2 13568	. . . . . . . . . . 11 ⊢ (𝑉 ∈ (0...𝑁) → 𝑉 ≤ 𝑁)
21	15, 20	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ≤ 𝑁)
22	17	zred 12722	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑉 ∈ ℝ)
23	13	nnred 12281	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑁 ∈ ℝ)
24	22, 23	letri3d 11403	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑉 = 𝑁 ↔ (𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉)))
25	24	biimprd 248	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 ≤ 𝑁 ∧ 𝑁 ≤ 𝑉) → 𝑉 = 𝑁))
26	21, 25	mpand 695	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝑉 → 𝑉 = 𝑁))
27	19, 26	sylbird 260	. . . . . . . 8 ⊢ (𝜑 → ((𝑁 − 1) < 𝑉 → 𝑉 = 𝑁))
28	27	necon3ad 2953	. . . . . . 7 ⊢ (𝜑 → (𝑉 ≠ 𝑁 → ¬ (𝑁 − 1) < 𝑉))
29		nnm1nn0 12567	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
30	13, 29	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁 − 1) ∈ ℕ₀)
31		nn0fz0 13665	. . . . . . . . . . . 12 ⊢ ((𝑁 − 1) ∈ ℕ₀ ↔ (𝑁 − 1) ∈ (0...(𝑁 − 1)))
32	30, 31	sylib 218	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
33	32	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
34		iffalse 4534	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑁 − 1) < 𝑉 → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = ((𝑁 − 1) + 1))
35	13	nncnd 12282	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℂ)
36		npcan1 11688	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) + 1) = 𝑁)
37	35, 36	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑁 − 1) + 1) = 𝑁)
38	34, 37	sylan9eqr 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) = 𝑁)
39	38	csbeq1d 3903	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
40		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → (1...𝑗) = (1...𝑁))
41	40	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...𝑁)))
42	41	xpeq1d 5714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...𝑁)) × {1}))
43		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = 𝑁 → (𝑗 + 1) = (𝑁 + 1))
44	43	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = 𝑁 → ((𝑗 + 1)...𝑁) = ((𝑁 + 1)...𝑁))
45	44	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝑁 → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ ((𝑁 + 1)...𝑁)))
46	45	xpeq1d 5714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑁 → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}))
47	42, 46	uneq12d 4169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑁 → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})))
48		poimirlem23.2	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))
49		f1ofo 6855	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈:(1...𝑁)–onto→(1...𝑁))
50		foima 6825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑈:(1...𝑁)–onto→(1...𝑁) → (𝑈 “ (1...𝑁)) = (1...𝑁))
51	48, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ (1...𝑁)) = (1...𝑁))
52	51	xpeq1d 5714	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) × {1}) = ((1...𝑁) × {1}))
53	23	ltp1d 12198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑁 < (𝑁 + 1))
54	14	peano2zd 12725	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
55		fzn 13580	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
56	54, 14, 55	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (𝑁 < (𝑁 + 1) ↔ ((𝑁 + 1)...𝑁) = ∅))
57	53, 56	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑁 + 1)...𝑁) = ∅)
58	57	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑈 “ ((𝑁 + 1)...𝑁)) = (𝑈 “ ∅))
59	58	xpeq1d 5714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ((𝑈 “ ∅) × {0}))
60		ima0 6095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑈 “ ∅) = ∅
61	60	xpeq1i 5711	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑈 “ ∅) × {0}) = (∅ × {0})
62		0xp 5784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ × {0}) = ∅
63	61, 62	eqtri 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑈 “ ∅) × {0}) = ∅
64	59, 63	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0}) = ∅)
65	52, 64	uneq12d 4169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = (((1...𝑁) × {1}) ∪ ∅))
66		un0 4394	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1...𝑁) × {1}) ∪ ∅) = ((1...𝑁) × {1})
67	65, 66	eqtrdi 2793	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (((𝑈 “ (1...𝑁)) × {1}) ∪ ((𝑈 “ ((𝑁 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
68	47, 67	sylan9eqr 2799	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = ((1...𝑁) × {1}))
69	68	oveq2d 7447	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 = 𝑁) → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
70	13, 69	csbied 3935	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋𝑁 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
72	39, 71	eqtrd 2777	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = (𝑇 ∘_f + ((1...𝑁) × {1})))
73	72	fveq1d 6908	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁))
74		elfzonn0 13747	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0..^𝐾) → 𝑗 ∈ ℕ₀)
75		nn0p1nn 12565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℕ₀ → (𝑗 + 1) ∈ ℕ)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑗 + 1) ∈ ℕ)
77		elsni 4643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ {1} → 𝑦 = 1)
78	77	oveq2d 7447	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ {1} → (𝑗 + 𝑦) = (𝑗 + 1))
79	78	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ {1} → ((𝑗 + 𝑦) ∈ ℕ ↔ (𝑗 + 1) ∈ ℕ))
80	76, 79	syl5ibrcom 247	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0..^𝐾) → (𝑦 ∈ {1} → (𝑗 + 𝑦) ∈ ℕ))
81	80	imp 406	. . . . . . . . . . . . . . . 16 ⊢ ((𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1}) → (𝑗 + 𝑦) ∈ ℕ)
82	81	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑗 ∈ (0..^𝐾) ∧ 𝑦 ∈ {1})) → (𝑗 + 𝑦) ∈ ℕ)
83		poimirlem23.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑇:(1...𝑁)⟶(0..^𝐾))
84		1ex 11257	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
85	84	fconst 6794	. . . . . . . . . . . . . . . 16 ⊢ ((1...𝑁) × {1}):(1...𝑁)⟶{1}
86	85	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((1...𝑁) × {1}):(1...𝑁)⟶{1})
87		ovexd 7466	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1...𝑁) ∈ V)
88		inidm 4227	. . . . . . . . . . . . . . 15 ⊢ ((1...𝑁) ∩ (1...𝑁)) = (1...𝑁)
89	82, 83, 86, 87, 87, 88	off 7715	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇 ∘_f + ((1...𝑁) × {1})):(1...𝑁)⟶ℕ)
90		elfz1end 13594	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (1...𝑁))
91	13, 90	sylib 218	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ (1...𝑁))
92	89, 91	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
93	92	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ((𝑇 ∘_f + ((1...𝑁) × {1}))‘𝑁) ∈ ℕ)
94	73, 93	eqeltrd 2841	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ∈ ℕ)
95	94	nnne0d 12316	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0)
96		breq1 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 < 𝑉 ↔ (𝑁 − 1) < 𝑉))
97		id 22	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → 𝑦 = (𝑁 − 1))
98		oveq1 7438	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑁 − 1) → (𝑦 + 1) = ((𝑁 − 1) + 1))
99	96, 97, 98	ifbieq12d 4554	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑁 − 1) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)))
100	99	csbeq1d 3903	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑁 − 1) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
101	100	fveq1d 6908	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑁 − 1) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
102	101	neeq1d 3000	. . . . . . . . . . . 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 285	. . . . . . . . . . 11 ⊢ (𝑦 = (𝑁 − 1) → (¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋if((𝑁 − 1) < 𝑉, (𝑁 − 1), ((𝑁 − 1) + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) ≠ 0))
104	103	rspcev 3622	. . . . . . . . . 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 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ∃𝑦 ∈ (0...(𝑁 − 1)) ¬ (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
106	105, 11	sylib 218	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝑁 − 1) < 𝑉) → ¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)
107	106	ex 412	. . . . . . 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 2959	. . . . 5 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 → 𝑉 = 𝑁))
110	109	pm4.71rd 562	. . . 4 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0)))
111	30	nn0zd 12639	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑁 − 1) ∈ ℤ)
112		uzid 12893	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ ℤ → (𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)))
113		peano2uz 12943	. . . . . . . . . . . . 13 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
114	111, 112, 113	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑁 − 1)))
115	37, 114	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(𝑁 − 1)))
116		fzss2 13604	. . . . . . . . . . 11 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑁 − 1)) → (0...(𝑁 − 1)) ⊆ (0...𝑁))
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (0...(𝑁 − 1)) ⊆ (0...𝑁))
118	117	sselda 3983	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ (0...𝑁))
119	91	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑁 ∈ (1...𝑁))
120	83	ffnd 6737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑇 Fn (1...𝑁))
121	120	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑇 Fn (1...𝑁))
122	84	fconst 6794	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1}
123		c0ex 11255	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
124	123	fconst 6794	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}
125	122, 124	pm3.2i 470	. . . . . . . . . . . . . . . 16 ⊢ (((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0})
126		dff1o3 6854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) ↔ (𝑈:(1...𝑁)–onto→(1...𝑁) ∧ Fun ^◡𝑈))
127	126	simprbi 496	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → Fun ^◡𝑈)
128		imain 6651	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
129	48, 127, 128	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))))
130		elfzelz 13564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
131	130	zred 12722	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℝ)
132	131	ltp1d 12198	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 < (𝑗 + 1))
133		fzdisj 13591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 < (𝑗 + 1) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
134	132, 133	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
135	134	imaeq2d 6078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
136	135, 60	eqtrdi 2793	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
137	129, 136	sylan9req 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
138		fun 6770	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}):(𝑈 “ (1...𝑗))⟶{1} ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}):(𝑈 “ ((𝑗 + 1)...𝑁))⟶{0}) ∧ ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
139	125, 137, 138	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}))
140		elfznn0 13660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℕ₀)
141	140, 75	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ ℕ)
142		nnuz 12921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℕ = (ℤ_≥‘1)
143	141, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (ℤ_≥‘1))
144		elfzuz3 13561	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...𝑁) → 𝑁 ∈ (ℤ_≥‘𝑗))
145		fzsplit2 13589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑗 + 1) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ (ℤ_≥‘𝑗)) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
146	143, 144, 145	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...𝑁) → (1...𝑁) = ((1...𝑗) ∪ ((𝑗 + 1)...𝑁)))
147	146	imaeq2d 6078	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...𝑁) → (𝑈 “ (1...𝑁)) = (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))))
148		imaundi 6169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑈 “ ((1...𝑗) ∪ ((𝑗 + 1)...𝑁))) = ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))
149	147, 148	eqtr2di 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...𝑁) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (𝑈 “ (1...𝑁)))
150	149, 51	sylan9eqr 2799	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁))) = (1...𝑁))
151	150	feq2d 6722	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):((𝑈 “ (1...𝑗)) ∪ (𝑈 “ ((𝑗 + 1)...𝑁)))⟶({1} ∪ {0}) ↔ (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0})))
152	139, 151	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})):(1...𝑁)⟶({1} ∪ {0}))
153	152	ffnd 6737	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) Fn (1...𝑁))
154		ovexd 7466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1...𝑁) ∈ V)
155		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → (𝑇‘𝑁) = (𝑇‘𝑁))
156		eqidd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
157	121, 153, 154, 154, 88, 155, 156	ofval 7708	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
158	119, 157	mpdan 687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)))
159	158	eqeq1d 2739	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0))
160	83, 91	ffvelcdmd 7105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑇‘𝑁) ∈ (0..^𝐾))
161		elfzonn0 13747	. . . . . . . . . . . . . 14 ⊢ ((𝑇‘𝑁) ∈ (0..^𝐾) → (𝑇‘𝑁) ∈ ℕ₀)
162	160, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℕ₀)
163	162	nn0red 12588	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑇‘𝑁) ∈ ℝ)
164	163	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑇‘𝑁) ∈ ℝ)
165	162	nn0ge0d 12590	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 ≤ (𝑇‘𝑁))
166	165	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 0 ≤ (𝑇‘𝑁))
167		1re 11261	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℝ
168		snssi 4808	. . . . . . . . . . . . . 14 ⊢ (1 ∈ ℝ → {1} ⊆ ℝ)
169	167, 168	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {1} ⊆ ℝ
170		0re 11263	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℝ
171		snssi 4808	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ)
172	170, 171	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {0} ⊆ ℝ
173	169, 172	unssi 4191	. . . . . . . . . . . 12 ⊢ ({1} ∪ {0}) ⊆ ℝ
174	152, 119	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}))
175	173, 174	sselid 3981	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ℝ)
176		elun 4153	. . . . . . . . . . . . 13 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ ({1} ∪ {0}) ↔ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}))
177		0le1 11786	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 1
178		elsni 4643	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 1)
179	177, 178	breqtrrid 5181	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
180		0le0 12367	. . . . . . . . . . . . . . 15 ⊢ 0 ≤ 0
181		elsni 4643	. . . . . . . . . . . . . . 15 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
182	180, 181	breqtrrid 5181	. . . . . . . . . . . . . 14 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0} → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
183	179, 182	jaoi 858	. . . . . . . . . . . . 13 ⊢ ((((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {1} ∨ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ∈ {0}) → 0 ≤ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁))
184	176, 183	sylbi 217	. . . . . . . . . . . 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 11775	. . . . . . . . . . 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 839	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇‘𝑁) + ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁)) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
188	159, 187	bitrd 279	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
189	118, 188	syldan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
190	189	ralbidva 3176	. . . . . . 7 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
191	190	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
192		breq2 5147	. . . . . . . . . . . . . 14 ⊢ (𝑉 = 𝑁 → (𝑦 < 𝑉 ↔ 𝑦 < 𝑁))
193	192	ifbid 4549	. . . . . . . . . . . . 13 ⊢ (𝑉 = 𝑁 → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)))
194		elfzelz 13564	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℤ)
195	194	zred 12722	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ∈ ℝ)
196	195	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ∈ ℝ)
197	30	nn0red 12588	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) ∈ ℝ)
198	197	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) ∈ ℝ)
199	23	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ℝ)
200		elfzle2 13568	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (0...(𝑁 − 1)) → 𝑦 ≤ (𝑁 − 1))
201	200	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 ≤ (𝑁 − 1))
202	23	ltm1d 12200	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 − 1) < 𝑁)
203	202	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (𝑁 − 1) < 𝑁)
204	196, 198, 199, 201, 203	lelttrd 11419	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → 𝑦 < 𝑁)
205	204	iftrued 4533	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑁, 𝑦, (𝑦 + 1)) = 𝑦)
206	193, 205	sylan9eqr 2799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ (0...(𝑁 − 1))) ∧ 𝑉 = 𝑁) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
207	206	an32s 652	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) = 𝑦)
208	207	csbeq1d 3903	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
209	208	fveq1d 6908	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → (⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
210	209	eqeq1d 2739	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑉 = 𝑁) ∧ 𝑦 ∈ (0...(𝑁 − 1))) → ((⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
211	210	ralbidva 3176	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
212		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑦((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
213		nfcsb1v 3923	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))
214		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑁
215	213, 214	nffv 6916	. . . . . . . . 9 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁)
216	215	nfeq1 2921	. . . . . . . 8 ⊢ Ⅎ𝑗(⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0
217		csbeq1a 3913	. . . . . . . . . 10 ⊢ (𝑗 = 𝑦 → (𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))) = ⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))))
218	217	fveq1d 6908	. . . . . . . . 9 ⊢ (𝑗 = 𝑦 → ((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = (⦋𝑦 / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁))
219	218	eqeq1d 2739	. . . . . . . 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 289	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0))
222		ne0i 4341	. . . . . . . . . 10 ⊢ ((𝑁 − 1) ∈ (0...(𝑁 − 1)) → (0...(𝑁 − 1)) ≠ ∅)
223		r19.3rzv 4499	. . . . . . . . . 10 ⊢ ((0...(𝑁 − 1)) ≠ ∅ → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
224	32, 222, 223	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((𝑇‘𝑁) = 0 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0))
225		elfzelz 13564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ)
226	225	zred 12722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℝ)
227	226	ltp1d 12198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 < (𝑗 + 1))
228	227, 133	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((1...𝑗) ∩ ((𝑗 + 1)...𝑁)) = ∅)
229	228	imaeq2d 6078	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = (𝑈 “ ∅))
230	229, 60	eqtrdi 2793	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑈 “ ((1...𝑗) ∩ ((𝑗 + 1)...𝑁))) = ∅)
231	129, 230	sylan9req 2798	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
232	231	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅)
233		simplr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) = 𝑁)
234		f1ofn 6849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑈:(1...𝑁)–1-1-onto→(1...𝑁) → 𝑈 Fn (1...𝑁))
235	48, 234	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑈 Fn (1...𝑁))
236	235	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑈 Fn (1...𝑁))
237		elfznn0 13660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ₀)
238	237, 75	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℕ)
239	238, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ (ℤ_≥‘1))
240		fzss1 13603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 + 1) ∈ (ℤ_≥‘1) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
242	241	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑗 + 1)...𝑁) ⊆ (1...𝑁))
243	37	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) = 𝑁)
244		elfzuz3 13561	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑁 − 1) ∈ (ℤ_≥‘𝑗))
245		eluzp1p1 12906	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑁 − 1) ∈ (ℤ_≥‘𝑗) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
246	244, 245	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
247	246	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((𝑁 − 1) + 1) ∈ (ℤ_≥‘(𝑗 + 1)))
248	243, 247	eqeltrrd 2842	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (ℤ_≥‘(𝑗 + 1)))
249		eluzfz2 13572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (ℤ_≥‘(𝑗 + 1)) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
250	248, 249	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ ((𝑗 + 1)...𝑁))
251		fnfvima 7253	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 Fn (1...𝑁) ∧ ((𝑗 + 1)...𝑁) ⊆ (1...𝑁) ∧ 𝑁 ∈ ((𝑗 + 1)...𝑁)) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
252	236, 242, 250, 251	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
253	252	adantlr 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑈‘𝑁) ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
254	233, 253	eqeltrrd 2842	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))
255		fnconstg 6796	. . . . . . . . . . . . . . . 16 ⊢ (1 ∈ V → ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)))
256	84, 255	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗))
257		fnconstg 6796	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)))
258	123, 257	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁))
259		fvun2 7001	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 “ (1...𝑗)) × {1}) Fn (𝑈 “ (1...𝑗)) ∧ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) Fn (𝑈 “ ((𝑗 + 1)...𝑁)) ∧ (((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
260	256, 258, 259	mp3an12 1453	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 “ (1...𝑗)) ∩ (𝑈 “ ((𝑗 + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
261	232, 254, 260	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁))
262	123	fvconst2 7224	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ (𝑈 “ ((𝑗 + 1)...𝑁)) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
263	254, 262	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})‘𝑁) = 0)
264	261, 263	eqtrd 2777	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑈‘𝑁) = 𝑁) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
265	264	ralrimiva 3146	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑈‘𝑁) = 𝑁) → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
266	265	ex 412	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 → ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
267	32	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (𝑁 − 1) ∈ (0...(𝑁 − 1)))
268		ax-1ne0 11224	. . . . . . . . . . . . . . 15 ⊢ 1 ≠ 0
269		imain 6651	. . . . . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (𝑁 − 1) < ((𝑁 − 1) + 1))
272		fzdisj 13591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑁 − 1) < ((𝑁 − 1) + 1) → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
273	271, 272	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁)) = ∅)
274	273	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = (𝑈 “ ∅))
275	274, 60	eqtrdi 2793	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑈 “ ((1...(𝑁 − 1)) ∩ (((𝑁 − 1) + 1)...𝑁))) = ∅)
276	270, 275	eqtr3d 2779	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
277	276	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅)
278	91	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (1...𝑁))
279		elimasni 6109	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁 ∈ (𝑈 “ {𝑁}) → 𝑁𝑈𝑁)
280		fnbrfvb 6959	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑈 Fn (1...𝑁) ∧ 𝑁 ∈ (1...𝑁)) → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
281	235, 91, 280	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ 𝑁𝑈𝑁))
282	279, 281	imbitrrid 246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑁 ∈ (𝑈 “ {𝑁}) → (𝑈‘𝑁) = 𝑁))
283	282	necon3ad 2953	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ 𝑁 ∈ (𝑈 “ {𝑁})))
284	283	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ¬ 𝑁 ∈ (𝑈 “ {𝑁}))
285	278, 284	eldifd 3962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ ((1...𝑁) ∖ (𝑈 “ {𝑁})))
286		imadif 6650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun ^◡𝑈 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
287	48, 127, 286	3syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})))
288		difun2 4481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...(𝑁 − 1)) ∖ {𝑁})
289		elun 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}))
290		velsn 4642	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ {𝑁} ↔ 𝑗 = 𝑁)
291	290	orbi2i 913	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 ∈ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
292	289, 291	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁))
293	13, 142	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘1))
294		fzm1 13647	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑁 ∈ (ℤ_≥‘1) → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝑗 ∈ (1...𝑁) ↔ (𝑗 ∈ (1...(𝑁 − 1)) ∨ 𝑗 = 𝑁)))
296	292, 295	bitr4id 290	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝑗 ∈ ((1...(𝑁 − 1)) ∪ {𝑁}) ↔ 𝑗 ∈ (1...𝑁)))
297	296	eqrdv 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∪ {𝑁}) = (1...𝑁))
298	297	difeq1d 4125	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (((1...(𝑁 − 1)) ∪ {𝑁}) ∖ {𝑁}) = ((1...𝑁) ∖ {𝑁}))
299	197, 23	ltnled 11408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ((𝑁 − 1) < 𝑁 ↔ ¬ 𝑁 ≤ (𝑁 − 1)))
300	202, 299	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → ¬ 𝑁 ≤ (𝑁 − 1))
301		elfzle2 13568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (1...(𝑁 − 1)) → 𝑁 ≤ (𝑁 − 1))
302	300, 301	nsyl 140	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ¬ 𝑁 ∈ (1...(𝑁 − 1)))
303		difsn 4798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑁 ∈ (1...(𝑁 − 1)) → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ((1...(𝑁 − 1)) ∖ {𝑁}) = (1...(𝑁 − 1)))
305	288, 298, 304	3eqtr3a 2801	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((1...𝑁) ∖ {𝑁}) = (1...(𝑁 − 1)))
306	305	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑈 “ ((1...𝑁) ∖ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
307	51	difeq1d 4125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑈 “ (1...𝑁)) ∖ (𝑈 “ {𝑁})) = ((1...𝑁) ∖ (𝑈 “ {𝑁})))
308	287, 306, 307	3eqtr3rd 2786	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
309	308	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((1...𝑁) ∖ (𝑈 “ {𝑁})) = (𝑈 “ (1...(𝑁 − 1))))
310	285, 309	eleqtrd 2843	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))))
311		fnconstg 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 ∈ V → ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1))))
312	84, 311	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (1...(𝑁 − 1))) × {1}) Fn (𝑈 “ (1...(𝑁 − 1)))
313		fnconstg 6796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0 ∈ V → ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
314	123, 313	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}) Fn (𝑈 “ (((𝑁 − 1) + 1)...𝑁))
315		fvun1 7000	. . . . . . . . . . . . . . . . . . 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 1453	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑈 “ (1...(𝑁 − 1))) ∩ (𝑈 “ (((𝑁 − 1) + 1)...𝑁))) = ∅ ∧ 𝑁 ∈ (𝑈 “ (1...(𝑁 − 1)))) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
317	277, 310, 316	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁))
318	84	fvconst2 7224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 ∈ (𝑈 “ (1...(𝑁 − 1))) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
319	310, 318	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((𝑈 “ (1...(𝑁 − 1))) × {1})‘𝑁) = 1)
320	317, 319	eqtrd 2777	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) = 1)
321	320	neeq1d 3000	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → (((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ 1 ≠ 0))
322	268, 321	mpbiri 258	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0)
323		df-ne 2941	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
324		oveq2 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → (1...𝑗) = (1...(𝑁 − 1)))
325	324	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ (1...𝑗)) = (𝑈 “ (1...(𝑁 − 1))))
326	325	xpeq1d 5714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ (1...𝑗)) × {1}) = ((𝑈 “ (1...(𝑁 − 1))) × {1}))
327		oveq1 7438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝑁 − 1) → (𝑗 + 1) = ((𝑁 − 1) + 1))
328	327	oveq1d 7446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 = (𝑁 − 1) → ((𝑗 + 1)...𝑁) = (((𝑁 − 1) + 1)...𝑁))
329	328	imaeq2d 6078	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = (𝑁 − 1) → (𝑈 “ ((𝑗 + 1)...𝑁)) = (𝑈 “ (((𝑁 − 1) + 1)...𝑁)))
330	329	xpeq1d 5714	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑁 − 1) → ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}) = ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))
331	326, 330	uneq12d 4169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑁 − 1) → (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})) = (((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0})))
332	331	fveq1d 6908	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑁 − 1) → ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁))
333	332	neeq1d 3000	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑁 − 1) → (((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) ≠ 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
334	323, 333	bitr3id 285	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑁 − 1) → (¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0))
335	334	rspcev 3622	. . . . . . . . . . . . . 14 ⊢ (((𝑁 − 1) ∈ (0...(𝑁 − 1)) ∧ ((((𝑈 “ (1...(𝑁 − 1))) × {1}) ∪ ((𝑈 “ (((𝑁 − 1) + 1)...𝑁)) × {0}))‘𝑁) ≠ 0) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
336	267, 322, 335	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑈‘𝑁) ≠ 𝑁) → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
337	336	ex 412	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
338		rexnal 3100	. . . . . . . . . . . 12 ⊢ (∃𝑗 ∈ (0...(𝑁 − 1)) ¬ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 ↔ ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)
339	337, 338	imbitrdi 251	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈‘𝑁) ≠ 𝑁 → ¬ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
340	339	necon4ad 2959	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0 → (𝑈‘𝑁) = 𝑁))
341	266, 340	impbid 212	. . . . . . . . 9 ⊢ (𝜑 → ((𝑈‘𝑁) = 𝑁 ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
342	224, 341	anbi12d 632	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
343		r19.26 3111	. . . . . . . 8 ⊢ (∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0) ↔ (∀𝑗 ∈ (0...(𝑁 − 1))(𝑇‘𝑁) = 0 ∧ ∀𝑗 ∈ (0...(𝑁 − 1))((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0))
344	342, 343	bitr4di 289	. . . . . . 7 ⊢ (𝜑 → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
345	344	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁) ↔ ∀𝑗 ∈ (0...(𝑁 − 1))((𝑇‘𝑁) = 0 ∧ ((((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0}))‘𝑁) = 0)))
346	191, 221, 345	3bitr4d 311	. . . . 5 ⊢ ((𝜑 ∧ 𝑉 = 𝑁) → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁)))
347	346	pm5.32da 579	. . . 4 ⊢ (𝜑 → ((𝑉 = 𝑁 ∧ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0) ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
348	110, 347	bitrd 279	. . 3 ⊢ (𝜑 → (∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
349	348	notbid 318	. 2 ⊢ (𝜑 → (¬ ∀𝑦 ∈ (0...(𝑁 − 1))(⦋if(𝑦 < 𝑉, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘_f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))‘𝑁) = 0 ↔ ¬ (𝑉 = 𝑁 ∧ ((𝑇‘𝑁) = 0 ∧ (𝑈‘𝑁) = 𝑁))))
350	12, 349	bitrid 283	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 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3480 ⦋csb 3899 ∖ cdif 3948 ∪ cun 3949 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 ifcif 4525 {csn 4626 class class class wbr 5143 ↦ cmpt 5225 × cxp 5683 ^◡ccnv 5684 ran crn 5686 “ cima 5688 Fun wfun 6555 Fn wfn 6556 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 (class class class)co 7431 ∘_f cof 7695 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 < clt 11295 ≤ cle 11296 − cmin 11492 ℕcn 12266 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 ...cfz 13547 ..^cfzo 13694

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

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

This theorem is referenced by: poimirlem24 37651

W3C validator