iccelpart - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > iccelpart		Structured version Visualization version GIF version

Theorem iccelpart 48609

Description: An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.)

**Assertion**
Ref	Expression
iccelpart	⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))

Distinct variable groups: 𝑖,𝑀,𝑝 𝑖,𝑋,𝑝

Proof of Theorem iccelpart Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6886	. . 3 ⊢ (𝑥 = 1 → (RePart‘𝑥) = (RePart‘1))
2		fveq2 6886	. . . . . 6 ⊢ (𝑥 = 1 → (𝑝‘𝑥) = (𝑝‘1))
3	2	oveq2d 7437	. . . . 5 ⊢ (𝑥 = 1 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘1)))
4	3	eleq2d 2846	. . . 4 ⊢ (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
5		oveq2 7429	. . . . . 6 ⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1))
6		fzo01 13886	. . . . . 6 ⊢ (0..^1) = {0}
7	5, 6	eqtrdi 2811	. . . . 5 ⊢ (𝑥 = 1 → (0..^𝑥) = {0})
8	7	rexeqdv 3320	. . . 4 ⊢ (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
9	4, 8	imbi12d 347	. . 3 ⊢ (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
10	1, 9	raleqbidv 3334	. 2 ⊢ (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
11		fveq2 6886	. . 3 ⊢ (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦))
12		fveq2 6886	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑝‘𝑥) = (𝑝‘𝑦))
13	12	oveq2d 7437	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑦)))
14	13	eleq2d 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
15		oveq2 7429	. . . . 5 ⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦))
16	15	rexeqdv 3320	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
17	14, 16	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
18	11, 17	raleqbidv 3334	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
19		fveq2 6886	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1)))
20		fveq2 6886	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑝‘𝑥) = (𝑝‘(𝑦 + 1)))
21	20	oveq2d 7437	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))
22	21	eleq2d 2846	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))))
23		oveq2 7429	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1)))
24	23	rexeqdv 3320	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
25	22, 24	imbi12d 347	. . 3 ⊢ (𝑥 = (𝑦 + 1) → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
26	19, 25	raleqbidv 3334	. 2 ⊢ (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
27		fveq2 6886	. . 3 ⊢ (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀))
28		fveq2 6886	. . . . . 6 ⊢ (𝑥 = 𝑀 → (𝑝‘𝑥) = (𝑝‘𝑀))
29	28	oveq2d 7437	. . . . 5 ⊢ (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑀)))
30	29	eleq2d 2846	. . . 4 ⊢ (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀))))
31		oveq2 7429	. . . . 5 ⊢ (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀))
32	31	rexeqdv 3320	. . . 4 ⊢ (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
33	30, 32	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
34	27, 33	raleqbidv 3334	. 2 ⊢ (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
35		0nn0 12625	. . . . 5 ⊢ 0 ∈ ℕ₀
36		fveq2 6886	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘𝑖) = (𝑝‘0))
37		fv0p1e1 12468	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1))
38	36, 37	oveq12d 7439	. . . . . . 7 ⊢ (𝑖 = 0 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1)))
39	38	eleq2d 2846	. . . . . 6 ⊢ (𝑖 = 0 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
40	39	rexsng 4633	. . . . 5 ⊢ (0 ∈ ℕ₀ → (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
41	35, 40	ax-mp 5	. . . 4 ⊢ (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))
42	41	biimpri 231	. . 3 ⊢ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
43	42	rgenw 3080	. 2 ⊢ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
44		nfv 1946	. . . . 5 ⊢ Ⅎ𝑝 𝑦 ∈ ℕ
45		nfra1 3286	. . . . 5 ⊢ Ⅎ𝑝∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
46	44, 45	nfan 1931	. . . 4 ⊢ Ⅎ𝑝(𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
47		nnnn0 12617	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
48		fzonn0p1 13881	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ (0..^(𝑦 + 1)))
49	47, 48	syl 18	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1)))
50	49	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1)))
51		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘𝑖) = (𝑝‘𝑦))
52		fvoveq1 7444	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1)))
53	51, 52	oveq12d 7439	. . . . . . . . . 10 ⊢ (𝑖 = 𝑦 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))
54	53	eleq2d 2846	. . . . . . . . 9 ⊢ (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
55	54	adantl 487	. . . . . . . 8 ⊢ ((((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
56		peano2nn 12351	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
57	56	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ ℕ)
58		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1)))
59	56	nnnn0d 12671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ₀)
60		0elfz 13762	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 + 1) ∈ ℕ₀ → 0 ∈ (0...(𝑦 + 1)))
61	59, 60	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 0 ∈ (0...(𝑦 + 1)))
62	61	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...(𝑦 + 1)))
63	57, 58, 62	iccpartxr 48595	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈ ℝ^*)
64		nn0fz0 13763	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 + 1) ∈ ℕ₀ ↔ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
65	59, 64	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
66	65	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
67	57, 58, 66	iccpartxr 48595	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘(𝑦 + 1)) ∈ ℝ^*)
68	63, 67	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
69	68	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
70		elico1 13523	. . . . . . . . . . . 12 ⊢ (((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
71	69, 70	syl 18	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
72		simp1 1154	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ℝ^*)
73	72	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ^*)
74		simpl 488	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘𝑦) ≤ 𝑋)
75		simpr3 1215	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘(𝑦 + 1)))
76	73, 74, 75	3jca 1146	. . . . . . . . . . . . . 14 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))
77	76	ex 418	. . . . . . . . . . . . 13 ⊢ ((𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
78	77	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
79	78	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
80	71, 79	sylbid 243	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
81	80	impr 460	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))
82		nn0fz0 13763	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ (0...𝑦))
83	47, 82	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦))
84		fzelp1 13714	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑦) → 𝑦 ∈ (0...(𝑦 + 1)))
85	83, 84	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...(𝑦 + 1)))
86	85	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...(𝑦 + 1)))
87	57, 58, 86	iccpartxr 48595	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) ∈ ℝ^*)
88	87, 67	jca 521	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
89	88	ad2ant2r 760	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
90		elico1 13523	. . . . . . . . . 10 ⊢ (((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
91	89, 90	syl 18	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
92	81, 91	mpbird 260	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))
93	50, 55, 92	rspcedvd 3578	. . . . . . 7 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
94	93	exp43 442	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
95	94	adantr 486	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
96		iccpartres 48594	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦))
97		rspsbca 3826	. . . . . . . . . . . 12 ⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
98		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑝 ∈ V
99	98	resex 6017	. . . . . . . . . . . . . 14 ⊢ (𝑝 ↾ (0...𝑦)) ∈ V
100		sbcimg 3786	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
101		sbcel2 4375	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)))
102		csbov12g 7467	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)))
103		csbfv12 6931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0)
104		csbvarg 4391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝 = (𝑝 ↾ (0...𝑦)))
105		csbconstg 3865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0 = 0)
106	104, 105	fveq12d 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) = ((𝑝 ↾ (0...𝑦))‘0))
107	103, 106	eqtrid 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
108		csbfv12 6931	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦)
109		csbconstg 3865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦 = 𝑦)
110	104, 109	fveq12d 6893	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
111	108, 110	eqtrid 2807	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
112	107, 111	oveq12d 7439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
113	102, 112	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
114	113	eleq2d 2846	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
115	101, 114	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
116		sbcrex 3821	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
117		sbcel2 4375	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
118		csbov12g 7467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))))
119		csbfv12 6931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖)
120		csbconstg 3865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖 = 𝑖)
121	104, 120	fveq12d 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
122	119, 121	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
123		csbfv12 6931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1))
124		csbconstg 3865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1) = (𝑖 + 1))
125	104, 124	fveq12d 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
126	123, 125	eqtrid 2807	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
127	122, 126	oveq12d 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
128	118, 127	eqtrd 2795	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
129	128	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
130	117, 129	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
131	130	rexbidv 3186	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
132	116, 131	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
133	115, 132	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))))
134	100, 133	bitrd 282	. . . . . . . . . . . . . 14 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))))
135	99, 134	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
136	68, 70	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
137	136	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
138	72	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ^*)
139		simpr2 1214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘0) ≤ 𝑋)
140		xrltnle 11380	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋))
141	72, 87, 140	syl2anr 609	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋))
142	141	exbiri 823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → 𝑋 < (𝑝‘𝑦))))
143	142	com23 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 < (𝑝‘𝑦))))
144	143	imp31 423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘𝑦))
145	138, 139, 144	3jca 1146	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))
146	63, 87	jca 521	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*))
147	146	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*))
148		elico1 13523	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))))
149	147, 148	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))))
150	145, 149	mpbird 260	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))
151	150	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
152	137, 151	sylbid 243	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
153		0elfz 13762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ₀ → 0 ∈ (0...𝑦))
154	47, 153	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → 0 ∈ (0...𝑦))
155	154	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...𝑦))
156		fvres 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
157	155, 156	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
158	157	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
159	83	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦))
160		fvres 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
161	159, 160	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
162	161	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
163	158, 162	oveq12d 7439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
164	163	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
165	164	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
166		elfzofz 13814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦))
167	166	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦))
168		fvres 6905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
169	167, 168	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
170		fzofzp1 13903	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦))
171	170	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦))
172		fvres 6905	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 + 1) ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
173	171, 172	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
174	173	adantlr 728	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
175	169, 174	oveq12d 7439	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
176	175	eleq2d 2846	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
177	176	rexbidva 3184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
178		nnz 12718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
179		uzid 12984	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ (ℤ_≥‘𝑦))
180		peano2uz 13032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (ℤ_≥‘𝑦) → (𝑦 + 1) ∈ (ℤ_≥‘𝑦))
181		fzoss2 13826	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘𝑦) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
182	178, 179, 180, 181	4syl 20	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
183	182	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
184		ssrexv 3978	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^𝑦) ⊆ (0..^(𝑦 + 1)) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
185	183, 184	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
186	177, 185	sylbid 243	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
187	165, 186	embantd 60	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
188	187	ex 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
189	188	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
190	152, 189	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
191	190	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
192	191	com34 92	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
193	192	com13 89	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
194	135, 193	sylbi 220	. . . . . . . . . . . 12 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
195	97, 194	syl 18	. . . . . . . . . . 11 ⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
196	195	ex 418	. . . . . . . . . 10 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
197	196	com24 96	. . . . . . . . 9 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
198	96, 197	mpcom 39	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
199	198	ex 418	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
200	199	com24 96	. . . . . 6 ⊢ (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
201	200	imp 412	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
202	95, 201	pm2.61d 181	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
203	46, 202	ralrimi 3260	. . 3 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
204	203	ex 418	. 2 ⊢ (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
205	10, 18, 26, 34, 43, 204	nnind 12357	1 ⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ∃wrex 3086 Vcvv 3450 [wsbc 3738 ⦋csb 3846 ⊆ wss 3895 {csn 4584 class class class wbr 5102 ↾ cres 5652 ‘cfv 6539 (class class class)co 7421 0cc0 11204 1c1 11205 + caddc 11207 ℝ^*cxr 11346 < clt 11347 ≤ cle 11348 ℕcn 12339 ℕ₀cn0 12610 ℤcz 12697 ℤ_≥cuz 12969 [,)cico 13482 ...cfz 13643 ..^cfzo 13792 RePartciccp 48589

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752 ax-cnex 11260 ax-resscn 11261 ax-1cn 11262 ax-icn 11263 ax-addcl 11264 ax-addrcl 11265 ax-mulcl 11266 ax-mulrcl 11267 ax-mulcom 11268 ax-addass 11269 ax-mulass 11270 ax-distr 11271 ax-i2m1 11272 ax-1ne0 11273 ax-1rid 11274 ax-rnegex 11275 ax-rrecex 11276 ax-cnre 11277 ax-pre-lttri 11278 ax-pre-lttrn 11279 ax-pre-ltadd 11280 ax-pre-mulgt0 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-om 7879 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-rdg 8422 df-er 8721 df-map 8853 df-en 8978 df-dom 8979 df-sdom 8980 df-pnf 11349 df-mnf 11350 df-xr 11351 df-ltxr 11352 df-le 11353 df-sub 11547 df-neg 11548 df-nn 12340 df-n0 12611 df-z 12698 df-uz 12970 df-ico 13486 df-fz 13644 df-fzo 13793 df-iccp 48590

This theorem is used by: iccpartiun 48610 icceuelpart 48612 bgoldbtbnd 49001

W3C validator