swrds1

Description: Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		swrdcl	$⊢ W \in Word A \to W substr ⟨I, I + 1⟩ \in Word A$
2		simpl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to W \in Word A$
3		elfzouz	$⊢ I \in (0 ..^\|W\|) \to I \in ℤ_{\geq 0}$
4	3	adantl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I \in ℤ_{\geq 0}$
5		elfzoelz	$⊢ I \in (0 ..^\|W\|) \to I \in ℤ$
6	5	adantl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I \in ℤ$
7		uzid	$⊢ I \in ℤ \to I \in ℤ_{\geq I}$
8		peano2uz	$⊢ I \in ℤ_{\geq I} \to I + 1 \in ℤ_{\geq I}$
9	6 7 8	3syl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I + 1 \in ℤ_{\geq I}$
10		elfzuzb	$⊢ I \in (0 \dots I + 1) \leftrightarrow (I \in ℤ_{\geq 0} \land I + 1 \in ℤ_{\geq I})$
11	4 9 10	sylanbrc	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I \in (0 \dots I + 1)$
12		fzofzp1	$⊢ I \in (0 ..^\|W\|) \to I + 1 \in (0 \dots \|W\|)$
13	12	adantl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I + 1 \in (0 \dots \|W\|)$
14		swrdlen	$⊢ (W \in Word A \land I \in (0 \dots I + 1) \land I + 1 \in (0 \dots \|W\|)) \to \|W substr ⟨I, I + 1⟩\| = I + 1 - I$
15	2 11 13 14	syl3anc	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to \|W substr ⟨I, I + 1⟩\| = I + 1 - I$
16	6	zcnd	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I \in ℂ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		pncan2	$⊢ (I \in ℂ \land 1 \in ℂ) \to I + 1 - I = 1$
19	16 17 18	sylancl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I + 1 - I = 1$
20	15 19	eqtrd	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to \|W substr ⟨I, I + 1⟩\| = 1$
21		eqs1	$⊢ (W substr ⟨I, I + 1⟩ \in Word A \land \|W substr ⟨I, I + 1⟩\| = 1) \to W substr ⟨I, I + 1⟩ = ⟨“ (W substr ⟨I, I + 1⟩) (0) ”⟩$
22	1 20 21	syl2an2r	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to W substr ⟨I, I + 1⟩ = ⟨“ (W substr ⟨I, I + 1⟩) (0) ”⟩$
23		0z	$⊢ 0 \in ℤ$
24		snidg	$⊢ 0 \in ℤ \to 0 \in \{0\}$
25	23 24	ax-mp	$⊢ 0 \in \{0\}$
26	19	oveq2d	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to (0 ..^I + 1 - I) = (0 ..^1)$
27		fzo01	$⊢ (0 ..^1) = \{0\}$
28	26 27	syl6eq	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to (0 ..^I + 1 - I) = \{0\}$
29	25 28	eleqtrrid	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to 0 \in (0 ..^I + 1 - I)$
30		swrdfv	$⊢ ((W \in Word A \land I \in (0 \dots I + 1) \land I + 1 \in (0 \dots \|W\|)) \land 0 \in (0 ..^I + 1 - I)) \to (W substr ⟨I, I + 1⟩) (0) = W (0 + I)$
31	2 11 13 29 30	syl31anc	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to (W substr ⟨I, I + 1⟩) (0) = W (0 + I)$
32		addid2	$⊢ I \in ℂ \to 0 + I = I$
33	32	eqcomd	$⊢ I \in ℂ \to I = 0 + I$
34	16 33	syl	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to I = 0 + I$
35	34	fveq2d	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to W (I) = W (0 + I)$
36	31 35	eqtr4d	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to (W substr ⟨I, I + 1⟩) (0) = W (I)$
37	36	s1eqd	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to ⟨“ (W substr ⟨I, I + 1⟩) (0) ”⟩ = ⟨“ W (I) ”⟩$
38	22 37	eqtrd	$⊢ (W \in Word A \land I \in (0 ..^\|W\|)) \to W substr ⟨I, I + 1⟩ = ⟨“ W (I) ”⟩$

Metamath Proof Explorer

Theorem swrds1

Proof