Step | Hyp | Ref
| Expression |
1 | | ivth.7 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
2 | | ivth.5 |
. . . 4
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
3 | | ivthinclemlopn.q |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝐿) |
4 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑤 = 𝑄 → (𝐹‘𝑤) = (𝐹‘𝑄)) |
5 | 4 | breq1d 3999 |
. . . . . . 7
⊢ (𝑤 = 𝑄 → ((𝐹‘𝑤) < 𝑈 ↔ (𝐹‘𝑄) < 𝑈)) |
6 | | ivthinclem.l |
. . . . . . 7
⊢ 𝐿 = {𝑤 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑤) < 𝑈} |
7 | 5, 6 | elrab2 2889 |
. . . . . 6
⊢ (𝑄 ∈ 𝐿 ↔ (𝑄 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑄) < 𝑈)) |
8 | 3, 7 | sylib 121 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑄) < 𝑈)) |
9 | 8 | simpld 111 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ (𝐴[,]𝐵)) |
10 | 2, 9 | sseldd 3148 |
. . 3
⊢ (𝜑 → 𝑄 ∈ 𝐷) |
11 | | ivth.3 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ ℝ) |
12 | | fveq2 5496 |
. . . . . . 7
⊢ (𝑥 = 𝑄 → (𝐹‘𝑥) = (𝐹‘𝑄)) |
13 | 12 | eleq1d 2239 |
. . . . . 6
⊢ (𝑥 = 𝑄 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑄) ∈ ℝ)) |
14 | | ivth.8 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
15 | 14 | ralrimiva 2543 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
16 | 13, 15, 9 | rspcdva 2839 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑄) ∈ ℝ) |
17 | 11, 16 | resubcld 8300 |
. . . 4
⊢ (𝜑 → (𝑈 − (𝐹‘𝑄)) ∈ ℝ) |
18 | 8 | simprd 113 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑄) < 𝑈) |
19 | 16, 11 | posdifd 8451 |
. . . . 5
⊢ (𝜑 → ((𝐹‘𝑄) < 𝑈 ↔ 0 < (𝑈 − (𝐹‘𝑄)))) |
20 | 18, 19 | mpbid 146 |
. . . 4
⊢ (𝜑 → 0 < (𝑈 − (𝐹‘𝑄))) |
21 | 17, 20 | elrpd 9650 |
. . 3
⊢ (𝜑 → (𝑈 − (𝐹‘𝑄)) ∈
ℝ+) |
22 | | cncfi 13359 |
. . 3
⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝑄 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝑄)) ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
23 | 1, 10, 21, 22 | syl3anc 1233 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ ℝ+ ∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
24 | | ivth.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
25 | | ivth.2 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
26 | | elicc2 9895 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑄 ∈ (𝐴[,]𝐵) ↔ (𝑄 ∈ ℝ ∧ 𝐴 ≤ 𝑄 ∧ 𝑄 ≤ 𝐵))) |
27 | 24, 25, 26 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄 ∈ (𝐴[,]𝐵) ↔ (𝑄 ∈ ℝ ∧ 𝐴 ≤ 𝑄 ∧ 𝑄 ≤ 𝐵))) |
28 | 9, 27 | mpbid 146 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∈ ℝ ∧ 𝐴 ≤ 𝑄 ∧ 𝑄 ≤ 𝐵)) |
29 | 28 | simp1d 1004 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℝ) |
30 | 29 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑄 ∈ ℝ) |
31 | | simprl 526 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑑 ∈ ℝ+) |
32 | 31 | rphalfcld 9666 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑑 / 2) ∈
ℝ+) |
33 | 32 | rpred 9653 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑑 / 2) ∈ ℝ) |
34 | 30, 33 | readdcld 7949 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) ∈ ℝ) |
35 | 24 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝐴 ∈ ℝ) |
36 | 28 | simp2d 1005 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝑄) |
37 | 36 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝐴 ≤ 𝑄) |
38 | 30, 32 | ltaddrpd 9687 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑄 < (𝑄 + (𝑑 / 2))) |
39 | 30, 34, 38 | ltled 8038 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑄 ≤ (𝑄 + (𝑑 / 2))) |
40 | 35, 30, 34, 37, 39 | letrd 8043 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝐴 ≤ (𝑄 + (𝑑 / 2))) |
41 | 25 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝐵 ∈ ℝ) |
42 | 31 | rpred 9653 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑑 ∈ ℝ) |
43 | 30, 42 | readdcld 7949 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + 𝑑) ∈ ℝ) |
44 | | rphalflt 9640 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℝ+
→ (𝑑 / 2) < 𝑑) |
45 | 31, 44 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑑 / 2) < 𝑑) |
46 | 33, 42, 30, 45 | ltadd2dd 8341 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) < (𝑄 + 𝑑)) |
47 | 29 | ad2antrr 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑄 ∈ ℝ) |
48 | 31 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑑 ∈ ℝ+) |
49 | 48 | rpred 9653 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑑 ∈ ℝ) |
50 | 47, 49 | resubcld 8300 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝑄 − 𝑑) ∈ ℝ) |
51 | 25 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝐵 ∈ ℝ) |
52 | 47, 48 | ltsubrpd 9686 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝑄 − 𝑑) < 𝑄) |
53 | 28 | simp3d 1006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑄 ≤ 𝐵) |
54 | 53 | ad2antrr 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑄 ≤ 𝐵) |
55 | 50, 47, 51, 52, 54 | ltletrd 8342 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝑄 − 𝑑) < 𝐵) |
56 | | simpr 109 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝐵 < (𝑄 + 𝑑)) |
57 | 51, 47, 49 | absdifltd 11142 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ((abs‘(𝐵 − 𝑄)) < 𝑑 ↔ ((𝑄 − 𝑑) < 𝐵 ∧ 𝐵 < (𝑄 + 𝑑)))) |
58 | 55, 56, 57 | mpbir2and 939 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (abs‘(𝐵 − 𝑄)) < 𝑑) |
59 | | fvoveq1 5876 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝐵 → (abs‘(𝑧 − 𝑄)) = (abs‘(𝐵 − 𝑄))) |
60 | 59 | breq1d 3999 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝐵 → ((abs‘(𝑧 − 𝑄)) < 𝑑 ↔ (abs‘(𝐵 − 𝑄)) < 𝑑)) |
61 | 60 | imbrov2fvoveq 5878 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝐵 → (((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))) ↔ ((abs‘(𝐵 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝐵) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) |
62 | | simplrr 531 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
63 | 24 | rexrd 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
64 | 25 | rexrd 7969 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
65 | | ivth.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 < 𝐵) |
66 | 24, 25, 65 | ltled 8038 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
67 | | ubicc2 9942 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
68 | 63, 64, 66, 67 | syl3anc 1233 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
69 | 2, 68 | sseldd 3148 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
70 | 69 | ad2antrr 485 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝐵 ∈ 𝐷) |
71 | 61, 62, 70 | rspcdva 2839 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ((abs‘(𝐵 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝐵) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
72 | 58, 71 | mpd 13 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (abs‘((𝐹‘𝐵) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))) |
73 | | fveq2 5496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
74 | 73 | eleq1d 2239 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ)) |
75 | 15 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
76 | 68 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝐵 ∈ (𝐴[,]𝐵)) |
77 | 74, 75, 76 | rspcdva 2839 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘𝐵) ∈ ℝ) |
78 | 77 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝐹‘𝐵) ∈ ℝ) |
79 | 16 | ad2antrr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝐹‘𝑄) ∈ ℝ) |
80 | 17 | ad2antrr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝑈 − (𝐹‘𝑄)) ∈ ℝ) |
81 | 78, 79, 80 | absdifltd 11142 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ((abs‘((𝐹‘𝐵) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)) ↔ (((𝐹‘𝑄) − (𝑈 − (𝐹‘𝑄))) < (𝐹‘𝐵) ∧ (𝐹‘𝐵) < ((𝐹‘𝑄) + (𝑈 − (𝐹‘𝑄)))))) |
82 | 72, 81 | mpbid 146 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (((𝐹‘𝑄) − (𝑈 − (𝐹‘𝑄))) < (𝐹‘𝐵) ∧ (𝐹‘𝐵) < ((𝐹‘𝑄) + (𝑈 − (𝐹‘𝑄))))) |
83 | 82 | simprd 113 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝐹‘𝐵) < ((𝐹‘𝑄) + (𝑈 − (𝐹‘𝑄)))) |
84 | 79 | recnd 7948 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝐹‘𝑄) ∈ ℂ) |
85 | 11 | recnd 7948 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℂ) |
86 | 85 | ad2antrr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑈 ∈ ℂ) |
87 | 84, 86 | pncan3d 8233 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ((𝐹‘𝑄) + (𝑈 − (𝐹‘𝑄))) = 𝑈) |
88 | 83, 87 | breqtrd 4015 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → (𝐹‘𝐵) < 𝑈) |
89 | | ivth.9 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
90 | 89 | simprd 113 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑈 < (𝐹‘𝐵)) |
91 | 90 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑈 < (𝐹‘𝐵)) |
92 | 88, 91 | jca 304 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
93 | 11 | ad2antrr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → 𝑈 ∈ ℝ) |
94 | | ltnsym2 8010 |
. . . . . . . . . 10
⊢ (((𝐹‘𝐵) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ¬ ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
95 | 78, 93, 94 | syl2anc 409 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) ∧ 𝐵 < (𝑄 + 𝑑)) → ¬ ((𝐹‘𝐵) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
96 | 92, 95 | pm2.65da 656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ¬ 𝐵 < (𝑄 + 𝑑)) |
97 | 43, 41, 96 | nltled 8040 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + 𝑑) ≤ 𝐵) |
98 | 34, 43, 41, 46, 97 | ltletrd 8342 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) < 𝐵) |
99 | 34, 41, 98 | ltled 8038 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) ≤ 𝐵) |
100 | | elicc2 9895 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝑄 + (𝑑 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝑄 + (𝑑 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝑄 + (𝑑 / 2)) ∧ (𝑄 + (𝑑 / 2)) ≤ 𝐵))) |
101 | 35, 41, 100 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ((𝑄 + (𝑑 / 2)) ∈ (𝐴[,]𝐵) ↔ ((𝑄 + (𝑑 / 2)) ∈ ℝ ∧ 𝐴 ≤ (𝑄 + (𝑑 / 2)) ∧ (𝑄 + (𝑑 / 2)) ≤ 𝐵))) |
102 | 34, 40, 99, 101 | mpbir3and 1175 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) ∈ (𝐴[,]𝐵)) |
103 | 16 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘𝑄) ∈ ℝ) |
104 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑥 = (𝑄 + (𝑑 / 2)) → (𝐹‘𝑥) = (𝐹‘(𝑄 + (𝑑 / 2)))) |
105 | 104 | eleq1d 2239 |
. . . . . . . 8
⊢ (𝑥 = (𝑄 + (𝑑 / 2)) → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘(𝑄 + (𝑑 / 2))) ∈ ℝ)) |
106 | 105, 75, 102 | rspcdva 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘(𝑄 + (𝑑 / 2))) ∈ ℝ) |
107 | | breq2 3993 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑄 + (𝑑 / 2)) → (𝑄 < 𝑦 ↔ 𝑄 < (𝑄 + (𝑑 / 2)))) |
108 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑄 + (𝑑 / 2)) → (𝐹‘𝑦) = (𝐹‘(𝑄 + (𝑑 / 2)))) |
109 | 108 | breq2d 4001 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑄 + (𝑑 / 2)) → ((𝐹‘𝑄) < (𝐹‘𝑦) ↔ (𝐹‘𝑄) < (𝐹‘(𝑄 + (𝑑 / 2))))) |
110 | 107, 109 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑄 + (𝑑 / 2)) → ((𝑄 < 𝑦 → (𝐹‘𝑄) < (𝐹‘𝑦)) ↔ (𝑄 < (𝑄 + (𝑑 / 2)) → (𝐹‘𝑄) < (𝐹‘(𝑄 + (𝑑 / 2)))))) |
111 | | breq1 3992 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑄 → (𝑥 < 𝑦 ↔ 𝑄 < 𝑦)) |
112 | 12 | breq1d 3999 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑄 → ((𝐹‘𝑥) < (𝐹‘𝑦) ↔ (𝐹‘𝑄) < (𝐹‘𝑦))) |
113 | 111, 112 | imbi12d 233 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑄 → ((𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ (𝑄 < 𝑦 → (𝐹‘𝑄) < (𝐹‘𝑦)))) |
114 | 113 | ralbidv 2470 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑄 → (∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦)) ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(𝑄 < 𝑦 → (𝐹‘𝑄) < (𝐹‘𝑦)))) |
115 | | ivthinc.i |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) < (𝐹‘𝑦)) |
116 | 115 | expr 373 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
117 | 116 | ralrimiva 2543 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
118 | 117 | ralrimiva 2543 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)∀𝑦 ∈ (𝐴[,]𝐵)(𝑥 < 𝑦 → (𝐹‘𝑥) < (𝐹‘𝑦))) |
119 | 114, 118,
9 | rspcdva 2839 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑄 < 𝑦 → (𝐹‘𝑄) < (𝐹‘𝑦))) |
120 | 119 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ∀𝑦 ∈ (𝐴[,]𝐵)(𝑄 < 𝑦 → (𝐹‘𝑄) < (𝐹‘𝑦))) |
121 | 110, 120,
102 | rspcdva 2839 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 < (𝑄 + (𝑑 / 2)) → (𝐹‘𝑄) < (𝐹‘(𝑄 + (𝑑 / 2))))) |
122 | 38, 121 | mpd 13 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘𝑄) < (𝐹‘(𝑄 + (𝑑 / 2)))) |
123 | 103, 106,
122 | ltled 8038 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘𝑄) ≤ (𝐹‘(𝑄 + (𝑑 / 2)))) |
124 | 103, 106,
123 | abssubge0d 11140 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄))) = ((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄))) |
125 | 30 | recnd 7948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑄 ∈ ℂ) |
126 | 33 | recnd 7948 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑑 / 2) ∈ ℂ) |
127 | 125, 126 | pncan2d 8232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ((𝑄 + (𝑑 / 2)) − 𝑄) = (𝑑 / 2)) |
128 | 127 | fveq2d 5500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) = (abs‘(𝑑 / 2))) |
129 | 32 | rpge0d 9657 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 0 ≤ (𝑑 / 2)) |
130 | 33, 129 | absidd 11131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘(𝑑 / 2)) = (𝑑 / 2)) |
131 | 128, 130 | eqtrd 2203 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) = (𝑑 / 2)) |
132 | 131, 45 | eqbrtrd 4011 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) < 𝑑) |
133 | | fvoveq1 5876 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑄 + (𝑑 / 2)) → (abs‘(𝑧 − 𝑄)) = (abs‘((𝑄 + (𝑑 / 2)) − 𝑄))) |
134 | 133 | breq1d 3999 |
. . . . . . . . 9
⊢ (𝑧 = (𝑄 + (𝑑 / 2)) → ((abs‘(𝑧 − 𝑄)) < 𝑑 ↔ (abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) < 𝑑)) |
135 | 134 | imbrov2fvoveq 5878 |
. . . . . . . 8
⊢ (𝑧 = (𝑄 + (𝑑 / 2)) → (((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))) ↔ ((abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) < 𝑑 → (abs‘((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) |
136 | | simprr 527 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
137 | 2 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐴[,]𝐵) ⊆ 𝐷) |
138 | 137, 102 | sseldd 3148 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) ∈ 𝐷) |
139 | 135, 136,
138 | rspcdva 2839 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ((abs‘((𝑄 + (𝑑 / 2)) − 𝑄)) < 𝑑 → (abs‘((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄)))) |
140 | 132, 139 | mpd 13 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (abs‘((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))) |
141 | 124, 140 | eqbrtrrd 4013 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄)) < (𝑈 − (𝐹‘𝑄))) |
142 | 11 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → 𝑈 ∈ ℝ) |
143 | 106, 142,
103 | ltsub1d 8473 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ((𝐹‘(𝑄 + (𝑑 / 2))) < 𝑈 ↔ ((𝐹‘(𝑄 + (𝑑 / 2))) − (𝐹‘𝑄)) < (𝑈 − (𝐹‘𝑄)))) |
144 | 141, 143 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝐹‘(𝑄 + (𝑑 / 2))) < 𝑈) |
145 | | fveq2 5496 |
. . . . . 6
⊢ (𝑤 = (𝑄 + (𝑑 / 2)) → (𝐹‘𝑤) = (𝐹‘(𝑄 + (𝑑 / 2)))) |
146 | 145 | breq1d 3999 |
. . . . 5
⊢ (𝑤 = (𝑄 + (𝑑 / 2)) → ((𝐹‘𝑤) < 𝑈 ↔ (𝐹‘(𝑄 + (𝑑 / 2))) < 𝑈)) |
147 | 146, 6 | elrab2 2889 |
. . . 4
⊢ ((𝑄 + (𝑑 / 2)) ∈ 𝐿 ↔ ((𝑄 + (𝑑 / 2)) ∈ (𝐴[,]𝐵) ∧ (𝐹‘(𝑄 + (𝑑 / 2))) < 𝑈)) |
148 | 102, 144,
147 | sylanbrc 415 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → (𝑄 + (𝑑 / 2)) ∈ 𝐿) |
149 | | breq2 3993 |
. . . 4
⊢ (𝑟 = (𝑄 + (𝑑 / 2)) → (𝑄 < 𝑟 ↔ 𝑄 < (𝑄 + (𝑑 / 2)))) |
150 | 149 | rspcev 2834 |
. . 3
⊢ (((𝑄 + (𝑑 / 2)) ∈ 𝐿 ∧ 𝑄 < (𝑄 + (𝑑 / 2))) → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟) |
151 | 148, 38, 150 | syl2anc 409 |
. 2
⊢ ((𝜑 ∧ (𝑑 ∈ ℝ+ ∧
∀𝑧 ∈ 𝐷 ((abs‘(𝑧 − 𝑄)) < 𝑑 → (abs‘((𝐹‘𝑧) − (𝐹‘𝑄))) < (𝑈 − (𝐹‘𝑄))))) → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟) |
152 | 23, 151 | rexlimddv 2592 |
1
⊢ (𝜑 → ∃𝑟 ∈ 𝐿 𝑄 < 𝑟) |