Metamath Proof Explorer

Theorem iblcnlem1

Description: Lemma for iblcnlem . (Contributed by Mario Carneiro, 6-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses itgcnlem.r ⊢ 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.s ⊢ 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.t ⊢ 𝑇 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem.u ⊢ 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
itgcnlem1.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
Assertion iblcnlem1 ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )

Proof

Step Hyp Ref Expression
1 itgcnlem.r ⊢ 𝑅 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
2 itgcnlem.s ⊢ 𝑆 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
3 itgcnlem.t ⊢ 𝑇 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
4 itgcnlem.u ⊢ 𝑈 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
5 itgcnlem1.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
7 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
8 6 7 5 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
9 c0ex ⊢ 0 ∈ V
10 1ex ⊢ 1 ∈ V
11 ax-icn ⊢ i ∈ ℂ
12 exp0 ⊢ ( i ∈ ℂ → ( i ↑ 0 ) = 1 )
13 11 12 ax-mp ⊢ ( i ↑ 0 ) = 1
14 13 itgvallem ⊢ ( 𝑘 = 0 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) )
15 14 eleq1d ⊢ ( 𝑘 = 0 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ∈ ℝ ) )
16 exp1 ⊢ ( i ∈ ℂ → ( i ↑ 1 ) = i )
17 11 16 ax-mp ⊢ ( i ↑ 1 ) = i
18 17 itgvallem ⊢ ( 𝑘 = 1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) )
19 18 eleq1d ⊢ ( 𝑘 = 1 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ∈ ℝ ) )
20 9 10 15 19 ralpr ⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ∈ ℝ ) )
21 5 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 / 1 ) = 𝐵 )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 / 1 ) ) = ( ℜ ‘ 𝐵 ) )
23 22 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) )
24 23 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
25 24 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) )
26 25 1 eqtr4di ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) = 𝑅 )
27 26 eleq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ∈ ℝ ↔ 𝑅 ∈ ℝ ) )
28 imval ⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / i ) ) )
29 5 28 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / i ) ) )
30 29 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) )
31 30 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) )
32 31 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) )
33 3 32 eqtr2id ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) = 𝑇 )
34 33 eleq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ∈ ℝ ↔ 𝑇 ∈ ℝ ) )
35 27 34 anbi12d ⊢ ( 𝜑 → ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / 1 ) ) ) , ( ℜ ‘ ( 𝐵 / 1 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / i ) ) ) , ( ℜ ‘ ( 𝐵 / i ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( 𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ ) ) )
36 20 35 bitrid ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 0 , 1 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( 𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ ) ) )
37 2ex ⊢ 2 ∈ V
38 3ex ⊢ 3 ∈ V
39 i2 ⊢ ( i ↑ 2 ) = - 1
40 39 itgvallem ⊢ ( 𝑘 = 2 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) )
41 40 eleq1d ⊢ ( 𝑘 = 2 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ∈ ℝ ) )
42 i3 ⊢ ( i ↑ 3 ) = - i
43 42 itgvallem ⊢ ( 𝑘 = 3 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) )
44 43 eleq1d ⊢ ( 𝑘 = 3 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ∈ ℝ ) )
45 37 38 41 44 ralpr ⊢ ( ∀ 𝑘 ∈ { 2 , 3 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ∈ ℝ ) )
46 5 renegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ - 𝐵 ) = - ( ℜ ‘ 𝐵 ) )
47 ax-1cn ⊢ 1 ∈ ℂ
48 47 negnegi ⊢ - - 1 = 1
49 48 oveq2i ⊢ ( - 𝐵 / - - 1 ) = ( - 𝐵 / 1 )
50 5 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 ∈ ℂ )
51 50 div1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / 1 ) = - 𝐵 )
52 49 51 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - 1 ) = - 𝐵 )
53 47 negcli ⊢ - 1 ∈ ℂ
54 neg1ne0 ⊢ - 1 ≠ 0
55 div2neg ⊢ ( ( 𝐵 ∈ ℂ ∧ - 1 ∈ ℂ ∧ - 1 ≠ 0 ) → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
56 53 54 55 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
57 5 56 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - 1 ) = ( 𝐵 / - 1 ) )
58 52 57 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 = ( 𝐵 / - 1 ) )
59 58 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ - 𝐵 ) = ( ℜ ‘ ( 𝐵 / - 1 ) ) )
60 46 59 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / - 1 ) ) )
61 60 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) )
62 61 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) )
63 62 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) )
64 2 63 eqtr2id ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) = 𝑆 )
65 64 eleq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ∈ ℝ ↔ 𝑆 ∈ ℝ ) )
66 imval ⊢ ( - 𝐵 ∈ ℂ → ( ℑ ‘ - 𝐵 ) = ( ℜ ‘ ( - 𝐵 / i ) ) )
67 50 66 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ - 𝐵 ) = ( ℜ ‘ ( - 𝐵 / i ) ) )
68 5 imnegd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ - 𝐵 ) = - ( ℑ ‘ 𝐵 ) )
69 11 negnegi ⊢ - - i = i
70 69 eqcomi ⊢ i = - - i
71 70 oveq2i ⊢ ( - 𝐵 / i ) = ( - 𝐵 / - - i )
72 11 negcli ⊢ - i ∈ ℂ
73 ine0 ⊢ i ≠ 0
74 11 73 negne0i ⊢ - i ≠ 0
75 div2neg ⊢ ( ( 𝐵 ∈ ℂ ∧ - i ∈ ℂ ∧ - i ≠ 0 ) → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
76 72 74 75 mp3an23 ⊢ ( 𝐵 ∈ ℂ → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
77 5 76 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / - - i ) = ( 𝐵 / - i ) )
78 71 77 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 𝐵 / i ) = ( 𝐵 / - i ) )
79 78 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( - 𝐵 / i ) ) = ( ℜ ‘ ( 𝐵 / - i ) ) )
80 67 68 79 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐵 ) = ( ℜ ‘ ( 𝐵 / - i ) ) )
81 80 ibllem ⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) )
82 81 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) )
83 82 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) )
84 4 83 eqtr2id ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) = 𝑈 )
85 84 eleq1d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ∈ ℝ ↔ 𝑈 ∈ ℝ ) )
86 65 85 anbi12d ⊢ ( 𝜑 → ( ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - 1 ) ) ) , ( ℜ ‘ ( 𝐵 / - 1 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / - i ) ) ) , ( ℜ ‘ ( 𝐵 / - i ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) )
87 45 86 bitrid ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ { 2 , 3 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) )
88 36 87 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑘 ∈ { 0 , 1 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ { 2 , 3 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ ) ∧ ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )
89 fz0to3un2pr ⊢ ( 0 ... 3 ) = ( { 0 , 1 } ∪ { 2 , 3 } )
90 89 raleqi ⊢ ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
91 ralunb ⊢ ( ∀ 𝑘 ∈ ( { 0 , 1 } ∪ { 2 , 3 } ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∀ 𝑘 ∈ { 0 , 1 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ { 2 , 3 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
92 90 91 bitri ⊢ ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ∀ 𝑘 ∈ { 0 , 1 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ { 2 , 3 } ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) )
93 an4 ⊢ ( ( ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ↔ ( ( 𝑅 ∈ ℝ ∧ 𝑇 ∈ ℝ ) ∧ ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) )
94 88 92 93 3bitr4g ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ↔ ( ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )
95 94 anbi2d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) ) )
96 3anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )
97 95 96 bitr4di ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )
98 8 97 bitrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( 𝑅 ∈ ℝ ∧ 𝑆 ∈ ℝ ) ∧ ( 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ) ) )