| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = 0s → (𝐴↑s𝑚) = (𝐴↑s 0s
)) | 
| 2 | 1 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑚 = 0s → ((𝐴↑s𝑚) = 0s ↔ (𝐴↑s 0s
) = 0s )) | 
| 3 | 2 | imbi1d 341 | . . . . . . 7
⊢ (𝑚 = 0s → (((𝐴↑s𝑚) = 0s → 𝐴 = 0s ) ↔
((𝐴↑s
0s ) = 0s → 𝐴 = 0s ))) | 
| 4 | 3 | imbi2d 340 | . . . . . 6
⊢ (𝑚 = 0s → ((𝐴 ∈ 
No  → ((𝐴↑s𝑚) = 0s → 𝐴 = 0s )) ↔ (𝐴 ∈ 
No  → ((𝐴↑s 0s ) =
0s → 𝐴 =
0s )))) | 
| 5 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (𝐴↑s𝑚) = (𝐴↑s𝑛)) | 
| 6 | 5 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → ((𝐴↑s𝑚) = 0s ↔ (𝐴↑s𝑛) = 0s )) | 
| 7 | 6 | imbi1d 341 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (((𝐴↑s𝑚) = 0s → 𝐴 = 0s ) ↔ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s
))) | 
| 8 | 7 | imbi2d 340 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((𝐴 ∈  No 
→ ((𝐴↑s𝑚) = 0s → 𝐴 = 0s )) ↔ (𝐴 ∈ 
No  → ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )))) | 
| 9 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = (𝑛 +s 1s ) → (𝐴↑s𝑚) = (𝐴↑s(𝑛 +s 1s
))) | 
| 10 | 9 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑚 = (𝑛 +s 1s ) → ((𝐴↑s𝑚) = 0s ↔ (𝐴↑s(𝑛 +s 1s ))
= 0s )) | 
| 11 | 10 | imbi1d 341 | . . . . . . 7
⊢ (𝑚 = (𝑛 +s 1s ) →
(((𝐴↑s𝑚) = 0s → 𝐴 = 0s ) ↔
((𝐴↑s(𝑛 +s 1s ))
= 0s → 𝐴 =
0s ))) | 
| 12 | 11 | imbi2d 340 | . . . . . 6
⊢ (𝑚 = (𝑛 +s 1s ) → ((𝐴 ∈ 
No  → ((𝐴↑s𝑚) = 0s → 𝐴 = 0s )) ↔ (𝐴 ∈ 
No  → ((𝐴↑s(𝑛 +s 1s )) =
0s → 𝐴 =
0s )))) | 
| 13 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑚 = 𝑁 → (𝐴↑s𝑚) = (𝐴↑s𝑁)) | 
| 14 | 13 | eqeq1d 2738 | . . . . . . . 8
⊢ (𝑚 = 𝑁 → ((𝐴↑s𝑚) = 0s ↔ (𝐴↑s𝑁) = 0s )) | 
| 15 | 14 | imbi1d 341 | . . . . . . 7
⊢ (𝑚 = 𝑁 → (((𝐴↑s𝑚) = 0s → 𝐴 = 0s ) ↔ ((𝐴↑s𝑁) = 0s → 𝐴 = 0s
))) | 
| 16 | 15 | imbi2d 340 | . . . . . 6
⊢ (𝑚 = 𝑁 → ((𝐴 ∈  No 
→ ((𝐴↑s𝑚) = 0s → 𝐴 = 0s )) ↔ (𝐴 ∈ 
No  → ((𝐴↑s𝑁) = 0s → 𝐴 = 0s )))) | 
| 17 |  | 0slt1s 27875 | . . . . . . . . . 10
⊢ 
0s <s 1s | 
| 18 |  | sgt0ne0 27880 | . . . . . . . . . 10
⊢ (
0s <s 1s → 1s ≠ 0s
) | 
| 19 | 17, 18 | ax-mp 5 | . . . . . . . . 9
⊢ 
1s ≠ 0s | 
| 20 |  | exps0 28411 | . . . . . . . . . 10
⊢ (𝐴 ∈ 
No  → (𝐴↑s 0s ) =
1s ) | 
| 21 | 20 | neeq1d 2999 | . . . . . . . . 9
⊢ (𝐴 ∈ 
No  → ((𝐴↑s 0s ) ≠
0s ↔ 1s ≠ 0s )) | 
| 22 | 19, 21 | mpbiri 258 | . . . . . . . 8
⊢ (𝐴 ∈ 
No  → (𝐴↑s 0s ) ≠
0s ) | 
| 23 | 22 | neneqd 2944 | . . . . . . 7
⊢ (𝐴 ∈ 
No  → ¬ (𝐴↑s 0s ) =
0s ) | 
| 24 | 23 | pm2.21d 121 | . . . . . 6
⊢ (𝐴 ∈ 
No  → ((𝐴↑s 0s ) =
0s → 𝐴 =
0s )) | 
| 25 |  | expsp1 28413 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → (𝐴↑s(𝑛 +s 1s )) = ((𝐴↑s𝑛) ·s 𝐴)) | 
| 26 | 25 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → ((𝐴↑s(𝑛 +s 1s )) =
0s ↔ ((𝐴↑s𝑛) ·s 𝐴) = 0s )) | 
| 27 |  | expscl 28414 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → (𝐴↑s𝑛) ∈  No
) | 
| 28 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → 𝐴 ∈  No
) | 
| 29 | 27, 28 | muls0ord 28212 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → (((𝐴↑s𝑛) ·s 𝐴) = 0s ↔ ((𝐴↑s𝑛) = 0s ∨ 𝐴 = 0s ))) | 
| 30 | 26, 29 | bitrd 279 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → ((𝐴↑s(𝑛 +s 1s )) =
0s ↔ ((𝐴↑s𝑛) = 0s ∨ 𝐴 = 0s ))) | 
| 31 | 30 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) ∧ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → ((𝐴↑s(𝑛 +s 1s ))
= 0s ↔ ((𝐴↑s𝑛) = 0s ∨ 𝐴 = 0s ))) | 
| 32 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) ∧ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → ((𝐴↑s𝑛) = 0s → 𝐴 = 0s
)) | 
| 33 |  | idd 24 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) ∧ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → (𝐴 = 0s → 𝐴 = 0s
)) | 
| 34 | 32, 33 | jaod 859 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) ∧ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → (((𝐴↑s𝑛) = 0s ∨ 𝐴 = 0s ) → 𝐴 = 0s
)) | 
| 35 | 31, 34 | sylbid 240 | . . . . . . . . 9
⊢ (((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) ∧ ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → ((𝐴↑s(𝑛 +s 1s ))
= 0s → 𝐴 =
0s )) | 
| 36 | 35 | ex 412 | . . . . . . . 8
⊢ ((𝐴 ∈ 
No  ∧ 𝑛 ∈
ℕ0s) → (((𝐴↑s𝑛) = 0s → 𝐴 = 0s ) → ((𝐴↑s(𝑛 +s 1s ))
= 0s → 𝐴 =
0s ))) | 
| 37 | 36 | expcom 413 | . . . . . . 7
⊢ (𝑛 ∈ ℕ0s
→ (𝐴 ∈  No  → (((𝐴↑s𝑛) = 0s → 𝐴 = 0s ) → ((𝐴↑s(𝑛 +s 1s ))
= 0s → 𝐴 =
0s )))) | 
| 38 | 37 | a2d 29 | . . . . . 6
⊢ (𝑛 ∈ ℕ0s
→ ((𝐴 ∈  No  → ((𝐴↑s𝑛) = 0s → 𝐴 = 0s )) → (𝐴 ∈ 
No  → ((𝐴↑s(𝑛 +s 1s )) =
0s → 𝐴 =
0s )))) | 
| 39 | 4, 8, 12, 16, 24, 38 | n0sind 28338 | . . . . 5
⊢ (𝑁 ∈ ℕ0s
→ (𝐴 ∈  No  → ((𝐴↑s𝑁) = 0s → 𝐴 = 0s ))) | 
| 40 | 39 | imp 406 | . . . 4
⊢ ((𝑁 ∈ ℕ0s
∧ 𝐴 ∈  No ) → ((𝐴↑s𝑁) = 0s → 𝐴 = 0s )) | 
| 41 | 40 | necon3d 2960 | . . 3
⊢ ((𝑁 ∈ ℕ0s
∧ 𝐴 ∈  No ) → (𝐴 ≠ 0s → (𝐴↑s𝑁) ≠ 0s
)) | 
| 42 | 41 | ex 412 | . 2
⊢ (𝑁 ∈ ℕ0s
→ (𝐴 ∈  No  → (𝐴 ≠ 0s → (𝐴↑s𝑁) ≠ 0s
))) | 
| 43 | 42 | 3imp231 1112 | 1
⊢ ((𝐴 ∈ 
No  ∧ 𝐴 ≠
0s ∧ 𝑁
∈ ℕ0s) → (𝐴↑s𝑁) ≠ 0s ) |