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 45810

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 6873	. . 3 ⊢ (𝑥 = 1 → (RePart‘𝑥) = (RePart‘1))
2		fveq2 6873	. . . . . 6 ⊢ (𝑥 = 1 → (𝑝‘𝑥) = (𝑝‘1))
3	2	oveq2d 7404	. . . . 5 ⊢ (𝑥 = 1 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘1)))
4	3	eleq2d 2818	. . . 4 ⊢ (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
5		oveq2 7396	. . . . . 6 ⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1))
6		fzo01 13691	. . . . . 6 ⊢ (0..^1) = {0}
7	5, 6	eqtrdi 2787	. . . . 5 ⊢ (𝑥 = 1 → (0..^𝑥) = {0})
8	7	rexeqdv 3325	. . . 4 ⊢ (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
9	4, 8	imbi12d 344	. . 3 ⊢ (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
10	1, 9	raleqbidv 3341	. 2 ⊢ (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
11		fveq2 6873	. . 3 ⊢ (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦))
12		fveq2 6873	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑝‘𝑥) = (𝑝‘𝑦))
13	12	oveq2d 7404	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑦)))
14	13	eleq2d 2818	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
15		oveq2 7396	. . . . 5 ⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦))
16	15	rexeqdv 3325	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
17	14, 16	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
18	11, 17	raleqbidv 3341	. 2 ⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
19		fveq2 6873	. . 3 ⊢ (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1)))
20		fveq2 6873	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑝‘𝑥) = (𝑝‘(𝑦 + 1)))
21	20	oveq2d 7404	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))
22	21	eleq2d 2818	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))))
23		oveq2 7396	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1)))
24	23	rexeqdv 3325	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
25	22, 24	imbi12d 344	. . 3 ⊢ (𝑥 = (𝑦 + 1) → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
26	19, 25	raleqbidv 3341	. 2 ⊢ (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
27		fveq2 6873	. . 3 ⊢ (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀))
28		fveq2 6873	. . . . . 6 ⊢ (𝑥 = 𝑀 → (𝑝‘𝑥) = (𝑝‘𝑀))
29	28	oveq2d 7404	. . . . 5 ⊢ (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑀)))
30	29	eleq2d 2818	. . . 4 ⊢ (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀))))
31		oveq2 7396	. . . . 5 ⊢ (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀))
32	31	rexeqdv 3325	. . . 4 ⊢ (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
33	30, 32	imbi12d 344	. . 3 ⊢ (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
34	27, 33	raleqbidv 3341	. 2 ⊢ (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
35		0nn0 12464	. . . . 5 ⊢ 0 ∈ ℕ₀
36		fveq2 6873	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘𝑖) = (𝑝‘0))
37		fv0p1e1 12312	. . . . . . . 8 ⊢ (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1))
38	36, 37	oveq12d 7406	. . . . . . 7 ⊢ (𝑖 = 0 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1)))
39	38	eleq2d 2818	. . . . . 6 ⊢ (𝑖 = 0 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
40	39	rexsng 4666	. . . . 5 ⊢ (0 ∈ ℕ₀ → (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
41	35, 40	ax-mp 5	. . . 4 ⊢ (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))
42	41	biimpri 227	. . 3 ⊢ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
43	42	rgenw 3064	. 2 ⊢ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
44		nfv 1917	. . . . 5 ⊢ Ⅎ𝑝 𝑦 ∈ ℕ
45		nfra1 3280	. . . . 5 ⊢ Ⅎ𝑝∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
46	44, 45	nfan 1902	. . . 4 ⊢ Ⅎ𝑝(𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
47		nnnn0 12456	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℕ₀)
48		fzonn0p1 13686	. . . . . . . . . 10 ⊢ (𝑦 ∈ ℕ₀ → 𝑦 ∈ (0..^(𝑦 + 1)))
49	47, 48	syl 17	. . . . . . . . 9 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1)))
50	49	ad2antrr 724	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1)))
51		fveq2 6873	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘𝑖) = (𝑝‘𝑦))
52		fvoveq1 7411	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1)))
53	51, 52	oveq12d 7406	. . . . . . . . . 10 ⊢ (𝑖 = 𝑦 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))
54	53	eleq2d 2818	. . . . . . . . 9 ⊢ (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
55	54	adantl 482	. . . . . . . 8 ⊢ ((((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))))
56		peano2nn 12201	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
57	56	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ ℕ)
58		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1)))
59	56	nnnn0d 12509	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ₀)
60		0elfz 13575	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 + 1) ∈ ℕ₀ → 0 ∈ (0...(𝑦 + 1)))
61	59, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → 0 ∈ (0...(𝑦 + 1)))
62	61	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...(𝑦 + 1)))
63	57, 58, 62	iccpartxr 45796	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈ ℝ^*)
64		nn0fz0 13576	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 + 1) ∈ ℕ₀ ↔ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
65	59, 64	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
66	65	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
67	57, 58, 66	iccpartxr 45796	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘(𝑦 + 1)) ∈ ℝ^*)
68	63, 67	jca 512	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
69	68	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
70		elico1 13344	. . . . . . . . . . . 12 ⊢ (((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
71	69, 70	syl 17	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
72		simp1 1136	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ℝ^*)
73	72	adantl 482	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ^*)
74		simpl 483	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘𝑦) ≤ 𝑋)
75		simpr3 1196	. . . . . . . . . . . . . . 15 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘(𝑦 + 1)))
76	73, 74, 75	3jca 1128	. . . . . . . . . . . . . 14 ⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))
77	76	ex 413	. . . . . . . . . . . . 13 ⊢ ((𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
78	77	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
79	78	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
80	71, 79	sylbid 239	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
81	80	impr 455	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))
82		nn0fz0 13576	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℕ₀ ↔ 𝑦 ∈ (0...𝑦))
83	47, 82	sylib 217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦))
84		fzelp1 13530	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (0...𝑦) → 𝑦 ∈ (0...(𝑦 + 1)))
85	83, 84	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...(𝑦 + 1)))
86	85	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...(𝑦 + 1)))
87	57, 58, 86	iccpartxr 45796	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) ∈ ℝ^*)
88	87, 67	jca 512	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
89	88	ad2ant2r 745	. . . . . . . . . 10 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^*))
90		elico1 13344	. . . . . . . . . 10 ⊢ (((𝑝‘𝑦) ∈ ℝ^* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
91	89, 90	syl 17	. . . . . . . . 9 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
92	81, 91	mpbird 256	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))
93	50, 55, 92	rspcedvd 3607	. . . . . . 7 ⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
94	93	exp43 437	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
95	94	adantr 481	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
96		iccpartres 45795	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦))
97		rspsbca 3865	. . . . . . . . . . . 12 ⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
98		vex 3473	. . . . . . . . . . . . . . 15 ⊢ 𝑝 ∈ V
99	98	resex 6016	. . . . . . . . . . . . . 14 ⊢ (𝑝 ↾ (0...𝑦)) ∈ V
100		sbcimg 3819	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
101		sbcel2 4406	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)))
102		csbov12g 7432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)))
103		csbfv12 6921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0)
104		csbvarg 4422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝 = (𝑝 ↾ (0...𝑦)))
105		csbconstg 3903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0 = 0)
106	104, 105	fveq12d 6880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) = ((𝑝 ↾ (0...𝑦))‘0))
107	103, 106	eqtrid 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
108		csbfv12 6921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦)
109		csbconstg 3903	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦 = 𝑦)
110	104, 109	fveq12d 6880	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
111	108, 110	eqtrid 2783	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
112	107, 111	oveq12d 7406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
113	102, 112	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
114	113	eleq2d 2818	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
115	101, 114	bitrid 282	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
116		sbcrex 3860	. . . . . . . . . . . . . . . . 17 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
117		sbcel2 4406	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
118		csbov12g 7432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))))
119		csbfv12 6921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖)
120		csbconstg 3903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖 = 𝑖)
121	104, 120	fveq12d 6880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
122	119, 121	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
123		csbfv12 6921	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1))
124		csbconstg 3903	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1) = (𝑖 + 1))
125	104, 124	fveq12d 6880	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
126	123, 125	eqtrid 2783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
127	122, 126	oveq12d 7406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
128	118, 127	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
129	128	eleq2d 2818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
130	117, 129	bitrid 282	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
131	130	rexbidv 3177	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
132	116, 131	bitrid 282	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
133	115, 132	imbi12d 344	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))))
134	100, 133	bitrd 278	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
137	136	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))))
138	72	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ^*)
139		simpr2 1195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘0) ≤ 𝑋)
140		xrltnle 11258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑋 ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋))
141	72, 87, 140	syl2anr 597	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋))
142	141	exbiri 809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → 𝑋 < (𝑝‘𝑦))))
143	142	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 < (𝑝‘𝑦))))
144	143	imp31 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘𝑦))
145	138, 139, 144	3jca 1128	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))
146	63, 87	jca 512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*))
147	146	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → ((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^*))
148		elico1 13344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑝‘0) ∈ ℝ^* ∧ (𝑝‘𝑦) ∈ ℝ^) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ^ ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))))
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))))
150	145, 149	mpbird 256	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))
151	150	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ^* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
152	137, 151	sylbid 239	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))))
153		0elfz 13575	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑦 ∈ ℕ₀ → 0 ∈ (0...𝑦))
154	47, 153	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 ∈ ℕ → 0 ∈ (0...𝑦))
155	154	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...𝑦))
156		fvres 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
157	155, 156	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
158	157	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
159	83	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦))
160		fvres 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
161	159, 160	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦))
162	161	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
163	158, 162	oveq12d 7406	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
164	163	eleq2d 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
165	164	biimpa 477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
166		elfzofz 13625	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦))
167	166	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦))
168		fvres 6892	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
169	167, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖))
170		fzofzp1 13706	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦))
171	170	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦))
172		fvres 6892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑖 + 1) ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
173	171, 172	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
174	173	adantlr 713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
175	169, 174	oveq12d 7406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))
176	175	eleq2d 2818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
177	176	rexbidva 3175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
178		nnz 12556	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
179		uzid 12814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ (ℤ_≥‘𝑦))
180	178, 179	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ_≥‘𝑦))
181		peano2uz 12862	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (ℤ_≥‘𝑦) → (𝑦 + 1) ∈ (ℤ_≥‘𝑦))
182		fzoss2 13637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 + 1) ∈ (ℤ_≥‘𝑦) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
183	180, 181, 182	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
184	183	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
185		ssrexv 4042	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((0..^𝑦) ⊆ (0..^(𝑦 + 1)) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
186	184, 185	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
187	177, 186	sylbid 239	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
188	165, 187	embantd 59	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
189	188	ex 413	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
190	189	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
191	152, 190	syld 47	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
192	191	ex 413	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
193	192	com34 91	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
194	193	com13 88	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
195	135, 194	sylbi 216	. . . . . . . . . . . 12 ⊢ ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
196	97, 195	syl 17	. . . . . . . . . . 11 ⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
197	196	ex 413	. . . . . . . . . 10 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
198	197	com24 95	. . . . . . . . 9 ⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
199	96, 198	mpcom 38	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
200	199	ex 413	. . . . . . 7 ⊢ (𝑦 ∈ ℕ → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
201	200	com24 95	. . . . . 6 ⊢ (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))))
202	201	imp 407	. . . . 5 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))
203	95, 202	pm2.61d 179	. . . 4 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
204	46, 203	ralrimi 3253	. . 3 ⊢ ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
205	204	ex 413	. 2 ⊢ (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))
206	10, 18, 26, 34, 43, 205	nnind 12207	1 ⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 Vcvv 3469 [wsbc 3768 ⦋csb 3884 ⊆ wss 3939 {csn 4617 class class class wbr 5136 ↾ cres 5666 ‘cfv 6527 (class class class)co 7388 0cc0 11087 1c1 11088 + caddc 11090 ℝ^*cxr 11224 < clt 11225 ≤ cle 11226 ℕcn 12189 ℕ₀cn0 12449 ℤcz 12535 ℤ_≥cuz 12799 [,)cico 13303 ...cfz 13461 ..^cfzo 13604 RePartciccp 45790

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5287 ax-nul 5294 ax-pow 5351 ax-pr 5415 ax-un 7703 ax-cnex 11143 ax-resscn 11144 ax-1cn 11145 ax-icn 11146 ax-addcl 11147 ax-addrcl 11148 ax-mulcl 11149 ax-mulrcl 11150 ax-mulcom 11151 ax-addass 11152 ax-mulass 11153 ax-distr 11154 ax-i2m1 11155 ax-1ne0 11156 ax-1rid 11157 ax-rnegex 11158 ax-rrecex 11159 ax-cnre 11160 ax-pre-lttri 11161 ax-pre-lttrn 11162 ax-pre-ltadd 11163 ax-pre-mulgt0 11164

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3375 df-rab 3429 df-v 3471 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-pss 3958 df-nul 4314 df-if 4518 df-pw 4593 df-sn 4618 df-pr 4620 df-op 4624 df-uni 4897 df-iun 4987 df-br 5137 df-opab 5199 df-mpt 5220 df-tr 5254 df-id 5562 df-eprel 5568 df-po 5576 df-so 5577 df-fr 5619 df-we 5621 df-xp 5670 df-rel 5671 df-cnv 5672 df-co 5673 df-dm 5674 df-rn 5675 df-res 5676 df-ima 5677 df-pred 6284 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6529 df-fn 6530 df-f 6531 df-f1 6532 df-fo 6533 df-f1o 6534 df-fv 6535 df-riota 7344 df-ov 7391 df-oprab 7392 df-mpo 7393 df-om 7834 df-1st 7952 df-2nd 7953 df-frecs 8243 df-wrecs 8274 df-recs 8348 df-rdg 8387 df-er 8681 df-map 8800 df-en 8918 df-dom 8919 df-sdom 8920 df-pnf 11227 df-mnf 11228 df-xr 11229 df-ltxr 11230 df-le 11231 df-sub 11423 df-neg 11424 df-nn 12190 df-n0 12450 df-z 12536 df-uz 12800 df-ico 13307 df-fz 13462 df-fzo 13605 df-iccp 45791

This theorem is referenced by: iccpartiun 45811 icceuelpart 45813 bgoldbtbnd 46186

W3C validator