Users' Mathboxes 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 42127
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.
StepHypRef Expression
1 fveq2 6379 . . 3 (𝑥 = 1 → (RePart‘𝑥) = (RePart‘1))
2 fveq2 6379 . . . . . 6 (𝑥 = 1 → (𝑝𝑥) = (𝑝‘1))
32oveq2d 6862 . . . . 5 (𝑥 = 1 → ((𝑝‘0)[,)(𝑝𝑥)) = ((𝑝‘0)[,)(𝑝‘1)))
43eleq2d 2830 . . . 4 (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
5 oveq2 6854 . . . . . 6 (𝑥 = 1 → (0..^𝑥) = (0..^1))
6 fzo01 12763 . . . . . 6 (0..^1) = {0}
75, 6syl6eq 2815 . . . . 5 (𝑥 = 1 → (0..^𝑥) = {0})
87rexeqdv 3293 . . . 4 (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
94, 8imbi12d 335 . . 3 (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
101, 9raleqbidv 3300 . 2 (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
11 fveq2 6379 . . 3 (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦))
12 fveq2 6379 . . . . . 6 (𝑥 = 𝑦 → (𝑝𝑥) = (𝑝𝑦))
1312oveq2d 6862 . . . . 5 (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝𝑥)) = ((𝑝‘0)[,)(𝑝𝑦)))
1413eleq2d 2830 . . . 4 (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))))
15 oveq2 6854 . . . . 5 (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦))
1615rexeqdv 3293 . . . 4 (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
1714, 16imbi12d 335 . . 3 (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
1811, 17raleqbidv 3300 . 2 (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
19 fveq2 6379 . . 3 (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1)))
20 fveq2 6379 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝑝𝑥) = (𝑝‘(𝑦 + 1)))
2120oveq2d 6862 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))
2221eleq2d 2830 . . . 4 (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))))
23 oveq2 6854 . . . . 5 (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1)))
2423rexeqdv 3293 . . . 4 (𝑥 = (𝑦 + 1) → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
2522, 24imbi12d 335 . . 3 (𝑥 = (𝑦 + 1) → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
2619, 25raleqbidv 3300 . 2 (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
27 fveq2 6379 . . 3 (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀))
28 fveq2 6379 . . . . . 6 (𝑥 = 𝑀 → (𝑝𝑥) = (𝑝𝑀))
2928oveq2d 6862 . . . . 5 (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝𝑥)) = ((𝑝‘0)[,)(𝑝𝑀)))
3029eleq2d 2830 . . . 4 (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀))))
31 oveq2 6854 . . . . 5 (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀))
3231rexeqdv 3293 . . . 4 (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
3330, 32imbi12d 335 . . 3 (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
3427, 33raleqbidv 3300 . 2 (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
35 0nn0 11559 . . . . 5 0 ∈ ℕ0
36 fveq2 6379 . . . . . . . 8 (𝑖 = 0 → (𝑝𝑖) = (𝑝‘0))
37 fv0p1e1 11406 . . . . . . . 8 (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1))
3836, 37oveq12d 6864 . . . . . . 7 (𝑖 = 0 → ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1)))
3938eleq2d 2830 . . . . . 6 (𝑖 = 0 → (𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
4039rexsng 4378 . . . . 5 (0 ∈ ℕ0 → (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))))
4135, 40ax-mp 5 . . . 4 (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))
4241biimpri 219 . . 3 (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
4342rgenw 3071 . 2 𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
44 nfv 2009 . . . . 5 𝑝 𝑦 ∈ ℕ
45 nfra1 3088 . . . . 5 𝑝𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
4644, 45nfan 1998 . . . 4 𝑝(𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
47 nnnn0 11550 . . . . . . . . . 10 (𝑦 ∈ ℕ → 𝑦 ∈ ℕ0)
48 fzonn0p1 12758 . . . . . . . . . 10 (𝑦 ∈ ℕ0𝑦 ∈ (0..^(𝑦 + 1)))
4947, 48syl 17 . . . . . . . . 9 (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1)))
5049ad2antrr 717 . . . . . . . 8 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1)))
51 fveq2 6379 . . . . . . . . . . 11 (𝑖 = 𝑦 → (𝑝𝑖) = (𝑝𝑦))
52 fvoveq1 6869 . . . . . . . . . . 11 (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1)))
5351, 52oveq12d 6864 . . . . . . . . . 10 (𝑖 = 𝑦 → ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1))))
5453eleq2d 2830 . . . . . . . . 9 (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1)))))
5554adantl 473 . . . . . . . 8 ((((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1)))))
56 peano2nn 11292 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ)
5756adantr 472 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ ℕ)
58 simpr 477 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1)))
5956nnnn0d 11602 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ ℕ0)
60 0elfz 12649 . . . . . . . . . . . . . . . . 17 ((𝑦 + 1) ∈ ℕ0 → 0 ∈ (0...(𝑦 + 1)))
6159, 60syl 17 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → 0 ∈ (0...(𝑦 + 1)))
6261adantr 472 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...(𝑦 + 1)))
6357, 58, 62iccpartxr 42113 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈ ℝ*)
64 nn0fz0 12650 . . . . . . . . . . . . . . . . 17 ((𝑦 + 1) ∈ ℕ0 ↔ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6559, 64sylib 209 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6665adantr 472 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6757, 58, 66iccpartxr 42113 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘(𝑦 + 1)) ∈ ℝ*)
6863, 67jca 507 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*))
6968adantlr 706 . . . . . . . . . . . 12 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*))
70 elico1 12425 . . . . . . . . . . . 12 (((𝑝‘0) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
7169, 70syl 17 . . . . . . . . . . 11 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
72 simp1 1166 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ℝ*)
7372adantl 473 . . . . . . . . . . . . . . 15 (((𝑝𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ*)
74 simpl 474 . . . . . . . . . . . . . . 15 (((𝑝𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝𝑦) ≤ 𝑋)
75 simpr3 1252 . . . . . . . . . . . . . . 15 (((𝑝𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘(𝑦 + 1)))
7673, 74, 753jca 1158 . . . . . . . . . . . . . 14 (((𝑝𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))))
7776ex 401 . . . . . . . . . . . . 13 ((𝑝𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
7877adantl 473 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
7978adantr 472 . . . . . . . . . . 11 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
8071, 79sylbid 231 . . . . . . . . . 10 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
8180impr 446 . . . . . . . . 9 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))))
82 nn0fz0 12650 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ℕ0𝑦 ∈ (0...𝑦))
8347, 82sylib 209 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦))
84 fzelp1 12605 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...𝑦) → 𝑦 ∈ (0...(𝑦 + 1)))
8583, 84syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ ℕ → 𝑦 ∈ (0...(𝑦 + 1)))
8685adantr 472 . . . . . . . . . . . . 13 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...(𝑦 + 1)))
8757, 58, 86iccpartxr 42113 . . . . . . . . . . . 12 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝𝑦) ∈ ℝ*)
8887, 67jca 507 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*))
8988ad2ant2r 753 . . . . . . . . . 10 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*))
90 elico1 12425 . . . . . . . . . 10 (((𝑝𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) → (𝑋 ∈ ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
9189, 90syl 17 . . . . . . . . 9 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
9281, 91mpbird 248 . . . . . . . 8 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑋 ∈ ((𝑝𝑦)[,)(𝑝‘(𝑦 + 1))))
9350, 55, 92rspcedvd 3469 . . . . . . 7 (((𝑦 ∈ ℕ ∧ (𝑝𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
9493exp43 427 . . . . . 6 (𝑦 ∈ ℕ → ((𝑝𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
9594adantr 472 . . . . 5 ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝑝𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
96 iccpartres 42112 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦))
97 rspsbca 3679 . . . . . . . . . . . 12 (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
98 vex 3353 . . . . . . . . . . . . . . 15 𝑝 ∈ V
9998resex 5622 . . . . . . . . . . . . . 14 (𝑝 ↾ (0...𝑦)) ∈ V
100 sbcimg 3640 . . . . . . . . . . . . . . 15 ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
101 sbcel2 4152 . . . . . . . . . . . . . . . . 17 ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) ↔ 𝑋(𝑝 ↾ (0...𝑦)) / 𝑝((𝑝‘0)[,)(𝑝𝑦)))
102 csbov12g 6889 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝((𝑝‘0)[,)(𝑝𝑦)) = ((𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘0)[,)(𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑦)))
103 csbfv12 6423 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘0) = ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝0)
104 csbvarg 4166 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝𝑝 = (𝑝 ↾ (0...𝑦)))
105 csbconstg 3706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝0 = 0)
106104, 105fveq12d 6386 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝0) = ((𝑝 ↾ (0...𝑦))‘0))
107103, 106syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
108 csbfv12 6423 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑦) = ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝𝑦)
109 csbconstg 3706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝𝑦 = 𝑦)
110104, 109fveq12d 6386 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
111108, 110syl5eq 2811 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
112107, 111oveq12d 6864 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘0)[,)(𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
113102, 112eqtrd 2799 . . . . . . . . . . . . . . . . . 18 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝((𝑝‘0)[,)(𝑝𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
114113eleq2d 2830 . . . . . . . . . . . . . . . . 17 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋(𝑝 ↾ (0...𝑦)) / 𝑝((𝑝‘0)[,)(𝑝𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
115101, 114syl5bb 274 . . . . . . . . . . . . . . . 16 ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
116 sbcrex 3674 . . . . . . . . . . . . . . . . 17 ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
117 sbcel2 4152 . . . . . . . . . . . . . . . . . . 19 ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋(𝑝 ↾ (0...𝑦)) / 𝑝((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
118 csbov12g 6889 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑖)[,)(𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘(𝑖 + 1))))
119 csbfv12 6423 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑖) = ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝𝑖)
120 csbconstg 3706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝𝑖 = 𝑖)
121104, 120fveq12d 6386 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
122119, 121syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖))
123 csbfv12 6423 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝(𝑖 + 1))
124 csbconstg 3706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝(𝑖 + 1) = (𝑖 + 1))
125104, 124fveq12d 6386 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝𝑝(𝑝 ↾ (0...𝑦)) / 𝑝(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
126123, 125syl5eq 2811 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))
127122, 126oveq12d 6864 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 ↾ (0...𝑦)) ∈ V → ((𝑝 ↾ (0...𝑦)) / 𝑝(𝑝𝑖)[,)(𝑝 ↾ (0...𝑦)) / 𝑝(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
128118, 127eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑝 ↾ (0...𝑦)) / 𝑝((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))
129128eleq2d 2830 . . . . . . . . . . . . . . . . . . 19 ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋(𝑝 ↾ (0...𝑦)) / 𝑝((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
130117, 129syl5bb 274 . . . . . . . . . . . . . . . . . 18 ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
131130rexbidv 3199 . . . . . . . . . . . . . . . . 17 ((𝑝 ↾ (0...𝑦)) ∈ V → (∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
132116, 131syl5bb 274 . . . . . . . . . . . . . . . 16 ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
133115, 132imbi12d 335 . . . . . . . . . . . . . . 15 ((𝑝 ↾ (0...𝑦)) ∈ V → (([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))))
134100, 133bitrd 270 . . . . . . . . . . . . . 14 ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))))
13599, 134ax-mp 5 . . . . . . . . . . . . 13 ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))
13668, 70syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
137136adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))))
13872adantl 473 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ℝ*)
139 simpr2 1250 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘0) ≤ 𝑋)
140 xrltnle 10363 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋 ∈ ℝ* ∧ (𝑝𝑦) ∈ ℝ*) → (𝑋 < (𝑝𝑦) ↔ ¬ (𝑝𝑦) ≤ 𝑋))
14172, 87, 140syl2anr 590 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 < (𝑝𝑦) ↔ ¬ (𝑝𝑦) ≤ 𝑋))
142141exbiri 845 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋𝑋 < (𝑝𝑦))))
143142com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 < (𝑝𝑦))))
144143imp31 408 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝𝑦))
145138, 139, 1443jca 1158 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝𝑦)))
14663, 87jca 507 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ* ∧ (𝑝𝑦) ∈ ℝ*))
147146ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → ((𝑝‘0) ∈ ℝ* ∧ (𝑝𝑦) ∈ ℝ*))
148 elico1 12425 . . . . . . . . . . . . . . . . . . . . 21 (((𝑝‘0) ∈ ℝ* ∧ (𝑝𝑦) ∈ ℝ*) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝𝑦))))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝𝑦))))
150145, 149mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)))
151150ex 401 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))))
152137, 151sylbid 231 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))))
153 0elfz 12649 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ ℕ0 → 0 ∈ (0...𝑦))
15447, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ ℕ → 0 ∈ (0...𝑦))
155154adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈ (0...𝑦))
156 fvres 6398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
157155, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0))
158157eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0))
15983adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦))
160 fvres 6398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝𝑦))
161159, 160syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝𝑦))
162161eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦))
163158, 162oveq12d 6864 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
164163eleq2d 2830 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))))
165164biimpa 468 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))
166 elfzofz 12698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦))
167166adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦))
168 fvres 6398 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝𝑖))
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝𝑖))
170 fzofzp1 12778 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦))
171170adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦))
172 fvres 6398 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 + 1) ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
174173adantlr 706 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1)))
175169, 174oveq12d 6864 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))
176175eleq2d 2830 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
177176rexbidva 3196 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
178 nnz 11651 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℕ → 𝑦 ∈ ℤ)
179 uzid 11906 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ ℤ → 𝑦 ∈ (ℤ𝑦))
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ ℕ → 𝑦 ∈ (ℤ𝑦))
181 peano2uz 11946 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (ℤ𝑦) → (𝑦 + 1) ∈ (ℤ𝑦))
182 fzoss2 12709 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 + 1) ∈ (ℤ𝑦) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
183180, 181, 1823syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ ℕ → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
184183ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → (0..^𝑦) ⊆ (0..^(𝑦 + 1)))
185 ssrexv 3829 . . . . . . . . . . . . . . . . . . . . . 22 ((0..^𝑦) ⊆ (0..^(𝑦 + 1)) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
186184, 185syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
187177, 186sylbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
188165, 187embantd 59 . . . . . . . . . . . . . . . . . . 19 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
189188ex 401 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
190189adantr 472 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
191152, 190syld 47 . . . . . . . . . . . . . . . 16 (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
192191ex 401 . . . . . . . . . . . . . . 15 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
193192com34 91 . . . . . . . . . . . . . 14 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
194193com13 88 . . . . . . . . . . . . 13 ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
195135, 194sylbi 208 . . . . . . . . . . . 12 ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
19697, 195syl 17 . . . . . . . . . . 11 (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
197196ex 401 . . . . . . . . . 10 ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))))
198197com24 95 . . . . . . . . 9 ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))))
19996, 198mpcom 38 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
200199ex 401 . . . . . . 7 (𝑦 ∈ ℕ → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (¬ (𝑝𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))))
201200com24 95 . . . . . 6 (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))))
202201imp 395 . . . . 5 ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))))
20395, 202pm2.61d 171 . . . 4 ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
20446, 203ralrimi 3104 . . 3 ((𝑦 ∈ ℕ ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
205204ex 401 . 2 (𝑦 ∈ ℕ → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))))
20610, 18, 26, 34, 43, 205nnind 11298 1 (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  Vcvv 3350  [wsbc 3598  csb 3693  wss 3734  {csn 4336   class class class wbr 4811  cres 5281  cfv 6070  (class class class)co 6846  0cc0 10193  1c1 10194   + caddc 10196  *cxr 10331   < clt 10332  cle 10333  cn 11278  0cn0 11542  cz 11628  cuz 11891  [,)cico 12384  ...cfz 12538  ..^cfzo 12678  RePartciccp 42107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151  ax-cnex 10249  ax-resscn 10250  ax-1cn 10251  ax-icn 10252  ax-addcl 10253  ax-addrcl 10254  ax-mulcl 10255  ax-mulrcl 10256  ax-mulcom 10257  ax-addass 10258  ax-mulass 10259  ax-distr 10260  ax-i2m1 10261  ax-1ne0 10262  ax-1rid 10263  ax-rnegex 10264  ax-rrecex 10265  ax-cnre 10266  ax-pre-lttri 10267  ax-pre-lttrn 10268  ax-pre-ltadd 10269  ax-pre-mulgt0 10270
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-riota 6807  df-ov 6849  df-oprab 6850  df-mpt2 6851  df-om 7268  df-1st 7370  df-2nd 7371  df-wrecs 7614  df-recs 7676  df-rdg 7714  df-er 7951  df-map 8066  df-en 8165  df-dom 8166  df-sdom 8167  df-pnf 10334  df-mnf 10335  df-xr 10336  df-ltxr 10337  df-le 10338  df-sub 10526  df-neg 10527  df-nn 11279  df-n0 11543  df-z 11629  df-uz 11892  df-ico 12388  df-fz 12539  df-fzo 12679  df-iccp 42108
This theorem is referenced by:  iccpartiun  42128  icceuelpart  42130  bgoldbtbnd  42397
  Copyright terms: Public domain W3C validator