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 46401
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 6892 . . 3 (π‘₯ = 1 β†’ (RePartβ€˜π‘₯) = (RePartβ€˜1))
2 fveq2 6892 . . . . . 6 (π‘₯ = 1 β†’ (π‘β€˜π‘₯) = (π‘β€˜1))
32oveq2d 7428 . . . . 5 (π‘₯ = 1 β†’ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) = ((π‘β€˜0)[,)(π‘β€˜1)))
43eleq2d 2818 . . . 4 (π‘₯ = 1 β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1))))
5 oveq2 7420 . . . . . 6 (π‘₯ = 1 β†’ (0..^π‘₯) = (0..^1))
6 fzo01 13719 . . . . . 6 (0..^1) = {0}
75, 6eqtrdi 2787 . . . . 5 (π‘₯ = 1 β†’ (0..^π‘₯) = {0})
87rexeqdv 3325 . . . 4 (π‘₯ = 1 β†’ (βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
94, 8imbi12d 343 . . 3 (π‘₯ = 1 β†’ ((𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1)) β†’ βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
101, 9raleqbidv 3341 . 2 (π‘₯ = 1 β†’ (βˆ€π‘ ∈ (RePartβ€˜π‘₯)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ βˆ€π‘ ∈ (RePartβ€˜1)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1)) β†’ βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
11 fveq2 6892 . . 3 (π‘₯ = 𝑦 β†’ (RePartβ€˜π‘₯) = (RePartβ€˜π‘¦))
12 fveq2 6892 . . . . . 6 (π‘₯ = 𝑦 β†’ (π‘β€˜π‘₯) = (π‘β€˜π‘¦))
1312oveq2d 7428 . . . . 5 (π‘₯ = 𝑦 β†’ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) = ((π‘β€˜0)[,)(π‘β€˜π‘¦)))
1413eleq2d 2818 . . . 4 (π‘₯ = 𝑦 β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))))
15 oveq2 7420 . . . . 5 (π‘₯ = 𝑦 β†’ (0..^π‘₯) = (0..^𝑦))
1615rexeqdv 3325 . . . 4 (π‘₯ = 𝑦 β†’ (βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
1714, 16imbi12d 343 . . 3 (π‘₯ = 𝑦 β†’ ((𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
1811, 17raleqbidv 3341 . 2 (π‘₯ = 𝑦 β†’ (βˆ€π‘ ∈ (RePartβ€˜π‘₯)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
19 fveq2 6892 . . 3 (π‘₯ = (𝑦 + 1) β†’ (RePartβ€˜π‘₯) = (RePartβ€˜(𝑦 + 1)))
20 fveq2 6892 . . . . . 6 (π‘₯ = (𝑦 + 1) β†’ (π‘β€˜π‘₯) = (π‘β€˜(𝑦 + 1)))
2120oveq2d 7428 . . . . 5 (π‘₯ = (𝑦 + 1) β†’ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) = ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))
2221eleq2d 2818 . . . 4 (π‘₯ = (𝑦 + 1) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1)))))
23 oveq2 7420 . . . . 5 (π‘₯ = (𝑦 + 1) β†’ (0..^π‘₯) = (0..^(𝑦 + 1)))
2423rexeqdv 3325 . . . 4 (π‘₯ = (𝑦 + 1) β†’ (βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
2522, 24imbi12d 343 . . 3 (π‘₯ = (𝑦 + 1) β†’ ((𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
2619, 25raleqbidv 3341 . 2 (π‘₯ = (𝑦 + 1) β†’ (βˆ€π‘ ∈ (RePartβ€˜π‘₯)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ βˆ€π‘ ∈ (RePartβ€˜(𝑦 + 1))(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
27 fveq2 6892 . . 3 (π‘₯ = 𝑀 β†’ (RePartβ€˜π‘₯) = (RePartβ€˜π‘€))
28 fveq2 6892 . . . . . 6 (π‘₯ = 𝑀 β†’ (π‘β€˜π‘₯) = (π‘β€˜π‘€))
2928oveq2d 7428 . . . . 5 (π‘₯ = 𝑀 β†’ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) = ((π‘β€˜0)[,)(π‘β€˜π‘€)))
3029eleq2d 2818 . . . 4 (π‘₯ = 𝑀 β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€))))
31 oveq2 7420 . . . . 5 (π‘₯ = 𝑀 β†’ (0..^π‘₯) = (0..^𝑀))
3231rexeqdv 3325 . . . 4 (π‘₯ = 𝑀 β†’ (βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
3330, 32imbi12d 343 . . 3 (π‘₯ = 𝑀 β†’ ((𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
3427, 33raleqbidv 3341 . 2 (π‘₯ = 𝑀 β†’ (βˆ€π‘ ∈ (RePartβ€˜π‘₯)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘₯)) β†’ βˆƒπ‘– ∈ (0..^π‘₯)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
35 0nn0 12492 . . . . 5 0 ∈ β„•0
36 fveq2 6892 . . . . . . . 8 (𝑖 = 0 β†’ (π‘β€˜π‘–) = (π‘β€˜0))
37 fv0p1e1 12340 . . . . . . . 8 (𝑖 = 0 β†’ (π‘β€˜(𝑖 + 1)) = (π‘β€˜1))
3836, 37oveq12d 7430 . . . . . . 7 (𝑖 = 0 β†’ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) = ((π‘β€˜0)[,)(π‘β€˜1)))
3938eleq2d 2818 . . . . . 6 (𝑖 = 0 β†’ (𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1))))
4039rexsng 4679 . . . . 5 (0 ∈ β„•0 β†’ (βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1))))
4135, 40ax-mp 5 . . . 4 (βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1)))
4241biimpri 227 . . 3 (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1)) β†’ βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
4342rgenw 3064 . 2 βˆ€π‘ ∈ (RePartβ€˜1)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜1)) β†’ βˆƒπ‘– ∈ {0}𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
44 nfv 1916 . . . . 5 Ⅎ𝑝 𝑦 ∈ β„•
45 nfra1 3280 . . . . 5 β„²π‘βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
4644, 45nfan 1901 . . . 4 Ⅎ𝑝(𝑦 ∈ β„• ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
47 nnnn0 12484 . . . . . . . . . 10 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„•0)
48 fzonn0p1 13714 . . . . . . . . . 10 (𝑦 ∈ β„•0 β†’ 𝑦 ∈ (0..^(𝑦 + 1)))
4947, 48syl 17 . . . . . . . . 9 (𝑦 ∈ β„• β†’ 𝑦 ∈ (0..^(𝑦 + 1)))
5049ad2antrr 723 . . . . . . . 8 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ 𝑦 ∈ (0..^(𝑦 + 1)))
51 fveq2 6892 . . . . . . . . . . 11 (𝑖 = 𝑦 β†’ (π‘β€˜π‘–) = (π‘β€˜π‘¦))
52 fvoveq1 7435 . . . . . . . . . . 11 (𝑖 = 𝑦 β†’ (π‘β€˜(𝑖 + 1)) = (π‘β€˜(𝑦 + 1)))
5351, 52oveq12d 7430 . . . . . . . . . 10 (𝑖 = 𝑦 β†’ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) = ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1))))
5453eleq2d 2818 . . . . . . . . 9 (𝑖 = 𝑦 β†’ (𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1)))))
5554adantl 481 . . . . . . . 8 ((((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) ∧ 𝑖 = 𝑦) β†’ (𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1)))))
56 peano2nn 12229 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„•)
5756adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑦 + 1) ∈ β„•)
58 simpr 484 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ 𝑝 ∈ (RePartβ€˜(𝑦 + 1)))
5956nnnn0d 12537 . . . . . . . . . . . . . . . . 17 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ β„•0)
60 0elfz 13603 . . . . . . . . . . . . . . . . 17 ((𝑦 + 1) ∈ β„•0 β†’ 0 ∈ (0...(𝑦 + 1)))
6159, 60syl 17 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ 0 ∈ (0...(𝑦 + 1)))
6261adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ 0 ∈ (0...(𝑦 + 1)))
6357, 58, 62iccpartxr 46387 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (π‘β€˜0) ∈ ℝ*)
64 nn0fz0 13604 . . . . . . . . . . . . . . . . 17 ((𝑦 + 1) ∈ β„•0 ↔ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6559, 64sylib 217 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„• β†’ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6665adantr 480 . . . . . . . . . . . . . . 15 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑦 + 1) ∈ (0...(𝑦 + 1)))
6757, 58, 66iccpartxr 46387 . . . . . . . . . . . . . 14 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (π‘β€˜(𝑦 + 1)) ∈ ℝ*)
6863, 67jca 511 . . . . . . . . . . . . 13 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*))
6968adantlr 712 . . . . . . . . . . . 12 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*))
70 elico1 13372 . . . . . . . . . . . 12 (((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
7169, 70syl 17 . . . . . . . . . . 11 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
72 simp1 1135 . . . . . . . . . . . . . . . 16 ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ 𝑋 ∈ ℝ*)
7372adantl 481 . . . . . . . . . . . . . . 15 (((π‘β€˜π‘¦) ≀ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ 𝑋 ∈ ℝ*)
74 simpl 482 . . . . . . . . . . . . . . 15 (((π‘β€˜π‘¦) ≀ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (π‘β€˜π‘¦) ≀ 𝑋)
75 simpr3 1195 . . . . . . . . . . . . . . 15 (((π‘β€˜π‘¦) ≀ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ 𝑋 < (π‘β€˜(𝑦 + 1)))
7673, 74, 753jca 1127 . . . . . . . . . . . . . 14 (((π‘β€˜π‘¦) ≀ 𝑋 ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))))
7776ex 412 . . . . . . . . . . . . 13 ((π‘β€˜π‘¦) ≀ 𝑋 β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
7877adantl 481 . . . . . . . . . . . 12 ((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
7978adantr 480 . . . . . . . . . . 11 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
8071, 79sylbid 239 . . . . . . . . . 10 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
8180impr 454 . . . . . . . . 9 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))))
82 nn0fz0 13604 . . . . . . . . . . . . . . . 16 (𝑦 ∈ β„•0 ↔ 𝑦 ∈ (0...𝑦))
8347, 82sylib 217 . . . . . . . . . . . . . . 15 (𝑦 ∈ β„• β†’ 𝑦 ∈ (0...𝑦))
84 fzelp1 13558 . . . . . . . . . . . . . . 15 (𝑦 ∈ (0...𝑦) β†’ 𝑦 ∈ (0...(𝑦 + 1)))
8583, 84syl 17 . . . . . . . . . . . . . 14 (𝑦 ∈ β„• β†’ 𝑦 ∈ (0...(𝑦 + 1)))
8685adantr 480 . . . . . . . . . . . . 13 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ 𝑦 ∈ (0...(𝑦 + 1)))
8757, 58, 86iccpartxr 46387 . . . . . . . . . . . 12 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (π‘β€˜π‘¦) ∈ ℝ*)
8887, 67jca 511 . . . . . . . . . . 11 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((π‘β€˜π‘¦) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*))
8988ad2ant2r 744 . . . . . . . . . 10 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ ((π‘β€˜π‘¦) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*))
90 elico1 13372 . . . . . . . . . 10 (((π‘β€˜π‘¦) ∈ ℝ* ∧ (π‘β€˜(𝑦 + 1)) ∈ ℝ*) β†’ (𝑋 ∈ ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
9189, 90syl 17 . . . . . . . . 9 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ (𝑋 ∈ ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
9281, 91mpbird 256 . . . . . . . 8 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ 𝑋 ∈ ((π‘β€˜π‘¦)[,)(π‘β€˜(𝑦 + 1))))
9350, 55, 92rspcedvd 3615 . . . . . . 7 (((𝑦 ∈ β„• ∧ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
9493exp43 436 . . . . . 6 (𝑦 ∈ β„• β†’ ((π‘β€˜π‘¦) ≀ 𝑋 β†’ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))))
9594adantr 480 . . . . 5 ((𝑦 ∈ β„• ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ ((π‘β€˜π‘¦) ≀ 𝑋 β†’ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))))
96 iccpartres 46386 . . . . . . . . 9 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑝 β†Ύ (0...𝑦)) ∈ (RePartβ€˜π‘¦))
97 rspsbca 3875 . . . . . . . . . . . 12 (((𝑝 β†Ύ (0...𝑦)) ∈ (RePartβ€˜π‘¦) ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ [(𝑝 β†Ύ (0...𝑦)) / 𝑝](𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
98 vex 3477 . . . . . . . . . . . . . . 15 𝑝 ∈ V
9998resex 6030 . . . . . . . . . . . . . 14 (𝑝 β†Ύ (0...𝑦)) ∈ V
100 sbcimg 3829 . . . . . . . . . . . . . . 15 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ([(𝑝 β†Ύ (0...𝑦)) / 𝑝](𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ [(𝑝 β†Ύ (0...𝑦)) / 𝑝]βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
101 sbcel2 4416 . . . . . . . . . . . . . . . . 17 ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ 𝑋 ∈ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜0)[,)(π‘β€˜π‘¦)))
102 csbov12g 7456 . . . . . . . . . . . . . . . . . . 19 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜0)[,)(π‘β€˜π‘¦)) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜0)[,)⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘¦)))
103 csbfv12 6940 . . . . . . . . . . . . . . . . . . . . 21 ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜0) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ0)
104 csbvarg 4432 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘ = (𝑝 β†Ύ (0...𝑦)))
105 csbconstg 3913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ0 = 0)
106104, 105fveq12d 6899 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ0) = ((𝑝 β†Ύ (0...𝑦))β€˜0))
107103, 106eqtrid 2783 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜0) = ((𝑝 β†Ύ (0...𝑦))β€˜0))
108 csbfv12 6940 . . . . . . . . . . . . . . . . . . . . 21 ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘¦) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘¦)
109 csbconstg 3913 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘¦ = 𝑦)
110104, 109fveq12d 6899 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘¦) = ((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))
111108, 110eqtrid 2783 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘¦) = ((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))
112107, 111oveq12d 7430 . . . . . . . . . . . . . . . . . . 19 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜0)[,)⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘¦)) = (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)))
113102, 112eqtrd 2771 . . . . . . . . . . . . . . . . . 18 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜0)[,)(π‘β€˜π‘¦)) = (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)))
114113eleq2d 2818 . . . . . . . . . . . . . . . . 17 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (𝑋 ∈ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))))
115101, 114bitrid 282 . . . . . . . . . . . . . . . 16 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))))
116 sbcrex 3870 . . . . . . . . . . . . . . . . 17 ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑦)[(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
117 sbcel2 4416 . . . . . . . . . . . . . . . . . . 19 ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
118 csbov12g 7456 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘–)[,)⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜(𝑖 + 1))))
119 csbfv12 6940 . . . . . . . . . . . . . . . . . . . . . . 23 ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘–) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘–)
120 csbconstg 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘– = 𝑖)
121104, 120fveq12d 6899 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘–) = ((𝑝 β†Ύ (0...𝑦))β€˜π‘–))
122119, 121eqtrid 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘–) = ((𝑝 β†Ύ (0...𝑦))β€˜π‘–))
123 csbfv12 6940 . . . . . . . . . . . . . . . . . . . . . . 23 ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜(𝑖 + 1)) = (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(𝑖 + 1))
124 csbconstg 3913 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(𝑖 + 1) = (𝑖 + 1))
125104, 124fveq12d 6899 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œπ‘β€˜β¦‹(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(𝑖 + 1)) = ((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))
126123, 125eqtrid 2783 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜(𝑖 + 1)) = ((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))
127122, 126oveq12d 7430 . . . . . . . . . . . . . . . . . . . . 21 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜π‘–)[,)⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ(π‘β€˜(𝑖 + 1))) = (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))))
128118, 127eqtrd 2771 . . . . . . . . . . . . . . . . . . . 20 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) = (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))))
129128eleq2d 2818 . . . . . . . . . . . . . . . . . . 19 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (𝑋 ∈ ⦋(𝑝 β†Ύ (0...𝑦)) / π‘β¦Œ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))))
130117, 129bitrid 282 . . . . . . . . . . . . . . . . . 18 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))))
131130rexbidv 3177 . . . . . . . . . . . . . . . . 17 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (βˆƒπ‘– ∈ (0..^𝑦)[(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))))
132116, 131bitrid 282 . . . . . . . . . . . . . . . 16 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ ([(𝑝 β†Ύ (0...𝑦)) / 𝑝]βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))))
133115, 132imbi12d 343 . . . . . . . . . . . . . . 15 ((𝑝 β†Ύ (0...𝑦)) ∈ V β†’ (([(𝑝 β†Ύ (0...𝑦)) / 𝑝]𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ [(𝑝 β†Ύ (0...𝑦)) / 𝑝]βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))))))
134100, 133bitrd 278 . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))))
13872adantl 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ 𝑋 ∈ ℝ*)
139 simpr2 1194 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (π‘β€˜0) ≀ 𝑋)
140 xrltnle 11286 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑋 ∈ ℝ* ∧ (π‘β€˜π‘¦) ∈ ℝ*) β†’ (𝑋 < (π‘β€˜π‘¦) ↔ Β¬ (π‘β€˜π‘¦) ≀ 𝑋))
14172, 87, 140syl2anr 596 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (𝑋 < (π‘β€˜π‘¦) ↔ Β¬ (π‘β€˜π‘¦) ≀ 𝑋))
142141exbiri 808 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ (Β¬ (π‘β€˜π‘¦) ≀ 𝑋 β†’ 𝑋 < (π‘β€˜π‘¦))))
143142com23 86 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (Β¬ (π‘β€˜π‘¦) ≀ 𝑋 β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ 𝑋 < (π‘β€˜π‘¦))))
144143imp31 417 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ 𝑋 < (π‘β€˜π‘¦))
145138, 139, 1443jca 1127 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜π‘¦)))
14663, 87jca 511 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜π‘¦) ∈ ℝ*))
147146ad2antrr 723 . . . . . . . . . . . . . . . . . . . . 21 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ ((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜π‘¦) ∈ ℝ*))
148 elico1 13372 . . . . . . . . . . . . . . . . . . . . 21 (((π‘β€˜0) ∈ ℝ* ∧ (π‘β€˜π‘¦) ∈ ℝ*) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜π‘¦))))
149147, 148syl 17 . . . . . . . . . . . . . . . . . . . 20 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜π‘¦))))
150145, 149mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) ∧ (𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1)))) β†’ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)))
151150ex 412 . . . . . . . . . . . . . . . . . 18 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) β†’ ((𝑋 ∈ ℝ* ∧ (π‘β€˜0) ≀ 𝑋 ∧ 𝑋 < (π‘β€˜(𝑦 + 1))) β†’ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))))
152137, 151sylbid 239 . . . . . . . . . . . . . . . . 17 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ Β¬ (π‘β€˜π‘¦) ≀ 𝑋) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))))
153 0elfz 13603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦 ∈ β„•0 β†’ 0 ∈ (0...𝑦))
15447, 153syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 ∈ β„• β†’ 0 ∈ (0...𝑦))
155154adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ 0 ∈ (0...𝑦))
156 fvres 6911 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ∈ (0...𝑦) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜0) = (π‘β€˜0))
157155, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜0) = (π‘β€˜0))
158157eqcomd 2737 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (π‘β€˜0) = ((𝑝 β†Ύ (0...𝑦))β€˜0))
15983adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ 𝑦 ∈ (0...𝑦))
160 fvres 6911 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ (0...𝑦) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜π‘¦) = (π‘β€˜π‘¦))
161159, 160syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜π‘¦) = (π‘β€˜π‘¦))
162161eqcomd 2737 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (π‘β€˜π‘¦) = ((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))
163158, 162oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) = (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)))
164163eleq2d 2818 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) ↔ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦))))
165164biimpa 476 . . . . . . . . . . . . . . . . . . . 20 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) β†’ 𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)))
166 elfzofz 13653 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑖 ∈ (0..^𝑦) β†’ 𝑖 ∈ (0...𝑦))
167166adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ 𝑖 ∈ (0...𝑦))
168 fvres 6911 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 ∈ (0...𝑦) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜π‘–) = (π‘β€˜π‘–))
169167, 168syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜π‘–) = (π‘β€˜π‘–))
170 fzofzp1 13734 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑖 ∈ (0..^𝑦) β†’ (𝑖 + 1) ∈ (0...𝑦))
171170adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑖 + 1) ∈ (0...𝑦))
172 fvres 6911 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑖 + 1) ∈ (0...𝑦) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)) = (π‘β€˜(𝑖 + 1)))
173171, 172syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)) = (π‘β€˜(𝑖 + 1)))
174173adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ ((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)) = (π‘β€˜(𝑖 + 1)))
175169, 174oveq12d 7430 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))) = ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))
176175eleq2d 2818 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) ∧ 𝑖 ∈ (0..^𝑦)) β†’ (𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
177176rexbidva 3175 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) β†’ (βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
178 nnz 12584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ β„• β†’ 𝑦 ∈ β„€)
179 uzid 12842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 ∈ β„€ β†’ 𝑦 ∈ (β„€β‰₯β€˜π‘¦))
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ β„• β†’ 𝑦 ∈ (β„€β‰₯β€˜π‘¦))
181 peano2uz 12890 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (β„€β‰₯β€˜π‘¦) β†’ (𝑦 + 1) ∈ (β„€β‰₯β€˜π‘¦))
182 fzoss2 13665 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 + 1) ∈ (β„€β‰₯β€˜π‘¦) β†’ (0..^𝑦) βŠ† (0..^(𝑦 + 1)))
183180, 181, 1823syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 ∈ β„• β†’ (0..^𝑦) βŠ† (0..^(𝑦 + 1)))
184183ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) β†’ (0..^𝑦) βŠ† (0..^(𝑦 + 1)))
185 ssrexv 4052 . . . . . . . . . . . . . . . . . . . . . 22 ((0..^𝑦) βŠ† (0..^(𝑦 + 1)) β†’ (βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
186184, 185syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) ∧ 𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦))) β†’ (βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
187177, 186sylbid 239 . . . . . . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ β„• ∧ 𝑝 ∈ (RePartβ€˜(𝑦 + 1))) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ ((𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜0)[,)((𝑝 β†Ύ (0...𝑦))β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ (((𝑝 β†Ύ (0...𝑦))β€˜π‘–)[,)((𝑝 β†Ύ (0...𝑦))β€˜(𝑖 + 1)))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
190189adantr 480 . . . . . . . . . . . . . . . . 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 412 . . . . . . . . . . . . . . 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 216 . . . . . . . . . . . 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 412 . . . . . . . . . 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 412 . . . . . . 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 406 . . . . 5 ((𝑦 ∈ β„• ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ (Β¬ (π‘β€˜π‘¦) ≀ 𝑋 β†’ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))))
20395, 202pm2.61d 179 . . . 4 ((𝑦 ∈ β„• ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ (𝑝 ∈ (RePartβ€˜(𝑦 + 1)) β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
20446, 203ralrimi 3253 . . 3 ((𝑦 ∈ β„• ∧ βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ βˆ€π‘ ∈ (RePartβ€˜(𝑦 + 1))(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
205204ex 412 . 2 (𝑦 ∈ β„• β†’ (βˆ€π‘ ∈ (RePartβ€˜π‘¦)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘¦)) β†’ βˆƒπ‘– ∈ (0..^𝑦)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) β†’ βˆ€π‘ ∈ (RePartβ€˜(𝑦 + 1))(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜(𝑦 + 1))) β†’ βˆƒπ‘– ∈ (0..^(𝑦 + 1))𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))))
20610, 18, 26, 34, 43, 205nnind 12235 1 (𝑀 ∈ β„• β†’ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473  [wsbc 3778  β¦‹csb 3894   βŠ† wss 3949  {csn 4629   class class class wbr 5149   β†Ύ cres 5679  β€˜cfv 6544  (class class class)co 7412  0cc0 11113  1c1 11114   + caddc 11116  β„*cxr 11252   < clt 11253   ≀ cle 11254  β„•cn 12217  β„•0cn0 12477  β„€cz 12563  β„€β‰₯cuz 12827  [,)cico 13331  ...cfz 13489  ..^cfzo 13632  RePartciccp 46381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-er 8706  df-map 8825  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-nn 12218  df-n0 12478  df-z 12564  df-uz 12828  df-ico 13335  df-fz 13490  df-fzo 13633  df-iccp 46382
This theorem is referenced by:  iccpartiun  46402  icceuelpart  46404  bgoldbtbnd  46777
  Copyright terms: Public domain W3C validator