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	37 40 43 66 73	elfzd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in (0 \dots \|x\|)$
75		pfxlen	$⊢ (x \in Word B \land \|x\| - 2 \in (0 \dots \|x\|)) \to \|x prefix (\|x\| - 2)\| = \|x\| - 2$
76	36 74 75	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x prefix (\|x\| - 2)\| = \|x\| - 2$
77	76 65	eqtr2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k = \|x prefix (\|x\| - 2)\|$
78	77	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)\|$
79		fveq2	$⊢ y = x prefix (\|x\| - 2) \to \|y\| = \|x prefix (\|x\| - 2)\|$
80	79	eqeq2d	$⊢ y = x prefix (\|x\| - 2) \to (2 k = \|y\| \leftrightarrow 2 k = \|x prefix (\|x\| - 2)\|)$
81		vex	$⊢ y \in V$
82	81 2	sbcie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow χ$
83		dfsbcq	$⊢ y = x prefix (\|x\| - 2) \to (\underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ)$
84	82 83	bitr3id	$⊢ y = x prefix (\|x\| - 2) \to (χ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 2)) / x \underset{˙}{]} φ)$
85	80 84	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{˙}{]} φ))$
86		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 χ)$
87		pfxcl	$⊢ x \in Word B \to x prefix (\|x\| - 2) \in Word B$
88	87	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$
89	85 86 88	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{˙}{]} φ)$
90	78 89	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{˙}{]} φ$
91		2nn0	$⊢ 2 \in ℕ_{0}$
92	91	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \in ℕ_{0}$
93	52	addid2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 + 2 = 2$
94		0red	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 \in ℝ$
95	65 67	eqeltrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 k \in ℝ$
96	94 95 70 51	leadd1dd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 0 + 2 \leq 2 k + 2$
97	93 96	eqbrtrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq 2 k + 2$
98	97 61	breqtrrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 \leq \|x\|$
99		nn0sub	$⊢ (2 \in ℕ_{0} \land \|x\| \in ℕ_{0}) \to (2 \leq \|x\| \leftrightarrow \|x\| - 2 \in ℕ_{0})$
100	99	biimpa	$⊢ ((2 \in ℕ_{0} \land \|x\| \in ℕ_{0}) \land 2 \leq \|x\|) \to \|x\| - 2 \in ℕ_{0}$
101	92 39 98 100	syl21anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in ℕ_{0}$
102	68	recnd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \in ℂ$
103	102 52 55	subsubd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - (2 - 1) = \|x\| - 2 + 1$
104		2m1e1	$⊢ 2 - 1 = 1$
105	104	a1i	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to 2 - 1 = 1$
106	105	oveq2d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - (2 - 1) = \|x\| - 1$
107	103 106	eqtr3d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 + 1 = \|x\| - 1$
108	68	lem1d	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \leq \|x\|$
109	107 108	eqbrtrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 + 1 \leq \|x\|$
110		nn0p1elfzo	$⊢ (\|x\| - 2 \in ℕ_{0} \land \|x\| \in ℕ_{0} \land \|x\| - 2 + 1 \leq \|x\|) \to \|x\| - 2 \in (0 ..^\|x\|)$
111	101 39 109 110	syl3anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 2 \in (0 ..^\|x\|)$
112		wrdsymbcl	$⊢ (x \in Word B \land \|x\| - 2 \in (0 ..^\|x\|)) \to x (\|x\| - 2) \in B$
113	36 111 112	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 2) \in B$
114	113	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$
115		nn0ge2m1nn0	$⊢ (\|x\| \in ℕ_{0} \land 2 \leq \|x\|) \to \|x\| - 1 \in ℕ_{0}$
116	39 98 115	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \in ℕ_{0}$
117	102 55	npcand	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 + 1 = \|x\|$
118	68	leidd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| \leq \|x\|$
119	117 118	eqbrtrd	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 + 1 \leq \|x\|$
120		nn0p1elfzo	$⊢ (\|x\| - 1 \in ℕ_{0} \land \|x\| \in ℕ_{0} \land \|x\| - 1 + 1 \leq \|x\|) \to \|x\| - 1 \in (0 ..^\|x\|)$
121	116 39 119 120	syl3anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to \|x\| - 1 \in (0 ..^\|x\|)$
122		wrdsymbcl	$⊢ (x \in Word B \land \|x\| - 1 \in (0 ..^\|x\|)) \to x (\|x\| - 1) \in B$
123	36 121 122	syl2anc	$⊢ (k \in ℕ_{0} \land (x \in Word B \land 2 (k + 1) = \|x\|)) \to x (\|x\| - 1) \in B$
124	123	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$
125		oveq1	$⊢ y = x prefix (\|x\| - 2) \to y ++ ⟨“ i j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩$
126	125	sbceq1d	$⊢ y = x prefix (\|x\| - 2) \to (\underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ)$
127	83 126	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{˙}{]} φ))$
128		id	$⊢ i = x (\|x\| - 2) \to i = x (\|x\| - 2)$
129		eqidd	$⊢ i = x (\|x\| - 2) \to j = j$
130	128 129	s2eqd	$⊢ i = x (\|x\| - 2) \to ⟨“ i j ”⟩ = ⟨“ x (\|x\| - 2) j ”⟩$
131	130	oveq2d	$⊢ i = x (\|x\| - 2) \to (x prefix (\|x\| - 2)) ++ ⟨“ i j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩$
132	131	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{˙}{]} φ)$
133	132	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{˙}{]} φ))$
134		eqidd	$⊢ j = x (\|x\| - 1) \to x (\|x\| - 2) = x (\|x\| - 2)$
135		id	$⊢ j = x (\|x\| - 1) \to j = x (\|x\| - 1)$
136	134 135	s2eqd	$⊢ j = x (\|x\| - 1) \to ⟨“ x (\|x\| - 2) j ”⟩ = ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
137	136	oveq2d	$⊢ j = x (\|x\| - 1) \to (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) j ”⟩ = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
138	137	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{˙}{]} φ)$
139	138	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{˙}{]} φ))$
140		ovex	$⊢ y ++ ⟨“ i j ”⟩ \in V$
141	140 3	sbcie	$⊢ \underset{˙}{[} (y ++ ⟨“ i j ”⟩) / x \underset{˙}{]} φ \leftrightarrow θ$
142	6 82 141	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{˙}{]} φ)$
143	127 133 139 142	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{˙}{]} φ)$
144	88 114 124 143	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{˙}{]} φ)$
145	90 144	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{˙}{]} φ$
146		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$
147		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 ℝ$
148		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}$
149	148	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 ℝ$
150	149 147	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 ℝ$
151	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 ℝ$
152	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$
153		0p1e1	$⊢ 0 + 1 = 1$
154		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 ℝ$
155	148	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$
156	147	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$
157	154 147 149 147 155 156	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$
158	153 157	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$
159	147 150 151 152 158	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)$
160	58 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 2 \leq 2 (k + 1)$
161		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\|$
162	160 161	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\|$
163		eqid	$⊢ \|x\| = \|x\|$
164	163	pfxlsw2ccat	$⊢ (x \in Word B \land 2 \leq \|x\|) \to x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
165	164	eqcomd	$⊢ (x \in Word B \land 2 \leq \|x\|) \to (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩ = x$
166	165	eqcomd	$⊢ (x \in Word B \land 2 \leq \|x\|) \to x = (x prefix (\|x\| - 2)) ++ ⟨“ x (\|x\| - 2) x (\|x\| - 1) ”⟩$
167	146 162 166	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) ”⟩$
168		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{˙}{]} φ)$
169	167 168	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{˙}{]} φ)$
170	145 169	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 φ$
171	170	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 φ)$
172	171	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 φ)$
173	172	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 φ))$
174	35 173	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 φ))$
175	10 14 18 22 31 174	nn0ind	$⊢ m \in ℕ_{0} \to \forall x \in Word B (2 m = \|x\| \to φ)$
176	175	adantl	$⊢ (A \in Word B \land m \in ℕ_{0}) \to \forall x \in Word B (2 m = \|x\| \to φ)$
177		simpl	$⊢ (A \in Word B \land m \in ℕ_{0}) \to A \in Word B$
178		fveq2	$⊢ x = A \to \|x\| = \|A\|$
179	178	eqeq2d	$⊢ x = A \to (2 m = \|x\| \leftrightarrow 2 m = \|A\|)$
180	179 4	imbi12d	$⊢ x = A \to ((2 m = \|x\| \to φ) \leftrightarrow (2 m = \|A\| \to τ))$
181	180	adantl	$⊢ ((A \in Word B \land m \in ℕ_{0}) \land x = A) \to ((2 m = \|x\| \to φ) \leftrightarrow (2 m = \|A\| \to τ))$
182	177 181	rspcdv	$⊢ (A \in Word B \land m \in ℕ_{0}) \to (\forall x \in Word B (2 m = \|x\| \to φ) \to (2 m = \|A\| \to τ))$
183	176 182	mpd	$⊢ (A \in Word B \land m \in ℕ_{0}) \to (2 m = \|A\| \to τ)$
184	183	imp	$⊢ ((A \in Word B \land m \in ℕ_{0}) \land 2 m = \|A\|) \to τ$
185	184	adantllr	$⊢ (((A \in Word B \land 2 ∥ \|A\|) \land m \in ℕ_{0}) \land 2 m = \|A\|) \to τ$
186		lencl	$⊢ A \in Word B \to \|A\| \in ℕ_{0}$
187		evennn02n	$⊢ \|A\| \in ℕ_{0} \to (2 ∥ \|A\| \leftrightarrow \exists m \in ℕ_{0} 2 m = \|A\|)$
188	187	biimpa	$⊢ (\|A\| \in ℕ_{0} \land 2 ∥ \|A\|) \to \exists m \in ℕ_{0} 2 m = \|A\|$
189	186 188	sylan	$⊢ (A \in Word B \land 2 ∥ \|A\|) \to \exists m \in ℕ_{0} 2 m = \|A\|$
190	185 189	r19.29a	$⊢ (A \in Word B \land 2 ∥ \|A\|) \to τ$

Metamath Proof Explorer

Theorem wrdt2ind

Proof