Proof of Theorem stoweidlem40
Step | Hyp | Ref
| Expression |
1 | | stoweidlem40.3 |
. . 3
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀)) |
2 | | stoweidlem40.2 |
. . . 4
⊢
Ⅎ𝑡𝜑 |
3 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
4 | | 1red 9934 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℝ) |
5 | | stoweidlem40.8 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) |
6 | 5 | fnvinran 38196 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑃‘𝑡) ∈ ℝ) |
7 | | stoweidlem40.13 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) |
8 | 7 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈
ℕ0) |
10 | 6, 9 | reexpcld 12887 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑃‘𝑡)↑𝑁) ∈ ℝ) |
11 | 4, 10 | resubcld 10337 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) |
12 | | stoweidlem40.4 |
. . . . . . . 8
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) |
13 | 12 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑡 ∈ 𝑇 ∧ (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) → (𝐹‘𝑡) = (1 − ((𝑃‘𝑡)↑𝑁))) |
14 | 3, 11, 13 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = (1 − ((𝑃‘𝑡)↑𝑁))) |
15 | 14 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) = (𝐹‘𝑡)) |
16 | 15 | oveq1d 6564 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀) = ((𝐹‘𝑡)↑𝑀)) |
17 | 2, 16 | mpteq2da 4671 |
. . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀))) |
18 | 1, 17 | syl5eq 2656 |
. 2
⊢ (𝜑 → 𝑄 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀))) |
19 | | nfmpt1 4675 |
. . . 4
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) |
20 | 12, 19 | nfcxfr 2749 |
. . 3
⊢
Ⅎ𝑡𝐹 |
21 | | stoweidlem40.9 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
22 | | stoweidlem40.11 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
23 | | stoweidlem40.12 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
24 | | 1re 9918 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
25 | | stoweidlem40.5 |
. . . . . . . . . . 11
⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ 1) |
26 | 25 | fvmpt2 6200 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ) → (𝐺‘𝑡) = 1) |
27 | 24, 26 | mpan2 703 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝑇 → (𝐺‘𝑡) = 1) |
28 | 27 | eqcomd 2616 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝑇 → 1 = (𝐺‘𝑡)) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 = (𝐺‘𝑡)) |
30 | | stoweidlem40.6 |
. . . . . . . . . 10
⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) |
31 | 30 | fvmpt2 6200 |
. . . . . . . . 9
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝑃‘𝑡)↑𝑁) ∈ ℝ) → (𝐻‘𝑡) = ((𝑃‘𝑡)↑𝑁)) |
32 | 3, 10, 31 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) = ((𝑃‘𝑡)↑𝑁)) |
33 | 32 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑃‘𝑡)↑𝑁) = (𝐻‘𝑡)) |
34 | 29, 33 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) = ((𝐺‘𝑡) − (𝐻‘𝑡))) |
35 | 2, 34 | mpteq2da 4671 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡)))) |
36 | 12, 35 | syl5eq 2656 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡)))) |
37 | 23 | stoweidlem4 38897 |
. . . . . . 7
⊢ ((𝜑 ∧ 1 ∈ ℝ) →
(𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
38 | 24, 37 | mpan2 703 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) |
39 | 25, 38 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝐴) |
40 | | stoweidlem40.1 |
. . . . . . 7
⊢
Ⅎ𝑡𝑃 |
41 | | stoweidlem40.7 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
42 | 40, 2, 21, 22, 23, 41, 8 | stoweidlem19 38912 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) ∈ 𝐴) |
43 | 30, 42 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝐴) |
44 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 1) |
45 | 25, 44 | nfcxfr 2749 |
. . . . . 6
⊢
Ⅎ𝑡𝐺 |
46 | | nfmpt1 4675 |
. . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) |
47 | 30, 46 | nfcxfr 2749 |
. . . . . 6
⊢
Ⅎ𝑡𝐻 |
48 | | stoweidlem40.10 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
49 | 45, 47, 2, 21, 48, 22, 23 | stoweidlem33 38926 |
. . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡))) ∈ 𝐴) |
50 | 39, 43, 49 | mpd3an23 1418 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡))) ∈ 𝐴) |
51 | 36, 50 | eqeltrd 2688 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) |
52 | | stoweidlem40.14 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) |
53 | 52 | nnnn0d 11228 |
. . 3
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
54 | 20, 2, 21, 22, 23, 51, 53 | stoweidlem19 38912 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀)) ∈ 𝐴) |
55 | 18, 54 | eqeltrd 2688 |
1
⊢ (𝜑 → 𝑄 ∈ 𝐴) |