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 48215

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 6885	. . 3 ⊢ (𝑥 = 1 → (RePart‘𝑥) = (RePart‘1))
2		fveq2 6885	. . . . . 6 ⊢ (𝑥 = 1 → (𝑝‘𝑥) = (𝑝‘1))
3	2	oveq2d 7432	. . . . 5 ⊢ (𝑥 = 1 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘1)))
4	3	eleq2d 2851	. . . 4 ⊢ (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
5		oveq2 7424	. . . . . 6 ⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1))
6		fzo01 13789	. . . . . 6 ⊢ (0..^1) = {0}
7	5, 6	eqtrdi 2816	. . . . 5 ⊢ (𝑥 = 1 → (0..^𝑥) = {0})
8	7	rexeqdv 3326	. . . 4 ⊢ (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
9	4, 8	imbi12d 347	. . 3 ⊢ (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
10	1, 9	raleqbidv 3340	. 2 ⊢ (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
11		fveq2 6885	. . 3 ⊢ (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦))
12		fveq2 6885	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑝‘𝑥) = (𝑝‘𝑦))
13	12	oveq2d 7432	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑦)))
14	13	eleq2d 2851	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
15		oveq2 7424	. . . . 5 ⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦))
16	15	rexeqdv 3326	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
17	14, 16	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
18	11, 17	raleqbidv 3340	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
19		fveq2 6885	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1)))
20		fveq2 6885	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑝‘𝑥) = (𝑝‘(𝑦 + 1)))
21	20	oveq2d 7432	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))
22	21	eleq2d 2851	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))))
23		oveq2 7424	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1)))
24	23	rexeqdv 3326	. . . 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 3340	. 2 ⊢ (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
27		fveq2 6885	. . 3 ⊢ (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀))
28		fveq2 6885	. . . . . 6 ⊢ (𝑥 = 𝑀 → (𝑝‘𝑥) = (𝑝‘𝑀))
29	28	oveq2d 7432	. . . . 5 ⊢ (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑀)))
30	29	eleq2d 2851	. . . 4 ⊢ (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀))))
31		oveq2 7424	. . . . 5 ⊢ (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀))
32	31	rexeqdv 3326	. . . 4 ⊢ (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
33	30, 32	imbi12d 347	. . 3 ⊢ (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
34	27, 33	raleqbidv 3340	. 2 ⊢ (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
35		0nn0 12530	. . . . 5 ⊢ 0 ∈ ℕ₀
36		fveq2 6885	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘𝑖) = (𝑝‘0))
37		fv0p1e1 12373	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1))
38	36, 37	oveq12d 7434	. . . . . . 7 ⊢ (𝑖 = 0 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1)))
39	38	eleq2d 2851	. . . . . 6 ⊢ (𝑖 = 0 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
40	39	rexsng 4644	. . . . 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 3085	. 2 ⊢ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
44		nfv 1947	. . . . 5 ⊢ Ⅎ𝑝 𝑦 ∈ ℕ
45		nfra1 3291	. . . . 5 ⊢ Ⅎ𝑝∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
46	44, 45	nfan 1932	. . . 4 ⊢ Ⅎ𝑝(𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
47		nnnn0 12522	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
48		fzonn0p1 13784	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ (0..^(𝑦 + 1)))
49	47, 48	syl 18	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1)))
50	49	ad2antrr 739	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1)))
51		fveq2 6885	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘𝑖) = (𝑝‘𝑦))
52		fvoveq1 7439	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1)))
53	51, 52	oveq12d 7434	. . . . . . . . . 10 ⊢ (𝑖 = 𝑦 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))
54	53	eleq2d 2851	. . . . . . . . 9 ⊢ (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
55	54	adantl 487	. . . . . . . 8 ⊢ ((((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
56		peano2nn 12256	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
57	56	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ ℕ)
58		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1)))
59	56	nnnn0d 12576	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ₀)
60		0elfz 13665	. . . . . . . . . . . . . . . . 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 48201	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈ ℝ^*)
64		nn0fz0 13666	. . . . . . . . . . . . . . . . 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 48201	. . . . . . . . . . . . . 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 13427	. . . . . . . . . . . 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 13666	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ (0...𝑦))
83	47, 82	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦))
84		fzelp1 13617	. . . . . . . . . . . . . . 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 48201	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) ∈ ℝ^*)
88	87, 67	jca 521	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
89	88	ad2ant2r 760	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
90		elico1 13427	. . . . . . . . . 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 3585	. . . . . . 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 48200	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦))
97		rspsbca 3834	. . . . . . . . . . . 12 ⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
98		vex 3461	. . . . . . . . . . . . . . 15 ⊢ 𝑝 ∈ V
99	98	resex 6030	. . . . . . . . . . . . . 14 ⊢ (𝑝 ↾ (0...𝑦)) ∈ V
100		sbcimg 3794	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
101		sbcel2 4383	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)))
102		csbov12g 7462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)))
103		csbfv12 6930	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0)
104		csbvarg 4399	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝 = (𝑝 ↾ (0...𝑦)))
105		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0 = 0)
106	104, 105	fveq12d 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) = ((𝑝 ↾ (0...𝑦))‘0))
107	103, 106	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
108		csbfv12 6930	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦)
109		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦 = 𝑦)
110	104, 109	fveq12d 6892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
111	108, 110	eqtrid 2812	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
112	107, 111	oveq12d 7434	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
113	102, 112	eqtrd 2800	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
114	113	eleq2d 2851	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
115	101, 114	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
116		sbcrex 3829	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
117		sbcel2 4383	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
118		csbov12g 7462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))))
119		csbfv12 6930	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖)
120		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖 = 𝑖)
121	104, 120	fveq12d 6892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
122	119, 121	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
123		csbfv12 6930	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1))
124		csbconstg 3873	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1) = (𝑖 + 1))
125	104, 124	fveq12d 6892	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
126	123, 125	eqtrid 2812	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
127	122, 126	oveq12d 7434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
128	118, 127	eqtrd 2800	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
129	128	eleq2d 2851	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
130	117, 129	bitrid 286	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
131	130	rexbidv 3191	. . . . . . . . . . . . . . . . 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 11287	. . . . . . . . . . . . . . . . . . . . . . . . 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 13427	. . . . . . . . . . . . . . . . . . . . 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 13665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ₀ → 0 ∈ (0...𝑦))
154	47, 153	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → 0 ∈ (0...𝑦))
155	154	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...𝑦))
156		fvres 6904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
157	155, 156	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
158	157	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
159	83	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦))
160		fvres 6904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
161	159, 160	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
162	161	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
163	158, 162	oveq12d 7434	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
164	163	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
165	164	biimpa 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
166		elfzofz 13717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦))
167	166	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦))
168		fvres 6904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
169	167, 168	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
170		fzofzp1 13806	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦))
171	170	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦))
172		fvres 6904	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7434	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
176	175	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
177	176	rexbidva 3189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
178		nnz 12623	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
179		uzid 12889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ (ℤ_≥‘𝑦))
180		peano2uz 12937	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (ℤ_≥‘𝑦) → (𝑦 + 1) ∈ (ℤ_≥‘𝑦))
181		fzoss2 13729	. . . . . . . . . . . . . . . . . . . . . . . 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 4008	. . . . . . . . . . . . . . . . . . . . . 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 3265	. . 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 12262	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 1570 ∈ wcel 2146 ∀wral 3081 ∃wrex 3091 Vcvv 3457 [wsbc 3746 ⦋csb 3854 ⊆ wss 3906 {csn 4591 class class class wbr 5111 ↾ cres 5665 ‘cfv 6540 (class class class)co 7416 0cc0 11111 1c1 11112 + caddc 11114 ℝ^*cxr 11253 < clt 11254 ≤ cle 11255 ℕcn 12244 ℕ₀cn0 12515 ℤcz 12602 ℤ_≥cuz 12874 [,)cico 13386 ...cfz 13547 ..^cfzo 13695 RePartciccp 48195

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-er 8696 df-map 8828 df-en 8946 df-dom 8947 df-sdom 8948 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-nn 12245 df-n0 12516 df-z 12603 df-uz 12875 df-ico 13390 df-fz 13548 df-fzo 13696 df-iccp 48196

This theorem is used by: iccpartiun 48216 icceuelpart 48218 bgoldbtbnd 48607

W3C validator