Proof of Theorem expsp1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eln0s 28359 | . 2
⊢ (𝑁 ∈ ℕ0s
↔ (𝑁 ∈
ℕs ∨ 𝑁
= 0s )) | 
| 2 |  | 1sno 27873 | . . . . . . 7
⊢ 
1s ∈  No | 
| 3 | 2 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → 1s ∈  No
) | 
| 4 |  | dfnns2 28363 | . . . . . . 7
⊢
ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω) | 
| 5 | 4 | a1i 11 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → ℕs = (rec((𝑥 ∈ V ↦ (𝑥 +s 1s )),
1s ) “ ω)) | 
| 6 |  | simpr 484 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → 𝑁 ∈
ℕs) | 
| 7 | 3, 5, 6 | seqsp1 28318 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → (seqs 1s (
·s , (ℕs × {𝐴}))‘(𝑁 +s 1s )) =
((seqs 1s ( ·s , (ℕs
× {𝐴}))‘𝑁) ·s
((ℕs × {𝐴})‘(𝑁 +s 1s
)))) | 
| 8 |  | peano2nns 28354 | . . . . . . 7
⊢ (𝑁 ∈ ℕs
→ (𝑁 +s
1s ) ∈ ℕs) | 
| 9 |  | fvconst2g 7223 | . . . . . . 7
⊢ ((𝐴 ∈ 
No  ∧ (𝑁
+s 1s ) ∈ ℕs) →
((ℕs × {𝐴})‘(𝑁 +s 1s )) = 𝐴) | 
| 10 | 8, 9 | sylan2 593 | . . . . . 6
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → ((ℕs × {𝐴})‘(𝑁 +s 1s )) = 𝐴) | 
| 11 | 10 | oveq2d 7448 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → ((seqs 1s (
·s , (ℕs × {𝐴}))‘𝑁) ·s ((ℕs
× {𝐴})‘(𝑁 +s 1s )))
= ((seqs 1s ( ·s , (ℕs
× {𝐴}))‘𝑁) ·s 𝐴)) | 
| 12 | 7, 11 | eqtrd 2776 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → (seqs 1s (
·s , (ℕs × {𝐴}))‘(𝑁 +s 1s )) =
((seqs 1s ( ·s , (ℕs
× {𝐴}))‘𝑁) ·s 𝐴)) | 
| 13 |  | expsnnval 28410 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ (𝑁
+s 1s ) ∈ ℕs) → (𝐴↑s(𝑁 +s 1s ))
= (seqs 1s ( ·s , (ℕs
× {𝐴}))‘(𝑁 +s 1s
))) | 
| 14 | 8, 13 | sylan2 593 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → (𝐴↑s(𝑁 +s 1s )) =
(seqs 1s ( ·s , (ℕs
× {𝐴}))‘(𝑁 +s 1s
))) | 
| 15 |  | expsnnval 28410 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → (𝐴↑s𝑁) = (seqs 1s (
·s , (ℕs × {𝐴}))‘𝑁)) | 
| 16 | 15 | oveq1d 7447 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → ((𝐴↑s𝑁) ·s 𝐴) = ((seqs 1s (
·s , (ℕs × {𝐴}))‘𝑁) ·s 𝐴)) | 
| 17 | 12, 14, 16 | 3eqtr4d 2786 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕs) → (𝐴↑s(𝑁 +s 1s )) = ((𝐴↑s𝑁) ·s 𝐴)) | 
| 18 |  | mulslid 28169 | . . . . 5
⊢ (𝐴 ∈ 
No  → ( 1s ·s 𝐴) = 𝐴) | 
| 19 | 18 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 =
0s ) → ( 1s ·s 𝐴) = 𝐴) | 
| 20 |  | oveq2 7440 | . . . . . 6
⊢ (𝑁 = 0s → (𝐴↑s𝑁) = (𝐴↑s 0s
)) | 
| 21 |  | exps0 28411 | . . . . . 6
⊢ (𝐴 ∈ 
No  → (𝐴↑s 0s ) =
1s ) | 
| 22 | 20, 21 | sylan9eqr 2798 | . . . . 5
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 =
0s ) → (𝐴↑s𝑁) = 1s ) | 
| 23 | 22 | oveq1d 7447 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 =
0s ) → ((𝐴↑s𝑁) ·s 𝐴) = ( 1s ·s
𝐴)) | 
| 24 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑁 = 0s → (𝑁 +s 1s ) =
( 0s +s 1s )) | 
| 25 |  | addslid 28002 | . . . . . . . 8
⊢ (
1s ∈  No  → ( 0s
+s 1s ) = 1s ) | 
| 26 | 2, 25 | ax-mp 5 | . . . . . . 7
⊢ (
0s +s 1s ) = 1s | 
| 27 | 24, 26 | eqtrdi 2792 | . . . . . 6
⊢ (𝑁 = 0s → (𝑁 +s 1s ) =
1s ) | 
| 28 | 27 | oveq2d 7448 | . . . . 5
⊢ (𝑁 = 0s → (𝐴↑s(𝑁 +s 1s ))
= (𝐴↑s
1s )) | 
| 29 |  | exps1 28412 | . . . . 5
⊢ (𝐴 ∈ 
No  → (𝐴↑s 1s ) = 𝐴) | 
| 30 | 28, 29 | sylan9eqr 2798 | . . . 4
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 =
0s ) → (𝐴↑s(𝑁 +s 1s )) = 𝐴) | 
| 31 | 19, 23, 30 | 3eqtr4rd 2787 | . . 3
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 =
0s ) → (𝐴↑s(𝑁 +s 1s )) = ((𝐴↑s𝑁) ·s 𝐴)) | 
| 32 | 17, 31 | jaodan 959 | . 2
⊢ ((𝐴 ∈ 
No  ∧ (𝑁 ∈
ℕs ∨ 𝑁
= 0s )) → (𝐴↑s(𝑁 +s 1s )) = ((𝐴↑s𝑁) ·s 𝐴)) | 
| 33 | 1, 32 | sylan2b 594 | 1
⊢ ((𝐴 ∈ 
No  ∧ 𝑁 ∈
ℕ0s) → (𝐴↑s(𝑁 +s 1s )) = ((𝐴↑s𝑁) ·s 𝐴)) |