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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem10.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem10.3 ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem10.4 ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
fourierdlem10.5 ⊢ ( 𝜑 → 𝐶 < 𝐷 )
fourierdlem10.6 ⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
Assertion fourierdlem10 ( 𝜑 → ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) )

Proof

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