| Step | Hyp | Ref
| Expression |
| 1 | | breq2 5147 |
. . . . 5
⊢ (𝑗 = 𝑖 → ((1 / 𝐷) < 𝑗 ↔ (1 / 𝐷) < 𝑖)) |
| 2 | 1 | cbvrabv 3447 |
. . . 4
⊢ {𝑗 ∈ ℕ ∣ (1 /
𝐷) < 𝑗} = {𝑖 ∈ ℕ ∣ (1 / 𝐷) < 𝑖} |
| 3 | | stoweidlem49.4 |
. . . 4
⊢ (𝜑 → 𝐷 ∈
ℝ+) |
| 4 | | stoweidlem49.5 |
. . . 4
⊢ (𝜑 → 𝐷 < 1) |
| 5 | 2, 3, 4 | stoweidlem14 46029 |
. . 3
⊢ (𝜑 → ∃𝑘 ∈ ℕ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
↦ ((1 / (𝑘 ·
𝐷))↑𝑖)) = (𝑖 ∈ ℕ0 ↦ ((1 /
(𝑘 · 𝐷))↑𝑖)) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (𝑖 ∈ ℕ0
↦ (((𝑘 · 𝐷) / 2)↑𝑖)) = (𝑖 ∈ ℕ0 ↦ (((𝑘 · 𝐷) / 2)↑𝑖)) |
| 8 | | nnre 12273 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ) |
| 9 | 8 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ) |
| 10 | 3 | rpred 13077 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 11 | 10 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐷 ∈ ℝ) |
| 12 | 9, 11 | remulcld 11291 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑘 · 𝐷) ∈ ℝ) |
| 13 | 12 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → (𝑘 · 𝐷) ∈ ℝ) |
| 14 | | simprl 771 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → 1 < (𝑘 · 𝐷)) |
| 15 | 12 | rehalfcld 12513 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 · 𝐷) / 2) ∈ ℝ) |
| 16 | | nngt0 12297 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 0 <
𝑘) |
| 17 | 16 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝑘) |
| 18 | 3 | rpgt0d 13080 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < 𝐷) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < 𝐷) |
| 20 | 9, 11, 17, 19 | mulgt0d 11416 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < (𝑘 · 𝐷)) |
| 21 | | 2re 12340 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
| 22 | | 2pos 12369 |
. . . . . . . . . . 11
⊢ 0 <
2 |
| 23 | 21, 22 | pm3.2i 470 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (2 ∈ ℝ
∧ 0 < 2)) |
| 25 | | divgt0 12136 |
. . . . . . . . 9
⊢ ((((𝑘 · 𝐷) ∈ ℝ ∧ 0 < (𝑘 · 𝐷)) ∧ (2 ∈ ℝ ∧ 0 < 2))
→ 0 < ((𝑘 ·
𝐷) / 2)) |
| 26 | 12, 20, 24, 25 | syl21anc 838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 0 < ((𝑘 · 𝐷) / 2)) |
| 27 | 15, 26 | elrpd 13074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑘 · 𝐷) / 2) ∈
ℝ+) |
| 28 | 27 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → ((𝑘 · 𝐷) / 2) ∈
ℝ+) |
| 29 | | simprr 773 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → ((𝑘 · 𝐷) / 2) < 1) |
| 30 | | stoweidlem49.14 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
| 31 | 30 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → 𝐸 ∈
ℝ+) |
| 32 | 6, 7, 13, 14, 28, 29, 31 | stoweidlem7 46022 |
. . . . 5
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ) ∧ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1)) → ∃𝑛 ∈ ℕ ((1 −
𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) |
| 33 | 32 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1) → ∃𝑛 ∈ ℕ ((1 −
𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸))) |
| 34 | 33 | reximdva 3168 |
. . 3
⊢ (𝜑 → (∃𝑘 ∈ ℕ (1 < (𝑘 · 𝐷) ∧ ((𝑘 · 𝐷) / 2) < 1) → ∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ((1 −
𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸))) |
| 35 | 5, 34 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) |
| 36 | | stoweidlem49.1 |
. . . . 5
⊢
Ⅎ𝑡𝑃 |
| 37 | | stoweidlem49.2 |
. . . . . . 7
⊢
Ⅎ𝑡𝜑 |
| 38 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑘 ∈ ℕ ∧ 𝑛 ∈
ℕ) |
| 39 | 37, 38 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑡(𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) |
| 40 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑡((1 −
𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸) |
| 41 | 39, 40 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑡((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) |
| 42 | | stoweidlem49.3 |
. . . . 5
⊢ 𝑉 = {𝑡 ∈ 𝑇 ∣ (𝑃‘𝑡) < (𝐷 / 2)} |
| 43 | | eqid 2737 |
. . . . 5
⊢ (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑛))↑(𝑘↑𝑛))) = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑛))↑(𝑘↑𝑛))) |
| 44 | | simplrr 778 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝑛 ∈ ℕ) |
| 45 | | simplrl 777 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝑘 ∈ ℕ) |
| 46 | 3 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝐷 ∈
ℝ+) |
| 47 | 4 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝐷 < 1) |
| 48 | | stoweidlem49.6 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
| 49 | 48 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝑃 ∈ 𝐴) |
| 50 | | stoweidlem49.7 |
. . . . . 6
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) |
| 51 | 50 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝑃:𝑇⟶ℝ) |
| 52 | | stoweidlem49.8 |
. . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
| 53 | 52 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → ∀𝑡 ∈ 𝑇 (0 ≤ (𝑃‘𝑡) ∧ (𝑃‘𝑡) ≤ 1)) |
| 54 | | stoweidlem49.9 |
. . . . . 6
⊢ (𝜑 → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡)) |
| 55 | 54 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → ∀𝑡 ∈ (𝑇 ∖ 𝑈)𝐷 ≤ (𝑃‘𝑡)) |
| 56 | | stoweidlem49.10 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 57 | 56 | ad4ant14 752 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
| 58 | | simp1ll 1237 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → 𝜑) |
| 59 | | stoweidlem49.11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 60 | 58, 59 | syld3an1 1412 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
| 61 | | stoweidlem49.12 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 62 | 58, 61 | syld3an1 1412 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
| 63 | | stoweidlem49.13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 64 | 63 | ad4ant14 752 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
| 65 | 30 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → 𝐸 ∈
ℝ+) |
| 66 | | simprl 771 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → (1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛))) |
| 67 | | simprr 773 |
. . . . 5
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸) |
| 68 | 36, 41, 42, 43, 44, 45, 46, 47, 49, 51, 53, 55, 57, 60, 62, 64, 65, 66, 67 | stoweidlem45 46060 |
. . . 4
⊢ (((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) ∧ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸)) → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸)) |
| 69 | 68 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑘 ∈ ℕ ∧ 𝑛 ∈ ℕ)) → (((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸) → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸))) |
| 70 | 69 | rexlimdvva 3213 |
. 2
⊢ (𝜑 → (∃𝑘 ∈ ℕ ∃𝑛 ∈ ℕ ((1 − 𝐸) < (1 − (((𝑘 · 𝐷) / 2)↑𝑛)) ∧ (1 / ((𝑘 · 𝐷)↑𝑛)) < 𝐸) → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸))) |
| 71 | 35, 70 | mpd 15 |
1
⊢ (𝜑 → ∃𝑦 ∈ 𝐴 (∀𝑡 ∈ 𝑇 (0 ≤ (𝑦‘𝑡) ∧ (𝑦‘𝑡) ≤ 1) ∧ ∀𝑡 ∈ 𝑉 (1 − 𝐸) < (𝑦‘𝑡) ∧ ∀𝑡 ∈ (𝑇 ∖ 𝑈)(𝑦‘𝑡) < 𝐸)) |