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 46189
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 481 . . 3 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ 𝑃 ∈ (RePartβ€˜π‘€))
3 iccpartiun.m . . . . 5 (πœ‘ β†’ 𝑀 ∈ β„•)
4 iccelpart 46186 . . . . 5 (𝑀 ∈ β„• β†’ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
53, 4syl 17 . . . 4 (πœ‘ β†’ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
65adantr 481 . . 3 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))))
7 fveq1 6890 . . . . . . . . 9 (𝑝 = 𝑃 β†’ (π‘β€˜0) = (π‘ƒβ€˜0))
8 fveq1 6890 . . . . . . . . 9 (𝑝 = 𝑃 β†’ (π‘β€˜π‘€) = (π‘ƒβ€˜π‘€))
97, 8oveq12d 7429 . . . . . . . 8 (𝑝 = 𝑃 β†’ ((π‘β€˜0)[,)(π‘β€˜π‘€)) = ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€)))
109eleq2d 2819 . . . . . . 7 (𝑝 = 𝑃 β†’ (𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) ↔ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))))
11 fveq1 6890 . . . . . . . . . 10 (𝑝 = 𝑃 β†’ (π‘β€˜π‘–) = (π‘ƒβ€˜π‘–))
12 fveq1 6890 . . . . . . . . . 10 (𝑝 = 𝑃 β†’ (π‘β€˜(𝑖 + 1)) = (π‘ƒβ€˜(𝑖 + 1)))
1311, 12oveq12d 7429 . . . . . . . . 9 (𝑝 = 𝑃 β†’ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) = ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))))
1413eleq2d 2819 . . . . . . . 8 (𝑝 = 𝑃 β†’ (𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1)))))
1514rexbidv 3178 . . . . . . 7 (𝑝 = 𝑃 β†’ (βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))) ↔ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1)))))
1610, 15imbi12d 344 . . . . . 6 (𝑝 = 𝑃 β†’ ((𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1)))) ↔ (𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))))))
1716rspcva 3610 . . . . 5 ((𝑃 ∈ (RePartβ€˜π‘€) ∧ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ (𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1)))))
1817adantld 491 . . . 4 ((𝑃 ∈ (RePartβ€˜π‘€) ∧ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1)))))
1918com12 32 . . 3 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ ((𝑃 ∈ (RePartβ€˜π‘€) ∧ βˆ€π‘ ∈ (RePartβ€˜π‘€)(𝑋 ∈ ((π‘β€˜0)[,)(π‘β€˜π‘€)) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘β€˜π‘–)[,)(π‘β€˜(𝑖 + 1))))) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1)))))
202, 6, 19mp2and 697 . 2 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))))
213adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑀 ∈ β„•)
221adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑃 ∈ (RePartβ€˜π‘€))
23 elfzofz 13650 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ (0...𝑀))
2423adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0...𝑀))
2521, 22, 24iccpartxr 46172 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘ƒβ€˜π‘–) ∈ ℝ*)
26 fzofzp1 13731 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) β†’ (𝑖 + 1) ∈ (0...𝑀))
2726adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑖 + 1) ∈ (0...𝑀))
2821, 22, 27iccpartxr 46172 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*)
2925, 28jca 512 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘ƒβ€˜π‘–) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*))
3029adantrr 715 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((π‘ƒβ€˜π‘–) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*))
31 elico1 13369 . . . . . . 7 (((π‘ƒβ€˜π‘–) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*) β†’ (𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1)))))
3230, 31syl 17 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1)))))
333adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ 𝑀 ∈ β„•)
341adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ 𝑃 ∈ (RePartβ€˜π‘€))
35 elfzofz 13650 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) β†’ 𝑗 ∈ (0...𝑀))
3635adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ 𝑗 ∈ (0...𝑀))
3733, 34, 36iccpartxr 46172 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ (π‘ƒβ€˜π‘—) ∈ ℝ*)
38 fzofzp1 13731 . . . . . . . . . . 11 (𝑗 ∈ (0..^𝑀) β†’ (𝑗 + 1) ∈ (0...𝑀))
3938adantl 482 . . . . . . . . . 10 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ (𝑗 + 1) ∈ (0...𝑀))
4033, 34, 39iccpartxr 46172 . . . . . . . . 9 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*)
4137, 40jca 512 . . . . . . . 8 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑀)) β†’ ((π‘ƒβ€˜π‘—) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*))
4241adantrl 714 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((π‘ƒβ€˜π‘—) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*))
43 elico1 13369 . . . . . . 7 (((π‘ƒβ€˜π‘—) ∈ ℝ* ∧ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*) β†’ (𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))))
4442, 43syl 17 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1))) ↔ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))))
4532, 44anbi12d 631 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))) ↔ ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))))))
46 elfzoelz 13634 . . . . . . . . . 10 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ β„€)
4746zred 12668 . . . . . . . . 9 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ ℝ)
48 elfzoelz 13634 . . . . . . . . . 10 (𝑗 ∈ (0..^𝑀) β†’ 𝑗 ∈ β„€)
4948zred 12668 . . . . . . . . 9 (𝑗 ∈ (0..^𝑀) β†’ 𝑗 ∈ ℝ)
5047, 49anim12i 613 . . . . . . . 8 ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) β†’ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ))
5150adantl 482 . . . . . . 7 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ))
52 lttri4 11300 . . . . . . 7 ((𝑖 ∈ ℝ ∧ 𝑗 ∈ ℝ) β†’ (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖))
5351, 52syl 17 . . . . . 6 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖))
543, 1icceuelpartlem 46188 . . . . . . . . . 10 (πœ‘ β†’ ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) β†’ (𝑖 < 𝑗 β†’ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—))))
5554imp31 418 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑖 < 𝑗) β†’ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—))
56 simpl 483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ 𝑋 ∈ ℝ*)
5728adantrr 715 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*)
5857adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ*)
5937adantrl 714 . . . . . . . . . . . . . . . . . . . . . . 23 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (π‘ƒβ€˜π‘—) ∈ ℝ*)
6059adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (π‘ƒβ€˜π‘—) ∈ ℝ*)
61 nltle2tri 46106 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜(𝑖 + 1)) ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ∈ ℝ*) β†’ Β¬ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋))
6256, 58, 60, 61syl3anc 1371 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ Β¬ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋))
6362pm2.21d 121 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ ((𝑋 < (π‘ƒβ€˜(𝑖 + 1)) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋) β†’ 𝑖 = 𝑗))
64633expd 1353 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ ((π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) β†’ ((π‘ƒβ€˜π‘—) ≀ 𝑋 β†’ 𝑖 = 𝑗))))
6564ex 413 . . . . . . . . . . . . . . . . . 18 (𝑋 ∈ ℝ* β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ ((π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) β†’ ((π‘ƒβ€˜π‘—) ≀ 𝑋 β†’ 𝑖 = 𝑗)))))
6665com23 86 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ℝ* β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) β†’ ((π‘ƒβ€˜π‘—) ≀ 𝑋 β†’ 𝑖 = 𝑗)))))
6766com25 99 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℝ* β†’ ((π‘ƒβ€˜π‘—) ≀ 𝑋 β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ 𝑖 = 𝑗)))))
6867imp4b 422 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ 𝑖 = 𝑗)))
6968com23 86 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ 𝑖 = 𝑗)))
70693adant3 1132 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ 𝑖 = 𝑗)))
7170com12 32 . . . . . . . . . . . 12 (𝑋 < (π‘ƒβ€˜(𝑖 + 1)) β†’ ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ 𝑖 = 𝑗)))
72713ad2ant3 1135 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) β†’ ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ 𝑖 = 𝑗)))
7372imp 407 . . . . . . . . . 10 (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ 𝑖 = 𝑗))
7473com12 32 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑖 + 1)) ≀ (π‘ƒβ€˜π‘—)) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
7555, 74syldan 591 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑖 < 𝑗) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
7675expcom 414 . . . . . . 7 (𝑖 < 𝑗 β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗)))
77 2a1 28 . . . . . . 7 (𝑖 = 𝑗 β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗)))
783, 1icceuelpartlem 46188 . . . . . . . . . . 11 (πœ‘ β†’ ((𝑗 ∈ (0..^𝑀) ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑗 < 𝑖 β†’ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–))))
7978ancomsd 466 . . . . . . . . . 10 (πœ‘ β†’ ((𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)) β†’ (𝑗 < 𝑖 β†’ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–))))
8079imp31 418 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑗 < 𝑖) β†’ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–))
8140adantrl 714 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*)
8281adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ*)
8325adantrr 715 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (π‘ƒβ€˜π‘–) ∈ ℝ*)
8483adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (π‘ƒβ€˜π‘–) ∈ ℝ*)
85 nltle2tri 46106 . . . . . . . . . . . . . . . . . . . . 21 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜(𝑗 + 1)) ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ∈ ℝ*) β†’ Β¬ (𝑋 < (π‘ƒβ€˜(𝑗 + 1)) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋))
8656, 82, 84, 85syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ Β¬ (𝑋 < (π‘ƒβ€˜(𝑗 + 1)) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋))
8786pm2.21d 121 . . . . . . . . . . . . . . . . . . 19 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ ((𝑋 < (π‘ƒβ€˜(𝑗 + 1)) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋) β†’ 𝑖 = 𝑗))
88873expd 1353 . . . . . . . . . . . . . . . . . 18 ((𝑋 ∈ ℝ* ∧ (πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀)))) β†’ (𝑋 < (π‘ƒβ€˜(𝑗 + 1)) β†’ ((π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ 𝑖 = 𝑗))))
8988ex 413 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ℝ* β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (𝑋 < (π‘ƒβ€˜(𝑗 + 1)) β†’ ((π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ 𝑖 = 𝑗)))))
9089com23 86 . . . . . . . . . . . . . . . 16 (𝑋 ∈ ℝ* β†’ (𝑋 < (π‘ƒβ€˜(𝑗 + 1)) β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ 𝑖 = 𝑗)))))
9190imp4b 422 . . . . . . . . . . . . . . 15 ((𝑋 ∈ ℝ* ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ 𝑖 = 𝑗)))
9291com23 86 . . . . . . . . . . . . . 14 ((𝑋 ∈ ℝ* ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ 𝑖 = 𝑗)))
93923adant2 1131 . . . . . . . . . . . . 13 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ 𝑖 = 𝑗)))
9493com12 32 . . . . . . . . . . . 12 ((π‘ƒβ€˜π‘–) ≀ 𝑋 β†’ ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ 𝑖 = 𝑗)))
95943ad2ant2 1134 . . . . . . . . . . 11 ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) β†’ ((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ 𝑖 = 𝑗)))
9695imp 407 . . . . . . . . . 10 (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ 𝑖 = 𝑗))
9796com12 32 . . . . . . . . 9 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ (π‘ƒβ€˜(𝑗 + 1)) ≀ (π‘ƒβ€˜π‘–)) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
9880, 97syldan 591 . . . . . . . 8 (((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) ∧ 𝑗 < 𝑖) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
9998expcom 414 . . . . . . 7 (𝑗 < 𝑖 β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗)))
10076, 77, 993jaoi 1427 . . . . . 6 ((𝑖 < 𝑗 ∨ 𝑖 = 𝑗 ∨ 𝑗 < 𝑖) β†’ ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗)))
10153, 100mpcom 38 . . . . 5 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ (((𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘–) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑖 + 1))) ∧ (𝑋 ∈ ℝ* ∧ (π‘ƒβ€˜π‘—) ≀ 𝑋 ∧ 𝑋 < (π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
10245, 101sylbid 239 . . . 4 ((πœ‘ ∧ (𝑖 ∈ (0..^𝑀) ∧ 𝑗 ∈ (0..^𝑀))) β†’ ((𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
103102ralrimivva 3200 . . 3 (πœ‘ β†’ βˆ€π‘– ∈ (0..^𝑀)βˆ€π‘— ∈ (0..^𝑀)((𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
104103adantr 481 . 2 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ βˆ€π‘– ∈ (0..^𝑀)βˆ€π‘— ∈ (0..^𝑀)((𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗))
105 fveq2 6891 . . . . 5 (𝑖 = 𝑗 β†’ (π‘ƒβ€˜π‘–) = (π‘ƒβ€˜π‘—))
106 fvoveq1 7434 . . . . 5 (𝑖 = 𝑗 β†’ (π‘ƒβ€˜(𝑖 + 1)) = (π‘ƒβ€˜(𝑗 + 1)))
107105, 106oveq12d 7429 . . . 4 (𝑖 = 𝑗 β†’ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) = ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1))))
108107eleq2d 2819 . . 3 (𝑖 = 𝑗 β†’ (𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ↔ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))))
109108reu4 3727 . 2 (βˆƒ!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ↔ (βˆƒπ‘– ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ βˆ€π‘– ∈ (0..^𝑀)βˆ€π‘— ∈ (0..^𝑀)((𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))) ∧ 𝑋 ∈ ((π‘ƒβ€˜π‘—)[,)(π‘ƒβ€˜(𝑗 + 1)))) β†’ 𝑖 = 𝑗)))
11020, 104, 109sylanbrc 583 1 ((πœ‘ ∧ 𝑋 ∈ ((π‘ƒβ€˜0)[,)(π‘ƒβ€˜π‘€))) β†’ βˆƒ!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((π‘ƒβ€˜π‘–)[,)(π‘ƒβ€˜(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  βˆƒwrex 3070  βˆƒ!wreu 3374   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7411  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115  β„*cxr 11249   < clt 11250   ≀ cle 11251  β„•cn 12214  [,)cico 13328  ...cfz 13486  ..^cfzo 13629  RePartciccp 46166
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-n0 12475  df-z 12561  df-uz 12825  df-ico 13332  df-fz 13487  df-fzo 13630  df-iccp 46167
This theorem is referenced by:  iccpartdisj  46190
  Copyright terms: Public domain W3C validator