Description: An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | itgex | ⊢ ∫ 𝐴 𝐵 d 𝑥 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-itg | ⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) | |
2 | sumex | ⊢ Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ) ∈ V | |
3 | 1 2 | eqeltri | ⊢ ∫ 𝐴 𝐵 d 𝑥 ∈ V |