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 ⊢R=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
itgcnlem.s ⊢S=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
itgcnlem.t ⊢T=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
itgcnlem.u ⊢U=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
itgcnlem1.v ⊢φ∧x∈A→B∈ℂ
Assertion iblcnlem1 ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼B∈MblFn∧R∈ℝ∧S∈ℝ∧T∈ℝ∧U∈ℝ

Proof

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