swrds2

Description: Extract two adjacent symbols from a word. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 26-Feb-2016)

		Ref	Expression
	Assertion	swrds2	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I, I + 2⟩ = ⟨“ W (I) W (I + 1) ”⟩$

Proof

Step	Hyp	Ref	Expression
1		df-s2	$⊢ ⟨“ W (I) W (I + 1) ”⟩ = ⟨“ W (I) ”⟩ ++ ⟨“ W (I + 1) ”⟩$
2		simp1	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W \in Word A$
3		simp2	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \in ℕ_{0}$
4		elfzo0	$⊢ I + 1 \in (0 ..^\|W\|) \leftrightarrow (I + 1 \in ℕ_{0} \land \|W\| \in ℕ \land I + 1 < \|W\|)$
5	4	simp2bi	$⊢ I + 1 \in (0 ..^\|W\|) \to \|W\| \in ℕ$
6	5	3ad2ant3	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to \|W\| \in ℕ$
7	3	nn0red	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \in ℝ$
8		peano2nn0	$⊢ I \in ℕ_{0} \to I + 1 \in ℕ_{0}$
9	3 8	syl	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 \in ℕ_{0}$
10	9	nn0red	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 \in ℝ$
11	6	nnred	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to \|W\| \in ℝ$
12	7	lep1d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \leq I + 1$
13		elfzolt2	$⊢ I + 1 \in (0 ..^\|W\|) \to I + 1 < \|W\|$
14	13	3ad2ant3	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 < \|W\|$
15	7 10 11 12 14	lelttrd	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I < \|W\|$
16		elfzo0	$⊢ I \in (0 ..^\|W\|) \leftrightarrow (I \in ℕ_{0} \land \|W\| \in ℕ \land I < \|W\|)$
17	3 6 15 16	syl3anbrc	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \in (0 ..^\|W\|)$
18		swrds1	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to W substr ⟨I, I + 1⟩ = ⟨“ W (I) ”⟩$
19	2 17 18	syl2anc	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I, I + 1⟩ = ⟨“ W (I) ”⟩$
20		nn0cn	$⊢ I \in ℕ_{0} \to I \in ℂ$
21	20	3ad2ant2	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \in ℂ$
22		df-2	$⊢ 2 = 1 + 1$
23	22	oveq2i	$⊢ I + 2 = I + 1 + 1$
24		ax-1cn	$⊢ 1 \in ℂ$
25		addass	$⊢ (I \in ℂ \land 1 \in ℂ \land 1 \in ℂ) \to I + 1 + 1 = I + 1 + 1$
26	24 24 25	mp3an23	$⊢ I \in ℂ \to I + 1 + 1 = I + 1 + 1$
27	23 26	eqtr4id	$⊢ I \in ℂ \to I + 2 = I + 1 + 1$
28	21 27	syl	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 2 = I + 1 + 1$
29	28	opeq2d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to ⟨I + 1, I + 2⟩ = ⟨I + 1, I + 1 + 1⟩$
30	29	oveq2d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I + 1, I + 2⟩ = W substr ⟨I + 1, I + 1 + 1⟩$
31		swrds1	$⊢ (W \in Word A \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I + 1, I + 1 + 1⟩ = ⟨“ W (I + 1) ”⟩$
32	31	3adant2	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I + 1, I + 1 + 1⟩ = ⟨“ W (I + 1) ”⟩$
33	30 32	eqtrd	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I + 1, I + 2⟩ = ⟨“ W (I + 1) ”⟩$
34	19 33	oveq12d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to (W substr ⟨I, I + 1⟩) ++ (W substr ⟨I + 1, I + 2⟩) = ⟨“ W (I) ”⟩ ++ ⟨“ W (I + 1) ”⟩$
35	1 34	eqtr4id	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to ⟨“ W (I) W (I + 1) ”⟩ = (W substr ⟨I, I + 1⟩) ++ (W substr ⟨I + 1, I + 2⟩)$
36		elfz2nn0	$⊢ I \in (0 \dots I + 1) \leftrightarrow (I \in ℕ_{0} \land I + 1 \in ℕ_{0} \land I \leq I + 1)$
37	3 9 12 36	syl3anbrc	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I \in (0 \dots I + 1)$
38		peano2nn0	$⊢ I + 1 \in ℕ_{0} \to I + 1 + 1 \in ℕ_{0}$
39	9 38	syl	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 + 1 \in ℕ_{0}$
40	28 39	eqeltrd	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 2 \in ℕ_{0}$
41	10	lep1d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 \leq I + 1 + 1$
42	41 28	breqtrrd	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 \leq I + 2$
43		elfz2nn0	$⊢ I + 1 \in (0 \dots I + 2) \leftrightarrow (I + 1 \in ℕ_{0} \land I + 2 \in ℕ_{0} \land I + 1 \leq I + 2)$
44	9 40 42 43	syl3anbrc	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 \in (0 \dots I + 2)$
45		fzofzp1	$⊢ I + 1 \in (0 ..^\|W\|) \to I + 1 + 1 \in (0 \dots \|W\|)$
46	45	3ad2ant3	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 1 + 1 \in (0 \dots \|W\|)$
47	28 46	eqeltrd	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to I + 2 \in (0 \dots \|W\|)$
48		ccatswrd	$⊢ (W \in Word A \land (I \in (0 \dots I + 1) \land I + 1 \in (0 \dots I + 2) \land I + 2 \in (0 \dots \|W\|))) \to (W substr ⟨I, I + 1⟩) ++ (W substr ⟨I + 1, I + 2⟩) = W substr ⟨I, I + 2⟩$
49	2 37 44 47 48	syl13anc	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to (W substr ⟨I, I + 1⟩) ++ (W substr ⟨I + 1, I + 2⟩) = W substr ⟨I, I + 2⟩$
50	35 49	eqtr2d	$⊢ (W \in Word A \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I, I + 2⟩ = ⟨“ W (I) W (I + 1) ”⟩$

Metamath Proof Explorer

Theorem swrds2

Proof