| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . 3
⊢ (𝑥 = 1 → (RePart‘𝑥) =
(RePart‘1)) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑝‘𝑥) = (𝑝‘1)) |
| 3 | 2 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘1))) |
| 4 | 3 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
| 5 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1)) |
| 6 | | fzo01 13786 |
. . . . . 6
⊢ (0..^1) =
{0} |
| 7 | 5, 6 | eqtrdi 2793 |
. . . . 5
⊢ (𝑥 = 1 → (0..^𝑥) = {0}) |
| 8 | 7 | rexeqdv 3327 |
. . . 4
⊢ (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 9 | 4, 8 | imbi12d 344 |
. . 3
⊢ (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 10 | 1, 9 | raleqbidv 3346 |
. 2
⊢ (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 11 | | fveq2 6906 |
. . 3
⊢ (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦)) |
| 12 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑝‘𝑥) = (𝑝‘𝑦)) |
| 13 | 12 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑦))) |
| 14 | 13 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
| 15 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦)) |
| 16 | 15 | rexeqdv 3327 |
. . . 4
⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 17 | 14, 16 | imbi12d 344 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 18 | 11, 17 | raleqbidv 3346 |
. 2
⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 19 | | fveq2 6906 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1))) |
| 20 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑝‘𝑥) = (𝑝‘(𝑦 + 1))) |
| 21 | 20 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))) |
| 22 | 21 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) |
| 23 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1))) |
| 24 | 23 | rexeqdv 3327 |
. . . 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 3346 |
. 2
⊢ (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 27 | | fveq2 6906 |
. . 3
⊢ (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀)) |
| 28 | | fveq2 6906 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑝‘𝑥) = (𝑝‘𝑀)) |
| 29 | 28 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑀))) |
| 30 | 29 | eleq2d 2827 |
. . . 4
⊢ (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)))) |
| 31 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀)) |
| 32 | 31 | rexeqdv 3327 |
. . . 4
⊢ (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 33 | 30, 32 | imbi12d 344 |
. . 3
⊢ (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 34 | 27, 33 | raleqbidv 3346 |
. 2
⊢ (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 35 | | 0nn0 12541 |
. . . . 5
⊢ 0 ∈
ℕ0 |
| 36 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑝‘𝑖) = (𝑝‘0)) |
| 37 | | fv0p1e1 12389 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1)) |
| 38 | 36, 37 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1))) |
| 39 | 38 | eleq2d 2827 |
. . . . . 6
⊢ (𝑖 = 0 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
| 40 | 39 | rexsng 4676 |
. . . . 5
⊢ (0 ∈
ℕ0 → (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
| 41 | 35, 40 | ax-mp 5 |
. . . 4
⊢
(∃𝑖 ∈
{0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))) |
| 42 | 41 | biimpri 228 |
. . 3
⊢ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 43 | 42 | rgenw 3065 |
. 2
⊢
∀𝑝 ∈
(RePart‘1)(𝑋 ∈
((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 44 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑝 𝑦 ∈ ℕ |
| 45 | | nfra1 3284 |
. . . . 5
⊢
Ⅎ𝑝∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 46 | 44, 45 | nfan 1899 |
. . . 4
⊢
Ⅎ𝑝(𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 47 | | nnnn0 12533 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
| 48 | | fzonn0p1 13781 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈ (0..^(𝑦 + 1))) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1))) |
| 50 | 49 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1))) |
| 51 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑦 → (𝑝‘𝑖) = (𝑝‘𝑦)) |
| 52 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1))) |
| 53 | 51, 52 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑦 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))) |
| 54 | 53 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))) |
| 55 | 54 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))) |
| 56 | | peano2nn 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈
ℕ) |
| 58 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1))) |
| 59 | 56 | nnnn0d 12587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ0) |
| 60 | | 0elfz 13664 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 + 1) ∈ ℕ0
→ 0 ∈ (0...(𝑦 +
1))) |
| 61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 0 ∈
(0...(𝑦 +
1))) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈
(0...(𝑦 +
1))) |
| 63 | 57, 58, 62 | iccpartxr 47406 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈
ℝ*) |
| 64 | | nn0fz0 13665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 + 1) ∈ ℕ0
↔ (𝑦 + 1) ∈
(0...(𝑦 +
1))) |
| 65 | 59, 64 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ (0...(𝑦 + 1))) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ (0...(𝑦 + 1))) |
| 67 | 57, 58, 66 | iccpartxr 47406 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘(𝑦 + 1)) ∈
ℝ*) |
| 68 | 63, 67 | jca 511 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈
ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
| 69 | 68 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ* ∧
(𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
| 70 | | elico1 13430 |
. . . . . . . . . . . 12
⊢ (((𝑝‘0) ∈
ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) →
(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 72 | | simp1 1137 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℝ*
∧ (𝑝‘0) ≤
𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈
ℝ*) |
| 73 | 72 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈
ℝ*) |
| 74 | | simpl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘𝑦) ≤ 𝑋) |
| 75 | | simpr3 1197 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘(𝑦 + 1))) |
| 76 | 73, 74, 75 | 3jca 1129 |
. . . . . . . . . . . . . 14
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) |
| 77 | 76 | ex 412 |
. . . . . . . . . . . . 13
⊢ ((𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 80 | 71, 79 | sylbid 240 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 81 | 80 | impr 454 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) |
| 82 | | nn0fz0 13665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈ (0...𝑦)) |
| 83 | 47, 82 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦)) |
| 84 | | fzelp1 13616 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0...𝑦) → 𝑦 ∈ (0...(𝑦 + 1))) |
| 85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...(𝑦 + 1))) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...(𝑦 + 1))) |
| 87 | 57, 58, 86 | iccpartxr 47406 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) ∈
ℝ*) |
| 88 | 87, 67 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
| 89 | 88 | ad2ant2r 747 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
| 90 | | elico1 13430 |
. . . . . . . . . 10
⊢ (((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) →
(𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 91 | 89, 90 | syl 17 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 92 | 81, 91 | mpbird 257 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))) |
| 93 | 50, 55, 92 | rspcedvd 3624 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 94 | 93 | exp43 436 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 95 | 94 | adantr 480 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 96 | | iccpartres 47405 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦)) |
| 97 | | rspsbca 3880 |
. . . . . . . . . . . 12
⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 98 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑝 ∈ V |
| 99 | 98 | resex 6047 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ↾ (0...𝑦)) ∈ V |
| 100 | | sbcimg 3837 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 101 | | sbcel2 4418 |
. . . . . . . . . . . . . . . . 17
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦))) |
| 102 | | csbov12g 7477 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦))) |
| 103 | | csbfv12 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) =
(⦋(𝑝 ↾
(0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) |
| 104 | | csbvarg 4434 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝 = (𝑝 ↾ (0...𝑦))) |
| 105 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0 = 0) |
| 106 | 104, 105 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) = ((𝑝 ↾ (0...𝑦))‘0)) |
| 107 | 103, 106 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0)) |
| 108 | | csbfv12 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) |
| 109 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦 = 𝑦) |
| 110 | 104, 109 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
| 111 | 108, 110 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
| 112 | 107, 111 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
| 113 | 102, 112 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
| 114 | 113 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
| 115 | 101, 114 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
| 116 | | sbcrex 3875 |
. . . . . . . . . . . . . . . . 17
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 117 | | sbcel2 4418 |
. . . . . . . . . . . . . . . . . . 19
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 118 | | csbov12g 7477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)))) |
| 119 | | csbfv12 6954 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) |
| 120 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖 = 𝑖) |
| 121 | 104, 120 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖)) |
| 122 | 119, 121 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖)) |
| 123 | | csbfv12 6954 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) |
| 124 | | csbconstg 3918 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1) = (𝑖 + 1)) |
| 125 | 104, 124 | fveq12d 6913 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) |
| 126 | 123, 125 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) |
| 127 | 122, 126 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) |
| 128 | 118, 127 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) |
| 129 | 128 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
| 130 | 117, 129 | bitrid 283 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
| 131 | 130 | rexbidv 3179 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
| 132 | 116, 131 | bitrid 283 |
. . . . . . . . . . . . . . . 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 279 |
. . . . . . . . . . . . . 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 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
| 138 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈
ℝ*) |
| 139 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘0) ≤ 𝑋) |
| 140 | | xrltnle 11328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑋 ∈ ℝ*
∧ (𝑝‘𝑦) ∈ ℝ*)
→ (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋)) |
| 141 | 72, 87, 140 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋)) |
| 142 | 141 | exbiri 811 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ*
∧ (𝑝‘0) ≤
𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → 𝑋 < (𝑝‘𝑦)))) |
| 143 | 142 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 < (𝑝‘𝑦)))) |
| 144 | 143 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘𝑦)) |
| 145 | 138, 139,
144 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))) |
| 146 | 63, 87 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈
ℝ* ∧ (𝑝‘𝑦) ∈
ℝ*)) |
| 147 | 146 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → ((𝑝‘0) ∈ ℝ* ∧
(𝑝‘𝑦) ∈
ℝ*)) |
| 148 | | elico1 13430 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝‘0) ∈
ℝ* ∧ (𝑝‘𝑦) ∈ ℝ*) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))) |
| 149 | 147, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))) |
| 150 | 145, 149 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) |
| 151 | 150 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
| 152 | 137, 151 | sylbid 240 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
| 153 | | 0elfz 13664 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ0
→ 0 ∈ (0...𝑦)) |
| 154 | 47, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 0 ∈
(0...𝑦)) |
| 155 | 154 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈
(0...𝑦)) |
| 156 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
(0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0)) |
| 157 | 155, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0)) |
| 158 | 157 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0)) |
| 159 | 83 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦)) |
| 160 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦)) |
| 161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦)) |
| 162 | 161 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
| 163 | 158, 162 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
| 164 | 163 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
| 165 | 164 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
| 166 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦)) |
| 167 | 166 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦)) |
| 168 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖)) |
| 169 | 167, 168 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖)) |
| 170 | | fzofzp1 13803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦)) |
| 171 | 170 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦)) |
| 172 | | fvres 6925 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 + 1) ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
| 173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
| 174 | 173 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
| 175 | 169, 174 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
| 176 | 175 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 177 | 176 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 178 | | nnz 12634 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
| 179 | | uzid 12893 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
(ℤ≥‘𝑦)) |
| 180 | | peano2uz 12943 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈
(ℤ≥‘𝑦) → (𝑦 + 1) ∈
(ℤ≥‘𝑦)) |
| 181 | | fzoss2 13727 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 + 1) ∈
(ℤ≥‘𝑦) → (0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
| 182 | 178, 179,
180, 181 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ →
(0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
| 183 | 182 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
| 184 | | ssrexv 4053 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0..^𝑦) ⊆
(0..^(𝑦 + 1)) →
(∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 185 | 183, 184 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 186 | 177, 185 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 187 | 165, 186 | embantd 59 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 188 | 187 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 189 | 188 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 190 | 152, 189 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 191 | 190 | ex 412 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 192 | 191 | com34 91 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 193 | 192 | com13 88 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 194 | 135, 193 | sylbi 217 |
. . . . . . . . . . . 12
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 195 | 97, 194 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 196 | 195 | ex 412 |
. . . . . . . . . 10
⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
| 197 | 196 | com24 95 |
. . . . . . . . 9
⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
| 198 | 96, 197 | mpcom 38 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 199 | 198 | ex 412 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
| 200 | 199 | com24 95 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
(∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
| 201 | 200 | imp 406 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
| 202 | 95, 201 | pm2.61d 179 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 203 | 46, 202 | ralrimi 3257 |
. . 3
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
| 204 | 203 | ex 412 |
. 2
⊢ (𝑦 ∈ ℕ →
(∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
| 205 | 10, 18, 26, 34, 43, 204 | nnind 12284 |
1
⊢ (𝑀 ∈ ℕ →
∀𝑝 ∈
(RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |