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 ⊢ φ → C D ⊆ A B
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 ⊢ φ → C D ⊆ A B
7 6 adantr ⊢ φ ∧ C < A → C D ⊆ A B
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 + A 2 ∈ ℝ
14 3 4 readdcld ⊢ φ → C + D ∈ ℝ
15 14 rehalfcld ⊢ φ → C + D 2 ∈ ℝ
16 13 15 ifcld ⊢ φ → if A ≤ D C + A 2 C + D 2 ∈ ℝ
17 16 adantr ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 ∈ ℝ
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 + A 2
22 19 20 21 syl2anc ⊢ φ ∧ C < A ∧ A ≤ D → C < A ↔ C < C + A 2
23 18 22 mpbid ⊢ φ ∧ 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 ⊢ φ ∧ C < A ∧ A ≤ D → if A ≤ D C + A 2 C + D 2 = C + A 2
26 23 25 breqtrrd ⊢ φ ∧ C < A ∧ A ≤ D → C < if A ≤ D C + A 2 C + D 2
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 + D 2
31 28 29 30 syl2anc ⊢ φ ∧ ¬ A ≤ D → C < D ↔ C < C + D 2
32 27 31 mpbid ⊢ φ ∧ ¬ 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 ⊢ φ ∧ ¬ A ≤ D → C + D 2 = if A ≤ D C + A 2 C + D 2
36 32 35 breqtrd ⊢ φ ∧ ¬ A ≤ D → C < if A ≤ D C + A 2 C + D 2
37 36 adantlr ⊢ φ ∧ C < A ∧ ¬ A ≤ D → C < if A ≤ D C + A 2 C + D 2
38 26 37 pm2.61dan ⊢ φ ∧ C < A → C < if A ≤ D C + A 2 C + D 2
39 24 adantl ⊢ φ ∧ A ≤ D → if A ≤ D C + A 2 C + D 2 = C + A 2
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 + A 2 ≤ C + D 2
50 39 49 eqbrtrd ⊢ φ ∧ A ≤ D → if A ≤ D C + A 2 C + D 2 ≤ C + D 2
51 33 adantl ⊢ φ ∧ ¬ A ≤ D → if A ≤ D C + A 2 C + D 2 = C + D 2
52 15 leidd ⊢ φ → C + D 2 ≤ C + D 2
53 52 adantr ⊢ φ ∧ ¬ A ≤ D → C + D 2 ≤ C + D 2
54 51 53 eqbrtrd ⊢ φ ∧ ¬ A ≤ D → if A ≤ D C + A 2 C + D 2 ≤ C + D 2
55 50 54 pm2.61dan ⊢ φ → if A ≤ D C + A 2 C + D 2 ≤ C + D 2
56 avglt2 ⊢ C ∈ ℝ ∧ D ∈ ℝ → C < D ↔ C + D 2 < D
57 3 4 56 syl2anc ⊢ φ → C < D ↔ C + D 2 < D
58 5 57 mpbid ⊢ φ → C + D 2 < D
59 16 15 4 55 58 lelttrd ⊢ φ → if A ≤ D C + A 2 C + D 2 < D
60 59 adantr ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 < D
61 9 11 17 38 60 eliood ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 ∈ C D
62 1 adantr ⊢ φ ∧ C < A → A ∈ ℝ
63 13 adantr ⊢ φ ∧ C < A → C + A 2 ∈ ℝ
64 16 adantr ⊢ φ ∧ A ≤ D → if A ≤ D C + A 2 C + D 2 ∈ ℝ
65 64 39 eqled ⊢ φ ∧ A ≤ D → if A ≤ D C + A 2 C + D 2 ≤ C + A 2
66 16 adantr ⊢ φ ∧ ¬ A ≤ D → if A ≤ D C + A 2 C + D 2 ∈ ℝ
67 13 adantr ⊢ φ ∧ ¬ A ≤ D → C + A 2 ∈ ℝ
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 + D 2 < C + A 2
81 71 80 syldan ⊢ φ ∧ ¬ A ≤ D → C + D 2 < C + A 2
82 51 81 eqbrtrd ⊢ φ ∧ ¬ A ≤ D → if A ≤ D C + A 2 C + D 2 < C + A 2
83 66 67 82 ltled ⊢ φ ∧ ¬ A ≤ D → if A ≤ D C + A 2 C + D 2 ≤ C + A 2
84 65 83 pm2.61dan ⊢ φ → if A ≤ D C + A 2 C + D 2 ≤ C + A 2
85 84 adantr ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 ≤ C + A 2
86 simpr ⊢ φ ∧ C < A → C < A
87 3 adantr ⊢ φ ∧ C < A → C ∈ ℝ
88 avglt2 ⊢ C ∈ ℝ ∧ A ∈ ℝ → C < A ↔ C + A 2 < A
89 87 62 88 syl2anc ⊢ φ ∧ C < A → C < A ↔ C + A 2 < A
90 86 89 mpbid ⊢ φ ∧ C < A → C + A 2 < A
91 17 63 62 85 90 lelttrd ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 < A
92 17 62 91 ltnsymd ⊢ φ ∧ C < A → ¬ A < if A ≤ D C + A 2 C + D 2
93 92 intn3an2d ⊢ φ ∧ C < A → ¬ if A ≤ D C + A 2 C + D 2 ∈ ℝ ∧ A < if A ≤ D C + A 2 C + D 2 ∧ if A ≤ D C + A 2 C + D 2 < 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 ∈ ℝ * → if A ≤ D C + A 2 C + D 2 ∈ A B ↔ if A ≤ D C + A 2 C + D 2 ∈ ℝ ∧ 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 ⊢ φ ∧ C < A → if A ≤ D C + A 2 C + D 2 ∈ A B ↔ if A ≤ D C + A 2 C + D 2 ∈ ℝ ∧ A < if A ≤ D C + A 2 C + D 2 ∧ if A ≤ D C + A 2 C + D 2 < B
100 93 99 mtbird ⊢ φ ∧ C < A → ¬ if A ≤ D C + A 2 C + D 2 ∈ A B
101 nelss ⊢ if A ≤ D C + A 2 C + D 2 ∈ C D ∧ ¬ if A ≤ D C + A 2 C + D 2 ∈ A B → ¬ C D ⊆ A B
102 61 100 101 syl2anc ⊢ φ ∧ C < A → ¬ C D ⊆ A B
103 7 102 pm2.65da ⊢ φ → ¬ C < A
104 1 3 103 nltled ⊢ φ → A ≤ C
105 6 adantr ⊢ φ ∧ B < D → C D ⊆ A B
106 8 adantr ⊢ φ ∧ B < D → C ∈ ℝ *
107 10 adantr ⊢ φ ∧ B < D → D ∈ ℝ *
108 2 4 readdcld ⊢ φ → B + D ∈ ℝ
109 108 rehalfcld ⊢ φ → B + D 2 ∈ ℝ
110 109 15 ifcld ⊢ φ → if C ≤ B B + D 2 C + D 2 ∈ ℝ
111 110 adantr ⊢ φ ∧ B < D → if C ≤ B B + D 2 C + D 2 ∈ ℝ
112 3 adantr ⊢ φ ∧ C ≤ B → C ∈ ℝ
113 15 adantr ⊢ φ ∧ C ≤ B → C + D 2 ∈ ℝ
114 110 adantr ⊢ φ ∧ C ≤ B → if C ≤ B B + D 2 C + D 2 ∈ ℝ
115 3 4 30 syl2anc ⊢ φ → C < D ↔ C < C + D 2
116 5 115 mpbid ⊢ φ → C < C + D 2
117 116 adantr ⊢ φ ∧ C ≤ B → C < C + D 2
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 + D 2 ≤ B + D 2
126 iftrue ⊢ C ≤ B → if C ≤ B B + D 2 C + D 2 = B + D 2
127 126 adantl ⊢ φ ∧ C ≤ B → if C ≤ B B + D 2 C + D 2 = B + D 2
128 125 127 breqtrrd ⊢ φ ∧ C ≤ B → C + D 2 ≤ if C ≤ B B + D 2 C + D 2
129 112 113 114 117 128 ltletrd ⊢ φ ∧ C ≤ B → C < if C ≤ B B + D 2 C + D 2
130 116 adantr ⊢ φ ∧ ¬ 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 ⊢ φ ∧ ¬ C ≤ B → C + D 2 = if C ≤ B B + D 2 C + D 2
134 130 133 breqtrd ⊢ φ ∧ ¬ C ≤ B → C < if C ≤ B B + D 2 C + D 2
135 129 134 pm2.61dan ⊢ φ → C < if C ≤ B B + D 2 C + D 2
136 135 adantr ⊢ φ ∧ B < D → C < if C ≤ B B + D 2 C + D 2
137 126 adantl ⊢ φ ∧ B < D ∧ C ≤ B → if C ≤ B B + D 2 C + D 2 = B + D 2
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 + D 2 < D
142 139 140 141 syl2anc ⊢ φ ∧ B < D → B < D ↔ B + D 2 < D
143 138 142 mpbid ⊢ φ ∧ B < D → B + D 2 < D
144 143 adantr ⊢ φ ∧ B < D ∧ C ≤ B → B + D 2 < D
145 137 144 eqbrtrd ⊢ φ ∧ B < D ∧ C ≤ B → if C ≤ B B + D 2 C + D 2 < D
146 131 adantl ⊢ φ ∧ ¬ C ≤ B → if C ≤ B B + D 2 C + D 2 = C + D 2
147 58 adantr ⊢ φ ∧ ¬ C ≤ B → C + D 2 < D
148 146 147 eqbrtrd ⊢ φ ∧ ¬ C ≤ B → if C ≤ B B + D 2 C + D 2 < D
149 148 adantlr ⊢ φ ∧ B < D ∧ ¬ C ≤ B → if C ≤ B B + D 2 C + D 2 < D
150 145 149 pm2.61dan ⊢ φ ∧ B < D → if C ≤ B B + D 2 C + D 2 < D
151 106 107 111 136 150 eliood ⊢ φ ∧ B < D → if C ≤ B B + D 2 C + D 2 ∈ C D
152 109 adantr ⊢ φ ∧ B < D → B + D 2 ∈ ℝ
153 avglt1 ⊢ B ∈ ℝ ∧ D ∈ ℝ → B < D ↔ B < B + D 2
154 139 140 153 syl2anc ⊢ φ ∧ B < D → B < D ↔ B < B + D 2
155 138 154 mpbid ⊢ φ ∧ B < D → B < B + D 2
156 139 152 155 ltled ⊢ φ ∧ B < D → B ≤ B + D 2
157 156 adantr ⊢ φ ∧ B < D ∧ C ≤ B → B ≤ B + D 2
158 157 137 breqtrrd ⊢ φ ∧ B < D ∧ C ≤ B → B ≤ if C ≤ B B + D 2 C + D 2
159 2 adantr ⊢ φ ∧ ¬ C ≤ B → B ∈ ℝ
160 15 adantr ⊢ φ ∧ ¬ C ≤ B → C + D 2 ∈ ℝ
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 + D 2
166 159 160 165 ltled ⊢ φ ∧ ¬ C ≤ B → B ≤ C + D 2
167 166 133 breqtrd ⊢ φ ∧ ¬ C ≤ B → B ≤ if C ≤ B B + D 2 C + D 2
168 167 adantlr ⊢ φ ∧ B < D ∧ ¬ C ≤ B → B ≤ if C ≤ B B + D 2 C + D 2
169 158 168 pm2.61dan ⊢ φ ∧ B < D → B ≤ if C ≤ B B + D 2 C + D 2
170 139 111 169 lensymd ⊢ φ ∧ B < D → ¬ if C ≤ B B + D 2 C + D 2 < B
171 170 intn3an3d ⊢ φ ∧ B < D → ¬ if C ≤ B B + D 2 C + D 2 ∈ ℝ ∧ A < if C ≤ B B + D 2 C + D 2 ∧ if C ≤ B B + D 2 C + D 2 < B
172 94 adantr ⊢ φ ∧ B < D → A ∈ ℝ *
173 96 adantr ⊢ φ ∧ B < D → B ∈ ℝ *
174 elioo2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → if C ≤ B B + D 2 C + D 2 ∈ A B ↔ if C ≤ B B + D 2 C + D 2 ∈ ℝ ∧ 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 ⊢ φ ∧ B < D → if C ≤ B B + D 2 C + D 2 ∈ A B ↔ if C ≤ B B + D 2 C + D 2 ∈ ℝ ∧ A < if C ≤ B B + D 2 C + D 2 ∧ if C ≤ B B + D 2 C + D 2 < B
176 171 175 mtbird ⊢ φ ∧ B < D → ¬ if C ≤ B B + D 2 C + D 2 ∈ A B
177 nelss ⊢ if C ≤ B B + D 2 C + D 2 ∈ C D ∧ ¬ if C ≤ B B + D 2 C + D 2 ∈ A B → ¬ C D ⊆ A B
178 151 176 177 syl2anc ⊢ φ ∧ B < D → ¬ C D ⊆ A B
179 105 178 pm2.65da ⊢ φ → ¬ B < D
180 4 2 179 nltled ⊢ φ → D ≤ B
181 104 180 jca ⊢ φ → A ≤ C ∧ D ≤ B