Detailed syntax breakdown of Definition df-itg
| Step | Hyp | Ref
| Expression |
| 1 | | vx |
. . 3
setvar 𝑥 |
| 2 | | cA |
. . 3
class 𝐴 |
| 3 | | cB |
. . 3
class 𝐵 |
| 4 | 1, 2, 3 | citg 25653 |
. 2
class
∫𝐴𝐵 d𝑥 |
| 5 | | cc0 11155 |
. . . 4
class
0 |
| 6 | | c3 12322 |
. . . 4
class
3 |
| 7 | | cfz 13547 |
. . . 4
class
... |
| 8 | 5, 6, 7 | co 7431 |
. . 3
class
(0...3) |
| 9 | | ci 11157 |
. . . . 5
class
i |
| 10 | | vk |
. . . . . 6
setvar 𝑘 |
| 11 | 10 | cv 1539 |
. . . . 5
class 𝑘 |
| 12 | | cexp 14102 |
. . . . 5
class
↑ |
| 13 | 9, 11, 12 | co 7431 |
. . . 4
class
(i↑𝑘) |
| 14 | | cr 11154 |
. . . . . 6
class
ℝ |
| 15 | | vy |
. . . . . . 7
setvar 𝑦 |
| 16 | | cdiv 11920 |
. . . . . . . . 9
class
/ |
| 17 | 3, 13, 16 | co 7431 |
. . . . . . . 8
class (𝐵 / (i↑𝑘)) |
| 18 | | cre 15136 |
. . . . . . . 8
class
ℜ |
| 19 | 17, 18 | cfv 6561 |
. . . . . . 7
class
(ℜ‘(𝐵 /
(i↑𝑘))) |
| 20 | 1 | cv 1539 |
. . . . . . . . . 10
class 𝑥 |
| 21 | 20, 2 | wcel 2108 |
. . . . . . . . 9
wff 𝑥 ∈ 𝐴 |
| 22 | 15 | cv 1539 |
. . . . . . . . . 10
class 𝑦 |
| 23 | | cle 11296 |
. . . . . . . . . 10
class
≤ |
| 24 | 5, 22, 23 | wbr 5143 |
. . . . . . . . 9
wff 0 ≤
𝑦 |
| 25 | 21, 24 | wa 395 |
. . . . . . . 8
wff (𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦) |
| 26 | 25, 22, 5 | cif 4525 |
. . . . . . 7
class if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0) |
| 27 | 15, 19, 26 | csb 3899 |
. . . . . 6
class
⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0) |
| 28 | 1, 14, 27 | cmpt 5225 |
. . . . 5
class (𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)) |
| 29 | | citg2 25651 |
. . . . 5
class
∫2 |
| 30 | 28, 29 | cfv 6561 |
. . . 4
class
(∫2‘(𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0))) |
| 31 | | cmul 11160 |
. . . 4
class
· |
| 32 | 13, 30, 31 | co 7431 |
. . 3
class
((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))) |
| 33 | 8, 32, 10 | csu 15722 |
. 2
class
Σ𝑘 ∈
(0...3)((i↑𝑘) ·
(∫2‘(𝑥
∈ ℝ ↦ ⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))) |
| 34 | 4, 33 | wceq 1540 |
1
wff ∫𝐴𝐵 d𝑥 = Σ𝑘 ∈ (0...3)((i↑𝑘) · (∫2‘(𝑥 ∈ ℝ ↦
⦋(ℜ‘(𝐵 / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑦), 𝑦, 0)))) |