Metamath Proof Explorer


Theorem itgex

Description: An integral is a set. (Contributed by Mario Carneiro, 28-Jun-2014)

Ref Expression
Assertion itgex 𝐴 𝐵 d 𝑥 ∈ V

Proof

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