This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem10

Description: Condition on the bounds of a nonempty subinterval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem10.1 
|- ( ph -> A e. RR )
fourierdlem10.2 
|- ( ph -> B e. RR )
fourierdlem10.3 
|- ( ph -> C e. RR )
fourierdlem10.4 
|- ( ph -> D e. RR )
fourierdlem10.5 
|- ( ph -> C < D )
fourierdlem10.6 
|- ( ph -> ( C (,) D ) C_ ( A (,) B ) )
Assertion fourierdlem10 
|- ( ph -> ( A <_ C /\ D <_ B ) )

Proof

Step Hyp Ref Expression
1 fourierdlem10.1 
 |-  ( ph -> A e. RR )
2 fourierdlem10.2 
 |-  ( ph -> B e. RR )
3 fourierdlem10.3 
 |-  ( ph -> C e. RR )
4 fourierdlem10.4 
 |-  ( ph -> D e. RR )
5 fourierdlem10.5 
 |-  ( ph -> C < D )
6 fourierdlem10.6 
 |-  ( ph -> ( C (,) D ) C_ ( A (,) B ) )
7 6 adantr 
 |-  ( ( ph /\ C < A ) -> ( C (,) D ) C_ ( A (,) B ) )
8 3 rexrd 
 |-  ( ph -> C e. RR* )
9 8 adantr 
 |-  ( ( ph /\ C < A ) -> C e. RR* )
10 4 rexrd 
 |-  ( ph -> D e. RR* )
11 10 adantr 
 |-  ( ( ph /\ C < A ) -> D e. RR* )
12 3 1 readdcld 
 |-  ( ph -> ( C + A ) e. RR )
13 12 rehalfcld 
 |-  ( ph -> ( ( C + A ) / 2 ) e. RR )
14 3 4 readdcld 
 |-  ( ph -> ( C + D ) e. RR )
15 14 rehalfcld 
 |-  ( ph -> ( ( C + D ) / 2 ) e. RR )
16 13 15 ifcld 
 |-  ( ph -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
17 16 adantr 
 |-  ( ( ph /\ C < A ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
18 simplr 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> C < A )
19 3 ad2antrr 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> C e. RR )
20 1 ad2antrr 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> A e. RR )
21 avglt1 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C < A <-> C < ( ( C + A ) / 2 ) ) )
22 19 20 21 syl2anc 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> ( C < A <-> C < ( ( C + A ) / 2 ) ) )
23 18 22 mpbid 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> C < ( ( C + A ) / 2 ) )
24 iftrue 
 |-  ( A <_ D -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + A ) / 2 ) )
25 24 adantl 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + A ) / 2 ) )
26 23 25 breqtrrd 
 |-  ( ( ( ph /\ C < A ) /\ A <_ D ) -> C < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
27 5 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> C < D )
28 3 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> C e. RR )
29 4 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> D e. RR )
30 avglt1 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C < D <-> C < ( ( C + D ) / 2 ) ) )
31 28 29 30 syl2anc 
 |-  ( ( ph /\ -. A <_ D ) -> ( C < D <-> C < ( ( C + D ) / 2 ) ) )
32 27 31 mpbid 
 |-  ( ( ph /\ -. A <_ D ) -> C < ( ( C + D ) / 2 ) )
33 iffalse 
 |-  ( -. A <_ D -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + D ) / 2 ) )
