Proof of Theorem stoweidlem41
Step | Hyp | Ref
| Expression |
1 | | stoweidlem41.1 |
. . . . 5
⊢
Ⅎ𝑡𝜑 |
2 | | 1re 10838 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
3 | | stoweidlem41.3 |
. . . . . . . . 9
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ 1) |
4 | 3 | fvmpt2 6834 |
. . . . . . . 8
⊢ ((𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ) → (𝐹‘𝑡) = 1) |
5 | 2, 4 | mpan2 691 |
. . . . . . 7
⊢ (𝑡 ∈ 𝑇 → (𝐹‘𝑡) = 1) |
6 | 5 | adantl 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = 1) |
7 | 6 | oveq1d 7233 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡) − (𝑦‘𝑡)) = (1 − (𝑦‘𝑡))) |
8 | 1, 7 | mpteq2da 5154 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝑦‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡)))) |
9 | | stoweidlem41.2 |
. . . 4
⊢ 𝑋 = (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡))) |
10 | 8, 9 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝑦‘𝑡))) = 𝑋) |
11 | | stoweidlem41.10 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑤) ∈ 𝐴) |
12 | 11 | stoweidlem4 43228 |
. . . . . 6
⊢ ((𝜑 ∧ 1 ∈ ℝ) →
(𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
13 | 2, 12 | mpan2 691 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
14 | 3, 13 | eqeltrid 2842 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
15 | | stoweidlem41.5 |
. . . 4
⊢ (𝜑 → 𝑦 ∈ 𝐴) |
16 | | nfmpt1 5158 |
. . . . . 6
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 1) |
17 | 3, 16 | nfcxfr 2902 |
. . . . 5
⊢
Ⅎ𝑡𝐹 |
18 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑡𝑦 |
19 | | stoweidlem41.7 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
20 | | stoweidlem41.8 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
21 | | stoweidlem41.9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
22 | 17, 18, 1, 19, 20, 21, 11 | stoweidlem33 43257 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝑦‘𝑡))) ∈ 𝐴) |
23 | 14, 15, 22 | mpd3an23 1465 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡) − (𝑦‘𝑡))) ∈ 𝐴) |
24 | 10, 23 | eqeltrrd 2839 |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
25 | | stoweidlem41.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑦:𝑇⟶ℝ) |
26 | 25 | ffvelrnda 6909 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑦‘𝑡) ∈ ℝ) |
27 | | 1red 10839 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℝ) |
28 | | 0red 10841 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ∈ ℝ) |
29 | | stoweidlem41.12 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)) |
30 | 29 | r19.21bi 3130 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)) |
31 | 30 | simprd 499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑦‘𝑡) ≤ 1) |
32 | | 1m0e1 11956 |
. . . . . . . 8
⊢ (1
− 0) = 1 |
33 | 31, 32 | breqtrrdi 5100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑦‘𝑡) ≤ (1 − 0)) |
34 | 26, 27, 28, 33 | lesubd 11441 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (1 − (𝑦‘𝑡))) |
35 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
36 | 27, 26 | resubcld 11265 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − (𝑦‘𝑡)) ∈ ℝ) |
37 | 9 | fvmpt2 6834 |
. . . . . . 7
⊢ ((𝑡 ∈ 𝑇 ∧ (1 − (𝑦‘𝑡)) ∈ ℝ) → (𝑋‘𝑡) = (1 − (𝑦‘𝑡))) |
38 | 35, 36, 37 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) = (1 − (𝑦‘𝑡))) |
39 | 34, 38 | breqtrrd 5086 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝑋‘𝑡)) |
40 | 30 | simpld 498 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 0 ≤ (𝑦‘𝑡)) |
41 | 28, 26, 27, 40 | lesub2dd 11454 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − (𝑦‘𝑡)) ≤ (1 − 0)) |
42 | 41, 32 | breqtrdi 5099 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − (𝑦‘𝑡)) ≤ 1) |
43 | 38, 42 | eqbrtrd 5080 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑋‘𝑡) ≤ 1) |
44 | 39, 43 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1)) |
45 | 44 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 → (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
46 | 1, 45 | ralrimi 3137 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1)) |
47 | | stoweidlem41.4 |
. . . . . . 7
⊢ 𝑉 ⊆ 𝑇 |
48 | 47 | sseli 3901 |
. . . . . 6
⊢ (𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑇) |
49 | 48, 38 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑋‘𝑡) = (1 − (𝑦‘𝑡))) |
50 | | 1red 10839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 1 ∈ ℝ) |
51 | | stoweidlem41.11 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
52 | 51 | rpred 12633 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℝ) |
53 | 52 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐸 ∈ ℝ) |
54 | 48, 26 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑦‘𝑡) ∈ ℝ) |
55 | | stoweidlem41.13 |
. . . . . . 7
⊢ (𝜑 → ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡)) |
56 | 55 | r19.21bi 3130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − 𝐸) < (𝑦‘𝑡)) |
57 | 50, 53, 54, 56 | ltsub23d 11442 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (1 − (𝑦‘𝑡)) < 𝐸) |
58 | 49, 57 | eqbrtrd 5080 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑋‘𝑡) < 𝐸) |
59 | 58 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑉 → (𝑋‘𝑡) < 𝐸)) |
60 | 1, 59 | ralrimi 3137 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ 𝑉 (𝑋‘𝑡) < 𝐸) |
61 | | eldifi 4046 |
. . . . . . 7
⊢ (𝑡 ∈ (𝑇 ∖ 𝑈) → 𝑡 ∈ 𝑇) |
62 | 61, 26 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑦‘𝑡) ∈ ℝ) |
63 | 52 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 𝐸 ∈ ℝ) |
64 | | 1red 10839 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → 1 ∈ ℝ) |
65 | | stoweidlem41.14 |
. . . . . . 7
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸) |
66 | 65 | r19.21bi 3130 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑦‘𝑡) < 𝐸) |
67 | 62, 63, 64, 66 | ltsub2dd 11450 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − 𝐸) < (1 − (𝑦‘𝑡))) |
68 | 61, 38 | sylan2 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (𝑋‘𝑡) = (1 − (𝑦‘𝑡))) |
69 | 67, 68 | breqtrrd 5086 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ (𝑇 ∖ 𝑈)) → (1 − 𝐸) < (𝑋‘𝑡)) |
70 | 69 | ex 416 |
. . 3
⊢ (𝜑 → (𝑡 ∈ (𝑇 ∖ 𝑈) → (1 − 𝐸) < (𝑋‘𝑡))) |
71 | 1, 70 | ralrimi 3137 |
. 2
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑋‘𝑡)) |
72 | | nfmpt1 5158 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡))) |
73 | 9, 72 | nfcxfr 2902 |
. . . . . 6
⊢
Ⅎ𝑡𝑋 |
74 | 73 | nfeq2 2921 |
. . . . 5
⊢
Ⅎ𝑡 𝑥 = 𝑋 |
75 | | fveq1 6721 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥‘𝑡) = (𝑋‘𝑡)) |
76 | 75 | breq2d 5070 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (0 ≤ (𝑥‘𝑡) ↔ 0 ≤ (𝑋‘𝑡))) |
77 | 75 | breq1d 5068 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((𝑥‘𝑡) ≤ 1 ↔ (𝑋‘𝑡) ≤ 1)) |
78 | 76, 77 | anbi12d 634 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ↔ (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
79 | 74, 78 | ralbid 3156 |
. . . 4
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ↔ ∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1))) |
80 | 75 | breq1d 5068 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥‘𝑡) < 𝐸 ↔ (𝑋‘𝑡) < 𝐸)) |
81 | 74, 80 | ralbid 3156 |
. . . 4
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ↔ ∀𝑡 ∈ 𝑉 (𝑋‘𝑡) < 𝐸)) |
82 | 75 | breq2d 5070 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((1 − 𝐸) < (𝑥‘𝑡) ↔ (1 − 𝐸) < (𝑋‘𝑡))) |
83 | 74, 82 | ralbid 3156 |
. . . 4
⊢ (𝑥 = 𝑋 → (∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡) ↔ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑋‘𝑡))) |
84 | 79, 81, 83 | 3anbi123d 1438 |
. . 3
⊢ (𝑥 = 𝑋 → ((∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑋‘𝑡)))) |
85 | 84 | rspcev 3542 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑋‘𝑡) ∧ (𝑋‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑋‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑋‘𝑡))) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡))) |
86 | 24, 46, 60, 71, 85 | syl13anc 1374 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝐸 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝐸) < (𝑥‘𝑡))) |