Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 1 → (RePart‘𝑥) =
(RePart‘1)) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 1 → (𝑝‘𝑥) = (𝑝‘1)) |
3 | 2 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 1 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘1))) |
4 | 3 | eleq2d 2673 |
. . . 4
⊢ (𝑥 = 1 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
5 | | oveq2 6557 |
. . . . . 6
⊢ (𝑥 = 1 → (0..^𝑥) = (0..^1)) |
6 | | fzo01 12417 |
. . . . . 6
⊢ (0..^1) =
{0} |
7 | 5, 6 | syl6eq 2660 |
. . . . 5
⊢ (𝑥 = 1 → (0..^𝑥) = {0}) |
8 | 7 | rexeqdv 3122 |
. . . 4
⊢ (𝑥 = 1 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
9 | 4, 8 | imbi12d 333 |
. . 3
⊢ (𝑥 = 1 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
10 | 1, 9 | raleqbidv 3129 |
. 2
⊢ (𝑥 = 1 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘1)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
11 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑦 → (RePart‘𝑥) = (RePart‘𝑦)) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑝‘𝑥) = (𝑝‘𝑦)) |
13 | 12 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑦))) |
14 | 13 | eleq2d 2673 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
15 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑦 → (0..^𝑥) = (0..^𝑦)) |
16 | 15 | rexeqdv 3122 |
. . . 4
⊢ (𝑥 = 𝑦 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
17 | 14, 16 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
18 | 11, 17 | raleqbidv 3129 |
. 2
⊢ (𝑥 = 𝑦 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
19 | | fveq2 6103 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → (RePart‘𝑥) = (RePart‘(𝑦 + 1))) |
20 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑝‘𝑥) = (𝑝‘(𝑦 + 1))) |
21 | 20 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘(𝑦 + 1)))) |
22 | 21 | eleq2d 2673 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) |
23 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (0..^𝑥) = (0..^(𝑦 + 1))) |
24 | 23 | rexeqdv 3122 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
25 | 22, 24 | imbi12d 333 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
26 | 19, 25 | raleqbidv 3129 |
. 2
⊢ (𝑥 = (𝑦 + 1) → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
27 | | fveq2 6103 |
. . 3
⊢ (𝑥 = 𝑀 → (RePart‘𝑥) = (RePart‘𝑀)) |
28 | | fveq2 6103 |
. . . . . 6
⊢ (𝑥 = 𝑀 → (𝑝‘𝑥) = (𝑝‘𝑀)) |
29 | 28 | oveq2d 6565 |
. . . . 5
⊢ (𝑥 = 𝑀 → ((𝑝‘0)[,)(𝑝‘𝑥)) = ((𝑝‘0)[,)(𝑝‘𝑀))) |
30 | 29 | eleq2d 2673 |
. . . 4
⊢ (𝑥 = 𝑀 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)))) |
31 | | oveq2 6557 |
. . . . 5
⊢ (𝑥 = 𝑀 → (0..^𝑥) = (0..^𝑀)) |
32 | 31 | rexeqdv 3122 |
. . . 4
⊢ (𝑥 = 𝑀 → (∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
33 | 30, 32 | imbi12d 333 |
. . 3
⊢ (𝑥 = 𝑀 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
34 | 27, 33 | raleqbidv 3129 |
. 2
⊢ (𝑥 = 𝑀 → (∀𝑝 ∈ (RePart‘𝑥)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑥)) → ∃𝑖 ∈ (0..^𝑥)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
35 | | 0nn0 11184 |
. . . . 5
⊢ 0 ∈
ℕ0 |
36 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑝‘𝑖) = (𝑝‘0)) |
37 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → (𝑖 + 1) = (0 + 1)) |
38 | | 0p1e1 11009 |
. . . . . . . . . 10
⊢ (0 + 1) =
1 |
39 | 37, 38 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝑖 + 1) = 1) |
40 | 39 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑖 = 0 → (𝑝‘(𝑖 + 1)) = (𝑝‘1)) |
41 | 36, 40 | oveq12d 6567 |
. . . . . . 7
⊢ (𝑖 = 0 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘0)[,)(𝑝‘1))) |
42 | 41 | eleq2d 2673 |
. . . . . 6
⊢ (𝑖 = 0 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
43 | 42 | rexsng 4166 |
. . . . 5
⊢ (0 ∈
ℕ0 → (∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)))) |
44 | 35, 43 | ax-mp 5 |
. . . 4
⊢
(∃𝑖 ∈
{0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1))) |
45 | 44 | biimpri 217 |
. . 3
⊢ (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
46 | 45 | rgenw 2908 |
. 2
⊢
∀𝑝 ∈
(RePart‘1)(𝑋 ∈
((𝑝‘0)[,)(𝑝‘1)) → ∃𝑖 ∈ {0}𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
47 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑝 𝑦 ∈ ℕ |
48 | | nfra1 2925 |
. . . . 5
⊢
Ⅎ𝑝∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
49 | 47, 48 | nfan 1816 |
. . . 4
⊢
Ⅎ𝑝(𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
50 | | nnnn0 11176 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℕ0) |
51 | | fzonn0p1 12411 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈ (0..^(𝑦 + 1))) |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0..^(𝑦 + 1))) |
53 | 52 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑦 ∈ (0..^(𝑦 + 1))) |
54 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑦 → (𝑝‘𝑖) = (𝑝‘𝑦)) |
55 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑦 → (𝑖 + 1) = (𝑦 + 1)) |
56 | 55 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑦 → (𝑝‘(𝑖 + 1)) = (𝑝‘(𝑦 + 1))) |
57 | 54, 56 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑦 → ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))) |
58 | 57 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑖 = 𝑦 → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))) |
59 | 58 | adantl 481 |
. . . . . . . 8
⊢ ((((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) ∧ 𝑖 = 𝑦) → (𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))))) |
60 | | peano2nn 10909 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ) |
61 | 60 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈
ℕ) |
62 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑝 ∈ (RePart‘(𝑦 + 1))) |
63 | 60 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ0) |
64 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 + 1) ∈ ℕ0
→ 0 ∈ (0...(𝑦 +
1))) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → 0 ∈
(0...(𝑦 +
1))) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈
(0...(𝑦 +
1))) |
67 | 61, 62, 66 | iccpartxr 39957 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) ∈
ℝ*) |
68 | | nn0fz0 12306 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 + 1) ∈ ℕ0
↔ (𝑦 + 1) ∈
(0...(𝑦 +
1))) |
69 | 63, 68 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈ (0...(𝑦 + 1))) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑦 + 1) ∈ (0...(𝑦 + 1))) |
71 | 61, 62, 70 | iccpartxr 39957 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘(𝑦 + 1)) ∈
ℝ*) |
72 | 67, 71 | jca 553 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈
ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
73 | 72 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈ ℝ* ∧
(𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
74 | | elico1 12089 |
. . . . . . . . . . . 12
⊢ (((𝑝‘0) ∈
ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) →
(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
76 | | simp1 1054 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋 ∈ ℝ*
∧ (𝑝‘0) ≤
𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈
ℝ*) |
77 | 76 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈
ℝ*) |
78 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘𝑦) ≤ 𝑋) |
79 | | simpr3 1062 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘(𝑦 + 1))) |
80 | 77, 78, 79 | 3jca 1235 |
. . . . . . . . . . . . . 14
⊢ (((𝑝‘𝑦) ≤ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) |
81 | 80 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
82 | 81 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
83 | 82 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
84 | 75, 83 | sylbid 229 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
85 | 84 | impr 647 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) |
86 | | nn0fz0 12306 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℕ0
↔ 𝑦 ∈ (0...𝑦)) |
87 | 50, 86 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...𝑦)) |
88 | | fzelp1 12263 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (0...𝑦) → 𝑦 ∈ (0...(𝑦 + 1))) |
89 | 87, 88 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℕ → 𝑦 ∈ (0...(𝑦 + 1))) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...(𝑦 + 1))) |
91 | 61, 62, 90 | iccpartxr 39957 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) ∈
ℝ*) |
92 | 91, 71 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
93 | 92 | ad2ant2r 779 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈
ℝ*)) |
94 | | elico1 12089 |
. . . . . . . . . 10
⊢ (((𝑝‘𝑦) ∈ ℝ* ∧ (𝑝‘(𝑦 + 1)) ∈ ℝ*) →
(𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
95 | 93, 94 | syl 17 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → (𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘𝑦) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
96 | 85, 95 | mpbird 246 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → 𝑋 ∈ ((𝑝‘𝑦)[,)(𝑝‘(𝑦 + 1)))) |
97 | 53, 59, 96 | rspcedvd 3289 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑝 ∈ (RePart‘(𝑦 + 1)) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
98 | 97 | exp43 638 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
99 | 98 | adantr 480 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
100 | | iccpartres 39956 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦)) |
101 | | rspsbca 3485 |
. . . . . . . . . . . 12
⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → [(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
102 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑝 ∈ V |
103 | 102 | resex 5363 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ↾ (0...𝑦)) ∈ V |
104 | | sbcimg 3444 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
105 | | sbcel2 3941 |
. . . . . . . . . . . . . . . . 17
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦))) |
106 | | csbov12g 6587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦))) |
107 | | csbfv12 6141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) =
(⦋(𝑝 ↾
(0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) |
108 | | csbvarg 3955 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝 = (𝑝 ↾ (0...𝑦))) |
109 | | csbconstg 3512 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0 = 0) |
110 | 108, 109 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌0) = ((𝑝 ↾ (0...𝑦))‘0)) |
111 | 107, 110 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0)) |
112 | | csbfv12 6141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) |
113 | | csbconstg 3512 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦 = 𝑦) |
114 | 108, 113 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
115 | 112, 114 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
116 | 111, 115 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘0)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
117 | 106, 116 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
118 | 117 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
119 | 105, 118 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
120 | | sbcrex 3481 |
. . . . . . . . . . . . . . . . 17
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
121 | | sbcel2 3941 |
. . . . . . . . . . . . . . . . . . 19
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
122 | | csbov12g 6587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)))) |
123 | | csbfv12 6141 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) |
124 | | csbconstg 3512 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖 = 𝑖) |
125 | 108, 124 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖)) |
126 | 123, 125 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖) = ((𝑝 ↾ (0...𝑦))‘𝑖)) |
127 | | csbfv12 6141 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
⦋(𝑝
↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) |
128 | | csbconstg 3512 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1) = (𝑖 + 1)) |
129 | 108, 128 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌𝑝‘⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) |
130 | 127, 129 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1)) = ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) |
131 | 126, 130 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘𝑖)[,)⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) |
132 | 122, 131 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) = (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) |
133 | 132 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (𝑋 ∈ ⦋(𝑝 ↾ (0...𝑦)) / 𝑝⦌((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
134 | 121, 133 | syl5bb 271 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
135 | 134 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (∃𝑖 ∈ (0..^𝑦)[(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
136 | 120, 135 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
137 | 119, 136 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → (([(𝑝 ↾ (0...𝑦)) / 𝑝]𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → [(𝑝 ↾ (0...𝑦)) / 𝑝]∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))) |
138 | 104, 137 | bitrd 267 |
. . . . . . . . . . . . . 14
⊢ ((𝑝 ↾ (0...𝑦)) ∈ V → ([(𝑝 ↾ (0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))))) |
139 | 103, 138 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))))) |
140 | 72, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))))) |
142 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈
ℝ*) |
143 | | simpr2 1061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑝‘0) ≤ 𝑋) |
144 | | xrltnle 9984 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑋 ∈ ℝ*
∧ (𝑝‘𝑦) ∈ ℝ*)
→ (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋)) |
145 | 76, 91, 144 | syl2anr 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 < (𝑝‘𝑦) ↔ ¬ (𝑝‘𝑦) ≤ 𝑋)) |
146 | 145 | exbiri 650 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑋 ∈ ℝ*
∧ (𝑝‘0) ≤
𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → 𝑋 < (𝑝‘𝑦)))) |
147 | 146 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 < (𝑝‘𝑦)))) |
148 | 147 | imp31 447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 < (𝑝‘𝑦)) |
149 | 142, 143,
148 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦))) |
150 | 67, 91 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0) ∈
ℝ* ∧ (𝑝‘𝑦) ∈
ℝ*)) |
151 | 150 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → ((𝑝‘0) ∈ ℝ* ∧
(𝑝‘𝑦) ∈
ℝ*)) |
152 | | elico1 12089 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝‘0) ∈
ℝ* ∧ (𝑝‘𝑦) ∈ ℝ*) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘𝑦)))) |
154 | 149, 153 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1)))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) |
155 | 154 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → ((𝑋 ∈ ℝ* ∧ (𝑝‘0) ≤ 𝑋 ∧ 𝑋 < (𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
156 | 141, 155 | sylbid 229 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)))) |
157 | | 0elfz 12305 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑦 ∈ ℕ0
→ 0 ∈ (0...𝑦)) |
158 | 50, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ℕ → 0 ∈
(0...𝑦)) |
159 | 158 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 0 ∈
(0...𝑦)) |
160 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (0 ∈
(0...𝑦) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0)) |
161 | 159, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘0) = (𝑝‘0)) |
162 | 161 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘0) = ((𝑝 ↾ (0...𝑦))‘0)) |
163 | 87 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → 𝑦 ∈ (0...𝑦)) |
164 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦)) |
165 | 163, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝 ↾ (0...𝑦))‘𝑦) = (𝑝‘𝑦)) |
166 | 165 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑝‘𝑦) = ((𝑝 ↾ (0...𝑦))‘𝑦)) |
167 | 162, 166 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → ((𝑝‘0)[,)(𝑝‘𝑦)) = (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
168 | 167 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) ↔ 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)))) |
169 | 168 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → 𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦))) |
170 | | elfzofz 12354 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑦) → 𝑖 ∈ (0...𝑦)) |
171 | 170 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → 𝑖 ∈ (0...𝑦)) |
172 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖)) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘𝑖) = (𝑝‘𝑖)) |
174 | | fzofzp1 12431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (0..^𝑦) → (𝑖 + 1) ∈ (0...𝑦)) |
175 | 174 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑖 + 1) ∈ (0...𝑦)) |
176 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 + 1) ∈ (0...𝑦) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
177 | 175, 176 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
178 | 177 | adantlr 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → ((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)) = (𝑝‘(𝑖 + 1))) |
179 | 173, 178 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) = ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) |
180 | 179 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) ∧ 𝑖 ∈ (0..^𝑦)) → (𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
181 | 180 | rexbidva 3031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
182 | | nnz 11276 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
183 | | uzid 11578 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
(ℤ≥‘𝑦)) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
(ℤ≥‘𝑦)) |
185 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 ∈
(ℤ≥‘𝑦) → (𝑦 + 1) ∈
(ℤ≥‘𝑦)) |
186 | | fzoss2 12365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 + 1) ∈
(ℤ≥‘𝑦) → (0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
187 | 184, 185,
186 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 ∈ ℕ →
(0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
188 | 187 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (0..^𝑦) ⊆ (0..^(𝑦 + 1))) |
189 | | ssrexv 3630 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((0..^𝑦) ⊆
(0..^(𝑦 + 1)) →
(∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
190 | 188, 189 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
191 | 181, 190 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → (∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
192 | 169, 191 | embantd 57 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ 𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
193 | 192 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
194 | 193 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
195 | 156, 194 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) ∧ ¬ (𝑝‘𝑦) ≤ 𝑋) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
196 | 195 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
197 | 196 | com34 89 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
198 | 197 | com13 86 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘0)[,)((𝑝 ↾ (0...𝑦))‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ (((𝑝 ↾ (0...𝑦))‘𝑖)[,)((𝑝 ↾ (0...𝑦))‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
199 | 139, 198 | sylbi 206 |
. . . . . . . . . . . 12
⊢
([(𝑝 ↾
(0...𝑦)) / 𝑝](𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
200 | 101, 199 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) ∧ ∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
201 | 200 | ex 449 |
. . . . . . . . . 10
⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
202 | 201 | com24 93 |
. . . . . . . . 9
⊢ ((𝑝 ↾ (0...𝑦)) ∈ (RePart‘𝑦) → ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
203 | 100, 202 | mpcom 37 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ 𝑝 ∈ (RePart‘(𝑦 + 1))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
204 | 203 | ex 449 |
. . . . . . 7
⊢ (𝑦 ∈ ℕ → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (∀𝑝 ∈ (RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
205 | 204 | com24 93 |
. . . . . 6
⊢ (𝑦 ∈ ℕ →
(∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))))) |
206 | 205 | imp 444 |
. . . . 5
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (¬ (𝑝‘𝑦) ≤ 𝑋 → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))))) |
207 | 99, 206 | pm2.61d 169 |
. . . 4
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑝 ∈ (RePart‘(𝑦 + 1)) → (𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
208 | 49, 207 | ralrimi 2940 |
. . 3
⊢ ((𝑦 ∈ ℕ ∧
∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |
209 | 208 | ex 449 |
. 2
⊢ (𝑦 ∈ ℕ →
(∀𝑝 ∈
(RePart‘𝑦)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑦)) → ∃𝑖 ∈ (0..^𝑦)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))) → ∀𝑝 ∈ (RePart‘(𝑦 + 1))(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘(𝑦 + 1))) → ∃𝑖 ∈ (0..^(𝑦 + 1))𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))) |
210 | 10, 18, 26, 34, 46, 209 | nnind 10915 |
1
⊢ (𝑀 ∈ ℕ →
∀𝑝 ∈
(RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1))))) |