34 33 eqcomd 
 |-  ( -. A <_ D -> ( ( C + D ) / 2 ) = if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
35 34 adantl 
 |-  ( ( ph /\ -. A <_ D ) -> ( ( C + D ) / 2 ) = if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
36 32 35 breqtrd 
 |-  ( ( ph /\ -. A <_ D ) -> C < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
37 36 adantlr 
 |-  ( ( ( ph /\ C < A ) /\ -. A <_ D ) -> C < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
38 26 37 pm2.61dan 
 |-  ( ( ph /\ C < A ) -> C < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
39 24 adantl 
 |-  ( ( ph /\ A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + A ) / 2 ) )
40 12 adantr 
 |-  ( ( ph /\ A <_ D ) -> ( C + A ) e. RR )
41 14 adantr 
 |-  ( ( ph /\ A <_ D ) -> ( C + D ) e. RR )
42 2rp 
 |-  2 e. RR+
43 42 a1i 
 |-  ( ( ph /\ A <_ D ) -> 2 e. RR+ )
44 1 adantr 
 |-  ( ( ph /\ A <_ D ) -> A e. RR )
45 4 adantr 
 |-  ( ( ph /\ A <_ D ) -> D e. RR )
46 3 adantr 
 |-  ( ( ph /\ A <_ D ) -> C e. RR )
47 simpr 
 |-  ( ( ph /\ A <_ D ) -> A <_ D )
48 44 45 46 47 leadd2dd 
 |-  ( ( ph /\ A <_ D ) -> ( C + A ) <_ ( C + D ) )
49 40 41 43 48 lediv1dd 
 |-  ( ( ph /\ A <_ D ) -> ( ( C + A ) / 2 ) <_ ( ( C + D ) / 2 ) )
50 39 49 eqbrtrd 
 |-  ( ( ph /\ A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + D ) / 2 ) )
51 33 adantl 
 |-  ( ( ph /\ -. A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + D ) / 2 ) )
52 15 leidd 
 |-  ( ph -> ( ( C + D ) / 2 ) <_ ( ( C + D ) / 2 ) )
53 52 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> ( ( C + D ) / 2 ) <_ ( ( C + D ) / 2 ) )
54 51 53 eqbrtrd 
 |-  ( ( ph /\ -. A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + D ) / 2 ) )
55 50 54 pm2.61dan 
 |-  ( ph -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + D ) / 2 ) )
56 avglt2 
 |-  ( ( C e. RR /\ D e. RR ) -> ( C < D <-> ( ( C + D ) / 2 ) < D ) )
57 3 4 56 syl2anc 
 |-  ( ph -> ( C < D <-> ( ( C + D ) / 2 ) < D ) )
58 5 57 mpbid 
 |-  ( ph -> ( ( C + D ) / 2 ) < D )
