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

Metamath Proof Explorer

Theorem ivthlem2

Description: Lemma for ivth . Show that the supremum of S cannot be less than U . If it was, continuity of F implies that there are points just above the supremum that are also less than U , a contradiction. (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypotheses ivth.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ivth.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ivth.3 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
ivth.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
ivth.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
ivth.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
ivth.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
ivth.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
ivth.10 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 }
ivth.11 ⊢ 𝐶 = sup ( 𝑆 , ℝ , < )
Assertion ivthlem2 ( 𝜑 → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 )

Proof

Step Hyp Ref Expression
1 ivth.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ivth.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ivth.3 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
4 ivth.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 ivth.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
6 ivth.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
7 ivth.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8 ivth.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
9 ivth.10 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 }
10 ivth.11 ⊢ 𝐶 = sup ( 𝑆 , ℝ , < )
11 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
12 9 ssrab3 ⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
13 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
15 12 14 sstrid ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
16 1 2 3 4 5 6 7 8 9 ivthlem1 ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
17 16 simpld ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
18 17 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
19 16 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 )
20 brralrspcev ⊢ ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 )
21 2 19 20 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 )
22 15 18 21 suprcld ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
23 10 22 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
24 15 18 21 17 suprubd ⊢ ( 𝜑 → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
25 24 10 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
26 15 18 21 3jca ⊢ ( 𝜑 → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) )
27 suprleub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
28 26 2 27 syl2anc ⊢ ( 𝜑 → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
29 19 28 mpbird ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ≤ 𝐵 )
30 10 29 eqbrtrid ⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
31 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
32 1 2 31 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
33 23 25 30 32 mpbir3and ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
34 5 33 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → 𝐶 ∈ 𝐷 )
36 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
37 36 eleq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐶 ) ∈ ℝ ) )
38 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
39 37 38 33 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
40 difrp ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( ( 𝐹 ‘ 𝐶 ) < 𝑈 ↔ ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∈ ℝ+ ) )
41 39 3 40 syl2anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < 𝑈 ↔ ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∈ ℝ+ ) )
42 41 biimpa ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∈ ℝ+ )
43 cncfi ⊢ ( ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ 𝐶 ∈ 𝐷 ∧ ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) )
44 11 35 42 43 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) )
45 ssralv ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ) )
46 5 45 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ) )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ) )
48 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
49 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
50 rphalfcl ⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) ∈ ℝ+ )
51 50 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 / 2 ) ∈ ℝ+ )
52 51 rpred ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 / 2 ) ∈ ℝ )
53 49 52 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 + ( 𝑧 / 2 ) ) ∈ ℝ )
54 48 53 ifcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ℝ )
55 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
56 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐴 ≤ 𝐶 )
57 8 simprd ⊢ ( 𝜑 → 𝑈 < ( 𝐹 ‘ 𝐵 ) )
58 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
59 58 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) )
60 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
61 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
62 1 2 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
63 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
64 60 61 62 63 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
65 59 38 64 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
66 lttr ⊢ ( ( ( 𝐹 ‘ 𝐶 ) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝐶 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
67 39 3 65 66 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐹 ‘ 𝐶 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
68 57 67 mpan2d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < 𝑈 → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
69 68 imp ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) )
71 39 ltnrd ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) )
72 fveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) )
73 72 breq2d ⊢ ( 𝐵 = 𝐶 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ) )
74 73 notbid ⊢ ( 𝐵 = 𝐶 → ( ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ↔ ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ) )
75 71 74 syl5ibrcom ⊢ ( 𝜑 → ( 𝐵 = 𝐶 → ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
76 75 necon2ad ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → 𝐵 ≠ 𝐶 ) )
77 76 30 jctild ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
78 23 2 ltlend ⊢ ( 𝜑 → ( 𝐶 < 𝐵 ↔ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
79 77 78 sylibrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → 𝐶 < 𝐵 ) )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → 𝐶 < 𝐵 ) )
81 70 80 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 < 𝐵 )
82 49 51 ltaddrpd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 < ( 𝐶 + ( 𝑧 / 2 ) ) )
83 breq2 ⊢ ( 𝐵 = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( 𝐶 < 𝐵 ↔ 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ) )
84 breq2 ⊢ ( ( 𝐶 + ( 𝑧 / 2 ) ) = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( 𝐶 < ( 𝐶 + ( 𝑧 / 2 ) ) ↔ 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ) )
85 83 84 ifboth ⊢ ( ( 𝐶 < 𝐵 ∧ 𝐶 < ( 𝐶 + ( 𝑧 / 2 ) ) ) → 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) )
86 81 82 85 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) )
87 49 54 86 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 ≤ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) )
88 55 49 54 56 87 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝐴 ≤ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) )
89 min1 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 + ( 𝑧 / 2 ) ) ∈ ℝ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ 𝐵 )
90 48 53 89 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ 𝐵 )
91 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ℝ ∧ 𝐴 ≤ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∧ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ 𝐵 ) ) )
92 1 2 91 syl2anc ⊢ ( 𝜑 → ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ℝ ∧ 𝐴 ≤ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∧ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ 𝐵 ) ) )
93 92 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ℝ ∧ 𝐴 ≤ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∧ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ 𝐵 ) ) )
94 54 88 90 93 mpbir3and ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) )
95 49 54 87 abssubge0d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) = ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) )
96 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
97 96 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → 𝑧 ∈ ℝ )
98 49 97 readdcld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 + 𝑧 ) ∈ ℝ )
99 min2 ⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 + ( 𝑧 / 2 ) ) ∈ ℝ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ ( 𝐶 + ( 𝑧 / 2 ) ) )
100 48 53 99 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ≤ ( 𝐶 + ( 𝑧 / 2 ) ) )
101 rphalflt ⊢ ( 𝑧 ∈ ℝ+ → ( 𝑧 / 2 ) < 𝑧 )
102 101 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑧 / 2 ) < 𝑧 )
103 52 97 49 102 ltadd2dd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 + ( 𝑧 / 2 ) ) < ( 𝐶 + 𝑧 ) )
104 54 53 98 100 103 lelttrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) < ( 𝐶 + 𝑧 ) )
105 54 49 97 ltsubadd2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) < 𝑧 ↔ if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) < ( 𝐶 + 𝑧 ) ) )
106 104 105 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) < 𝑧 )
107 95 106 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) < 𝑧 )
108 fvoveq1 ⊢ ( 𝑦 = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( abs ‘ ( 𝑦 − 𝐶 ) ) = ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) )
109 108 breq1d ⊢ ( 𝑦 = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ↔ ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) < 𝑧 ) )
110 breq2 ⊢ ( 𝑦 = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( 𝐶 < 𝑦 ↔ 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ) )
111 109 110 anbi12d ⊢ ( 𝑦 = if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ↔ ( ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) < 𝑧 ∧ 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ) ) )
112 111 rspcev ⊢ ( ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ∈ ( 𝐴 [,] 𝐵 ) ∧ ( ( abs ‘ ( if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) − 𝐶 ) ) < 𝑧 ∧ 𝐶 < if ( 𝐵 ≤ ( 𝐶 + ( 𝑧 / 2 ) ) , 𝐵 , ( 𝐶 + ( 𝑧 / 2 ) ) ) ) ) → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) )
113 94 107 86 112 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) )
114 r19.29 ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) )
115 pm3.45 ⊢ ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∧ 𝐶 < 𝑦 ) ) )
116 115 imp ⊢ ( ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∧ 𝐶 < 𝑦 ) )
117 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝐶 < 𝑦 )
118 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
119 118 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) )
120 simplll ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝜑 )
121 120 38 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
122 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
123 119 121 122 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
124 120 39 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
125 120 3 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝑈 ∈ ℝ )
126 125 124 resubcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∈ ℝ )
127 123 124 126 absdifltd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ↔ ( ( ( 𝐹 ‘ 𝐶 ) − ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ) ) )
128 ltle ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑦 ) < 𝑈 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
129 123 125 128 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) < 𝑈 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
130 124 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
131 125 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝑈 ∈ ℂ )
132 130 131 pncan3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) = 𝑈 )
133 132 breq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ↔ ( 𝐹 ‘ 𝑦 ) < 𝑈 ) )
134 118 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
135 134 9 elrab2 ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
136 135 baib ⊢ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) → ( 𝑦 ∈ 𝑆 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
137 136 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝑦 ∈ 𝑆 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
138 129 133 137 3imtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → 𝑦 ∈ 𝑆 ) )
139 suprub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ sup ( 𝑆 , ℝ , < ) )
140 139 10 breqtrrdi ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ 𝐶 )
141 140 ex ⊢ ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) → ( 𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶 ) )
142 120 26 141 3syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶 ) )
143 120 14 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
144 143 122 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝑦 ∈ ℝ )
145 120 23 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → 𝐶 ∈ ℝ )
146 144 145 lenltd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝑦 ≤ 𝐶 ↔ ¬ 𝐶 < 𝑦 ) )
147 142 146 sylibd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( 𝑦 ∈ 𝑆 → ¬ 𝐶 < 𝑦 ) )
148 138 147 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ¬ 𝐶 < 𝑦 ) )
149 148 adantld ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( ( ( 𝐹 ‘ 𝐶 ) − ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ) → ¬ 𝐶 < 𝑦 ) )
150 127 149 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) → ¬ 𝐶 < 𝑦 ) )
151 117 150 mt2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ¬ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) )
152 151 pm2.21d ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝐶 < 𝑦 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
153 152 expr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐶 < 𝑦 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ) )
154 153 impcomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ∧ 𝐶 < 𝑦 ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
155 116 154 syl5 ⊢ ( ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
156 155 rexlimdva ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
157 114 156 syl5 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) ∧ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝐶 < 𝑦 ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
158 113 157 mpan2d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
159 47 158 syld ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
160 159 rexlimdva ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( 𝑈 − ( 𝐹 ‘ 𝐶 ) ) ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) )
161 44 160 mpd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐶 ) < 𝑈 ) → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 )
162 161 pm2.01da ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 )