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 = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
itgcnlem.s 
|- S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
itgcnlem.t 
|- T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
itgcnlem.u 
|- U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
itgcnlem1.v 
|- ( ( ph /\ x e. A ) -> B e. CC )
Assertion iblcnlem1 
|- ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )

Proof

Step Hyp Ref Expression
1 itgcnlem.r 
 |-  R = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
2 itgcnlem.s 
 |-  S = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
3 itgcnlem.t 
 |-  T = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
4 itgcnlem.u 
 |-  U = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
5 itgcnlem1.v 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
7 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
8 6 7 5 isibl2 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
9 c0ex 
 |-  0 e. _V
10 1ex 
 |-  1 e. _V
11 ax-icn 
 |-  _i e. CC
12 exp0 
 |-  ( _i e. CC -> ( _i ^ 0 ) = 1 )
13 11 12 ax-mp 
 |-  ( _i ^ 0 ) = 1
14 13 itgvallem 
 |-  ( k = 0 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) )
15 14 eleq1d 
 |-  ( k = 0 -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) e. RR ) )
16 exp1 
 |-  ( _i e. CC -> ( _i ^ 1 ) = _i )
17 11 16 ax-mp 
 |-  ( _i ^ 1 ) = _i
18 17 itgvallem 
 |-  ( k = 1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) )
19 18 eleq1d 
 |-  ( k = 1 -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) e. RR ) )
20 9 10 15 19 ralpr 
 |-  ( A. k e. { 0 , 1 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) e. RR ) )
21 5 div1d 
 |-  ( ( ph /\ x e. A ) -> ( B / 1 ) = B )
22 21 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / 1 ) ) = ( Re ` B ) )
23 22 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) )
24 23 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
25 24 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) )
26 25 1 eqtr4di 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) = R )
27 26 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) e. RR <-> R e. RR ) )
28 imval 
 |-  ( B e. CC -> ( Im ` B ) = ( Re ` ( B / _i ) ) )
29 5 28 syl 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) = ( Re ` ( B / _i ) ) )
30 29 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) )
31 30 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) )
32 31 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) )
33 3 32 eqtr2id 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) = T )
34 33 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) e. RR <-> T e. RR ) )
35 27 34 anbi12d 
 |-  ( ph -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / 1 ) ) ) , ( Re ` ( B / 1 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / _i ) ) ) , ( Re ` ( B / _i ) ) , 0 ) ) ) e. RR ) <-> ( R e. RR /\ T e. RR ) ) )
36 20 35 syl5bb 
 |-  ( ph -> ( A. k e. { 0 , 1 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( R e. RR /\ T e. RR ) ) )
37 2ex 
 |-  2 e. _V
38 3ex 
 |-  3 e. _V
39 i2 
 |-  ( _i ^ 2 ) = -u 1
40 39 itgvallem 
 |-  ( k = 2 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) )
41 40 eleq1d 
 |-  ( k = 2 -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) e. RR ) )
42 i3 
 |-  ( _i ^ 3 ) = -u _i
43 42 itgvallem 
 |-  ( k = 3 -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) )
44 43 eleq1d 
 |-  ( k = 3 -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) e. RR ) )
45 37 38 41 44 ralpr 
 |-  ( A. k e. { 2 , 3 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) e. RR ) )
46 5 renegd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = -u ( Re ` B ) )
47 ax-1cn 
 |-  1 e. CC
48 47 negnegi 
 |-  -u -u 1 = 1
49 48 oveq2i 
 |-  ( -u B / -u -u 1 ) = ( -u B / 1 )
50 5 negcld 
 |-  ( ( ph /\ x e. A ) -> -u B e. CC )
51 50 div1d 
 |-  ( ( ph /\ x e. A ) -> ( -u B / 1 ) = -u B )
52 49 51 eqtrid 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u 1 ) = -u B )
53 47 negcli 
 |-  -u 1 e. CC
54 neg1ne0 
 |-  -u 1 =/= 0
55 div2neg 
 |-  ( ( B e. CC /\ -u 1 e. CC /\ -u 1 =/= 0 ) -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
56 53 54 55 mp3an23 
 |-  ( B e. CC -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
57 5 56 syl 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u 1 ) = ( B / -u 1 ) )
58 52 57 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u B = ( B / -u 1 ) )
59 58 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` -u B ) = ( Re ` ( B / -u 1 ) ) )
60 46 59 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) = ( Re ` ( B / -u 1 ) ) )
61 60 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) )
62 61 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) )
63 62 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) )
64 2 63 eqtr2id 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) = S )
65 64 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) e. RR <-> S e. RR ) )
66 imval 
 |-  ( -u B e. CC -> ( Im ` -u B ) = ( Re ` ( -u B / _i ) ) )