59 16 15 4 55 58 lelttrd 
 |-  ( ph -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
60 59 adantr 
 |-  ( ( ph /\ C < A ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
61 9 11 17 38 60 eliood 
 |-  ( ( ph /\ C < A ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( C (,) D ) )
62 1 adantr 
 |-  ( ( ph /\ C < A ) -> A e. RR )
63 13 adantr 
 |-  ( ( ph /\ C < A ) -> ( ( C + A ) / 2 ) e. RR )
64 16 adantr 
 |-  ( ( ph /\ A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
65 64 39 eqled 
 |-  ( ( ph /\ A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + A ) / 2 ) )
66 16 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
67 13 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> ( ( C + A ) / 2 ) e. RR )
68 simpr 
 |-  ( ( ph /\ -. A <_ D ) -> -. A <_ D )
69 1 adantr 
 |-  ( ( ph /\ -. A <_ D ) -> A e. RR )
70 29 69 ltnled 
 |-  ( ( ph /\ -. A <_ D ) -> ( D < A <-> -. A <_ D ) )
71 68 70 mpbird 
 |-  ( ( ph /\ -. A <_ D ) -> D < A )
72 14 adantr 
 |-  ( ( ph /\ D < A ) -> ( C + D ) e. RR )
73 12 adantr 
 |-  ( ( ph /\ D < A ) -> ( C + A ) e. RR )
74 42 a1i 
 |-  ( ( ph /\ D < A ) -> 2 e. RR+ )
75 4 adantr 
 |-  ( ( ph /\ D < A ) -> D e. RR )
76 1 adantr 
 |-  ( ( ph /\ D < A ) -> A e. RR )
77 3 adantr 
 |-  ( ( ph /\ D < A ) -> C e. RR )
78 simpr 
 |-  ( ( ph /\ D < A ) -> D < A )
79 75 76 77 78 ltadd2dd 
 |-  ( ( ph /\ D < A ) -> ( C + D ) < ( C + A ) )
80 72 73 74 79 ltdiv1dd 
 |-  ( ( ph /\ D < A ) -> ( ( C + D ) / 2 ) < ( ( C + A ) / 2 ) )
81 71 80 syldan 
 |-  ( ( ph /\ -. A <_ D ) -> ( ( C + D ) / 2 ) < ( ( C + A ) / 2 ) )
82 51 81 eqbrtrd 
 |-  ( ( ph /\ -. A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < ( ( C + A ) / 2 ) )
83 66 67 82 ltled 
 |-  ( ( ph /\ -. A <_ D ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + A ) / 2 ) )
84 65 83 pm2.61dan 
 |-  ( ph -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + A ) / 2 ) )
85 84 adantr 
 |-  ( ( ph /\ C < A ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) <_ ( ( C + A ) / 2 ) )
86 simpr 
 |-  ( ( ph /\ C < A ) -> C < A )
87 3 adantr 
 |-  ( ( ph /\ C < A ) -> C e. RR )
88 avglt2 
 |-  ( ( C e. RR /\ A e. RR ) -> ( C < A <-> ( ( C + A ) / 2 ) < A ) )
89 87 62 88 syl2anc 
 |-  ( ( ph /\ C < A ) -> ( C < A <-> ( ( C + A ) / 2 ) < A ) )
90 86 89 mpbid 
 |-  ( ( ph /\ C < A ) -> ( ( C + A ) / 2 ) < A )
91 17 63 62 85 90 lelttrd 
 |-  ( ( ph /\ C < A ) -> if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < A )
92 17 62 91 ltnsymd 
 |-  ( ( ph /\ C < A ) -> -. A < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) )
93 92 intn3an2d 
 |-  ( ( ph /\ C < A ) -> -. ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) )
94 1 rexrd 
 |-  ( ph -> A e. RR* )
95 94 adantr 
 |-  ( ( ph /\ C < A ) -> A e. RR* )
96 2 rexrd 
 |-  ( ph -> B e. RR* )
97 96 adantr 
 |-  ( ( ph /\ C < A ) -> B e. RR* )
98 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) <-> ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) ) )
99 95 97 98 syl2anc 
 |-  ( ( ph /\ C < A ) -> ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) <-> ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) ) )
100 93 99 mtbird 
 |-  ( ( ph /\ C < A ) -> -. if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) )
