Metamath Proof Explorer

Theorem iblitg

Description: If a function is integrable, then the S.2 integrals of the function's decompositions all exist. (Contributed by Mario Carneiro, 7-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblitg.1 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
iblitg.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝐾 ) ) ) )
iblitg.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
iblitg.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion iblitg ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 iblitg.1 ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
2 iblitg.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝐾 ) ) ) )
3 iblitg.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 iblitg.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) )
6 2 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝐾 ) ) ) )
7 iexpcyc ⊢ ( 𝐾 ∈ ℤ → ( i ↑ ( 𝐾 mod 4 ) ) = ( i ↑ 𝐾 ) )
8 7 oveq2d ⊢ ( 𝐾 ∈ ℤ → ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) = ( 𝐵 / ( i ↑ 𝐾 ) ) )
9 8 fveq2d ⊢ ( 𝐾 ∈ ℤ → ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝐾 ) ) ) )
10 9 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝐾 ) ) ) )
11 6 10 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑇 = ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) )
12 11 ibllem ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) )
13 12 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝑇 ) , 𝑇 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) )
14 5 13 eqtrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) )
15 14 fveq2d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( ∫2 ‘ 𝐺 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) ) )
16 oveq2 ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( i ↑ 𝑘 ) = ( i ↑ ( 𝐾 mod 4 ) ) )
17 16 oveq2d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( 𝐵 / ( i ↑ 𝑘 ) ) = ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) )
18 17 fveq2d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) )
19 18 breq2d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ↔ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) )
20 19 anbi2d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) ) )
21 20 18 ifbieq1d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) )
22 21 mpteq2dv ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) )
23 22 fveq2d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) ) )
24 23 eleq1d ⊢ ( 𝑘 = ( 𝐾 mod 4 ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) ) ∈ ℝ ) )
25 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
27 25 26 4 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
28 3 27 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
29 28 simprd ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
31 4nn ⊢ 4 ∈ ℕ
32 zmodfz ⊢ ( ( 𝐾 ∈ ℤ ∧ 4 ∈ ℕ ) → ( 𝐾 mod 4 ) ∈ ( 0 ... ( 4 − 1 ) ) )
33 31 32 mpan2 ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 mod 4 ) ∈ ( 0 ... ( 4 − 1 ) ) )
34 4m1e3 ⊢ ( 4 − 1 ) = 3
35 34 oveq2i ⊢ ( 0 ... ( 4 − 1 ) ) = ( 0 ... 3 )
36 33 35 eleqtrdi ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 mod 4 ) ∈ ( 0 ... 3 ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( 𝐾 mod 4 ) ∈ ( 0 ... 3 ) )
38 24 30 37 rspcdva ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ ( 𝐾 mod 4 ) ) ) ) , 0 ) ) ) ∈ ℝ )
39 15 38 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐾 ∈ ℤ ) → ( ∫2 ‘ 𝐺 ) ∈ ℝ )