Step | Hyp | Ref
| Expression |
1 | | ivth.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
2 | | ivth.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | ivth.3 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ ℝ) |
4 | 3 | renegcld 10336 |
. . 3
⊢ (𝜑 → -𝑈 ∈ ℝ) |
5 | | ivth.4 |
. . 3
⊢ (𝜑 → 𝐴 < 𝐵) |
6 | | ivth.5 |
. . 3
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
7 | | ivth.7 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
8 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦)) = (𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦)) |
9 | 8 | negfcncf 22530 |
. . . 4
⊢ (𝐹 ∈ (𝐷–cn→ℂ) → (𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦)) ∈ (𝐷–cn→ℂ)) |
10 | 7, 9 | syl 17 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦)) ∈ (𝐷–cn→ℂ)) |
11 | 6 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ 𝐷) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
13 | 12 | negeqd 10154 |
. . . . . 6
⊢ (𝑦 = 𝑥 → -(𝐹‘𝑦) = -(𝐹‘𝑥)) |
14 | | negex 10158 |
. . . . . 6
⊢ -(𝐹‘𝑥) ∈ V |
15 | 13, 8, 14 | fvmpt 6191 |
. . . . 5
⊢ (𝑥 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑥) = -(𝐹‘𝑥)) |
16 | 11, 15 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑥) = -(𝐹‘𝑥)) |
17 | | ivth.8 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
18 | 17 | renegcld 10336 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → -(𝐹‘𝑥) ∈ ℝ) |
19 | 16, 18 | eqeltrd 2688 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑥) ∈ ℝ) |
20 | 1 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
21 | 2 | rexrd 9968 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
22 | 1, 2, 5 | ltled 10064 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
23 | | lbicc2 12159 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
24 | 20, 21, 22, 23 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
25 | 6, 24 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝐷) |
26 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝐹‘𝑦) = (𝐹‘𝐴)) |
27 | 26 | negeqd 10154 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → -(𝐹‘𝑦) = -(𝐹‘𝐴)) |
28 | | negex 10158 |
. . . . . . 7
⊢ -(𝐹‘𝐴) ∈ V |
29 | 27, 8, 28 | fvmpt 6191 |
. . . . . 6
⊢ (𝐴 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐴) = -(𝐹‘𝐴)) |
30 | 25, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐴) = -(𝐹‘𝐴)) |
31 | | ivth2.9 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐴))) |
32 | 31 | simprd 478 |
. . . . . 6
⊢ (𝜑 → 𝑈 < (𝐹‘𝐴)) |
33 | 17 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
34 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
35 | 34 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐴) ∈ ℝ)) |
36 | 35 | rspcv 3278 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐴) ∈ ℝ)) |
37 | 24, 33, 36 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
38 | 3, 37 | ltnegd 10484 |
. . . . . 6
⊢ (𝜑 → (𝑈 < (𝐹‘𝐴) ↔ -(𝐹‘𝐴) < -𝑈)) |
39 | 32, 38 | mpbid 221 |
. . . . 5
⊢ (𝜑 → -(𝐹‘𝐴) < -𝑈) |
40 | 30, 39 | eqbrtrd 4605 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐴) < -𝑈) |
41 | 31 | simpld 474 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐵) < 𝑈) |
42 | | ubicc2 12160 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
43 | 20, 21, 22, 42 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
44 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
45 | 44 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ)) |
46 | 45 | rspcv 3278 |
. . . . . . . 8
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐵) ∈ ℝ)) |
47 | 43, 33, 46 | sylc 63 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
48 | 47, 3 | ltnegd 10484 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝐵) < 𝑈 ↔ -𝑈 < -(𝐹‘𝐵))) |
49 | 41, 48 | mpbid 221 |
. . . . 5
⊢ (𝜑 → -𝑈 < -(𝐹‘𝐵)) |
50 | 6, 43 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
51 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐹‘𝑦) = (𝐹‘𝐵)) |
52 | 51 | negeqd 10154 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → -(𝐹‘𝑦) = -(𝐹‘𝐵)) |
53 | | negex 10158 |
. . . . . . 7
⊢ -(𝐹‘𝐵) ∈ V |
54 | 52, 8, 53 | fvmpt 6191 |
. . . . . 6
⊢ (𝐵 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐵) = -(𝐹‘𝐵)) |
55 | 50, 54 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐵) = -(𝐹‘𝐵)) |
56 | 49, 55 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → -𝑈 < ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐵)) |
57 | 40, 56 | jca 553 |
. . 3
⊢ (𝜑 → (((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐴) < -𝑈 ∧ -𝑈 < ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝐵))) |
58 | 1, 2, 4, 5, 6, 10,
19, 57 | ivth 23030 |
. 2
⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -𝑈) |
59 | | ioossicc 12130 |
. . . . . . . 8
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
60 | 59, 6 | syl5ss 3579 |
. . . . . . 7
⊢ (𝜑 → (𝐴(,)𝐵) ⊆ 𝐷) |
61 | 60 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑐 ∈ 𝐷) |
62 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑐 → (𝐹‘𝑦) = (𝐹‘𝑐)) |
63 | 62 | negeqd 10154 |
. . . . . . 7
⊢ (𝑦 = 𝑐 → -(𝐹‘𝑦) = -(𝐹‘𝑐)) |
64 | | negex 10158 |
. . . . . . 7
⊢ -(𝐹‘𝑐) ∈ V |
65 | 63, 8, 64 | fvmpt 6191 |
. . . . . 6
⊢ (𝑐 ∈ 𝐷 → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -(𝐹‘𝑐)) |
66 | 61, 65 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → ((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -(𝐹‘𝑐)) |
67 | 66 | eqeq1d 2612 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -𝑈 ↔ -(𝐹‘𝑐) = -𝑈)) |
68 | | cncff 22504 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐷–cn→ℂ) → 𝐹:𝐷⟶ℂ) |
69 | 7, 68 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐷⟶ℂ) |
70 | 69 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐷) → (𝐹‘𝑐) ∈ ℂ) |
71 | 61, 70 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (𝐹‘𝑐) ∈ ℂ) |
72 | 3 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ ℂ) |
73 | 72 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → 𝑈 ∈ ℂ) |
74 | 71, 73 | neg11ad 10267 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (-(𝐹‘𝑐) = -𝑈 ↔ (𝐹‘𝑐) = 𝑈)) |
75 | 67, 74 | bitrd 267 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ (𝐴(,)𝐵)) → (((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -𝑈 ↔ (𝐹‘𝑐) = 𝑈)) |
76 | 75 | rexbidva 3031 |
. 2
⊢ (𝜑 → (∃𝑐 ∈ (𝐴(,)𝐵)((𝑦 ∈ 𝐷 ↦ -(𝐹‘𝑦))‘𝑐) = -𝑈 ↔ ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈)) |
77 | 58, 76 | mpbid 221 |
1
⊢ (𝜑 → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) |