ccatsymb - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ccatsymb		GIF version

Theorem ccatsymb 11348

Description: The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)

**Assertion**
Ref	Expression
ccatsymb	⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))))

**Proof of Theorem ccatsymb**
Step	Hyp	Ref	Expression
1		simprll 543	. . . . . . . 8 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉))
2		simpr 110	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → 𝐼 < (♯‘𝐴))
3	2	anim2i 342	. . . . . . . . 9 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴)))
4		simpr 110	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℤ)
5		0zd 9635	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 0 ∈ ℤ)
6		lencl 11286	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ₀)
7	6	nn0zd 9745	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ)
8	7	ad2antrr 492	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈ ℤ)
9		elfzo 10534	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 0 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴))))
10	4, 5, 8, 9	syl3anc 1278	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴))))
11	10	ad2antrl 494	. . . . . . . . 9 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐼 ∈ (0..^(♯‘𝐴)) ↔ (0 ≤ 𝐼 ∧ 𝐼 < (♯‘𝐴))))
12	3, 11	mpbird 167	. . . . . . . 8 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → 𝐼 ∈ (0..^(♯‘𝐴)))
13		df-3an 1011	. . . . . . . 8 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ (0..^(♯‘𝐴))))
14	1, 12, 13	sylanbrc 421	. . . . . . 7 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))))
15		ccatval1 11343	. . . . . . . 8 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘𝐼) = (𝐴‘𝐼))
16	15	eqcomd 2244	. . . . . . 7 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝐴))) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
17	14, 16	syl 14	. . . . . 6 ⊢ ((0 ≤ 𝐼 ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴))) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
18	17	ancoms 268	. . . . 5 ⊢ (((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) ∧ 0 ≤ 𝐼) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
19		0z 9634	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
20		zltnle 9669	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ 0 ∈ ℤ) → (𝐼 < 0 ↔ ¬ 0 ≤ 𝐼))
21	19, 20	mpan2 429	. . . . . . . . . 10 ⊢ (𝐼 ∈ ℤ → (𝐼 < 0 ↔ ¬ 0 ≤ 𝐼))
22	21	adantl 277	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 < 0 ↔ ¬ 0 ≤ 𝐼))
23		simpl 109	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
24	23	anim1i 340	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ))
25	24	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ))
26		animorrl 838	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐼 < 0 ∨ (♯‘𝐴) ≤ 𝐼))
27		wrdsymb0 11315	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝐴) ≤ 𝐼) → (𝐴‘𝐼) = ∅))
28	25, 26, 27	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴‘𝐼) = ∅)
29		ccatcl 11339	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉)
30	29	anim1i 340	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ))
31	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ))
32		animorrl 838	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼))
33		wrdsymb0 11315	. . . . . . . . . . . 12 ⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵)‘𝐼) = ∅))
34	31, 32, 33	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → ((𝐴 ++ 𝐵)‘𝐼) = ∅)
35	28, 34	eqtr4d 2274	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < 0) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
36	35	ex 115	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 < 0 → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)))
37	22, 36	sylbird 170	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (¬ 0 ≤ 𝐼 → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)))
38	37	com12 30	. . . . . . 7 ⊢ (¬ 0 ≤ 𝐼 → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)))
39	38	adantrd 279	. . . . . 6 ⊢ (¬ 0 ≤ 𝐼 → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼)))
40	39	impcom 125	. . . . 5 ⊢ (((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) ∧ ¬ 0 ≤ 𝐼) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
41		simplr 533	. . . . . . 7 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → 𝐼 ∈ ℤ)
42		zdcle 9700	. . . . . . 7 ⊢ ((0 ∈ ℤ ∧ 𝐼 ∈ ℤ) → DECID 0 ≤ 𝐼)
43	19, 41, 42	sylancr 418	. . . . . 6 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → DECID 0 ≤ 𝐼)
44		exmiddc 848	. . . . . 6 ⊢ (DECID 0 ≤ 𝐼 → (0 ≤ 𝐼 ∨ ¬ 0 ≤ 𝐼))
45	43, 44	syl 14	. . . . 5 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (0 ≤ 𝐼 ∨ ¬ 0 ≤ 𝐼))
46	18, 40, 45	mpjaodan 810	. . . 4 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ 𝐼 < (♯‘𝐴)) → (𝐴‘𝐼) = ((𝐴 ++ 𝐵)‘𝐼))
47		simprll 543	. . . . . . . 8 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉))
48		id 19	. . . . . . . . . 10 ⊢ (𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))
49	6	nn0red 9600	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℝ)
50		zre 9627	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ ℤ → 𝐼 ∈ ℝ)
51		lenlt 8391	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℝ ∧ 𝐼 ∈ ℝ) → ((♯‘𝐴) ≤ 𝐼 ↔ ¬ 𝐼 < (♯‘𝐴)))
52	49, 50, 51	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((♯‘𝐴) ≤ 𝐼 ↔ ¬ 𝐼 < (♯‘𝐴)))
53	52	adantlr 481	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((♯‘𝐴) ≤ 𝐼 ↔ ¬ 𝐼 < (♯‘𝐴)))
54	53	biimpar 297	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (♯‘𝐴) ≤ 𝐼)
55	48, 54	anim12ci 339	. . . . . . . . 9 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))
56		lencl 11286	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ₀)
57	56	nn0zd 9745	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℤ)
58		zaddcl 9663	. . . . . . . . . . . . 13 ⊢ (((♯‘𝐴) ∈ ℤ ∧ (♯‘𝐵) ∈ ℤ) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
59	7, 57, 58	syl2an 289	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
60	59	adantr 276	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
61		elfzo 10534	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))))
62	4, 8, 60, 61	syl3anc 1278	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))))
63	62	ad2antrl 494	. . . . . . . . 9 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ ((♯‘𝐴) ≤ 𝐼 ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))))
64	55, 63	mpbird 167	. . . . . . . 8 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
65		df-3an 1011	. . . . . . . 8 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) ↔ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
66	47, 64, 65	sylanbrc 421	. . . . . . 7 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
67		ccatval2 11344	. . . . . . . 8 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘𝐼) = (𝐵‘(𝐼 − (♯‘𝐴))))
68	67	eqcomd 2244	. . . . . . 7 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
69	66, 68	syl 14	. . . . . 6 ⊢ ((𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∧ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
70	69	ancoms 268	. . . . 5 ⊢ (((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) ∧ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
71	56	nn0red 9600	. . . . . . . . . . 11 ⊢ (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℝ)
72		readdcl 8295	. . . . . . . . . . 11 ⊢ (((♯‘𝐴) ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℝ)
73	49, 71, 72	syl2an 289	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℝ)
74		lenlt 8391	. . . . . . . . . 10 ⊢ ((((♯‘𝐴) + (♯‘𝐵)) ∈ ℝ ∧ 𝐼 ∈ ℝ) → (((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼 ↔ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))
75	73, 50, 74	syl2an 289	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼 ↔ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))
76		simplr 533	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐵 ∈ Word 𝑉)
77		simpr 110	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℤ)
78	7	adantr 276	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈ ℤ)
79	77, 78	zsubcld 9752	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → (𝐼 − (♯‘𝐴)) ∈ ℤ)
80	79	adantlr 481	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐼 − (♯‘𝐴)) ∈ ℤ)
81	76, 80	jca 306	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ))
82	81	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ))
83	49	ad2antrr 492	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐴) ∈ ℝ)
84	71	ad2antlr 493	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (♯‘𝐵) ∈ ℝ)
85	50	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → 𝐼 ∈ ℝ)
86	83, 84, 85	leaddsub2d 8865	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼 ↔ (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴))))
87	86	biimpa 296	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴)))
88	87	olcd 746	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐼 − (♯‘𝐴)) < 0 ∨ (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴))))
89		wrdsymb0 11315	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ Word 𝑉 ∧ (𝐼 − (♯‘𝐴)) ∈ ℤ) → (((𝐼 − (♯‘𝐴)) < 0 ∨ (♯‘𝐵) ≤ (𝐼 − (♯‘𝐴))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ∅))
90	82, 88, 89	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵‘(𝐼 − (♯‘𝐴))) = ∅)
91	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ))
92		ccatlen 11341	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵)))
93	92	ad2antrr 492	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘(𝐴 ++ 𝐵)) = ((♯‘𝐴) + (♯‘𝐵)))
94		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼)
95	93, 94	eqbrtrd 4147	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼)
96	95	olcd 746	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐼 < 0 ∨ (♯‘(𝐴 ++ 𝐵)) ≤ 𝐼))
97	91, 96, 33	sylc 62	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → ((𝐴 ++ 𝐵)‘𝐼) = ∅)
98	90, 97	eqtr4d 2274	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
99	98	ex 115	. . . . . . . . 9 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (((♯‘𝐴) + (♯‘𝐵)) ≤ 𝐼 → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)))
100	75, 99	sylbird 170	. . . . . . . 8 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)))
101	100	com12 30	. . . . . . 7 ⊢ (¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)))
102	101	adantrd 279	. . . . . 6 ⊢ (¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼)))
103	102	impcom 125	. . . . 5 ⊢ (((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) ∧ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
104		simplr 533	. . . . . . 7 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → 𝐼 ∈ ℤ)
105	60	adantr 276	. . . . . . 7 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ)
106		zdclt 9701	. . . . . . 7 ⊢ ((𝐼 ∈ ℤ ∧ ((♯‘𝐴) + (♯‘𝐵)) ∈ ℤ) → DECID 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))
107	104, 105, 106	syl2anc 415	. . . . . 6 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → DECID 𝐼 < ((♯‘𝐴) + (♯‘𝐵)))
108		exmiddc 848	. . . . . 6 ⊢ (DECID 𝐼 < ((♯‘𝐴) + (♯‘𝐵)) → (𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∨ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))
109	107, 108	syl 14	. . . . 5 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐼 < ((♯‘𝐴) + (♯‘𝐵)) ∨ ¬ 𝐼 < ((♯‘𝐴) + (♯‘𝐵))))
110	70, 103, 109	mpjaodan 810	. . . 4 ⊢ ((((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) ∧ ¬ 𝐼 < (♯‘𝐴)) → (𝐵‘(𝐼 − (♯‘𝐴))) = ((𝐴 ++ 𝐵)‘𝐼))
111		zdclt 9701	. . . . 5 ⊢ ((𝐼 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → DECID 𝐼 < (♯‘𝐴))
112	4, 8, 111	syl2anc 415	. . . 4 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → DECID 𝐼 < (♯‘𝐴))
113	46, 110, 112	ifeqdadc 3670	. . 3 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))) = ((𝐴 ++ 𝐵)‘𝐼))
114	113	eqcomd 2244	. 2 ⊢ (((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))))
115	114	3impa 1225	1 ⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 720 DECID wdc 846 ∧ w3a 1009 = wceq 1402 ∈ wcel 2209 ∅c0 3520 ifcif 3635 class class class wbr 4125 ‘cfv 5372 (class class class)co 6075 ℝcr 8168 0cc0 8169 + caddc 8172 < clt 8350 ≤ cle 8351 − cmin 8487 ℤcz 9623 ..^cfzo 10527 ♯chash 11192 Word cword 11282 ++ cconcat 11336

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4241 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-iinf 4730 ax-cnex 8260 ax-resscn 8261 ax-1cn 8262 ax-1re 8263 ax-icn 8264 ax-addcl 8265 ax-addrcl 8266 ax-mulcl 8267 ax-addcom 8269 ax-addass 8271 ax-distr 8273 ax-i2m1 8274 ax-0lt1 8275 ax-0id 8277 ax-rnegex 8278 ax-cnre 8280 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283 ax-pre-apti 8284 ax-pre-ltadd 8285

This theorem depends on definitions: df-bi 117 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3636 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-int 3966 df-iun 4009 df-br 4126 df-opab 4188 df-mpt 4189 df-tr 4225 df-id 4433 df-iord 4506 df-on 4508 df-ilim 4509 df-suc 4511 df-iom 4733 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-res 4781 df-ima 4782 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-f1 5377 df-fo 5378 df-f1o 5379 df-fv 5380 df-riota 6028 df-ov 6078 df-oprab 6079 df-mpo 6080 df-1st 6364 df-2nd 6365 df-recs 6566 df-frec 6652 df-1o 6677 df-er 6797 df-en 7013 df-dom 7014 df-fin 7015 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355 df-le 8356 df-sub 8489 df-neg 8490 df-inn 9284 df-n0 9543 df-z 9624 df-uz 9901 df-fz 10391 df-fzo 10528 df-ihash 11193 df-word 11283 df-concat 11337

This theorem is referenced by: swrdccatin2 11479

W3C validator