Proof of Theorem ivthle
Step | Hyp | Ref
| Expression |
1 | | ioossicc 12130 |
. . . . 5
⊢ (𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) |
2 | | ivth.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → 𝐴 ∈ ℝ) |
4 | | ivth.2 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) |
5 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → 𝐵 ∈ ℝ) |
6 | | ivth.3 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ ℝ) |
7 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → 𝑈 ∈ ℝ) |
8 | | ivth.4 |
. . . . . . 7
⊢ (𝜑 → 𝐴 < 𝐵) |
9 | 8 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → 𝐴 < 𝐵) |
10 | | ivth.5 |
. . . . . . 7
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
11 | 10 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → (𝐴[,]𝐵) ⊆ 𝐷) |
12 | | ivth.7 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
13 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → 𝐹 ∈ (𝐷–cn→ℂ)) |
14 | | ivth.8 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
15 | 14 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
16 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
17 | 3, 5, 7, 9, 11, 13, 15, 16 | ivth 23030 |
. . . . 5
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → ∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈) |
18 | | ssrexv 3630 |
. . . . 5
⊢ ((𝐴(,)𝐵) ⊆ (𝐴[,]𝐵) → (∃𝑐 ∈ (𝐴(,)𝐵)(𝐹‘𝑐) = 𝑈 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈)) |
19 | 1, 17, 18 | mpsyl 66 |
. . . 4
⊢ ((𝜑 ∧ ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
20 | 19 | anassrs 678 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝐴) < 𝑈) ∧ 𝑈 < (𝐹‘𝐵)) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
21 | 2 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
22 | 4 | rexrd 9968 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
23 | 2, 4, 8 | ltled 10064 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
24 | | ubicc2 12160 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
25 | 21, 22, 23, 24 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
26 | | eqcom 2617 |
. . . . . . 7
⊢ ((𝐹‘𝑐) = 𝑈 ↔ 𝑈 = (𝐹‘𝑐)) |
27 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑐 = 𝐵 → (𝐹‘𝑐) = (𝐹‘𝐵)) |
28 | 27 | eqeq2d 2620 |
. . . . . . 7
⊢ (𝑐 = 𝐵 → (𝑈 = (𝐹‘𝑐) ↔ 𝑈 = (𝐹‘𝐵))) |
29 | 26, 28 | syl5bb 271 |
. . . . . 6
⊢ (𝑐 = 𝐵 → ((𝐹‘𝑐) = 𝑈 ↔ 𝑈 = (𝐹‘𝐵))) |
30 | 29 | rspcev 3282 |
. . . . 5
⊢ ((𝐵 ∈ (𝐴[,]𝐵) ∧ 𝑈 = (𝐹‘𝐵)) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
31 | 25, 30 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝑈 = (𝐹‘𝐵)) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
32 | 31 | adantlr 747 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝐴) < 𝑈) ∧ 𝑈 = (𝐹‘𝐵)) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
33 | | ivthle.9 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ∧ 𝑈 ≤ (𝐹‘𝐵))) |
34 | 33 | simprd 478 |
. . . . 5
⊢ (𝜑 → 𝑈 ≤ (𝐹‘𝐵)) |
35 | 14 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
36 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
37 | 36 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ)) |
38 | 37 | rspcv 3278 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐵) ∈ ℝ)) |
39 | 25, 35, 38 | sylc 63 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
40 | 6, 39 | leloed 10059 |
. . . . 5
⊢ (𝜑 → (𝑈 ≤ (𝐹‘𝐵) ↔ (𝑈 < (𝐹‘𝐵) ∨ 𝑈 = (𝐹‘𝐵)))) |
41 | 34, 40 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑈 < (𝐹‘𝐵) ∨ 𝑈 = (𝐹‘𝐵))) |
42 | 41 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐴) < 𝑈) → (𝑈 < (𝐹‘𝐵) ∨ 𝑈 = (𝐹‘𝐵))) |
43 | 20, 32, 42 | mpjaodan 823 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐴) < 𝑈) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
44 | | lbicc2 12159 |
. . . 4
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐴 ∈ (𝐴[,]𝐵)) |
45 | 21, 22, 23, 44 | syl3anc 1318 |
. . 3
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
46 | | fveq2 6103 |
. . . . 5
⊢ (𝑐 = 𝐴 → (𝐹‘𝑐) = (𝐹‘𝐴)) |
47 | 46 | eqeq1d 2612 |
. . . 4
⊢ (𝑐 = 𝐴 → ((𝐹‘𝑐) = 𝑈 ↔ (𝐹‘𝐴) = 𝑈)) |
48 | 47 | rspcev 3282 |
. . 3
⊢ ((𝐴 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝐴) = 𝑈) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
49 | 45, 48 | sylan 487 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐴) = 𝑈) → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |
50 | 33 | simpld 474 |
. . 3
⊢ (𝜑 → (𝐹‘𝐴) ≤ 𝑈) |
51 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
52 | 51 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐴) ∈ ℝ)) |
53 | 52 | rspcv 3278 |
. . . . 5
⊢ (𝐴 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐴) ∈ ℝ)) |
54 | 45, 35, 53 | sylc 63 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐴) ∈ ℝ) |
55 | 54, 6 | leloed 10059 |
. . 3
⊢ (𝜑 → ((𝐹‘𝐴) ≤ 𝑈 ↔ ((𝐹‘𝐴) < 𝑈 ∨ (𝐹‘𝐴) = 𝑈))) |
56 | 50, 55 | mpbid 221 |
. 2
⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∨ (𝐹‘𝐴) = 𝑈)) |
57 | 43, 49, 56 | mpjaodan 823 |
1
⊢ (𝜑 → ∃𝑐 ∈ (𝐴[,]𝐵)(𝐹‘𝑐) = 𝑈) |