wrdt2ind

Description: Perform an induction over the structure of a word of even length. (Contributed by Thierry Arnoux, 26-Sep-2023)

	Ref	Expression
Hypotheses	wrdt2ind.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
	wrdt2ind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	wrdt2ind.3	$⊢ x = y ++ ⟨“ i j ”⟩ \to (φ \leftrightarrow θ)$
	wrdt2ind.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	wrdt2ind.5	$⊢ ψ$
	wrdt2ind.6	$⊢ (y \in Word B \land i \in B \land j \in B) \to (χ \to θ)$
Assertion	wrdt2ind	$⊢ (A \in Word B \land 2 ∥ \|A\|) \to τ$

Proof

Step	Hyp	Ref	Expression
1		wrdt2ind.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
2		wrdt2ind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		wrdt2ind.3	$⊢ x = y ++ ⟨“ i j ”⟩ \to (φ \leftrightarrow θ)$
4		wrdt2ind.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		wrdt2ind.5	$⊢ ψ$
6		wrdt2ind.6	$⊢ (y \in Word B \land i \in B \land j \in B) \to (χ \to θ)$
7		oveq2	$⊢ n = 0 \to 2 n = 2 \cdot 0$
8	7	eqeq1d	$⊢ n = 0 \to (2 n = \|x\| \leftrightarrow 2 \cdot 0 = \|x\|)$
9	8	imbi1d	$⊢ n = 0 \to ((2 n = \|x\| \to φ) \leftrightarrow (2 \cdot 0 = \|x\| \to φ))$
10	9	ralbidv	$⊢ n = 0 \to (\forall x \in Word B (2 n = \|x\| \to φ) \leftrightarrow \forall x \in Word B (2 \cdot 0 = \|x\| \to φ))$
11		oveq2	$⊢ n = k \to 2 n = 2 k$
12	11	eqeq1d	$⊢ n = k \to (2 n = \|x\| \leftrightarrow 2 k = \|x\|)$
13	12	imbi1d	$⊢ n = k \to ((2 n = \|x\| \to φ) \leftrightarrow (2 k = \|x\| \to φ))$
14	13	ralbidv	$⊢ n = k \to (\forall x \in Word B (2 n = \|x\| \to φ) \leftrightarrow \forall x \in Word B (2 k = \|x\| \to φ))$
15		oveq2	$⊢ n = k + 1 \to 2 n = 2 (k + 1)$
16	15	eqeq1d	$⊢ n = k + 1 \to (2 n = \|x\| \leftrightarrow 2 (k + 1) = \|x\|)$
17	16	imbi1d	$⊢ n = k + 1 \to ((2 n = \|x\| \to φ) \leftrightarrow (2 (k + 1) = \|x\| \to φ))$
18	17	ralbidv	$⊢ n = k + 1 \to (\forall x \in Word B (2 n = \|x\| \to φ) \leftrightarrow \forall x \in Word B (2 (k + 1) = \|x\| \to φ))$
19		oveq2	$⊢ n = m \to 2 n = 2 m$
20	19	eqeq1d	$⊢ n = m \to (2 n = \|x\| \leftrightarrow 2 m = \|x\|)$
21	20	imbi1d	$⊢ n = m \to ((2 n = \|x\| \to φ) \leftrightarrow (2 m = \|x\| \to φ))$
22	21	ralbidv	$⊢ n = m \to (\forall x \in Word B (2 n = \|x\| \to φ) \leftrightarrow \forall x \in Word B (2 m = \|x\| \to φ))$
23		2t0e0	$⊢ 2 \cdot 0 = 0$
24	23	eqeq1i	$⊢ 2 \cdot 0 = \|x\| \leftrightarrow 0 = \|x\|$
25		eqcom	$⊢ 0 = \|x\| \leftrightarrow \|x\| = 0$
26	24 25	bitri	$⊢ 2 \cdot 0 = \|x\| \leftrightarrow \|x\| = 0$
27		hasheq0	$⊢ x \in Word B \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
28	26 27	syl5bb	$⊢ x \in Word B \to (2 \cdot 0 = \|x\| \leftrightarrow x = \emptyset)$
29	5 1	mpbiri	$⊢ x = \emptyset \to φ$
30	28 29	syl6bi	$⊢ x \in Word B \to (2 \cdot 0 = \|x\| \to φ)$
31	30	rgen	$⊢ \forall x \in Word B (2 \cdot 0 = \|x\| \to φ)$
32		fveq2	$⊢ x = y \to \|x\| = \|y\|$
33	32	eqeq2d	$⊢ x = y \to (2 k = \|x\| \leftrightarrow 2 k = \|y\|)$
34	33 2	imbi12d	$⊢ x = y \to ((2 k = \|x\| \to φ) \leftrightarrow (2 k = \|y\| \to χ))$
35	34	cbvralvw	$⊢ \forall x \in Word B (2 k = \|x\| \to φ) \leftrightarrow \forall y \in Word B (2 k = \|y\| \to χ)$
36		simprl	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x \in Word B$
37		0zd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \in ℤ$
38		lencl	$⊢ x \in Word B \to \|x\| \in ℕ_{0}$
39	36 38	syl	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \in ℕ_{0}$
40	39	nn0zd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \in ℤ$
41		2z	$⊢ 2 \in ℤ$
42	41	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℤ$
43	40 42	zsubcld	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in ℤ$
44		2re	$⊢ 2 \in ℝ$
45	44	a1i	$⊢ k \in ℕ_{0} \to 2 \in ℝ$
46		nn0re	$⊢ k \in ℕ_{0} \to k \in ℝ$
47		0le2	$⊢ 0 \leq 2$
48	47	a1i	$⊢ k \in ℕ_{0} \to 0 \leq 2$
49		nn0ge0	$⊢ k \in ℕ_{0} \to 0 \leq k$
50	45 46 48 49	mulge0d	$⊢ k \in ℕ_{0} \to 0 \leq 2 k$
51	50	adantr	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \leq 2 k$
52		2cnd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℂ$
53		simpl	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to k \in ℕ_{0}$
54	53	nn0cnd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to k \in ℂ$
55		1cnd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 1 \in ℂ$
56	52 54 55	adddid	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 (k + 1) = 2 k + 2 \cdot 1$
57		simprr	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 (k + 1) = \|x\|$
58		2t1e2	$⊢ 2 \cdot 1 = 2$
59	58	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \cdot 1 = 2$
60	59	oveq2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k + 2 \cdot 1 = 2 k + 2$
61	56 57 60	3eqtr3d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| = 2 k + 2$
62	61	oveq1d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 = 2 k + 2 - 2$
63	52 54	mulcld	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k \in ℂ$
64	63 52	pncand	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k + 2 - 2 = 2 k$
65	62 64	eqtrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 = 2 k$
66	51 65	breqtrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \leq \|x\| - 2$
67	43	zred	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in ℝ$
68	39	nn0red	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \in ℝ$
69		2pos	$⊢ 0 < 2$
70	44	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℝ$
71	70 68	ltsubposd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to (0 < 2 \leftrightarrow \|x\| - 2 < \|x\|)$
72	69 71	mpbii	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 < \|x\|$
73	67 68 72	ltled	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \leq \|x\|$
74		elfz2	$⊢ \|x\| - 2 \in (0 \dots \|x\|) \leftrightarrow ((0 \in ℤ \land \|x\| \in ℤ \land \|x\| - 2 \in ℤ) \land (0 \leq \|x\| - 2 \land \|x\| - 2 \leq \|x\|))$
75	74	biimpri	$⊢ ((0 \in ℤ \land \|x\| \in ℤ \land \|x\| - 2 \in ℤ) \land (0 \leq \|x\| - 2 \land \|x\| - 2 \leq \|x\|)) \to \|x\| - 2 \in (0 \dots \|x\|)$
76	37 40 43 66 73 75	syl32anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in (0 \dots \|x\|)$
77		pfxlen	$⊢ (x \in Word B \land \|x\| - 2 \in (0 \dots \|x\|)) \to \|x prefix (\|x\| - 2)\| = \|x\| - 2$
78	36 76 77	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x prefix (\|x\| - 2)\| = \|x\| - 2$
79	78 65	eqtr2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k = \|x prefix (\|x\| - 2)\|$
80	79	adantlr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k = \|x prefix (\|x\| - 2)\|$
81		fveq2	$⊢ y = x prefix (\|x\| - 2) \to \|y\| = \|x prefix (\|x\| - 2)\|$
82	81	eqeq2d	$⊢ y = x prefix (\|x\| - 2) \to (2 k = \|y\| \leftrightarrow 2 k = \|x prefix (\|x\| - 2)\|)$
83		vex	$⊢ y \in V$
84	83 2	sbcie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow χ$
85		dfsbcq	$⊢ y = x prefix (\|x\| - 2) \to (\underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ)$
86	84 85	syl5bbr	$⊢ y = x prefix (\|x\| - 2) \to (χ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ)$
87	82 86	imbi12d	$⊢ y = x prefix (\|x\| - 2) \to ((2 k = \|y\| \to χ) \leftrightarrow (2 k = \|x prefix (\|x\| - 2)\| \to \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ))$
88		simplr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \forall y \in Word B (2 k = \|y\| \to χ)$
89		pfxcl	$⊢ x \in Word B \to x prefix (\|x\| - 2) \in Word B$
90	89	ad2antrl	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x prefix (\|x\| - 2) \in Word B$
91	87 88 90	rspcdva	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to (2 k = \|x prefix (\|x\| - 2)\| \to \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ)$
92	80 91	mpd	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ$
93		2nn0	$⊢ 2 \in ℕ_{0}$
94	93	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℕ_{0}$
95	52	addid2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 + 2 = 2$
96		0red	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \in ℝ$
97	65 67	eqeltrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k \in ℝ$
98	96 97 70 51	leadd1dd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 + 2 \leq 2 k + 2$
99	95 98	eqbrtrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq 2 k + 2$
100	99 61	breqtrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq \|x\|$
101		nn0sub	$⊢ (2 \in ℕ_{0} \land \|x\| \in ℕ_{0}) \to (2 \leq \|x\| \leftrightarrow \|x\| - 2 \in ℕ_{0})$
102	101	biimpa	$⊢ ((2 \in ℕ_{0} \land \|x\| \in ℕ_{0}) \land 2 \leq \|x\|) \to \|x\| - 2 \in ℕ_{0}$
103	94 39 100 102	syl21anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in ℕ_{0}$
104	68	recnd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \in ℂ$
105	104 52 55	subsubd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - (2 - 1) = \|x\| - 2 + 1$
106		2m1e1	$⊢ 2 - 1 = 1$
107	106	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 - 1 = 1$
108	107	oveq2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - (2 - 1) = \|x\| - 1$
109	105 108	eqtr3d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 + 1 = \|x\| - 1$
110	68	lem1d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \leq \|x\|$
111	109 110	eqbrtrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 + 1 \leq \|x\|$
112		nn0p1elfzo	$⊢ (\|x\| - 2 \in ℕ_{0} \land \|x\| \in ℕ_{0} \land \|x\| - 2 + 1 \leq \|x\|) \to \|x\| - 2 \in (0 ..^\|x\|)$
113	103 39 111 112	syl3anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in (0 ..^\|x\|)$
114		wrdsymbcl	$⊢ (x \in Word B \land \|x\| - 2 \in (0 ..^\|x\|)) \to x (\|x\| - 2) \in B$
115	36 113 114	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 2) \in B$
116	115	adantlr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 2) \in B$
117		nn0ge2m1nn0	$⊢ (\|x\| \in ℕ_{0} \land 2 \leq \|x\|) \to \|x\| - 1 \in ℕ_{0}$
118	39 100 117	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \in ℕ_{0}$
119	104 55	npcand	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 + 1 = \|x\|$
120	68	leidd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \leq \|x\|$
121	119 120	eqbrtrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 + 1 \leq \|x\|$
122		nn0p1elfzo	$⊢ (\|x\| - 1 \in ℕ_{0} \land \|x\| \in ℕ_{0} \land \|x\| - 1 + 1 \leq \|x\|) \to \|x\| - 1 \in (0 ..^\|x\|)$
123	118 39 121 122	syl3anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \in (0 ..^\|x\|)$
124		wrdsymbcl	$⊢ (x \in Word B \land \|x\| - 1 \in (0 ..^\|x\|)) \to x (\|x\| - 1) \in B$
125	36 123 124	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 1) \in B$
126	125	adantlr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 1) \in B$
127		oveq1	$⊢ y = x prefix (\|x\| - 2) \to y ++ ⟨“ i j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩$
128	127	sbceq1d	$⊢ y = x prefix (\|x\| - 2) \to (\underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ)$
129	85 128	imbi12d	$⊢ y = x prefix (\|x\| - 2) \to ((\underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ))$
130		id	$⊢ i = x (\|x\| - 2) \to i = x (\|x\| - 2)$
131		eqidd	$⊢ i = x (\|x\| - 2) \to j = j$
132	130 131	s2eqd	$⊢ i = x (\|x\| - 2) \to ⟨“ i j ”⟩ = ⟨“ x (\|x\| - 2) j ”⟩$
133	132	oveq2d	$⊢ i = x (\|x\| - 2) \to (x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩$
134	133	sbceq1d	$⊢ i = x (\|x\| - 2) \to (\underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩) / x \underset{˙}{]} φ)$
135	134	imbi2d	$⊢ i = x (\|x\| - 2) \to ((\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩) / x \underset{˙}{]} φ))$
136		eqidd	$⊢ j = x (\|x\| - 1) \to x (\|x\| - 2) = x (\|x\| - 2)$
137		id	$⊢ j = x (\|x\| - 1) \to j = x (\|x\| - 1)$
138	136 137	s2eqd	$⊢ j = x (\|x\| - 1) \to ⟨“ x (\|x\| - 2) j ”⟩ = ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
139	138	oveq2d	$⊢ j = x (\|x\| - 1) \to (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
140	139	sbceq1d	$⊢ j = x (\|x\| - 1) \to (\underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ)$
141	140	imbi2d	$⊢ j = x (\|x\| - 1) \to ((\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩) / x \underset{˙}{]} φ) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ))$
142		ovex	$⊢ y ++ ⟨“ i j ”⟩ \in V$
143	142 3	sbcie	$⊢ \underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ \leftrightarrow θ$
144	6 84 143	3imtr4g	$⊢ (y \in Word B \land i \in B \land j \in B) \to (\underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ)$
145	129 135 141 144	vtocl3ga	$⊢ (x prefix (\|x\| - 2) \in Word B \land x (\|x\| - 2) \in B \land x (\|x\| - 1) \in B) \to (\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ)$
146	90 116 126 145	syl3anc	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to (\underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ)$
147	92 146	mpd	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ$
148		simprl	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x \in Word B$
149		1red	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 1 \in ℝ$
150		simpll	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to k \in ℕ_{0}$
151	150	nn0red	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to k \in ℝ$
152	151 149	readdcld	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to k + 1 \in ℝ$
153	44	a1i	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℝ$
154	47	a1i	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \leq 2$
155		0p1e1	$⊢ 0 + 1 = 1$
156		0red	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \in ℝ$
157	150	nn0ge0d	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \leq k$
158	149	leidd	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 1 \leq 1$
159	156 149 151 149 157 158	le2addd	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 + 1 \leq k + 1$
160	155 159	eqbrtrrid	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 1 \leq k + 1$
161	149 152 153 154 160	lemul2ad	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \cdot 1 \leq 2 (k + 1)$
162	58 161	eqbrtrrid	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq 2 (k + 1)$
163		simprr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 (k + 1) = \|x\|$
164	162 163	breqtrd	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq \|x\|$
165		eqid	$⊢ \|x\| = \|x\|$
166	165	pfxlsw2ccat	$⊢ (x \in Word B \land 2 \leq \|x\|) \to x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
167	166	eqcomd	$⊢ (x \in Word B \land 2 \leq \|x\|) \to (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩ = x$
168	167	eqcomd	$⊢ (x \in Word B \land 2 \leq \|x\|) \to x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
169	148 164 168	syl2anc	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
170		sbceq1a	$⊢ x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩ \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ)$
171	169 170	syl	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩) / x \underset{˙}{]} φ)$
172	147 171	mpbird	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to φ$
173	172	expr	$⊢ ((k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \land x \in Word B) \to (2 (k + 1) = \|x\| \to φ)$
174	173	ralrimiva	$⊢ (k \in ℕ_{0} \land \forall y \in Word B (2 k = \|y\| \to χ)) \to \forall x \in Word B (2 (k + 1) = \|x\| \to φ)$
175	174	ex	$⊢ k \in ℕ_{0} \to (\forall y \in Word B (2 k = \|y\| \to χ) \to \forall x \in Word B (2 (k + 1) = \|x\| \to φ))$
176	35 175	syl5bi	$⊢ k \in ℕ_{0} \to (\forall x \in Word B (2 k = \|x\| \to φ) \to \forall x \in Word B (2 (k + 1) = \|x\| \to φ))$
177	10 14 18 22 31 176	nn0ind	$⊢ m \in ℕ_{0} \to \forall x \in Word B (2 m = \|x\| \to φ)$
178	177	adantl	$⊢ (A \in Word B \land m \in ℕ_{0}) \to \forall x \in Word B (2 m = \|x\| \to φ)$
179		simpl	$⊢ (A \in Word B \land m \in ℕ_{0}) \to A \in Word B$
180		fveq2	$⊢ x = A \to \|x\| = \|A\|$
181	180	eqeq2d	$⊢ x = A \to (2 m = \|x\| \leftrightarrow 2 m = \|A\|)$
182	181 4	imbi12d	$⊢ x = A \to ((2 m = \|x\| \to φ) \leftrightarrow (2 m = \|A\| \to τ))$
183	182	adantl	$⊢ ((A \in Word B \land m \in ℕ_{0}) \land x = A) \to ((2 m = \|x\| \to φ) \leftrightarrow (2 m = \|A\| \to τ))$
184	179 183	rspcdv	$⊢ (A \in Word B \land m \in ℕ_{0}) \to (\forall x \in Word B (2 m = \|x\| \to φ) \to (2 m = \|A\| \to τ))$
185	178 184	mpd	$⊢ (A \in Word B \land m \in ℕ_{0}) \to (2 m = \|A\| \to τ)$
186	185	imp	$⊢ ((A \in Word B \land m \in ℕ_{0}) \land 2 m = \|A\|) \to τ$
187	186	adantllr	$⊢ (((A \in Word B \land 2 ∥ \|A\|) \land m \in ℕ_{0}) \land 2 m = \|A\|) \to τ$
188		lencl	$⊢ A \in Word B \to \|A\| \in ℕ_{0}$
189		evennn02n	$⊢ \|A\| \in ℕ_{0} \to (2 ∥ \|A\| \leftrightarrow \exists m \in ℕ_{0} 2 m = \|A\|)$
190	189	biimpa	$⊢ (\|A\| \in ℕ_{0} \land 2 ∥ \|A\|) \to \exists m \in ℕ_{0} 2 m = \|A\|$
191	188 190	sylan	$⊢ (A \in Word B \land 2 ∥ \|A\|) \to \exists m \in ℕ_{0} 2 m = \|A\|$
192	187 191	r19.29a	$⊢ (A \in Word B \land 2 ∥ \|A\|) \to τ$

Metamath Proof Explorer

Theorem wrdt2ind

Proof