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∈WordV∧B∈WordV∧M∈0…L∧N∈L…L+B→A++B∈WordV∧M∈0…N∧N∈0…A++B

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢L=A
2 ccatcl ⊢A∈WordV∧B∈WordV→A++B∈WordV
3 2 adantr ⊢A∈WordV∧B∈WordV∧M∈0…L∧N∈L…L+B→A++B∈WordV
4 elfz0fzfz0 ⊢M∈0…L∧N∈L…L+B→M∈0…N
5 4 adantl ⊢A∈WordV∧B∈WordV∧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∈WordV∧B∈WordV→A++B=A+B
11 1 oveq1i ⊢L+B=A+B
12 10 11 eqtr4di ⊢A∈WordV∧B∈WordV→A++B=L+B
13 12 oveq2d ⊢A∈WordV∧B∈WordV→0…A++B=0…L+B
14 13 eleq2d ⊢A∈WordV∧B∈WordV→N∈0…A++B↔N∈0…L+B
15 9 14 imbitrrid ⊢A∈WordV∧B∈WordV→M∈0…L∧N∈L…L+B→N∈0…A++B
16 15 imp ⊢A∈WordV∧B∈WordV∧M∈0…L∧N∈L…L+B→N∈0…A++B
17 3 5 16 3jca ⊢A∈WordV∧B∈WordV∧M∈0…L∧N∈L…L+B→A++B∈WordV∧M∈0…N∧N∈0…A++B