101 nelss 
 |-  ( ( if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( C (,) D ) /\ -. if ( A <_ D , ( ( C + A ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) ) -> -. ( C (,) D ) C_ ( A (,) B ) )
102 61 100 101 syl2anc 
 |-  ( ( ph /\ C < A ) -> -. ( C (,) D ) C_ ( A (,) B ) )
103 7 102 pm2.65da 
 |-  ( ph -> -. C < A )
104 1 3 103 nltled 
 |-  ( ph -> A <_ C )
105 6 adantr 
 |-  ( ( ph /\ B < D ) -> ( C (,) D ) C_ ( A (,) B ) )
106 8 adantr 
 |-  ( ( ph /\ B < D ) -> C e. RR* )
107 10 adantr 
 |-  ( ( ph /\ B < D ) -> D e. RR* )
108 2 4 readdcld 
 |-  ( ph -> ( B + D ) e. RR )
109 108 rehalfcld 
 |-  ( ph -> ( ( B + D ) / 2 ) e. RR )
110 109 15 ifcld 
 |-  ( ph -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
111 110 adantr 
 |-  ( ( ph /\ B < D ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
112 3 adantr 
 |-  ( ( ph /\ C <_ B ) -> C e. RR )
113 15 adantr 
 |-  ( ( ph /\ C <_ B ) -> ( ( C + D ) / 2 ) e. RR )
114 110 adantr 
 |-  ( ( ph /\ C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR )
115 3 4 30 syl2anc 
 |-  ( ph -> ( C < D <-> C < ( ( C + D ) / 2 ) ) )
116 5 115 mpbid 
 |-  ( ph -> C < ( ( C + D ) / 2 ) )
117 116 adantr 
 |-  ( ( ph /\ C <_ B ) -> C < ( ( C + D ) / 2 ) )
118 14 adantr 
 |-  ( ( ph /\ C <_ B ) -> ( C + D ) e. RR )
119 108 adantr 
 |-  ( ( ph /\ C <_ B ) -> ( B + D ) e. RR )
120 42 a1i 
 |-  ( ( ph /\ C <_ B ) -> 2 e. RR+ )
121 2 adantr 
 |-  ( ( ph /\ C <_ B ) -> B e. RR )
122 4 adantr 
 |-  ( ( ph /\ C <_ B ) -> D e. RR )
123 simpr 
 |-  ( ( ph /\ C <_ B ) -> C <_ B )
124 112 121 122 123 leadd1dd 
 |-  ( ( ph /\ C <_ B ) -> ( C + D ) <_ ( B + D ) )
125 118 119 120 124 lediv1dd 
 |-  ( ( ph /\ C <_ B ) -> ( ( C + D ) / 2 ) <_ ( ( B + D ) / 2 ) )
126 iftrue 
 |-  ( C <_ B -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( B + D ) / 2 ) )
127 126 adantl 
 |-  ( ( ph /\ C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( B + D ) / 2 ) )
128 125 127 breqtrrd 
 |-  ( ( ph /\ C <_ B ) -> ( ( C + D ) / 2 ) <_ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
129 112 113 114 117 128 ltletrd 
 |-  ( ( ph /\ C <_ B ) -> C < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
130 116 adantr 
 |-  ( ( ph /\ -. C <_ B ) -> C < ( ( C + D ) / 2 ) )
131 iffalse 
 |-  ( -. C <_ B -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + D ) / 2 ) )
132 131 eqcomd 
 |-  ( -. C <_ B -> ( ( C + D ) / 2 ) = if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
133 132 adantl 
 |-  ( ( ph /\ -. C <_ B ) -> ( ( C + D ) / 2 ) = if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
134 130 133 breqtrd 
 |-  ( ( ph /\ -. C <_ B ) -> C < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
135 129 134 pm2.61dan 
 |-  ( ph -> C < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
136 135 adantr 
 |-  ( ( ph /\ B < D ) -> C < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
137 126 adantl 
 |-  ( ( ( ph /\ B < D ) /\ C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( B + D ) / 2 ) )
138 simpr 
 |-  ( ( ph /\ B < D ) -> B < D )
139 2 adantr 
 |-  ( ( ph /\ B < D ) -> B e. RR )
140 4 adantr 
 |-  ( ( ph /\ B < D ) -> D e. RR )
141 avglt2 
 |-  ( ( B e. RR /\ D e. RR ) -> ( B < D <-> ( ( B + D ) / 2 ) < D ) )
142 139 140 141 syl2anc 
 |-  ( ( ph /\ B < D ) -> ( B < D <-> ( ( B + D ) / 2 ) < D ) )
143 138 142 mpbid 
 |-  ( ( ph /\ B < D ) -> ( ( B + D ) / 2 ) < D )
144 143 adantr 
 |-  ( ( ( ph /\ B < D ) /\ C <_ B ) -> ( ( B + D ) / 2 ) < D )
145 137 144 eqbrtrd 
 |-  ( ( ( ph /\ B < D ) /\ C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
146 131 adantl 
 |-  ( ( ph /\ -. C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) = ( ( C + D ) / 2 ) )
147 58 adantr 
 |-  ( ( ph /\ -. C <_ B ) -> ( ( C + D ) / 2 ) < D )
148 146 147 eqbrtrd 
 |-  ( ( ph /\ -. C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
149 148 adantlr 
 |-  ( ( ( ph /\ B < D ) /\ -. C <_ B ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
150 145 149 pm2.61dan 
 |-  ( ( ph /\ B < D ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < D )
151 106 107 111 136 150 eliood 
 |-  ( ( ph /\ B < D ) -> if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( C (,) D ) )
152 109 adantr 
 |-  ( ( ph /\ B < D ) -> ( ( B + D ) / 2 ) e. RR )
153 avglt1 
 |-  ( ( B e. RR /\ D e. RR ) -> ( B < D <-> B < ( ( B + D ) / 2 ) ) )
154 139 140 153 syl2anc 
 |-  ( ( ph /\ B < D ) -> ( B < D <-> B < ( ( B + D ) / 2 ) ) )
155 138 154 mpbid 
 |-  ( ( ph /\ B < D ) -> B < ( ( B + D ) / 2 ) )
156 139 152 155 ltled 
 |-  ( ( ph /\ B < D ) -> B <_ ( ( B + D ) / 2 ) )
157 156 adantr 
 |-  ( ( ( ph /\ B < D ) /\ C <_ B ) -> B <_ ( ( B + D ) / 2 ) )
158 157 137 breqtrrd 
 |-  ( ( ( ph /\ B < D ) /\ C <_ B ) -> B <_ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
159 2 adantr 
 |-  ( ( ph /\ -. C <_ B ) -> B e. RR )
160 15 adantr 
 |-  ( ( ph /\ -. C <_ B ) -> ( ( C + D ) / 2 ) e. RR )
161 3 adantr 
 |-  ( ( ph /\ -. C <_ B ) -> C e. RR )
162 simpr 
 |-  ( ( ph /\ -. C <_ B ) -> -. C <_ B )
163 159 161 ltnled 
 |-  ( ( ph /\ -. C <_ B ) -> ( B < C <-> -. C <_ B ) )
164 162 163 mpbird 
 |-  ( ( ph /\ -. C <_ B ) -> B < C )
165 159 161 160 164 130 lttrd 
 |-  ( ( ph /\ -. C <_ B ) -> B < ( ( C + D ) / 2 ) )
166 159 160 165 ltled 
 |-  ( ( ph /\ -. C <_ B ) -> B <_ ( ( C + D ) / 2 ) )
167 166 133 breqtrd 
 |-  ( ( ph /\ -. C <_ B ) -> B <_ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
168 167 adantlr 
 |-  ( ( ( ph /\ B < D ) /\ -. C <_ B ) -> B <_ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
169 158 168 pm2.61dan 
 |-  ( ( ph /\ B < D ) -> B <_ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) )
170 139 111 169 lensymd 
 |-  ( ( ph /\ B < D ) -> -. if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < B )
171 170 intn3an3d 
 |-  ( ( ph /\ B < D ) -> -. ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) )
172 94 adantr 
 |-  ( ( ph /\ B < D ) -> A e. RR* )
173 96 adantr 
 |-  ( ( ph /\ B < D ) -> B e. RR* )
174 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) <-> ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) ) )
175 172 173 174 syl2anc 
 |-  ( ( ph /\ B < D ) -> ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) <-> ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. RR /\ A < if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) /\ if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) < B ) ) )
176 171 175 mtbird 
 |-  ( ( ph /\ B < D ) -> -. if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) )
177 nelss 
 |-  ( ( if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( C (,) D ) /\ -. if ( C <_ B , ( ( B + D ) / 2 ) , ( ( C + D ) / 2 ) ) e. ( A (,) B ) ) -> -. ( C (,) D ) C_ ( A (,) B ) )
178 151 176 177 syl2anc 
 |-  ( ( ph /\ B < D ) -> -. ( C (,) D ) C_ ( A (,) B ) )
179 105 178 pm2.65da 
 |-  ( ph -> -. B < D )
180 4 2 179 nltled 
 |-  ( ph -> D <_ B )
181 104 180 jca 
 |-  ( ph -> ( A <_ C /\ D <_ B ) )