Step | Hyp | Ref
| Expression |
1 | | ivth.7 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐷–cn→ℂ)) |
2 | 1 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐹 ∈ (𝐷–cn→ℂ)) |
3 | | ivth.5 |
. . . . . 6
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ 𝐷) |
4 | | ivth.11 |
. . . . . . . 8
⊢ 𝐶 = sup(𝑆, ℝ, < ) |
5 | | ivth.10 |
. . . . . . . . . . . 12
⊢ 𝑆 = {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈} |
6 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑥 ∈ (𝐴[,]𝐵) ∣ (𝐹‘𝑥) ≤ 𝑈} ⊆ (𝐴[,]𝐵) |
7 | 5, 6 | eqsstri 3635 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆ (𝐴[,]𝐵) |
8 | | ivth.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | | ivth.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
10 | | iccssre 12255 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ) |
11 | 8, 9, 10 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ) |
12 | 7, 11 | syl5ss 3614 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℝ) |
13 | | ivth.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑈 ∈ ℝ) |
14 | | ivth.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 𝐵) |
15 | | ivth.8 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘𝑥) ∈ ℝ) |
16 | | ivth.9 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘𝐴) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵))) |
17 | 8, 9, 13, 14, 3, 1, 15, 16, 5 | ivthlem1 23220 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ 𝑆 ∧ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)) |
18 | 17 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑆) |
19 | | ne0i 3921 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑆 → 𝑆 ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ≠ ∅) |
21 | 17 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) |
22 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐵 → (𝑧 ≤ 𝑥 ↔ 𝑧 ≤ 𝐵)) |
23 | 22 | ralbidv 2986 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝐵 → (∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)) |
24 | 23 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧
∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵) → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) |
25 | 9, 21, 24 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) |
26 | 12, 20, 25 | 3jca 1242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥)) |
27 | | suprcl 10983 |
. . . . . . . . 9
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → sup(𝑆, ℝ, < ) ∈
ℝ) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → sup(𝑆, ℝ, < ) ∈
ℝ) |
29 | 4, 28 | syl5eqel 2705 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) |
30 | | suprub 10984 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐴 ∈ 𝑆) → 𝐴 ≤ sup(𝑆, ℝ, < )) |
31 | 26, 18, 30 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ sup(𝑆, ℝ, < )) |
32 | 31, 4 | syl6breqr 4695 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≤ 𝐶) |
33 | | suprleub 10989 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝐵 ∈ ℝ) → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)) |
34 | 26, 9, 33 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (sup(𝑆, ℝ, < ) ≤ 𝐵 ↔ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝐵)) |
35 | 21, 34 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → sup(𝑆, ℝ, < ) ≤ 𝐵) |
36 | 4, 35 | syl5eqbr 4688 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≤ 𝐵) |
37 | | elicc2 12238 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
38 | 8, 9, 37 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ (𝐴[,]𝐵) ↔ (𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐵))) |
39 | 29, 32, 36, 38 | mpbir3and 1245 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ (𝐴[,]𝐵)) |
40 | 3, 39 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
41 | 40 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → 𝐶 ∈ 𝐷) |
42 | 15 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
43 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝐶 → (𝐹‘𝑥) = (𝐹‘𝐶)) |
44 | 43 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐶) ∈ ℝ)) |
45 | 44 | rspcv 3305 |
. . . . . . 7
⊢ (𝐶 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐶) ∈ ℝ)) |
46 | 39, 42, 45 | sylc 65 |
. . . . . 6
⊢ (𝜑 → (𝐹‘𝐶) ∈ ℝ) |
47 | | difrp 11868 |
. . . . . 6
⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈
ℝ+)) |
48 | 46, 13, 47 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 ↔ (𝑈 − (𝐹‘𝐶)) ∈
ℝ+)) |
49 | 48 | biimpa 501 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝑈 − (𝐹‘𝐶)) ∈
ℝ+) |
50 | | cncfi 22697 |
. . . 4
⊢ ((𝐹 ∈ (𝐷–cn→ℂ) ∧ 𝐶 ∈ 𝐷 ∧ (𝑈 − (𝐹‘𝐶)) ∈ ℝ+) →
∃𝑧 ∈
ℝ+ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))) |
51 | 2, 41, 49, 50 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ∃𝑧 ∈ ℝ+ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)))) |
52 | | ssralv 3666 |
. . . . . . 7
⊢ ((𝐴[,]𝐵) ⊆ 𝐷 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))) |
53 | 3, 52 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))) |
54 | 53 | ad2antrr 762 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))))) |
55 | 9 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐵 ∈
ℝ) |
56 | 29 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 ∈
ℝ) |
57 | | rphalfcl 11858 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ (𝑧 / 2) ∈
ℝ+) |
58 | 57 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) ∈
ℝ+) |
59 | 58 | rpred 11872 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) ∈
ℝ) |
60 | 56, 59 | readdcld 10069 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + (𝑧 / 2)) ∈ ℝ) |
61 | 55, 60 | ifcld 4131 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ) |
62 | 8 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴 ∈
ℝ) |
63 | 32 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴 ≤ 𝐶) |
64 | 16 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 < (𝐹‘𝐵)) |
65 | 8 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
66 | 9 | rexrd 10089 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℝ*) |
67 | 8, 9, 14 | ltled 10185 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
68 | | ubicc2 12289 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ* ∧ 𝐴
≤ 𝐵) → 𝐵 ∈ (𝐴[,]𝐵)) |
69 | 65, 66, 67, 68 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
70 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
71 | 70 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝐵 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝐵) ∈ ℝ)) |
72 | 71 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝐵) ∈ ℝ)) |
73 | 69, 42, 72 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℝ) |
74 | | lttr 10114 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘𝐶) ∈ ℝ ∧ 𝑈 ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵))) |
75 | 46, 13, 73, 74 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐹‘𝐶) < 𝑈 ∧ 𝑈 < (𝐹‘𝐵)) → (𝐹‘𝐶) < (𝐹‘𝐵))) |
76 | 64, 75 | mpan2d 710 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝐶) < 𝑈 → (𝐹‘𝐶) < (𝐹‘𝐵))) |
77 | 76 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (𝐹‘𝐶) < (𝐹‘𝐵)) |
78 | 77 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐹‘𝐶) < (𝐹‘𝐵)) |
79 | 46 | ltnrd 10171 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ¬ (𝐹‘𝐶) < (𝐹‘𝐶)) |
80 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 = 𝐶 → (𝐹‘𝐵) = (𝐹‘𝐶)) |
81 | 80 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = 𝐶 → ((𝐹‘𝐶) < (𝐹‘𝐵) ↔ (𝐹‘𝐶) < (𝐹‘𝐶))) |
82 | 81 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 = 𝐶 → (¬ (𝐹‘𝐶) < (𝐹‘𝐵) ↔ ¬ (𝐹‘𝐶) < (𝐹‘𝐶))) |
83 | 79, 82 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 = 𝐶 → ¬ (𝐹‘𝐶) < (𝐹‘𝐵))) |
84 | 83 | necon2ad 2809 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐵 ≠ 𝐶)) |
85 | 84, 36 | jctild 566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶))) |
86 | 29, 9 | ltlend 10182 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 < 𝐵 ↔ (𝐶 ≤ 𝐵 ∧ 𝐵 ≠ 𝐶))) |
87 | 85, 86 | sylibrd 249 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵)) |
88 | 87 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → ((𝐹‘𝐶) < (𝐹‘𝐵) → 𝐶 < 𝐵)) |
89 | 78, 88 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < 𝐵) |
90 | 56, 58 | ltaddrpd 11905 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < (𝐶 + (𝑧 / 2))) |
91 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝐵 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝐵 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) |
92 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ ((𝐶 + (𝑧 / 2)) = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < (𝐶 + (𝑧 / 2)) ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) |
93 | 91, 92 | ifboth 4124 |
. . . . . . . . . . 11
⊢ ((𝐶 < 𝐵 ∧ 𝐶 < (𝐶 + (𝑧 / 2))) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))) |
94 | 89, 90, 93 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))) |
95 | 56, 61, 94 | ltled 10185 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐶 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))) |
96 | 62, 56, 61, 63, 95 | letrd 10194 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))) |
97 | | min1 12020 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵) |
98 | 55, 60, 97 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵) |
99 | | elicc2 12238 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) →
(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵))) |
100 | 8, 9, 99 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵))) |
101 | 100 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ↔ (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ ℝ ∧ 𝐴 ≤ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∧ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ 𝐵))) |
102 | 61, 96, 98, 101 | mpbir3and 1245 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵)) |
103 | 56, 61, 95 | abssubge0d 14170 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(abs‘(if(𝐵 ≤
(𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) |
104 | | rpre 11839 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ 𝑧 ∈
ℝ) |
105 | 104 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → 𝑧 ∈
ℝ) |
106 | 56, 105 | readdcld 10069 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + 𝑧) ∈ ℝ) |
107 | | min2 12021 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ (𝐶 + (𝑧 / 2)) ∈ ℝ) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2))) |
108 | 55, 60, 107 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ≤ (𝐶 + (𝑧 / 2))) |
109 | | rphalflt 11860 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℝ+
→ (𝑧 / 2) < 𝑧) |
110 | 109 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝑧 / 2) < 𝑧) |
111 | 59, 105, 56, 110 | ltadd2dd 10196 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (𝐶 + (𝑧 / 2)) < (𝐶 + 𝑧)) |
112 | 61, 60, 106, 108, 111 | lelttrd 10195 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧)) |
113 | 61, 56, 105 | ltsubadd2d 10625 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧 ↔ if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) < (𝐶 + 𝑧))) |
114 | 112, 113 | mpbird 247 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) → (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶) < 𝑧) |
115 | 103, 114 | eqbrtrd 4675 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(abs‘(if(𝐵 ≤
(𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧) |
116 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝑦 − 𝐶) = (if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) |
117 | 116 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (abs‘(𝑦 − 𝐶)) = (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶))) |
118 | 117 | breq1d 4663 |
. . . . . . . . 9
⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → ((abs‘(𝑦 − 𝐶)) < 𝑧 ↔ (abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧)) |
119 | | breq2 4657 |
. . . . . . . . 9
⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (𝐶 < 𝑦 ↔ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) |
120 | 118, 119 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑦 = if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) ↔ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2)))))) |
121 | 120 | rspcev 3309 |
. . . . . . 7
⊢
((if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) ∈ (𝐴[,]𝐵) ∧ ((abs‘(if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))) − 𝐶)) < 𝑧 ∧ 𝐶 < if(𝐵 ≤ (𝐶 + (𝑧 / 2)), 𝐵, (𝐶 + (𝑧 / 2))))) → ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) |
122 | 102, 115,
94, 121 | syl12anc 1324 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) |
123 | | r19.29 3072 |
. . . . . . 7
⊢
((∀𝑦 ∈
(𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦))) |
124 | | pm3.45 879 |
. . . . . . . . . 10
⊢
(((abs‘(𝑦
− 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → (((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦))) |
125 | 124 | imp 445 |
. . . . . . . . 9
⊢
((((abs‘(𝑦
− 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦)) |
126 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 < 𝑦) |
127 | | simprl 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ (𝐴[,]𝐵)) |
128 | | simplll 798 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝜑) |
129 | 128, 42 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ) |
130 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
131 | 130 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ∈ ℝ ↔ (𝐹‘𝑦) ∈ ℝ)) |
132 | 131 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝐴[,]𝐵) → (∀𝑥 ∈ (𝐴[,]𝐵)(𝐹‘𝑥) ∈ ℝ → (𝐹‘𝑦) ∈ ℝ)) |
133 | 127, 129,
132 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝑦) ∈ ℝ) |
134 | 128, 46 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℝ) |
135 | 128, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℝ) |
136 | 135, 134 | resubcld 10458 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑈 − (𝐹‘𝐶)) ∈ ℝ) |
137 | 133, 134,
136 | absdifltd 14172 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ↔ (((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶)))))) |
138 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹‘𝑦) ∈ ℝ ∧ 𝑈 ∈ ℝ) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈)) |
139 | 133, 135,
138 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < 𝑈 → (𝐹‘𝑦) ≤ 𝑈)) |
140 | 134 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐹‘𝐶) ∈ ℂ) |
141 | 135 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑈 ∈ ℂ) |
142 | 140, 141 | pncan3d 10395 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) = 𝑈) |
143 | 142 | breq2d 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) ↔ (𝐹‘𝑦) < 𝑈)) |
144 | 130 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) ≤ 𝑈 ↔ (𝐹‘𝑦) ≤ 𝑈)) |
145 | 144, 5 | elrab2 3366 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑆 ↔ (𝑦 ∈ (𝐴[,]𝐵) ∧ (𝐹‘𝑦) ≤ 𝑈)) |
146 | 145 | baib 944 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝐴[,]𝐵) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈)) |
147 | 146 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 ↔ (𝐹‘𝑦) ≤ 𝑈)) |
148 | 139, 143,
147 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → 𝑦 ∈ 𝑆)) |
149 | | suprub 10984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ sup(𝑆, ℝ, < )) |
150 | 149, 4 | syl6breqr 4695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) ∧ 𝑦 ∈ 𝑆) → 𝑦 ≤ 𝐶) |
151 | 150 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑆 ⊆ ℝ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ 𝑆 𝑧 ≤ 𝑥) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶)) |
152 | 128, 26, 151 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → 𝑦 ≤ 𝐶)) |
153 | 128, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝐴[,]𝐵) ⊆ ℝ) |
154 | 153, 127 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝑦 ∈ ℝ) |
155 | 128, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → 𝐶 ∈ ℝ) |
156 | 154, 155 | lenltd 10183 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ≤ 𝐶 ↔ ¬ 𝐶 < 𝑦)) |
157 | 152, 156 | sylibd 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → (𝑦 ∈ 𝑆 → ¬ 𝐶 < 𝑦)) |
158 | 148, 157 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶))) → ¬ 𝐶 < 𝑦)) |
159 | 158 | adantld 483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((((𝐹‘𝐶) − (𝑈 − (𝐹‘𝐶))) < (𝐹‘𝑦) ∧ (𝐹‘𝑦) < ((𝐹‘𝐶) + (𝑈 − (𝐹‘𝐶)))) → ¬ 𝐶 < 𝑦)) |
160 | 137, 159 | sylbid 230 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ 𝐶 < 𝑦)) |
161 | 126, 160 | mt2d 131 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ¬ (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) |
162 | 161 | pm2.21d 118 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ (𝑦 ∈ (𝐴[,]𝐵) ∧ 𝐶 < 𝑦)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈)) |
163 | 162 | expr 643 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐶 < 𝑦 → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → ¬ (𝐹‘𝐶) < 𝑈))) |
164 | 163 | com23 86 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) → (𝐶 < 𝑦 → ¬ (𝐹‘𝐶) < 𝑈))) |
165 | 164 | impd 447 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (((abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶)) ∧ 𝐶 < 𝑦) → ¬ (𝐹‘𝐶) < 𝑈)) |
166 | 125, 165 | syl5 34 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) ∧ 𝑦 ∈ (𝐴[,]𝐵)) → ((((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈)) |
167 | 166 | rexlimdva 3031 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(∃𝑦 ∈ (𝐴[,]𝐵)(((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈)) |
168 | 123, 167 | syl5 34 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
((∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) ∧ ∃𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 ∧ 𝐶 < 𝑦)) → ¬ (𝐹‘𝐶) < 𝑈)) |
169 | 122, 168 | mpan2d 710 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(∀𝑦 ∈ (𝐴[,]𝐵)((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈)) |
170 | 54, 169 | syld 47 |
. . . 4
⊢ (((𝜑 ∧ (𝐹‘𝐶) < 𝑈) ∧ 𝑧 ∈ ℝ+) →
(∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈)) |
171 | 170 | rexlimdva 3031 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → (∃𝑧 ∈ ℝ+ ∀𝑦 ∈ 𝐷 ((abs‘(𝑦 − 𝐶)) < 𝑧 → (abs‘((𝐹‘𝑦) − (𝐹‘𝐶))) < (𝑈 − (𝐹‘𝐶))) → ¬ (𝐹‘𝐶) < 𝑈)) |
172 | 51, 171 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝐶) < 𝑈) → ¬ (𝐹‘𝐶) < 𝑈) |
173 | 172 | pm2.01da 458 |
1
⊢ (𝜑 → ¬ (𝐹‘𝐶) < 𝑈) |