Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  icceuelpart Structured version   Visualization version   GIF version

Theorem icceuelpart 43795
Description: An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.)
Hypotheses
Ref Expression
iccpartiun.m (𝜑𝑀 ∈ ℕ)
iccpartiun.p (𝜑𝑃 ∈ (RePart‘𝑀))
Assertion
Ref Expression
icceuelpart ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))))
Distinct variable groups:   𝑖,𝑀   𝑃,𝑖   𝑖,𝑋   𝜑,𝑖

Proof of Theorem icceuelpart
Dummy variables 𝑗 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iccpartiun.p . . . 4 (𝜑𝑃 ∈ (RePart‘𝑀))
21adantr 484 . . 3 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → 𝑃 ∈ (RePart‘𝑀))
3 iccpartiun.m . . . . 5 (𝜑𝑀 ∈ ℕ)
4 iccelpart 43792 . . . . 5 (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
53, 4syl 17 . . . 4 (𝜑 → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
65adantr 484 . . 3 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))))
7 fveq1 6650 . . . . . . . . 9 (𝑝 = 𝑃 → (𝑝‘0) = (𝑃‘0))
8 fveq1 6650 . . . . . . . . 9 (𝑝 = 𝑃 → (𝑝𝑀) = (𝑃𝑀))
97, 8oveq12d 7156 . . . . . . . 8 (𝑝 = 𝑃 → ((𝑝‘0)[,)(𝑝𝑀)) = ((𝑃‘0)[,)(𝑃𝑀)))
109eleq2d 2901 . . . . . . 7 (𝑝 = 𝑃 → (𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) ↔ 𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))))
11 fveq1 6650 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝𝑖) = (𝑃𝑖))
12 fveq1 6650 . . . . . . . . . 10 (𝑝 = 𝑃 → (𝑝‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
1311, 12oveq12d 7156 . . . . . . . . 9 (𝑝 = 𝑃 → ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) = ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))))
1413eleq2d 2901 . . . . . . . 8 (𝑝 = 𝑃 → (𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1)))))
1514rexbidv 3289 . . . . . . 7 (𝑝 = 𝑃 → (∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1)))))
1610, 15imbi12d 348 . . . . . 6 (𝑝 = 𝑃 → ((𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1)))) ↔ (𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))))))
1716rspcva 3606 . . . . 5 ((𝑃 ∈ (RePart‘𝑀) ∧ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → (𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1)))))
1817adantld 494 . . . 4 ((𝑃 ∈ (RePart‘𝑀) ∧ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1)))))
1918com12 32 . . 3 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ((𝑃 ∈ (RePart‘𝑀) ∧ ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝𝑖)[,)(𝑝‘(𝑖 + 1))))) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1)))))
202, 6, 19mp2and 698 . 2 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))))
213adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑀 ∈ ℕ)
221adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑃 ∈ (RePart‘𝑀))
23 elfzofz 13046 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2423adantl 485 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
2521, 22, 24iccpartxr 43778 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑃𝑖) ∈ ℝ*)
26 fzofzp1 13127 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
2726adantl 485 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
2821, 22, 27iccpartxr 43778 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
2925, 28jca 515 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*))
3029adantrr 716 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*))
31 elico1 12767 . . . . . . 7 (((𝑃𝑖) ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ*) → (𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1)))))
3230, 31syl 17 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1)))))
333adantr 484 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑀 ∈ ℕ)
341adantr 484 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑃 ∈ (RePart‘𝑀))
35 elfzofz 13046 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ (0...𝑀))
3635adantl 485 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑀)) → 𝑗 ∈ (0...𝑀))
3733, 34, 36iccpartxr 43778 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑃𝑗) ∈ ℝ*)
38 fzofzp1 13127 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) → (𝑗 + 1) ∈ (0...𝑀))
3938adantl 485 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑗 + 1) ∈ (0...𝑀))
4033, 34, 39iccpartxr 43778 . . . . . . . . 9 ((𝜑𝑗 ∈ (0..^𝑀)) → (𝑃‘(𝑗 + 1)) ∈ ℝ*)
4137, 40jca 515 . . . . . . . 8 ((𝜑𝑗 ∈ (0..^𝑀)) → ((𝑃𝑗) ∈ ℝ* ∧ (𝑃‘(𝑗 + 1)) ∈ ℝ*))
4241adantrl 715 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑃𝑗) ∈ ℝ* ∧ (𝑃‘(𝑗 + 1)) ∈ ℝ*))
43 elico1 12767 . . . . . . 7 (((𝑃𝑗) ∈ ℝ* ∧ (𝑃‘(𝑗 + 1)) ∈ ℝ*) → (𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))))
4442, 43syl 17 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))))
4532, 44anbi12d 633 . . . . 5 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))) ↔ ((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))))))
46 elfzoelz 13031 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
4746zred 12073 . . . . . . . . 9 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
48 elfzoelz 13031 . . . . . . . . . 10 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℤ)
4948zred 12073 . . . . . . . . 9 (𝑗 ∈ (0..^𝑀) → 𝑗 ∈ ℝ)
5047, 49anim12i 615 . . . . . . . 8 ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) → (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ))
5150adantl 485 . . . . . . 7 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ))
52 lttri4 10710 . . . . . . 7 ((𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ) → (𝑖 < 𝑗𝑖 = 𝑗𝑗 < 𝑖))
5351, 52syl 17 . . . . . 6 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑖 < 𝑗𝑖 = 𝑗𝑗 < 𝑖))
543, 1icceuelpartlem 43794 . . . . . . . . . 10 (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) → (𝑖 < 𝑗 → (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗))))
5554imp31 421 . . . . . . . . 9 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑖 < 𝑗) → (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗))
56 simpl 486 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → 𝑋 ∈ ℝ*)
5728adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
5857adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑃‘(𝑖 + 1)) ∈ ℝ*)
5937adantrl 715 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑃𝑗) ∈ ℝ*)
6059adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑃𝑗) ∈ ℝ*)
61 nltle2tri 43712 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (𝑃‘(𝑖 + 1)) ∈ ℝ* ∧ (𝑃𝑗) ∈ ℝ*) → ¬ (𝑋 < (𝑃‘(𝑖 + 1)) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) ∧ (𝑃𝑗) ≤ 𝑋))
6256, 58, 60, 61syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → ¬ (𝑋 < (𝑃‘(𝑖 + 1)) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) ∧ (𝑃𝑗) ≤ 𝑋))
6362pm2.21d 121 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → ((𝑋 < (𝑃‘(𝑖 + 1)) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) ∧ (𝑃𝑗) ≤ 𝑋) → 𝑖 = 𝑗))
64633expd 1350 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑋 < (𝑃‘(𝑖 + 1)) → ((𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) → ((𝑃𝑗) ≤ 𝑋𝑖 = 𝑗))))
6564ex 416 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ ℝ* → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑋 < (𝑃‘(𝑖 + 1)) → ((𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) → ((𝑃𝑗) ≤ 𝑋𝑖 = 𝑗)))))
6665com23 86 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ℝ* → (𝑋 < (𝑃‘(𝑖 + 1)) → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) → ((𝑃𝑗) ≤ 𝑋𝑖 = 𝑗)))))
6766com25 99 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℝ* → ((𝑃𝑗) ≤ 𝑋 → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗) → (𝑋 < (𝑃‘(𝑖 + 1)) → 𝑖 = 𝑗)))))
6867imp4b 425 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → (𝑋 < (𝑃‘(𝑖 + 1)) → 𝑖 = 𝑗)))
6968com23 86 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋) → (𝑋 < (𝑃‘(𝑖 + 1)) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → 𝑖 = 𝑗)))
70693adant3 1129 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → (𝑋 < (𝑃‘(𝑖 + 1)) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → 𝑖 = 𝑗)))
7170com12 32 . . . . . . . . . . . 12 (𝑋 < (𝑃‘(𝑖 + 1)) → ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → 𝑖 = 𝑗)))
72713ad2ant3 1132 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → 𝑖 = 𝑗)))
7372imp 410 . . . . . . . . . 10 (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → 𝑖 = 𝑗))
7473com12 32 . . . . . . . . 9 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑖 + 1)) ≤ (𝑃𝑗)) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
7555, 74syldan 594 . . . . . . . 8 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑖 < 𝑗) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
7675expcom 417 . . . . . . 7 (𝑖 < 𝑗 → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗)))
77 2a1 28 . . . . . . 7 (𝑖 = 𝑗 → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗)))
783, 1icceuelpartlem 43794 . . . . . . . . . . 11 (𝜑 → ((𝑗 ∈ (0..^𝑀) ∧ 𝑖 ∈ (0..^𝑀)) → (𝑗 < 𝑖 → (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖))))
7978ancomsd 469 . . . . . . . . . 10 (𝜑 → ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) → (𝑗 < 𝑖 → (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖))))
8079imp31 421 . . . . . . . . 9 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑗 < 𝑖) → (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖))
8140adantrl 715 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑃‘(𝑗 + 1)) ∈ ℝ*)
8281adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑃‘(𝑗 + 1)) ∈ ℝ*)
8325adantrr 716 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑃𝑖) ∈ ℝ*)
8483adantl 485 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑃𝑖) ∈ ℝ*)
85 nltle2tri 43712 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (𝑃‘(𝑗 + 1)) ∈ ℝ* ∧ (𝑃𝑖) ∈ ℝ*) → ¬ (𝑋 < (𝑃‘(𝑗 + 1)) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) ∧ (𝑃𝑖) ≤ 𝑋))
8656, 82, 84, 85syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → ¬ (𝑋 < (𝑃‘(𝑗 + 1)) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) ∧ (𝑃𝑖) ≤ 𝑋))
8786pm2.21d 121 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → ((𝑋 < (𝑃‘(𝑗 + 1)) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) ∧ (𝑃𝑖) ≤ 𝑋) → 𝑖 = 𝑗))
88873expd 1350 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ (𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) → (𝑋 < (𝑃‘(𝑗 + 1)) → ((𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) → ((𝑃𝑖) ≤ 𝑋𝑖 = 𝑗))))
8988ex 416 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ℝ* → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (𝑋 < (𝑃‘(𝑗 + 1)) → ((𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) → ((𝑃𝑖) ≤ 𝑋𝑖 = 𝑗)))))
9089com23 86 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℝ* → (𝑋 < (𝑃‘(𝑗 + 1)) → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖) → ((𝑃𝑖) ≤ 𝑋𝑖 = 𝑗)))))
9190imp4b 425 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ*𝑋 < (𝑃‘(𝑗 + 1))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → ((𝑃𝑖) ≤ 𝑋𝑖 = 𝑗)))
9291com23 86 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ*𝑋 < (𝑃‘(𝑗 + 1))) → ((𝑃𝑖) ≤ 𝑋 → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → 𝑖 = 𝑗)))
93923adant2 1128 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → ((𝑃𝑖) ≤ 𝑋 → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → 𝑖 = 𝑗)))
9493com12 32 . . . . . . . . . . . 12 ((𝑃𝑖) ≤ 𝑋 → ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → 𝑖 = 𝑗)))
95943ad2ant2 1131 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) → ((𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → 𝑖 = 𝑗)))
9695imp 410 . . . . . . . . . 10 (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → 𝑖 = 𝑗))
9796com12 32 . . . . . . . . 9 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (𝑃‘(𝑗 + 1)) ≤ (𝑃𝑖)) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
9880, 97syldan 594 . . . . . . . 8 (((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑗 < 𝑖) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
9998expcom 417 . . . . . . 7 (𝑗 < 𝑖 → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗)))
10076, 77, 993jaoi 1424 . . . . . 6 ((𝑖 < 𝑗𝑖 = 𝑗𝑗 < 𝑖) → ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗)))
10153, 100mpcom 38 . . . . 5 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → (((𝑋 ∈ ℝ* ∧ (𝑃𝑖) ≤ 𝑋𝑋 < (𝑃‘(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (𝑃𝑗) ≤ 𝑋𝑋 < (𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
10245, 101sylbid 243 . . . 4 ((𝜑 ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) → ((𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
103102ralrimivva 3185 . . 3 (𝜑 → ∀𝑖 ∈ (0..^𝑀)∀𝑗 ∈ (0..^𝑀)((𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
104103adantr 484 . 2 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∀𝑖 ∈ (0..^𝑀)∀𝑗 ∈ (0..^𝑀)((𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗))
105 fveq2 6651 . . . . 5 (𝑖 = 𝑗 → (𝑃𝑖) = (𝑃𝑗))
106 fvoveq1 7161 . . . . 5 (𝑖 = 𝑗 → (𝑃‘(𝑖 + 1)) = (𝑃‘(𝑗 + 1)))
107105, 106oveq12d 7156 . . . 4 (𝑖 = 𝑗 → ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) = ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1))))
108107eleq2d 2901 . . 3 (𝑖 = 𝑗 → (𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))))
109108reu4 3707 . 2 (∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ↔ (∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ ∀𝑖 ∈ (0..^𝑀)∀𝑗 ∈ (0..^𝑀)((𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))) ∧ 𝑋 ∈ ((𝑃𝑗)[,)(𝑃‘(𝑗 + 1)))) → 𝑖 = 𝑗)))
11020, 104, 109sylanbrc 586 1 ((𝜑𝑋 ∈ ((𝑃‘0)[,)(𝑃𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃𝑖)[,)(𝑃‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3o 1083  w3a 1084   = wceq 1538  wcel 2115  wral 3132  wrex 3133  ∃!wreu 3134   class class class wbr 5047  cfv 6336  (class class class)co 7138  cr 10521  0cc0 10522  1c1 10523   + caddc 10525  *cxr 10659   < clt 10660  cle 10661  cn 11623  [,)cico 12726  ...cfz 12883  ..^cfzo 13026  RePartciccp 43772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444  ax-cnex 10578  ax-resscn 10579  ax-1cn 10580  ax-icn 10581  ax-addcl 10582  ax-addrcl 10583  ax-mulcl 10584  ax-mulrcl 10585  ax-mulcom 10586  ax-addass 10587  ax-mulass 10588  ax-distr 10589  ax-i2m1 10590  ax-1ne0 10591  ax-1rid 10592  ax-rnegex 10593  ax-rrecex 10594  ax-cnre 10595  ax-pre-lttri 10596  ax-pre-lttrn 10597  ax-pre-ltadd 10598  ax-pre-mulgt0 10599
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-reu 3139  df-rmo 3140  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-pss 3937  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-tr 5154  df-id 5441  df-eprel 5446  df-po 5455  df-so 5456  df-fr 5495  df-we 5497  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-mpo 7143  df-om 7564  df-1st 7672  df-2nd 7673  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-er 8272  df-map 8391  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10662  df-mnf 10663  df-xr 10664  df-ltxr 10665  df-le 10666  df-sub 10857  df-neg 10858  df-nn 11624  df-2 11686  df-n0 11884  df-z 11968  df-uz 12230  df-ico 12730  df-fz 12884  df-fzo 13027  df-iccp 43773
This theorem is referenced by:  iccpartdisj  43796
  Copyright terms: Public domain W3C validator