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 |