67 50 66 syl 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = ( Re ` ( -u B / _i ) ) )
68 5 imnegd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` -u B ) = -u ( Im ` B ) )
69 11 negnegi 
 |-  -u -u _i = _i
70 69 eqcomi 
 |-  _i = -u -u _i
71 70 oveq2i 
 |-  ( -u B / _i ) = ( -u B / -u -u _i )
72 11 negcli 
 |-  -u _i e. CC
73 ine0 
 |-  _i =/= 0
74 11 73 negne0i 
 |-  -u _i =/= 0
75 div2neg 
 |-  ( ( B e. CC /\ -u _i e. CC /\ -u _i =/= 0 ) -> ( -u B / -u -u _i ) = ( B / -u _i ) )
76 72 74 75 mp3an23 
 |-  ( B e. CC -> ( -u B / -u -u _i ) = ( B / -u _i ) )
77 5 76 syl 
 |-  ( ( ph /\ x e. A ) -> ( -u B / -u -u _i ) = ( B / -u _i ) )
78 71 77 eqtrid 
 |-  ( ( ph /\ x e. A ) -> ( -u B / _i ) = ( B / -u _i ) )
79 78 fveq2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( -u B / _i ) ) = ( Re ` ( B / -u _i ) ) )
80 67 68 79 3eqtr3d 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) = ( Re ` ( B / -u _i ) ) )
81 80 ibllem 
 |-  ( ph -> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) )
82 81 mpteq2dv 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) )
83 82 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) )
84 4 83 eqtr2id 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) = U )
85 84 eleq1d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) e. RR <-> U e. RR ) )
86 65 85 anbi12d 
 |-  ( ph -> ( ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u 1 ) ) ) , ( Re ` ( B / -u 1 ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / -u _i ) ) ) , ( Re ` ( B / -u _i ) ) , 0 ) ) ) e. RR ) <-> ( S e. RR /\ U e. RR ) ) )
87 45 86 syl5bb 
 |-  ( ph -> ( A. k e. { 2 , 3 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( S e. RR /\ U e. RR ) ) )
88 36 87 anbi12d 
 |-  ( ph -> ( ( A. k e. { 0 , 1 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR /\ A. k e. { 2 , 3 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) <-> ( ( R e. RR /\ T e. RR ) /\ ( S e. RR /\ U e. RR ) ) ) )
89 fz0to3un2pr 
 |-  ( 0 ... 3 ) = ( { 0 , 1 } u. { 2 , 3 } )
90 89 raleqi 
 |-  ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
91 ralunb 
 |-  ( A. k e. ( { 0 , 1 } u. { 2 , 3 } ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( A. k e. { 0 , 1 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR /\ A. k e. { 2 , 3 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) )
92 90 91 bitri 
 |-  ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( A. k e. { 0 , 1 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR /\ A. k e. { 2 , 3 } ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) )
93 an4 
 |-  ( ( ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) <-> ( ( R e. RR /\ T e. RR ) /\ ( S e. RR /\ U e. RR ) ) )
94 88 92 93 3bitr4g 
 |-  ( ph -> ( A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR <-> ( ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
95 94 anbi2d 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) ) )
96 3anass 
 |-  ( ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
97 95 96 bitr4di 
 |-  ( ph -> ( ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )
98 8 97 bitrd 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( R e. RR /\ S e. RR ) /\ ( T e. RR /\ U e. RR ) ) ) )