Step | Hyp | Ref
| Expression |
1 | | iblitg.1 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0))) |
3 | | iblitg.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝐾)))) |
4 | 3 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℤ) ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑𝐾)))) |
5 | | iexpcyc 12831 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ →
(i↑(𝐾 mod 4)) =
(i↑𝐾)) |
6 | 5 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → (𝐵 / (i↑(𝐾 mod 4))) = (𝐵 / (i↑𝐾))) |
7 | 6 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝐾 ∈ ℤ →
(ℜ‘(𝐵 /
(i↑(𝐾 mod 4)))) =
(ℜ‘(𝐵 /
(i↑𝐾)))) |
8 | 7 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐾 ∈ ℤ) ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))) = (ℜ‘(𝐵 / (i↑𝐾)))) |
9 | 4, 8 | eqtr4d 2647 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐾 ∈ ℤ) ∧ 𝑥 ∈ 𝐴) → 𝑇 = (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))) |
10 | 9 | ibllem 23337 |
. . . . 5
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0)) |
11 | 10 | mpteq2dv 4673 |
. . . 4
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇), 𝑇, 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) |
12 | 2, 11 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → 𝐺 = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) |
13 | 12 | fveq2d 6107 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) →
(∫2‘𝐺)
= (∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0)))) |
14 | | 4nn 11064 |
. . . . . 6
⊢ 4 ∈
ℕ |
15 | | zmodfz 12554 |
. . . . . 6
⊢ ((𝐾 ∈ ℤ ∧ 4 ∈
ℕ) → (𝐾 mod 4)
∈ (0...(4 − 1))) |
16 | 14, 15 | mpan2 703 |
. . . . 5
⊢ (𝐾 ∈ ℤ → (𝐾 mod 4) ∈ (0...(4 −
1))) |
17 | | 4cn 10975 |
. . . . . . 7
⊢ 4 ∈
ℂ |
18 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
19 | | 3cn 10972 |
. . . . . . 7
⊢ 3 ∈
ℂ |
20 | 18, 19 | addcomi 10106 |
. . . . . . . 8
⊢ (1 + 3) =
(3 + 1) |
21 | | df-4 10958 |
. . . . . . . 8
⊢ 4 = (3 +
1) |
22 | 20, 21 | eqtr4i 2635 |
. . . . . . 7
⊢ (1 + 3) =
4 |
23 | 17, 18, 19, 22 | subaddrii 10249 |
. . . . . 6
⊢ (4
− 1) = 3 |
24 | 23 | oveq2i 6560 |
. . . . 5
⊢ (0...(4
− 1)) = (0...3) |
25 | 16, 24 | syl6eleq 2698 |
. . . 4
⊢ (𝐾 ∈ ℤ → (𝐾 mod 4) ∈
(0...3)) |
26 | 25 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → (𝐾 mod 4) ∈ (0...3)) |
27 | | iblitg.3 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈
𝐿1) |
28 | | eqidd 2611 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) |
29 | | eqidd 2611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑𝑘)))) |
30 | | iblitg.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
31 | 28, 29, 30 | isibl2 23339 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ 𝐿1 ↔
((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ))) |
32 | 27, 31 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ MblFn ∧ ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ)) |
33 | 32 | simprd 478 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
34 | 33 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) → ∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ) |
35 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝐾 mod 4) → (i↑𝑘) = (i↑(𝐾 mod 4))) |
36 | 35 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝐾 mod 4) → (𝐵 / (i↑𝑘)) = (𝐵 / (i↑(𝐾 mod 4)))) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑘 = (𝐾 mod 4) → (ℜ‘(𝐵 / (i↑𝑘))) = (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))) |
38 | 37 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑘 = (𝐾 mod 4) → (0 ≤ (ℜ‘(𝐵 / (i↑𝑘))) ↔ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))))) |
39 | 38 | anbi2d 736 |
. . . . . . . 8
⊢ (𝑘 = (𝐾 mod 4) → ((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))) ↔ (𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))))) |
40 | 39, 37 | ifbieq1d 4059 |
. . . . . . 7
⊢ (𝑘 = (𝐾 mod 4) → if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0) = if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0)) |
41 | 40 | mpteq2dv 4673 |
. . . . . 6
⊢ (𝑘 = (𝐾 mod 4) → (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0)) = (𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) |
42 | 41 | fveq2d 6107 |
. . . . 5
⊢ (𝑘 = (𝐾 mod 4) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) = (∫2‘(𝑥 ∈ ℝ ↦
if((𝑥 ∈ 𝐴 ∧ 0 ≤
(ℜ‘(𝐵 /
(i↑(𝐾 mod 4))))),
(ℜ‘(𝐵 /
(i↑(𝐾 mod 4)))),
0)))) |
43 | 42 | eleq1d 2672 |
. . . 4
⊢ (𝑘 = (𝐾 mod 4) →
((∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ ↔
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) ∈
ℝ)) |
44 | 43 | rspcv 3278 |
. . 3
⊢ ((𝐾 mod 4) ∈ (0...3) →
(∀𝑘 ∈
(0...3)(∫2‘(𝑥 ∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑𝑘)))), (ℜ‘(𝐵 / (i↑𝑘))), 0))) ∈ ℝ →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) ∈
ℝ)) |
45 | 26, 34, 44 | sylc 63 |
. 2
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) →
(∫2‘(𝑥
∈ ℝ ↦ if((𝑥 ∈ 𝐴 ∧ 0 ≤ (ℜ‘(𝐵 / (i↑(𝐾 mod 4))))), (ℜ‘(𝐵 / (i↑(𝐾 mod 4)))), 0))) ∈
ℝ) |
46 | 13, 45 | eqeltrd 2688 |
1
⊢ ((𝜑 ∧ 𝐾 ∈ ℤ) →
(∫2‘𝐺)
∈ ℝ) |