Proof of Theorem stoweidlem5
Step | Hyp | Ref
| Expression |
1 | | stoweidlem5.2 |
. . 3
⊢ 𝐷 = if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) |
2 | | stoweidlem5.5 |
. . . 4
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
3 | | halfre 11123 |
. . . . 5
⊢ (1 / 2)
∈ ℝ |
4 | | halfgt0 11125 |
. . . . 5
⊢ 0 < (1
/ 2) |
5 | 3, 4 | elrpii 11711 |
. . . 4
⊢ (1 / 2)
∈ ℝ+ |
6 | | ifcl 4080 |
. . . 4
⊢ ((𝐶 ∈ ℝ+
∧ (1 / 2) ∈ ℝ+) → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ∈
ℝ+) |
7 | 2, 5, 6 | sylancl 693 |
. . 3
⊢ (𝜑 → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ∈
ℝ+) |
8 | 1, 7 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
9 | 8 | rpred 11748 |
. . 3
⊢ (𝜑 → 𝐷 ∈ ℝ) |
10 | 3 | a1i 11 |
. . 3
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
11 | | 1red 9934 |
. . 3
⊢ (𝜑 → 1 ∈
ℝ) |
12 | 2 | rpred 11748 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
13 | | min2 11895 |
. . . . 5
⊢ ((𝐶 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → if(𝐶
≤ (1 / 2), 𝐶, (1 / 2))
≤ (1 / 2)) |
14 | 12, 3, 13 | sylancl 693 |
. . . 4
⊢ (𝜑 → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ≤ (1 / 2)) |
15 | 1, 14 | syl5eqbr 4618 |
. . 3
⊢ (𝜑 → 𝐷 ≤ (1 / 2)) |
16 | | halflt1 11127 |
. . . 4
⊢ (1 / 2)
< 1 |
17 | 16 | a1i 11 |
. . 3
⊢ (𝜑 → (1 / 2) <
1) |
18 | 9, 10, 11, 15, 17 | lelttrd 10074 |
. 2
⊢ (𝜑 → 𝐷 < 1) |
19 | | stoweidlem5.1 |
. . 3
⊢
Ⅎ𝑡𝜑 |
20 | 7 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ∈ ℝ) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ∈ ℝ) |
22 | 12 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → 𝐶 ∈ ℝ) |
23 | | stoweidlem5.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → 𝑃:𝑇⟶ℝ) |
25 | | stoweidlem5.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ⊆ 𝑇) |
26 | 25 | sselda 3568 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → 𝑡 ∈ 𝑇) |
27 | 24, 26 | ffvelrnd 6268 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → (𝑃‘𝑡) ∈ ℝ) |
28 | | min1 11894 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ (1 / 2)
∈ ℝ) → if(𝐶
≤ (1 / 2), 𝐶, (1 / 2))
≤ 𝐶) |
29 | 12, 3, 28 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ≤ 𝐶) |
30 | 29 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ≤ 𝐶) |
31 | | stoweidlem5.6 |
. . . . . . 7
⊢ (𝜑 → ∀𝑡 ∈ 𝑄 𝐶 ≤ (𝑃‘𝑡)) |
32 | 31 | r19.21bi 2916 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → 𝐶 ≤ (𝑃‘𝑡)) |
33 | 21, 22, 27, 30, 32 | letrd 10073 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → if(𝐶 ≤ (1 / 2), 𝐶, (1 / 2)) ≤ (𝑃‘𝑡)) |
34 | 1, 33 | syl5eqbr 4618 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑄) → 𝐷 ≤ (𝑃‘𝑡)) |
35 | 34 | ex 449 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑄 → 𝐷 ≤ (𝑃‘𝑡))) |
36 | 19, 35 | ralrimi 2940 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑄 𝐷 ≤ (𝑃‘𝑡)) |
37 | | eleq1 2676 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝑑 ∈ ℝ+ ↔ 𝐷 ∈
ℝ+)) |
38 | | breq1 4586 |
. . . . 5
⊢ (𝑑 = 𝐷 → (𝑑 < 1 ↔ 𝐷 < 1)) |
39 | | breq1 4586 |
. . . . . 6
⊢ (𝑑 = 𝐷 → (𝑑 ≤ (𝑃‘𝑡) ↔ 𝐷 ≤ (𝑃‘𝑡))) |
40 | 39 | ralbidv 2969 |
. . . . 5
⊢ (𝑑 = 𝐷 → (∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡) ↔ ∀𝑡 ∈ 𝑄 𝐷 ≤ (𝑃‘𝑡))) |
41 | 37, 38, 40 | 3anbi123d 1391 |
. . . 4
⊢ (𝑑 = 𝐷 → ((𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡)) ↔ (𝐷 ∈ ℝ+ ∧ 𝐷 < 1 ∧ ∀𝑡 ∈ 𝑄 𝐷 ≤ (𝑃‘𝑡)))) |
42 | 41 | spcegv 3267 |
. . 3
⊢ (𝐷 ∈ ℝ+
→ ((𝐷 ∈
ℝ+ ∧ 𝐷
< 1 ∧ ∀𝑡
∈ 𝑄 𝐷 ≤ (𝑃‘𝑡)) → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡)))) |
43 | 8, 42 | syl 17 |
. 2
⊢ (𝜑 → ((𝐷 ∈ ℝ+ ∧ 𝐷 < 1 ∧ ∀𝑡 ∈ 𝑄 𝐷 ≤ (𝑃‘𝑡)) → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡)))) |
44 | 8, 18, 36, 43 | mp3and 1419 |
1
⊢ (𝜑 → ∃𝑑(𝑑 ∈ ℝ+ ∧ 𝑑 < 1 ∧ ∀𝑡 ∈ 𝑄 𝑑 ≤ (𝑃‘𝑡))) |