| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | stoweidlem19.7 | . 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | oveq2 7440 | . . . . . 6
⊢ (𝑛 = 0 → ((𝐹‘𝑡)↑𝑛) = ((𝐹‘𝑡)↑0)) | 
| 3 | 2 | mpteq2dv 5243 | . . . . 5
⊢ (𝑛 = 0 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑0))) | 
| 4 | 3 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 0 → ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑0)) ∈ 𝐴)) | 
| 5 | 4 | imbi2d 340 | . . 3
⊢ (𝑛 = 0 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑0)) ∈ 𝐴))) | 
| 6 |  | oveq2 7440 | . . . . . 6
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑡)↑𝑛) = ((𝐹‘𝑡)↑𝑚)) | 
| 7 | 6 | mpteq2dv 5243 | . . . . 5
⊢ (𝑛 = 𝑚 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))) | 
| 8 | 7 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 𝑚 → ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) | 
| 9 | 8 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑚 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴))) | 
| 10 |  | oveq2 7440 | . . . . . 6
⊢ (𝑛 = (𝑚 + 1) → ((𝐹‘𝑡)↑𝑛) = ((𝐹‘𝑡)↑(𝑚 + 1))) | 
| 11 | 10 | mpteq2dv 5243 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1)))) | 
| 12 | 11 | eleq1d 2825 | . . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) ∈ 𝐴)) | 
| 13 | 12 | imbi2d 340 | . . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) ∈ 𝐴))) | 
| 14 |  | oveq2 7440 | . . . . . 6
⊢ (𝑛 = 𝑁 → ((𝐹‘𝑡)↑𝑛) = ((𝐹‘𝑡)↑𝑁)) | 
| 15 | 14 | mpteq2dv 5243 | . . . . 5
⊢ (𝑛 = 𝑁 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁))) | 
| 16 | 15 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 𝑁 → ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁)) ∈ 𝐴)) | 
| 17 | 16 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑁 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑛)) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁)) ∈ 𝐴))) | 
| 18 |  | stoweidlem19.2 | . . . . 5
⊢
Ⅎ𝑡𝜑 | 
| 19 |  | stoweidlem19.6 | . . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ 𝐴) | 
| 20 | 19 | ancli 548 | . . . . . . . . 9
⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ 𝐴)) | 
| 21 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → (𝑓 ∈ 𝐴 ↔ 𝐹 ∈ 𝐴)) | 
| 22 | 21 | anbi2d 630 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ 𝐹 ∈ 𝐴))) | 
| 23 |  | feq1 6715 | . . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → (𝑓:𝑇⟶ℝ ↔ 𝐹:𝑇⟶ℝ)) | 
| 24 | 22, 23 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ 𝐹 ∈ 𝐴) → 𝐹:𝑇⟶ℝ))) | 
| 25 |  | stoweidlem19.3 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) | 
| 26 | 24, 25 | vtoclg 3553 | . . . . . . . . 9
⊢ (𝐹 ∈ 𝐴 → ((𝜑 ∧ 𝐹 ∈ 𝐴) → 𝐹:𝑇⟶ℝ)) | 
| 27 | 19, 20, 26 | sylc 65 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝑇⟶ℝ) | 
| 28 | 27 | ffvelcdmda 7103 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) | 
| 29 |  | recn 11246 | . . . . . . 7
⊢ ((𝐹‘𝑡) ∈ ℝ → (𝐹‘𝑡) ∈ ℂ) | 
| 30 |  | exp0 14107 | . . . . . . 7
⊢ ((𝐹‘𝑡) ∈ ℂ → ((𝐹‘𝑡)↑0) = 1) | 
| 31 | 28, 29, 30 | 3syl 18 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)↑0) = 1) | 
| 32 | 31 | eqcomd 2742 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 1 = ((𝐹‘𝑡)↑0)) | 
| 33 | 18, 32 | mpteq2da 5239 | . . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑0))) | 
| 34 |  | 1re 11262 | . . . . 5
⊢ 1 ∈
ℝ | 
| 35 |  | stoweidlem19.5 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) | 
| 36 | 35 | stoweidlem4 46024 | . . . . 5
⊢ ((𝜑 ∧ 1 ∈ ℝ) →
(𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) | 
| 37 | 34, 36 | mpan2 691 | . . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 1) ∈ 𝐴) | 
| 38 | 33, 37 | eqeltrrd 2841 | . . 3
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑0)) ∈ 𝐴) | 
| 39 |  | simpr 484 | . . . . 5
⊢ (((𝑚 ∈ ℕ0
∧ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → 𝜑) | 
| 40 |  | simpll 766 | . . . . 5
⊢ (((𝑚 ∈ ℕ0
∧ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → 𝑚 ∈ ℕ0) | 
| 41 |  | simplr 768 | . . . . . 6
⊢ (((𝑚 ∈ ℕ0
∧ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) | 
| 42 | 39, 41 | mpd 15 | . . . . 5
⊢ (((𝑚 ∈ ℕ0
∧ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) | 
| 43 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑡 𝑚 ∈
ℕ0 | 
| 44 |  | nfmpt1 5249 | . . . . . . . . 9
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) | 
| 45 | 44 | nfel1 2921 | . . . . . . . 8
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴 | 
| 46 | 18, 43, 45 | nf3an 1900 | . . . . . . 7
⊢
Ⅎ𝑡(𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) | 
| 47 |  | simpl1 1191 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝜑) | 
| 48 |  | simpr 484 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) | 
| 49 | 28 | recnd 11290 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) | 
| 50 | 47, 48, 49 | syl2anc 584 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℂ) | 
| 51 |  | simpl2 1192 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → 𝑚 ∈ ℕ0) | 
| 52 | 50, 51 | expp1d 14188 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)↑(𝑚 + 1)) = (((𝐹‘𝑡)↑𝑚) · (𝐹‘𝑡))) | 
| 53 | 46, 52 | mpteq2da 5239 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) = (𝑡 ∈ 𝑇 ↦ (((𝐹‘𝑡)↑𝑚) · (𝐹‘𝑡)))) | 
| 54 | 28 | 3adant2 1131 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇) → (𝐹‘𝑡) ∈ ℝ) | 
| 55 |  | simp2 1137 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇) → 𝑚 ∈ ℕ0) | 
| 56 | 54, 55 | reexpcld 14204 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)↑𝑚) ∈ ℝ) | 
| 57 | 47, 51, 48, 56 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)↑𝑚) ∈ ℝ) | 
| 58 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) | 
| 59 | 58 | fvmpt2 7026 | . . . . . . . . . . 11
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐹‘𝑡)↑𝑚) ∈ ℝ) → ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) = ((𝐹‘𝑡)↑𝑚)) | 
| 60 | 59 | eqcomd 2742 | . . . . . . . . . 10
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐹‘𝑡)↑𝑚) ∈ ℝ) → ((𝐹‘𝑡)↑𝑚) = ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡)) | 
| 61 | 48, 57, 60 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → ((𝐹‘𝑡)↑𝑚) = ((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡)) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) ∧ 𝑡 ∈ 𝑇) → (((𝐹‘𝑡)↑𝑚) · (𝐹‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) · (𝐹‘𝑡))) | 
| 63 | 46, 62 | mpteq2da 5239 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝐹‘𝑡)↑𝑚) · (𝐹‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) · (𝐹‘𝑡)))) | 
| 64 | 19 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → 𝐹 ∈ 𝐴) | 
| 65 | 44 | nfeq2 2922 | . . . . . . . . . 10
⊢
Ⅎ𝑡 𝑓 = (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) | 
| 66 |  | stoweidlem19.1 | . . . . . . . . . . 11
⊢
Ⅎ𝑡𝐹 | 
| 67 | 66 | nfeq2 2922 | . . . . . . . . . 10
⊢
Ⅎ𝑡 𝑔 = 𝐹 | 
| 68 |  | stoweidlem19.4 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) | 
| 69 | 65, 67, 68 | stoweidlem6 46026 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴 ∧ 𝐹 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) | 
| 70 | 64, 69 | mpd3an3 1463 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) | 
| 71 | 70 | 3adant2 1131 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚))‘𝑡) · (𝐹‘𝑡))) ∈ 𝐴) | 
| 72 | 63, 71 | eqeltrd 2840 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝐹‘𝑡)↑𝑚) · (𝐹‘𝑡))) ∈ 𝐴) | 
| 73 | 53, 72 | eqeltrd 2840 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) ∈ 𝐴) | 
| 74 | 39, 40, 42, 73 | syl3anc 1372 | . . . 4
⊢ (((𝑚 ∈ ℕ0
∧ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴)) ∧ 𝜑) → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) ∈ 𝐴) | 
| 75 | 74 | exp31 419 | . . 3
⊢ (𝑚 ∈ ℕ0
→ ((𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑚)) ∈ 𝐴) → (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑(𝑚 + 1))) ∈ 𝐴))) | 
| 76 | 5, 9, 13, 17, 38, 75 | nn0ind 12715 | . 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁)) ∈ 𝐴)) | 
| 77 | 1, 76 | mpcom 38 | 1
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ ((𝐹‘𝑡)↑𝑁)) ∈ 𝐴) |