Metamath Proof Explorer

Theorem ivthlem3

Description: Lemma for ivth , the intermediate value theorem. Show that ( FC ) cannot be greater than U , and so establish the existence of a root of the function. (Contributed by Mario Carneiro, 30-Apr-2014) (Revised 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 ivthlem3 ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) = 𝑈 ) )

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 9 ssrab3 ⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
12 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
13 1 2 12 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
14 11 13 sstrid ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
15 1 2 3 4 5 6 7 8 9 ivthlem1 ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
16 15 simpld ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
17 16 ne0d ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
18 15 simprd ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 )
19 brralrspcev ⊢ ( ( 𝐵 ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 )
20 2 18 19 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 )
21 14 17 20 suprcld ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ∈ ℝ )
22 10 21 eqeltrid ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
23 8 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) < 𝑈 )
24 1 2 3 4 5 6 7 8 9 10 ivthlem2 ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
26 14 17 20 16 suprubd ⊢ ( 𝜑 → 𝐴 ≤ sup ( 𝑆 , ℝ , < ) )
27 26 10 breqtrrdi ⊢ ( 𝜑 → 𝐴 ≤ 𝐶 )
28 14 17 20 3jca ⊢ ( 𝜑 → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) )
29 suprleub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ 𝐵 ∈ ℝ ) → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
30 28 2 29 syl2anc ⊢ ( 𝜑 → ( sup ( 𝑆 , ℝ , < ) ≤ 𝐵 ↔ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )
31 18 30 mpbird ⊢ ( 𝜑 → sup ( 𝑆 , ℝ , < ) ≤ 𝐵 )
32 10 31 eqbrtrid ⊢ ( 𝜑 → 𝐶 ≤ 𝐵 )
33 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
34 1 2 33 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵 ) ) )
35 22 27 32 34 mpbir3and ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 [,] 𝐵 ) )
36 5 35 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝐷 )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → 𝐶 ∈ 𝐷 )
38 fveq2 ⊢ ( 𝑥 = 𝐶 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐶 ) )
39 38 eleq1d ⊢ ( 𝑥 = 𝐶 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐶 ) ∈ ℝ ) )
40 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
41 39 40 35 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
42 difrp ⊢ ( ( 𝑈 ∈ ℝ ∧ ( 𝐹 ‘ 𝐶 ) ∈ ℝ ) → ( 𝑈 < ( 𝐹 ‘ 𝐶 ) ↔ ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∈ ℝ+ ) )
43 3 41 42 syl2anc ⊢ ( 𝜑 → ( 𝑈 < ( 𝐹 ‘ 𝐶 ) ↔ ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∈ ℝ+ ) )
44 43 biimpa ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∈ ℝ+ )
45 cncfi ⊢ ( ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) ∧ 𝐶 ∈ 𝐷 ∧ ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) )
46 25 37 44 45 syl3anc ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) )
47 ssralv ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ) )
48 5 47 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ) )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ) )
50 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
51 ltsubrp ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 − 𝑧 ) < 𝐶 )
52 50 51 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 − 𝑧 ) < 𝐶 )
53 52 10 breqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 − 𝑧 ) < sup ( 𝑆 , ℝ , < ) )
54 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) )
55 rpre ⊢ ( 𝑧 ∈ ℝ+ → 𝑧 ∈ ℝ )
56 55 adantl ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → 𝑧 ∈ ℝ )
57 50 56 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝐶 − 𝑧 ) ∈ ℝ )
58 suprlub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ ( 𝐶 − 𝑧 ) ∈ ℝ ) → ( ( 𝐶 − 𝑧 ) < sup ( 𝑆 , ℝ , < ) ↔ ∃ 𝑦 ∈ 𝑆 ( 𝐶 − 𝑧 ) < 𝑦 ) )
59 54 57 58 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝐶 − 𝑧 ) < sup ( 𝑆 , ℝ , < ) ↔ ∃ 𝑦 ∈ 𝑆 ( 𝐶 − 𝑧 ) < 𝑦 ) )
60 53 59 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑦 ∈ 𝑆 ( 𝐶 − 𝑧 ) < 𝑦 )
61 11 sseli ⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
62 61 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
63 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝜑 )
64 63 13 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
65 64 62 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑦 ∈ ℝ )
66 63 22 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝐶 ∈ ℝ )
67 63 28 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) )
68 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑦 ∈ 𝑆 )
69 suprub ⊢ ( ( ( 𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ sup ( 𝑆 , ℝ , < ) )
70 67 68 69 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑦 ≤ sup ( 𝑆 , ℝ , < ) )
71 70 10 breqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑦 ≤ 𝐶 )
72 65 66 71 abssuble0d ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( abs ‘ ( 𝑦 − 𝐶 ) ) = ( 𝐶 − 𝑦 ) )
73 56 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → 𝑧 ∈ ℝ )
74 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( 𝐶 − 𝑧 ) < 𝑦 )
75 66 73 65 74 ltsub23d ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( 𝐶 − 𝑦 ) < 𝑧 )
76 72 75 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 )
77 62 76 68 jca32 ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) )
78 77 ex ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( 𝑦 ∈ 𝑆 ∧ ( 𝐶 − 𝑧 ) < 𝑦 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) ) )
79 78 reximdv2 ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ 𝑆 ( 𝐶 − 𝑧 ) < 𝑦 → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) )
80 60 79 mpd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) )
81 r19.29 ⊢ ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) → ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) )
82 pm3.45 ⊢ ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∧ 𝑦 ∈ 𝑆 ) ) )
83 82 imp ⊢ ( ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∧ 𝑦 ∈ 𝑆 ) )
84 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
85 84 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑦 ) ∈ ℝ ) )
86 40 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
87 61 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
88 85 86 87 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
89 41 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
90 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → 𝑈 ∈ ℝ )
91 89 90 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∈ ℝ )
92 88 89 91 absdifltd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ↔ ( ( ( 𝐹 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) < ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ) ) )
93 89 recnd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
94 90 recnd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → 𝑈 ∈ ℂ )
95 93 94 nncand ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) = 𝑈 )
96 95 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) < ( 𝐹 ‘ 𝑦 ) ↔ 𝑈 < ( 𝐹 ‘ 𝑦 ) ) )
97 84 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
98 97 9 elrab2 ⊢ ( 𝑦 ∈ 𝑆 ↔ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 ) )
99 98 simprbi ⊢ ( 𝑦 ∈ 𝑆 → ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 )
100 99 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝐹 ‘ 𝑦 ) ≤ 𝑈 )
101 88 90 100 lensymd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝑦 ) )
102 101 pm2.21d ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑈 < ( 𝐹 ‘ 𝑦 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
103 96 102 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( 𝐹 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) < ( 𝐹 ‘ 𝑦 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
104 103 adantrd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( 𝐹 ‘ 𝐶 ) − ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) < ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) < ( ( 𝐹 ‘ 𝐶 ) + ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
105 92 104 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ ( 𝑧 ∈ ℝ+ ∧ 𝑦 ∈ 𝑆 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
106 105 expr ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( 𝑦 ∈ 𝑆 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ) )
107 106 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∧ 𝑦 ∈ 𝑆 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
108 107 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ∧ 𝑦 ∈ 𝑆 ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
109 83 108 syl5 ⊢ ( ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
110 109 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
111 81 110 syl5 ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) ∧ ∃ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 ∧ 𝑦 ∈ 𝑆 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
112 80 111 mpan2d ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
113 49 112 syld ⊢ ( ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ∧ 𝑧 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
114 113 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → ( ∃ 𝑧 ∈ ℝ+ ∀ 𝑦 ∈ 𝐷 ( ( abs ‘ ( 𝑦 − 𝐶 ) ) < 𝑧 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝐶 ) ) ) < ( ( 𝐹 ‘ 𝐶 ) − 𝑈 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) )
115 46 114 mpd ⊢ ( ( 𝜑 ∧ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) )
116 115 pm2.01da ⊢ ( 𝜑 → ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) )
117 41 3 lttri3d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) = 𝑈 ↔ ( ¬ ( 𝐹 ‘ 𝐶 ) < 𝑈 ∧ ¬ 𝑈 < ( 𝐹 ‘ 𝐶 ) ) ) )
118 24 116 117 mpbir2and ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) = 𝑈 )
119 23 118 breqtrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) )
120 41 ltnrd ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) )
121 fveq2 ⊢ ( 𝐶 = 𝐴 → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐴 ) )
122 121 breq1d ⊢ ( 𝐶 = 𝐴 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ↔ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) ) )
123 122 notbid ⊢ ( 𝐶 = 𝐴 → ( ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ↔ ¬ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) ) )
124 120 123 syl5ibcom ⊢ ( 𝜑 → ( 𝐶 = 𝐴 → ¬ ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) ) )
125 124 necon2ad ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) → 𝐶 ≠ 𝐴 ) )
126 125 27 jctild ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) → ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ) )
127 1 22 ltlend ⊢ ( 𝜑 → ( 𝐴 < 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ) )
128 126 127 sylibrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < ( 𝐹 ‘ 𝐶 ) → 𝐴 < 𝐶 ) )
129 119 128 mpd ⊢ ( 𝜑 → 𝐴 < 𝐶 )
130 8 simprd ⊢ ( 𝜑 → 𝑈 < ( 𝐹 ‘ 𝐵 ) )
131 118 130 eqbrtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) )
132 fveq2 ⊢ ( 𝐵 = 𝐶 → ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐶 ) )
133 132 breq2d ⊢ ( 𝐵 = 𝐶 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ) )
134 133 notbid ⊢ ( 𝐵 = 𝐶 → ( ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ↔ ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐶 ) ) )
135 120 134 syl5ibrcom ⊢ ( 𝜑 → ( 𝐵 = 𝐶 → ¬ ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) ) )
136 135 necon2ad ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → 𝐵 ≠ 𝐶 ) )
137 136 32 jctild ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
138 22 2 ltlend ⊢ ( 𝜑 → ( 𝐶 < 𝐵 ↔ ( 𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ) )
139 137 138 sylibrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐶 ) < ( 𝐹 ‘ 𝐵 ) → 𝐶 < 𝐵 ) )
140 131 139 mpd ⊢ ( 𝜑 → 𝐶 < 𝐵 )
141 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
142 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
143 elioo2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
144 141 142 143 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 < 𝐶 ∧ 𝐶 < 𝐵 ) ) )
145 22 129 140 144 mpbir3and ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
146 145 118 jca ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐹 ‘ 𝐶 ) = 𝑈 ) )