Metamath Proof Explorer

Theorem pfxccatin12lem2c

Description: Lemma for pfxccatin12lem2 and pfxccatin12lem3 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

Ref Expression
Hypothesis swrdccatin2.l ⊢ L = A
Assertion pfxccatin12lem2c ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L ∧ N ∈ L … L + B → A ++ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A ++ B

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ L = A
2 ccatcl ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B ∈ Word V
3 2 adantr ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L ∧ N ∈ L … L + B → A ++ B ∈ Word V
4 elfz0fzfz0 ⊢ M ∈ 0 … L ∧ N ∈ L … L + B → M ∈ 0 … N
5 4 adantl ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L ∧ N ∈ L … L + B → M ∈ 0 … N
6 elfzuz2 ⊢ M ∈ 0 … L → L ∈ ℤ ≥ 0
7 fzss1 ⊢ L ∈ ℤ ≥ 0 → L … L + B ⊆ 0 … L + B
8 6 7 syl ⊢ M ∈ 0 … L → L … L + B ⊆ 0 … L + B
9 8 sselda ⊢ M ∈ 0 … L ∧ N ∈ L … L + B → N ∈ 0 … L + B
10 ccatlen ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = A + B
11 1 oveq1i ⊢ L + B = A + B
12 10 11 eqtr4di ⊢ A ∈ Word V ∧ B ∈ Word V → A ++ B = L + B
13 12 oveq2d ⊢ A ∈ Word V ∧ B ∈ Word V → 0 … A ++ B = 0 … L + B
14 13 eleq2d ⊢ A ∈ Word V ∧ B ∈ Word V → N ∈ 0 … A ++ B ↔ N ∈ 0 … L + B
15 9 14 imbitrrid ⊢ A ∈ Word V ∧ B ∈ Word V → M ∈ 0 … L ∧ N ∈ L … L + B → N ∈ 0 … A ++ B
16 15 imp ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L ∧ N ∈ L … L + B → N ∈ 0 … A ++ B
17 3 5 16 3jca ⊢ A ∈ Word V ∧ B ∈ Word V ∧ M ∈ 0 … L ∧ N ∈ L … L + B → A ++ B ∈ Word V ∧ M ∈ 0 … N ∧ N ∈ 0 … A ++ B