Step |
Hyp |
Ref |
Expression |
1 |
|
nfitg.1 |
⊢ Ⅎ 𝑦 𝐴 |
2 |
|
nfitg.2 |
⊢ Ⅎ 𝑦 𝐵 |
3 |
|
eqid |
⊢ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) |
4 |
3
|
dfitg |
⊢ ∫ 𝐴 𝐵 d 𝑥 = Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) |
5 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 0 ... 3 ) |
6 |
|
nfcv |
⊢ Ⅎ 𝑦 ( i ↑ 𝑘 ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑦 · |
8 |
|
nfcv |
⊢ Ⅎ 𝑦 ∫2 |
9 |
|
nfcv |
⊢ Ⅎ 𝑦 ℝ |
10 |
1
|
nfcri |
⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴 |
11 |
|
nfcv |
⊢ Ⅎ 𝑦 0 |
12 |
|
nfcv |
⊢ Ⅎ 𝑦 ≤ |
13 |
|
nfcv |
⊢ Ⅎ 𝑦 ℜ |
14 |
|
nfcv |
⊢ Ⅎ 𝑦 / |
15 |
2 14 6
|
nfov |
⊢ Ⅎ 𝑦 ( 𝐵 / ( i ↑ 𝑘 ) ) |
16 |
13 15
|
nffv |
⊢ Ⅎ 𝑦 ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) |
17 |
11 12 16
|
nfbr |
⊢ Ⅎ 𝑦 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) |
18 |
10 17
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) |
19 |
18 16 11
|
nfif |
⊢ Ⅎ 𝑦 if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) |
20 |
9 19
|
nfmpt |
⊢ Ⅎ 𝑦 ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) |
21 |
8 20
|
nffv |
⊢ Ⅎ 𝑦 ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) |
22 |
6 7 21
|
nfov |
⊢ Ⅎ 𝑦 ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) |
23 |
5 22
|
nfsum |
⊢ Ⅎ 𝑦 Σ 𝑘 ∈ ( 0 ... 3 ) ( ( i ↑ 𝑘 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ) |
24 |
4 23
|
nfcxfr |
⊢ Ⅎ 𝑦 ∫ 𝐴 𝐵 d 𝑥 |