Proof of Theorem stoweidlem40
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stoweidlem40.3 | . . 3
⊢ 𝑄 = (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀)) | 
| 2 |  | stoweidlem40.2 | . . . 4
⊢
Ⅎ𝑡𝜑 | 
| 3 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) | 
| 4 |  | 1red 11262 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℝ) | 
| 5 |  | stoweidlem40.8 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃:𝑇⟶ℝ) | 
| 6 | 5 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑃‘𝑡) ∈ ℝ) | 
| 7 |  | stoweidlem40.13 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 8 | 7 | nnnn0d 12587 | . . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 9 | 8 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑁 ∈
ℕ0) | 
| 10 | 6, 9 | reexpcld 14203 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑃‘𝑡)↑𝑁) ∈ ℝ) | 
| 11 | 4, 10 | resubcld 11691 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) | 
| 12 |  | stoweidlem40.4 | . . . . . . . 8
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) | 
| 13 | 12 | fvmpt2 7027 | . . . . . . 7
⊢ ((𝑡 ∈ 𝑇 ∧ (1 − ((𝑃‘𝑡)↑𝑁)) ∈ ℝ) → (𝐹‘𝑡) = (1 − ((𝑃‘𝑡)↑𝑁))) | 
| 14 | 3, 11, 13 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) = (1 − ((𝑃‘𝑡)↑𝑁))) | 
| 15 | 14 | eqcomd 2743 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) = (𝐹‘𝑡)) | 
| 16 | 15 | oveq1d 7446 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀) = ((𝐹‘𝑡)↑𝑀)) | 
| 17 | 2, 16 | mpteq2da 5240 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((1 − ((𝑃‘𝑡)↑𝑁))↑𝑀)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀))) | 
| 18 | 1, 17 | eqtrid 2789 | . 2
⊢ (𝜑 → 𝑄 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀))) | 
| 19 |  | nfmpt1 5250 | . . . 4
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) | 
| 20 | 12, 19 | nfcxfr 2903 | . . 3
⊢
Ⅎ𝑡𝐹 | 
| 21 |  | stoweidlem40.9 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) | 
| 22 |  | stoweidlem40.11 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) | 
| 23 |  | stoweidlem40.12 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) | 
| 24 |  | 1re 11261 | . . . . . . . . . 10
⊢ 1 ∈
ℝ | 
| 25 |  | stoweidlem40.5 | . . . . . . . . . . 11
⊢ 𝐺 = (𝑡 ∈ 𝑇 ↦ 1) | 
| 26 | 25 | fvmpt2 7027 | . . . . . . . . . 10
⊢ ((𝑡 ∈ 𝑇 ∧ 1 ∈ ℝ) → (𝐺‘𝑡) = 1) | 
| 27 | 24, 26 | mpan2 691 | . . . . . . . . 9
⊢ (𝑡 ∈ 𝑇 → (𝐺‘𝑡) = 1) | 
| 28 | 27 | eqcomd 2743 | . . . . . . . 8
⊢ (𝑡 ∈ 𝑇 → 1 = (𝐺‘𝑡)) | 
| 29 | 28 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 = (𝐺‘𝑡)) | 
| 30 |  | stoweidlem40.6 | . . . . . . . . . 10
⊢ 𝐻 = (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) | 
| 31 | 30 | fvmpt2 7027 | . . . . . . . . 9
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝑃‘𝑡)↑𝑁) ∈ ℝ) → (𝐻‘𝑡) = ((𝑃‘𝑡)↑𝑁)) | 
| 32 | 3, 10, 31 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐻‘𝑡) = ((𝑃‘𝑡)↑𝑁)) | 
| 33 | 32 | eqcomd 2743 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑃‘𝑡)↑𝑁) = (𝐻‘𝑡)) | 
| 34 | 29, 33 | oveq12d 7449 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (1 − ((𝑃‘𝑡)↑𝑁)) = ((𝐺‘𝑡) − (𝐻‘𝑡))) | 
| 35 | 2, 34 | mpteq2da 5240 | . . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (1 − ((𝑃‘𝑡)↑𝑁))) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡)))) | 
| 36 | 12, 35 | eqtrid 2789 | . . . 4
⊢ (𝜑 → 𝐹 = (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡)))) | 
| 37 | 23 | stoweidlem4 46019 | . . . . . . 7
⊢ ((𝜑 ∧ 1 ∈ ℝ) →
(𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) | 
| 38 | 24, 37 | mpan2 691 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) | 
| 39 | 25, 38 | eqeltrid 2845 | . . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝐴) | 
| 40 |  | stoweidlem40.1 | . . . . . . 7
⊢
Ⅎ𝑡𝑃 | 
| 41 |  | stoweidlem40.7 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ 𝐴) | 
| 42 | 40, 2, 21, 22, 23, 41, 8 | stoweidlem19 46034 | . . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) ∈ 𝐴) | 
| 43 | 30, 42 | eqeltrid 2845 | . . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝐴) | 
| 44 |  | nfmpt1 5250 | . . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ 1) | 
| 45 | 25, 44 | nfcxfr 2903 | . . . . . 6
⊢
Ⅎ𝑡𝐺 | 
| 46 |  | nfmpt1 5250 | . . . . . . 7
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝑃‘𝑡)↑𝑁)) | 
| 47 | 30, 46 | nfcxfr 2903 | . . . . . 6
⊢
Ⅎ𝑡𝐻 | 
| 48 |  | stoweidlem40.10 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) | 
| 49 | 45, 47, 2, 21, 48, 22, 23 | stoweidlem33 46048 | . . . . 5
⊢ ((𝜑 ∧ 𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡))) ∈ 𝐴) | 
| 50 | 39, 43, 49 | mpd3an23 1465 | . . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐺‘𝑡) − (𝐻‘𝑡))) ∈ 𝐴) | 
| 51 | 36, 50 | eqeltrd 2841 | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝐴) | 
| 52 |  | stoweidlem40.14 | . . . 4
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 53 | 52 | nnnn0d 12587 | . . 3
⊢ (𝜑 → 𝑀 ∈
ℕ0) | 
| 54 | 20, 2, 21, 22, 23, 51, 53 | stoweidlem19 46034 | . 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑀)) ∈ 𝐴) | 
| 55 | 18, 54 | eqeltrd 2841 | 1
⊢ (𝜑 → 𝑄 ∈ 𝐴) |