Step |
Hyp |
Ref |
Expression |
1 |
|
ccatws1len |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ) = ( ( ♯ ‘ 𝑊 ) + 1 ) ) |
3 |
2
|
eqeq1d |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ) = ( 𝑁 + 1 ) ↔ ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) ) ) |
4 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
5 |
4
|
nn0cnd |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
6 |
5
|
adantr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
7 |
|
nn0cn |
⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ ) |
8 |
7
|
adantl |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℂ ) |
9 |
|
1cnd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → 1 ∈ ℂ ) |
10 |
6 8 9
|
addcan2d |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ( ♯ ‘ 𝑊 ) + 1 ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) |
11 |
3 10
|
bitrd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( ( ♯ ‘ ( 𝑊 ++ 〈“ 𝑋 ”〉 ) ) = ( 𝑁 + 1 ) ↔ ( ♯ ‘ 𝑊 ) = 𝑁 ) ) |