Metamath Proof Explorer

Theorem ivth2

Description: The intermediate value theorem, decreasing case. (Contributed by Paul Chapman, 22-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypotheses ivth.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ivth.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ivth.3 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
ivth.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
ivth.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
ivth.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
ivth.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
ivth2.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐴 ) ) )
Assertion ivth2 ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )

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 ivth2.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐴 ) ) )
9 3 renegcld ⊢ ( 𝜑 → - 𝑈 ∈ ℝ )
10 eqid ⊢ ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) )
11 10 negfcncf ⊢ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) → ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ∈ ( 𝐷 –cn→ ℂ ) )
12 6 11 syl ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ∈ ( 𝐷 –cn→ ℂ ) )
13 5 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ 𝐷 )
14 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
15 14 negeqd ⊢ ( 𝑦 = 𝑥 → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑥 ) )
16 negex ⊢ - ( 𝐹 ‘ 𝑥 ) ∈ V
17 15 10 16 fvmpt ⊢ ( 𝑥 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
18 13 17 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑥 ) = - ( 𝐹 ‘ 𝑥 ) )
19 7 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → - ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
20 18 19 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ ℝ )
21 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
22 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
23 1 2 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
24 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
25 21 22 23 24 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
26 5 25 sseldd ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
27 fveq2 ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐴 ) )
28 27 negeqd ⊢ ( 𝑦 = 𝐴 → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝐴 ) )
29 negex ⊢ - ( 𝐹 ‘ 𝐴 ) ∈ V
30 28 10 29 fvmpt ⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
31 26 30 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) = - ( 𝐹 ‘ 𝐴 ) )
32 8 simprd ⊢ ( 𝜑 → 𝑈 < ( 𝐹 ‘ 𝐴 ) )
33 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
34 33 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) )
35 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
36 34 35 25 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
37 3 36 ltnegd ⊢ ( 𝜑 → ( 𝑈 < ( 𝐹 ‘ 𝐴 ) ↔ - ( 𝐹 ‘ 𝐴 ) < - 𝑈 ) )
38 32 37 mpbid ⊢ ( 𝜑 → - ( 𝐹 ‘ 𝐴 ) < - 𝑈 )
39 31 38 eqbrtrd ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) < - 𝑈 )
40 8 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) < 𝑈 )
41 fveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
42 41 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐵 ) ∈ ℝ ) )
43 ubicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
44 21 22 23 43 syl3anc ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 [,] 𝐵 ) )
45 42 35 44 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐵 ) ∈ ℝ )
46 45 3 ltnegd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐵 ) < 𝑈 ↔ - 𝑈 < - ( 𝐹 ‘ 𝐵 ) ) )
47 40 46 mpbid ⊢ ( 𝜑 → - 𝑈 < - ( 𝐹 ‘ 𝐵 ) )
48 5 44 sseldd ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
49 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
50 49 negeqd ⊢ ( 𝑦 = 𝐵 → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝐵 ) )
51 negex ⊢ - ( 𝐹 ‘ 𝐵 ) ∈ V
52 50 10 51 fvmpt ⊢ ( 𝐵 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) = - ( 𝐹 ‘ 𝐵 ) )
53 48 52 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) = - ( 𝐹 ‘ 𝐵 ) )
54 47 53 breqtrrd ⊢ ( 𝜑 → - 𝑈 < ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) )
55 39 54 jca ⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐴 ) < - 𝑈 ∧ - 𝑈 < ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝐵 ) ) )
56 1 2 9 4 5 12 20 55 ivth ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - 𝑈 )
57 ioossicc ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
58 57 5 sstrid ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
59 58 sselda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑐 ∈ 𝐷 )
60 fveq2 ⊢ ( 𝑦 = 𝑐 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑐 ) )
61 60 negeqd ⊢ ( 𝑦 = 𝑐 → - ( 𝐹 ‘ 𝑦 ) = - ( 𝐹 ‘ 𝑐 ) )
62 negex ⊢ - ( 𝐹 ‘ 𝑐 ) ∈ V
63 61 10 62 fvmpt ⊢ ( 𝑐 ∈ 𝐷 → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - ( 𝐹 ‘ 𝑐 ) )
64 59 63 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - ( 𝐹 ‘ 𝑐 ) )
65 64 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - 𝑈 ↔ - ( 𝐹 ‘ 𝑐 ) = - 𝑈 ) )
66 cncff ⊢ ( 𝐹 ∈ ( 𝐷 –cn→ ℂ ) → 𝐹 : 𝐷 ⟶ ℂ )
67 6 66 syl ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
68 67 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
69 59 68 syldan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
70 3 recnd ⊢ ( 𝜑 → 𝑈 ∈ ℂ )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → 𝑈 ∈ ℂ )
72 69 71 neg11ad ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( - ( 𝐹 ‘ 𝑐 ) = - 𝑈 ↔ ( 𝐹 ‘ 𝑐 ) = 𝑈 ) )
73 65 72 bitrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ) → ( ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - 𝑈 ↔ ( 𝐹 ‘ 𝑐 ) = 𝑈 ) )
74 73 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( ( 𝑦 ∈ 𝐷 ↦ - ( 𝐹 ‘ 𝑦 ) ) ‘ 𝑐 ) = - 𝑈 ↔ ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 ) )
75 56 74 mpbid ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 (,) 𝐵 ) ( 𝐹 ‘ 𝑐 ) = 𝑈 )