| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . 5
⊢ (𝑛 = 0s → (𝐴 ·s 𝑛) = (𝐴 ·s 0s
)) | 
| 2 | 1 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 0s → ((𝐴 ·s 𝑛) ∈ ℕ0s
↔ (𝐴
·s 0s ) ∈
ℕ0s)) | 
| 3 | 2 | imbi2d 340 | . . 3
⊢ (𝑛 = 0s → ((𝐴 ∈ ℕ0s
→ (𝐴
·s 𝑛)
∈ ℕ0s) ↔ (𝐴 ∈ ℕ0s → (𝐴 ·s
0s ) ∈ ℕ0s))) | 
| 4 |  | oveq2 7440 | . . . . 5
⊢ (𝑛 = 𝑚 → (𝐴 ·s 𝑛) = (𝐴 ·s 𝑚)) | 
| 5 | 4 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 𝑚 → ((𝐴 ·s 𝑛) ∈ ℕ0s ↔ (𝐴 ·s 𝑚) ∈
ℕ0s)) | 
| 6 | 5 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝑚 → ((𝐴 ∈ ℕ0s → (𝐴 ·s 𝑛) ∈ ℕ0s)
↔ (𝐴 ∈
ℕ0s → (𝐴 ·s 𝑚) ∈
ℕ0s))) | 
| 7 |  | oveq2 7440 | . . . . 5
⊢ (𝑛 = (𝑚 +s 1s ) → (𝐴 ·s 𝑛) = (𝐴 ·s (𝑚 +s 1s
))) | 
| 8 | 7 | eleq1d 2825 | . . . 4
⊢ (𝑛 = (𝑚 +s 1s ) → ((𝐴 ·s 𝑛) ∈ ℕ0s
↔ (𝐴
·s (𝑚
+s 1s )) ∈ ℕ0s)) | 
| 9 | 8 | imbi2d 340 | . . 3
⊢ (𝑛 = (𝑚 +s 1s ) → ((𝐴 ∈ ℕ0s
→ (𝐴
·s 𝑛)
∈ ℕ0s) ↔ (𝐴 ∈ ℕ0s → (𝐴 ·s (𝑚 +s 1s ))
∈ ℕ0s))) | 
| 10 |  | oveq2 7440 | . . . . 5
⊢ (𝑛 = 𝐵 → (𝐴 ·s 𝑛) = (𝐴 ·s 𝐵)) | 
| 11 | 10 | eleq1d 2825 | . . . 4
⊢ (𝑛 = 𝐵 → ((𝐴 ·s 𝑛) ∈ ℕ0s ↔ (𝐴 ·s 𝐵) ∈
ℕ0s)) | 
| 12 | 11 | imbi2d 340 | . . 3
⊢ (𝑛 = 𝐵 → ((𝐴 ∈ ℕ0s → (𝐴 ·s 𝑛) ∈ ℕ0s)
↔ (𝐴 ∈
ℕ0s → (𝐴 ·s 𝐵) ∈
ℕ0s))) | 
| 13 |  | n0sno 28329 | . . . . 5
⊢ (𝐴 ∈ ℕ0s
→ 𝐴 ∈  No ) | 
| 14 |  | muls01 28139 | . . . . 5
⊢ (𝐴 ∈ 
No  → (𝐴
·s 0s ) = 0s ) | 
| 15 | 13, 14 | syl 17 | . . . 4
⊢ (𝐴 ∈ ℕ0s
→ (𝐴
·s 0s ) = 0s ) | 
| 16 |  | 0n0s 28335 | . . . 4
⊢ 
0s ∈ ℕ0s | 
| 17 | 15, 16 | eqeltrdi 2848 | . . 3
⊢ (𝐴 ∈ ℕ0s
→ (𝐴
·s 0s ) ∈
ℕ0s) | 
| 18 | 13 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → 𝐴 ∈ 
No ) | 
| 19 |  | n0sno 28329 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0s
→ 𝑚 ∈  No ) | 
| 20 | 19 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → 𝑚 ∈ 
No ) | 
| 21 |  | 1sno 27873 | . . . . . . . . . 10
⊢ 
1s ∈  No | 
| 22 | 21 | a1i 11 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) →
1s ∈  No ) | 
| 23 | 18, 20, 22 | addsdid 28183 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → (𝐴 ·s (𝑚 +s 1s ))
= ((𝐴 ·s
𝑚) +s (𝐴 ·s
1s ))) | 
| 24 | 13 | mulsridd 28141 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℕ0s
→ (𝐴
·s 1s ) = 𝐴) | 
| 25 | 24 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝐴 ∈ ℕ0s
→ ((𝐴
·s 𝑚)
+s (𝐴
·s 1s )) = ((𝐴 ·s 𝑚) +s 𝐴)) | 
| 26 | 25 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → ((𝐴 ·s 𝑚) +s (𝐴 ·s
1s )) = ((𝐴
·s 𝑚)
+s 𝐴)) | 
| 27 | 23, 26 | eqtrd 2776 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → (𝐴 ·s (𝑚 +s 1s ))
= ((𝐴 ·s
𝑚) +s 𝐴)) | 
| 28 |  | n0addscl 28348 | . . . . . . . . 9
⊢ (((𝐴 ·s 𝑚) ∈ ℕ0s
∧ 𝐴 ∈
ℕ0s) → ((𝐴 ·s 𝑚) +s 𝐴) ∈
ℕ0s) | 
| 29 | 28 | ancoms 458 | . . . . . . . 8
⊢ ((𝐴 ∈ ℕ0s
∧ (𝐴
·s 𝑚)
∈ ℕ0s) → ((𝐴 ·s 𝑚) +s 𝐴) ∈
ℕ0s) | 
| 30 | 29 | adantlr 715 | . . . . . . 7
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → ((𝐴 ·s 𝑚) +s 𝐴) ∈
ℕ0s) | 
| 31 | 27, 30 | eqeltrd 2840 | . . . . . 6
⊢ (((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) ∧ (𝐴 ·s 𝑚) ∈ ℕ0s) → (𝐴 ·s (𝑚 +s 1s ))
∈ ℕ0s) | 
| 32 | 31 | ex 412 | . . . . 5
⊢ ((𝐴 ∈ ℕ0s
∧ 𝑚 ∈
ℕ0s) → ((𝐴 ·s 𝑚) ∈ ℕ0s → (𝐴 ·s (𝑚 +s 1s ))
∈ ℕ0s)) | 
| 33 | 32 | expcom 413 | . . . 4
⊢ (𝑚 ∈ ℕ0s
→ (𝐴 ∈
ℕ0s → ((𝐴 ·s 𝑚) ∈ ℕ0s → (𝐴 ·s (𝑚 +s 1s ))
∈ ℕ0s))) | 
| 34 | 33 | a2d 29 | . . 3
⊢ (𝑚 ∈ ℕ0s
→ ((𝐴 ∈
ℕ0s → (𝐴 ·s 𝑚) ∈ ℕ0s) → (𝐴 ∈ ℕ0s
→ (𝐴
·s (𝑚
+s 1s )) ∈ ℕ0s))) | 
| 35 | 3, 6, 9, 12, 17, 34 | n0sind 28338 | . 2
⊢ (𝐵 ∈ ℕ0s
→ (𝐴 ∈
ℕ0s → (𝐴 ·s 𝐵) ∈
ℕ0s)) | 
| 36 | 35 | impcom 407 | 1
⊢ ((𝐴 ∈ ℕ0s
∧ 𝐵 ∈
ℕ0s) → (𝐴 ·s 𝐵) ∈
ℕ0s) |