| Step | Hyp | Ref
| Expression |
| 1 | | nfcv 2905 |
. . 3
⊢
Ⅎ𝑡(𝐷 / 2) |
| 2 | | stoweidlem52.3 |
. . 3
⊢
Ⅎ𝑡𝑃 |
| 3 | | stoweidlem52.2 |
. . 3
⊢
Ⅎ𝑡𝜑 |
| 4 | | stoweidlem52.4 |
. . 3
⊢ 𝐾 = (topGen‘ran
(,)) |
| 5 | | stoweidlem52.7 |
. . 3
⊢ 𝑇 = ∪
𝐽 |
| 6 | | stoweidlem52.5 |
. . 3
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} |
| 7 | | stoweidlem52.13 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
| 8 | 7 | rpred 13077 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 9 | 8 | rehalfcld 12513 |
. . . 4
⊢ (𝜑 → (𝐷 / 2) ∈ ℝ) |
| 10 | 9 | rexrd 11311 |
. . 3
⊢ (𝜑 → (𝐷 / 2) ∈
ℝ*) |
| 11 | | stoweidlem52.9 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
| 12 | | stoweidlem52.8 |
. . . . 5
⊢ 𝐶 = (𝐽 Cn 𝐾) |
| 13 | 11, 12 | sseqtrdi 4024 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (𝐽 Cn 𝐾)) |
| 14 | | stoweidlem52.17 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
| 15 | 13, 14 | sseldd 3984 |
. . 3
⊢ (𝜑 → 𝑃 ∈ (𝐽 Cn 𝐾)) |
| 16 | 1, 2, 3, 4, 5, 6, 10, 15 | rfcnpre2 45036 |
. 2
⊢ (𝜑 → 𝑉 ∈ 𝐽) |
| 17 | | stoweidlem52.15 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 18 | | elssuni 4937 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝐽 → 𝑈 ⊆ ∪ 𝐽) |
| 19 | 17, 18 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ⊆ ∪ 𝐽) |
| 20 | 19, 5 | sseqtrrdi 4025 |
. . . . . 6
⊢ (𝜑 → 𝑈 ⊆ 𝑇) |
| 21 | | stoweidlem52.16 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑈) |
| 22 | 20, 21 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ 𝑇) |
| 23 | | stoweidlem52.19 |
. . . . . 6
⊢ (𝜑 → (𝑃‘𝑍) = 0) |
| 24 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 25 | 24 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) |
| 26 | 7 | rpgt0d 13080 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝐷) |
| 27 | | 2pos 12369 |
. . . . . . . 8
⊢ 0 <
2 |
| 28 | 27 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 < 2) |
| 29 | 8, 25, 26, 28 | divgt0d 12203 |
. . . . . 6
⊢ (𝜑 → 0 < (𝐷 / 2)) |
| 30 | 23, 29 | eqbrtrd 5165 |
. . . . 5
⊢ (𝜑 → (𝑃‘𝑍) < (𝐷 / 2)) |
| 31 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑍 |
| 32 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑡𝑇 |
| 33 | 2, 31 | nffv 6916 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑃‘𝑍) |
| 34 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑡
< |
| 35 | 33, 34, 1 | nfbr 5190 |
. . . . . 6
⊢
Ⅎ𝑡(𝑃‘𝑍) < (𝐷 / 2) |
| 36 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑡 = 𝑍 → (𝑃‘𝑡) = (𝑃‘𝑍)) |
| 37 | 36 | breq1d 5153 |
. . . . . 6
⊢ (𝑡 = 𝑍 → ((𝑃‘𝑡) < (𝐷 / 2) ↔ (𝑃‘𝑍) < (𝐷 / 2))) |
| 38 | 31, 32, 35, 37 | elrabf 3688 |
. . . . 5
⊢ (𝑍 ∈ {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} ↔ (𝑍 ∈ 𝑇 ∧ (𝑃‘𝑍) < (𝐷 / 2))) |
| 39 | 22, 30, 38 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)}) |
| 40 | 39, 6 | eleqtrrdi 2852 |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
| 41 | | nfrab1 3457 |
. . . . 5
⊢
Ⅎ𝑡{𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} |
| 42 | 6, 41 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑡𝑉 |
| 43 | | stoweidlem52.1 |
. . . 4
⊢
Ⅎ𝑡𝑈 |
| 44 | 11, 14 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ 𝐶) |
| 45 | 4, 5, 12, 44 | fcnre 45030 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) |
| 46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑃:𝑇⟶ℝ) |
| 47 | 6 | reqabi 3460 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝑉 ↔ (𝑡 ∈ 𝑇 ∧ (𝑃‘𝑡) < (𝐷 / 2))) |
| 48 | 47 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ 𝑉 → (𝑡 ∈ 𝑇 ∧ (𝑃‘𝑡) < (𝐷 / 2))) |
| 49 | 48 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑡 ∈ 𝑇 ∧ (𝑃‘𝑡) < (𝐷 / 2))) |
| 50 | 49 | simpld 494 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑡 ∈ 𝑇) |
| 51 | 46, 50 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) ∈ ℝ) |
| 52 | 9 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐷 / 2) ∈ ℝ) |
| 53 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝐷 ∈ ℝ) |
| 54 | 49 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) < (𝐷 / 2)) |
| 55 | | halfpos 12496 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ ℝ → (0 <
𝐷 ↔ (𝐷 / 2) < 𝐷)) |
| 56 | 8, 55 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (0 < 𝐷 ↔ (𝐷 / 2) < 𝐷)) |
| 57 | 26, 56 | mpbid 232 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 / 2) < 𝐷) |
| 58 | 57 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝐷 / 2) < 𝐷) |
| 59 | 51, 52, 53, 54, 58 | lttrd 11422 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → (𝑃‘𝑡) < 𝐷) |
| 60 | 59 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → (𝑃‘𝑡) < 𝐷) |
| 61 | 8 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → 𝐷 ∈ ℝ) |
| 62 | 51 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → (𝑃‘𝑡) ∈ ℝ) |
| 63 | | stoweidlem52.20 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡)) |
| 64 | 63 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡)) |
| 65 | 50 | anim1i 615 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → (𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈)) |
| 66 | | eldif 3961 |
. . . . . . . . 9
⊢ (𝑡 ∈ (𝑇 ∖ 𝑈) ↔ (𝑡 ∈ 𝑇 ∧ ¬ 𝑡 ∈ 𝑈)) |
| 67 | 65, 66 | sylibr 234 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → 𝑡 ∈ (𝑇 ∖ 𝑈)) |
| 68 | | rsp 3247 |
. . . . . . . 8
⊢
(∀𝑡 ∈
(𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡) → (𝑡 ∈ (𝑇 ∖ 𝑈) → 𝐷 ≤ (𝑃‘𝑡))) |
| 69 | 64, 67, 68 | sylc 65 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → 𝐷 ≤ (𝑃‘𝑡)) |
| 70 | 61, 62, 69 | lensymd 11412 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑉) ∧ ¬ 𝑡 ∈ 𝑈) → ¬ (𝑃‘𝑡) < 𝐷) |
| 71 | 60, 70 | condan 818 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑉) → 𝑡 ∈ 𝑈) |
| 72 | 71 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑉 → 𝑡 ∈ 𝑈)) |
| 73 | 3, 42, 43, 72 | ssrd 3988 |
. . 3
⊢ (𝜑 → 𝑉 ⊆ 𝑈) |
| 74 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑡 𝑒 ∈
ℝ+ |
| 75 | 3, 74 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑡(𝜑 ∧ 𝑒 ∈ ℝ+) |
| 76 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑡 𝑦 ∈ 𝐴 |
| 77 | 75, 76 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑡((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) |
| 78 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) |
| 79 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) |
| 80 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑡∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒 |
| 81 | 78, 79, 80 | nf3an 1901 |
. . . . . . 7
⊢
Ⅎ𝑡(∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒) |
| 82 | 77, 81 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑡(((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) |
| 83 | | eqid 2737 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (1 − (𝑦‘𝑡))) |
| 84 | | eqid 2737 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ 1) = (𝑡 ∈ 𝑇 ↦ 1) |
| 85 | | ssrab2 4080 |
. . . . . . 7
⊢ {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} ⊆ 𝑇 |
| 86 | 6, 85 | eqsstri 4030 |
. . . . . 6
⊢ 𝑉 ⊆ 𝑇 |
| 87 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → 𝑦 ∈ 𝐴) |
| 88 | | simplll 775 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → 𝜑) |
| 89 | 11 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐶) |
| 90 | 4, 5, 12, 89 | fcnre 45030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝑦:𝑇⟶ℝ) |
| 91 | 88, 87, 90 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → 𝑦:𝑇⟶ℝ) |
| 92 | 11 | sselda 3983 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓 ∈ 𝐶) |
| 93 | 4, 5, 12, 92 | fcnre 45030 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 94 | 88, 93 | sylan 580 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 95 | | stoweidlem52.10 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 96 | 88, 95 | syl3an1 1164 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 97 | | stoweidlem52.11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 98 | 88, 97 | syl3an1 1164 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 99 | | stoweidlem52.12 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴) |
| 100 | 88, 99 | sylan 580 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴) |
| 101 | | simpllr 776 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → 𝑒 ∈ ℝ+) |
| 102 | | simpr1 1195 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1)) |
| 103 | | simpr2 1196 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡)) |
| 104 | | simpr3 1197 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒) |
| 105 | 82, 83, 84, 86, 87, 91, 94, 96, 98, 100, 101, 102, 103, 104 | stoweidlem41 46056 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑦 ∈ 𝐴) ∧ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) → ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))) |
| 106 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝐷 ∈
ℝ+) |
| 107 | | stoweidlem52.14 |
. . . . . . 7
⊢ (𝜑 → 𝐷 < 1) |
| 108 | 107 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝐷 < 1) |
| 109 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑃 ∈ 𝐴) |
| 110 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑃:𝑇⟶ℝ) |
| 111 | | stoweidlem52.18 |
. . . . . . 7
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
| 112 | 111 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
| 113 | 63 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡)) |
| 114 | 93 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 115 | 95 | 3adant1r 1178 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 116 | 97 | 3adant1r 1178 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 117 | 99 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ 𝑎 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑎) ∈ 𝐴) |
| 118 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) → 𝑒 ∈
ℝ+) |
| 119 | 2, 75, 6, 106, 108, 109, 110, 112, 113, 114, 115, 116, 117, 118 | stoweidlem49 46064 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝑒) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝑒)) |
| 120 | 105, 119 | r19.29a 3162 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))) |
| 121 | 120 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))) |
| 122 | 40, 73, 121 | jca31 514 |
. 2
⊢ (𝜑 → ((𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |
| 123 | | eleq2 2830 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝑍 ∈ 𝑣 ↔ 𝑍 ∈ 𝑉)) |
| 124 | | sseq1 4009 |
. . . . 5
⊢ (𝑣 = 𝑉 → (𝑣 ⊆ 𝑈 ↔ 𝑉 ⊆ 𝑈)) |
| 125 | 123, 124 | anbi12d 632 |
. . . 4
⊢ (𝑣 = 𝑉 → ((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ↔ (𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈))) |
| 126 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑡𝑣 |
| 127 | 126, 42 | raleqf 3353 |
. . . . . . 7
⊢ (𝑣 = 𝑉 → (∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ↔ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒)) |
| 128 | 127 | 3anbi2d 1443 |
. . . . . 6
⊢ (𝑣 = 𝑉 → ((∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)) ↔ (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |
| 129 | 128 | rexbidv 3179 |
. . . . 5
⊢ (𝑣 = 𝑉 → (∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)) ↔ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |
| 130 | 129 | ralbidv 3178 |
. . . 4
⊢ (𝑣 = 𝑉 → (∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)) ↔ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |
| 131 | 125, 130 | anbi12d 632 |
. . 3
⊢ (𝑣 = 𝑉 → (((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))) ↔ ((𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡))))) |
| 132 | 131 | rspcev 3622 |
. 2
⊢ ((𝑉 ∈ 𝐽 ∧ ((𝑍 ∈ 𝑉 ∧ 𝑉 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) → ∃𝑣 ∈ 𝐽 ((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |
| 133 | 16, 122, 132 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑣 ∈ 𝐽 ((𝑍 ∈ 𝑣 ∧ 𝑣 ⊆ 𝑈) ∧ ∀𝑒 ∈ ℝ+ ∃𝑥 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑥‘𝑡) ∧ (𝑥‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑣 (𝑥‘𝑡) < 𝑒 ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(1 − 𝑒) < (𝑥‘𝑡)))) |