Proof of Theorem ccatsymb
| Step | Hyp | Ref
| Expression |
| 1 | | simprll 779 |
. . . . . . . 8
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
| 2 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → 𝐼 < (♯‘𝐴)) |
| 3 | 2 | anim2i 617 |
. . . . . . . . 9
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴))) |
| 4 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℤ) |
| 5 | | 0zd 12625 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 0 ∈
ℤ) |
| 6 | | lencl 14571 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
| 7 | 6 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈
ℤ) |
| 9 | | elfzo 13701 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ℤ ∧ 0 ∈
ℤ ∧ (♯‘𝐴) ∈ ℤ) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴)))) |
| 10 | 4, 5, 8, 9 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴)))) |
| 11 | 10 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴)))) |
| 12 | 3, 11 | mpbird 257 |
. . . . . . . 8
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → 𝐼 ∈ (0..^(♯‘𝐴))) |
| 13 | | df-3an 1089 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ (0..^(♯‘𝐴)))) |
| 14 | 1, 12, 13 | sylanbrc 583 |
. . . . . . 7
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴)))) |
| 15 | | ccatval1 14615 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝐼) = (𝐴‘𝐼)) |
| 16 | 15 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 17 | 14, 16 | syl 17 |
. . . . . 6
⊢ ((0 ≤
𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 18 | 17 | ex 412 |
. . . . 5
⊢ (0 ≤
𝐼 → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 19 | | zre 12617 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → 𝐼 ∈
ℝ) |
| 20 | | 0red 11264 |
. . . . . . . . . 10
⊢ (𝐼 ∈ ℤ → 0 ∈
ℝ) |
| 21 | 19, 20 | ltnled 11408 |
. . . . . . . . 9
⊢ (𝐼 ∈ ℤ → (𝐼 < 0 ↔ ¬ 0 ≤
𝐼)) |
| 22 | 21 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 < 0 ↔ ¬ 0 ≤ 𝐼)) |
| 23 | | simpl 482 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉) |
| 24 | 23 | anim1i 615 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ)) |
| 26 | | animorrl 983 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐼 < 0 ∨ (♯‘𝐴) ≤ 𝐼)) |
| 27 | | wrdsymb0 14587 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝐴) ≤ 𝐼) → (𝐴‘𝐼) = ∅)) |
| 28 | 25, 26, 27 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴‘𝐼) = ∅) |
| 29 | | ccatcl 14612 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
| 30 | 29 | anim1i 615 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ)) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ)) |
| 32 | | animorrl 983 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼)) |
| 33 | | wrdsymb0 14587 |
. . . . . . . . . . 11
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵)‘𝐼) = ∅)) |
| 34 | 31, 32, 33 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → ((𝐴 ++ 𝐵)‘𝐼) = ∅) |
| 35 | 28, 34 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 36 | 35 | ex 412 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 < 0 → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 37 | 22, 36 | sylbird 260 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (¬ 0 ≤ 𝐼 → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 38 | 37 | com12 32 |
. . . . . 6
⊢ (¬ 0
≤ 𝐼 → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 39 | 38 | adantrd 491 |
. . . . 5
⊢ (¬ 0
≤ 𝐼 → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 40 | 18, 39 | pm2.61i 182 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 41 | | simprll 779 |
. . . . . . . 8
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
| 42 | | id 22 |
. . . . . . . . . 10
⊢ (𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → 𝐼 < ((♯‘𝐴) + (♯‘𝐵))) |
| 43 | 6 | nn0red 12588 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℝ) |
| 44 | | lenlt 11339 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
∈ ℝ ∧ 𝐼
∈ ℝ) → ((♯‘𝐴) ≤ 𝐼 ↔ ¬ 𝐼 < (♯‘𝐴))) |
| 45 | 43, 19, 44 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) →
((♯‘𝐴) ≤
𝐼 ↔ ¬ 𝐼 < (♯‘𝐴))) |
| 46 | 45 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) →
((♯‘𝐴) ≤
𝐼 ↔ ¬ 𝐼 < (♯‘𝐴))) |
| 47 | 46 | biimpar 477 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (♯‘𝐴) ≤ 𝐼) |
| 48 | 42, 47 | anim12ci 614 |
. . . . . . . . 9
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))) |
| 49 | | lencl 14571 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈
ℕ0) |
| 50 | 49 | nn0zd 12639 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℤ) |
| 51 | | zaddcl 12657 |
. . . . . . . . . . . . 13
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 52 | 7, 50, 51 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) |
| 53 | 52 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℤ) |
| 54 | | elfzo 13701 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))) |
| 55 | 4, 8, 53, 54 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))) |
| 56 | 55 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))) |
| 57 | 48, 56 | mpbird 257 |
. . . . . . . 8
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) |
| 58 | | df-3an 1089 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
| 59 | 41, 57, 58 | sylanbrc 583 |
. . . . . . 7
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))) |
| 60 | | ccatval2 14616 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝐼) = (𝐵‘(𝐼 − (♯‘𝐴)))) |
| 61 | 60 | eqcomd 2743 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 62 | 59, 61 | syl 17 |
. . . . . 6
⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 63 | 62 | ex 412 |
. . . . 5
⊢ (𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 64 | 49 | nn0red 12588 |
. . . . . . . . . 10
⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℝ) |
| 65 | | readdcl 11238 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) →
((♯‘𝐴) +
(♯‘𝐵)) ∈
ℝ) |
| 66 | 43, 64, 65 | syl2an 596 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℝ) |
| 67 | | lenlt 11339 |
. . . . . . . . 9
⊢
((((♯‘𝐴)
+ (♯‘𝐵)) ∈
ℝ ∧ 𝐼 ∈
ℝ) → (((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼 ↔ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))) |
| 68 | 66, 19, 67 | syl2an 596 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) →
(((♯‘𝐴) +
(♯‘𝐵)) ≤
𝐼 ↔ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))) |
| 69 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐵 ∈ Word 𝑉) |
| 70 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℤ) |
| 71 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈
ℤ) |
| 72 | 70, 71 | zsubcld 12727 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → (𝐼 − (♯‘𝐴)) ∈ ℤ) |
| 73 | 72 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 − (♯‘𝐴)) ∈ ℤ) |
| 74 | 69, 73 | jca 511 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ)) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ)) |
| 76 | 43 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈
ℝ) |
| 77 | 64 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐵) ∈
ℝ) |
| 78 | 19 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℝ) |
| 79 | 76, 77, 78 | leaddsub2d 11865 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) →
(((♯‘𝐴) +
(♯‘𝐵)) ≤
𝐼 ↔
(♯‘𝐵) ≤
(𝐼 −
(♯‘𝐴)))) |
| 80 | 79 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴))) |
| 81 | 80 | olcd 875 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐼 − (♯‘𝐴)) < 0 ∨ (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴)))) |
| 82 | | wrdsymb0 14587 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ) → (((𝐼 − (♯‘𝐴)) < 0 ∨
(♯‘𝐵) ≤
(𝐼 −
(♯‘𝐴))) →
(𝐵‘(𝐼 − (♯‘𝐴))) = ∅)) |
| 83 | 75, 81, 82 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵‘(𝐼 − (♯‘𝐴))) = ∅) |
| 84 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ)) |
| 85 | | ccatlen 14613 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
| 86 | 85 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵))) |
| 87 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) |
| 88 | 86, 87 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼) |
| 89 | 88 | olcd 875 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼)) |
| 90 | 84, 89, 33 | sylc 65 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵)‘𝐼) = ∅) |
| 91 | 83, 90 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 92 | 91 | ex 412 |
. . . . . . . 8
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) →
(((♯‘𝐴) +
(♯‘𝐵)) ≤
𝐼 → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 93 | 68, 92 | sylbird 260 |
. . . . . . 7
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 94 | 93 | com12 32 |
. . . . . 6
⊢ (¬
𝐼 <
((♯‘𝐴) +
(♯‘𝐵)) →
(((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 95 | 94 | adantrd 491 |
. . . . 5
⊢ (¬
𝐼 <
((♯‘𝐴) +
(♯‘𝐵)) →
((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))) |
| 96 | 63, 95 | pm2.61i 182 |
. . . 4
⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 97 | 40, 96 | ifeqda 4562 |
. . 3
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))) = ((𝐴 ++ 𝐵)‘𝐼)) |
| 98 | 97 | eqcomd 2743 |
. 2
⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴))))) |
| 99 | 98 | 3impa 1110 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴))))) |