Metamath Proof Explorer

Theorem ccatval21sw

Description: The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion ccatval21sw ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B ⁡ A = B ⁡ 0

Proof

Step Hyp Ref Expression
1 lencl ⊢ A ∈ Word V → A ∈ ℕ 0
2 1 nn0zd ⊢ A ∈ Word V → A ∈ ℤ
3 lennncl ⊢ B ∈ Word V ∧ B ≠ ∅ → B ∈ ℕ
4 simpl ⊢ A ∈ ℤ ∧ B ∈ ℕ → A ∈ ℤ
5 nnz ⊢ B ∈ ℕ → B ∈ ℤ
6 zaddcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + B ∈ ℤ
7 5 6 sylan2 ⊢ A ∈ ℤ ∧ B ∈ ℕ → A + B ∈ ℤ
8 nngt0 ⊢ B ∈ ℕ → 0 < B
9 8 adantl ⊢ A ∈ ℤ ∧ B ∈ ℕ → 0 < B
10 nnre ⊢ B ∈ ℕ → B ∈ ℝ
11 zre ⊢ A ∈ ℤ → A ∈ ℝ
12 ltaddpos ⊢ B ∈ ℝ ∧ A ∈ ℝ → 0 < B ↔ A < A + B
13 10 11 12 syl2anr ⊢ A ∈ ℤ ∧ B ∈ ℕ → 0 < B ↔ A < A + B
14 9 13 mpbid ⊢ A ∈ ℤ ∧ B ∈ ℕ → A < A + B
15 4 7 14 3jca ⊢ A ∈ ℤ ∧ B ∈ ℕ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
16 2 3 15 syl2an ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
17 16 3impb ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
18 fzolb ⊢ A ∈ A ..^ A + B ↔ A ∈ ℤ ∧ A + B ∈ ℤ ∧ A < A + B
19 17 18 sylibr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ∈ A ..^ A + B
20 ccatval2 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ A ∈ A ..^ A + B → A ++ B ⁡ A = B ⁡ A − A
21 19 20 syld3an3 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B ⁡ A = B ⁡ A − A
22 1 nn0cnd ⊢ A ∈ Word V → A ∈ ℂ
23 22 subidd ⊢ A ∈ Word V → A − A = 0
24 23 fveq2d ⊢ A ∈ Word V → B ⁡ A − A = B ⁡ 0
25 24 3ad2ant1 ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → B ⁡ A − A = B ⁡ 0
26 21 25 eqtrd ⊢ A ∈ Word V ∧ B ∈ Word V ∧ B ≠ ∅ → A ++ B ⁡ A = B ⁡ 0