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 ⊢φ→A∈ℝ
fourierdlem10.2 ⊢φ→B∈ℝ
fourierdlem10.3 ⊢φ→C∈ℝ
fourierdlem10.4 ⊢φ→D∈ℝ
fourierdlem10.5 ⊢φ→C<D
fourierdlem10.6 ⊢φ→CD⊆AB
Assertion fourierdlem10 ⊢φ→A≤C∧D≤B

Proof

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