Theorem wrdt2ind 30627

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

Hypotheses

Ref	Expression
wrdt2ind.1	⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
wrdt2ind.2	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
wrdt2ind.3	⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))
wrdt2ind.4	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
wrdt2ind.5	⊢ 𝜓
wrdt2ind.6	⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))

Assertion

Ref	Expression
wrdt2ind	⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)

Distinct variable groups:   𝐴,𝑖,𝑥   𝐵,𝑖,𝑗,𝑥,𝑦   𝜒,𝑥   𝜑,𝑖,𝑗   𝜏,𝑥   𝜑,𝑦   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥,𝑦,𝑖,𝑗)   𝜒(𝑦,𝑖,𝑗)   𝜃(𝑦,𝑖,𝑗)   𝜏(𝑦,𝑖,𝑗)   𝐴(𝑦,𝑗)

Proof of Theorem wrdt2ind

Dummy variables 𝑚 𝑛 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7164	. . . . . . . . . 10 ⊢ (𝑛 = 0 → (2 · 𝑛) = (2 · 0))
2	1	eqeq1d 2823	. . . . . . . . 9 ⊢ (𝑛 = 0 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 0) = (♯‘𝑥)))
3	2	imbi1d 344	. . . . . . . 8 ⊢ (𝑛 = 0 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 0) = (♯‘𝑥) → 𝜑)))
4	3	ralbidv 3197	. . . . . . 7 ⊢ (𝑛 = 0 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 0) = (♯‘𝑥) → 𝜑)))
5		oveq2 7164	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
6	5	eqeq1d 2823	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑥)))
7	6	imbi1d 344	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑥) → 𝜑)))
8	7	ralbidv 3197	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑)))
9		oveq2 7164	. . . . . . . . . 10 ⊢ (𝑛 = (𝑘 + 1) → (2 · 𝑛) = (2 · (𝑘 + 1)))
10	9	eqeq1d 2823	. . . . . . . . 9 ⊢ (𝑛 = (𝑘 + 1) → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · (𝑘 + 1)) = (♯‘𝑥)))
11	10	imbi1d 344	. . . . . . . 8 ⊢ (𝑛 = (𝑘 + 1) → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
12	11	ralbidv 3197	. . . . . . 7 ⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
13		oveq2 7164	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚))
14	13	eqeq1d 2823	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝑥)))
15	14	imbi1d 344	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝑥) → 𝜑)))
16	15	ralbidv 3197	. . . . . . 7 ⊢ (𝑛 = 𝑚 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑)))
17		2t0e0 11807	. . . . . . . . . . . 12 ⊢ (2 · 0) = 0
18	17	eqeq1i 2826	. . . . . . . . . . 11 ⊢ ((2 · 0) = (♯‘𝑥) ↔ 0 = (♯‘𝑥))
19		eqcom 2828	. . . . . . . . . . 11 ⊢ (0 = (♯‘𝑥) ↔ (♯‘𝑥) = 0)
20	18, 19	bitri 277	. . . . . . . . . 10 ⊢ ((2 · 0) = (♯‘𝑥) ↔ (♯‘𝑥) = 0)
21		hasheq0 13725	. . . . . . . . . 10 ⊢ (𝑥 ∈ Word 𝐵 → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
22	20, 21	syl5bb 285	. . . . . . . . 9 ⊢ (𝑥 ∈ Word 𝐵 → ((2 · 0) = (♯‘𝑥) ↔ 𝑥 = ∅))
23		wrdt2ind.5	. . . . . . . . . 10 ⊢ 𝜓
24		wrdt2ind.1	. . . . . . . . . 10 ⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓))
25	23, 24	mpbiri 260	. . . . . . . . 9 ⊢ (𝑥 = ∅ → 𝜑)
26	22, 25	syl6bi 255	. . . . . . . 8 ⊢ (𝑥 ∈ Word 𝐵 → ((2 · 0) = (♯‘𝑥) → 𝜑))
27	26	rgen 3148	. . . . . . 7 ⊢ ∀𝑥 ∈ Word 𝐵((2 · 0) = (♯‘𝑥) → 𝜑)
28		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
29	28	eqeq2d 2832	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → ((2 · 𝑘) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑦)))
30		wrdt2ind.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
31	29, 30	imbi12d 347	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑦) → 𝜒)))
32	31	cbvralvw 3449	. . . . . . . 8 ⊢ (∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒))
33		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵)
34		0zd 11994	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℤ)
35		lencl 13883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ Word 𝐵 → (♯‘𝑥) ∈ ℕ0)
36	33, 35	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℕ0)
37	36	nn0zd 12086	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℤ)
38		2z 12015	. . . . . . . . . . . . . . . . . . . 20 ⊢ 2 ∈ ℤ
39	38	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℤ)
40	37, 39	zsubcld 12093	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℤ)
41		2re 11712	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 2 ∈ ℝ
42	41	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → 2 ∈ ℝ)
43		nn0re 11907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℝ)
44		0le2 11740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ≤ 2
45	44	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → 0 ≤ 2)
46		nn0ge0 11923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
47	42, 43, 45, 46	mulge0d 11217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ0 → 0 ≤ (2 · 𝑘))
48	47	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ (2 · 𝑘))
49		2cnd 11716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℂ)
50		simpl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0)
51	50	nn0cnd 11958	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℂ)
52		1cnd 10636	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈ ℂ)
53	49, 51, 52	adddid 10665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
54		simprr 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥))
55		2t1e2 11801	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 · 1) = 2
56	55	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) = 2)
57	56	oveq2d 7172	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2))
58	53, 54, 57	3eqtr3d 2864	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) = ((2 · 𝑘) + 2))
59	58	oveq1d 7171	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (((2 · 𝑘) + 2) − 2))
60	49, 51	mulcld 10661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈ ℂ)
61	60, 49	pncand 10998	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((2 · 𝑘) + 2) − 2) = (2 · 𝑘))
62	59, 61	eqtrd 2856	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (2 · 𝑘))
63	48, 62	breqtrrd 5094	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ ((♯‘𝑥) − 2))
64	40	zred 12088	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℝ)
65	36	nn0red 11957	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℝ)
66		2pos 11741	. . . . . . . . . . . . . . . . . . . 20 ⊢ 0 < 2
67	41	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℝ)
68	67, 65	ltsubposd 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 < 2 ↔ ((♯‘𝑥) − 2) < (♯‘𝑥)))
69	66, 68	mpbii 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) < (♯‘𝑥))
70	64, 65, 69	ltled 10788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ≤ (♯‘𝑥))
71		elfz2 12900	. . . . . . . . . . . . . . . . . . 19 ⊢ (((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)) ↔ ((0 ∈ ℤ ∧ (♯‘𝑥) ∈ ℤ ∧ ((♯‘𝑥) − 2) ∈ ℤ) ∧ (0 ≤ ((♯‘𝑥) − 2) ∧ ((♯‘𝑥) − 2) ≤ (♯‘𝑥))))
72	71	biimpri 230	. . . . . . . . . . . . . . . . . 18 ⊢ (((0 ∈ ℤ ∧ (♯‘𝑥) ∈ ℤ ∧ ((♯‘𝑥) − 2) ∈ ℤ) ∧ (0 ≤ ((♯‘𝑥) − 2) ∧ ((♯‘𝑥) − 2) ≤ (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)))
73	34, 37, 40, 63, 70, 72	syl32anc 1374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)))
74		pfxlen 14045	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) = ((♯‘𝑥) − 2))
75	33, 73, 74	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) = ((♯‘𝑥) − 2))
76	75, 62	eqtr2d 2857	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
77	76	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
78		fveq2 6670	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (♯‘𝑦) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
79	78	eqeq2d 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ((2 · 𝑘) = (♯‘𝑦) ↔ (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2)))))
80		vex 3497	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑦 ∈ V
81	80, 30	sbcie 3812	. . . . . . . . . . . . . . . . 17 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜒)
82		dfsbcq 3774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([𝑦 / 𝑥]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
83	81, 82	syl5bbr 287	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝜒 ↔ [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
84	79, 83	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (((2 · 𝑘) = (♯‘𝑦) → 𝜒) ↔ ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)))
85		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒))
86		pfxcl 14039	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ Word 𝐵 → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵)
87	86	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵)
88	84, 85, 87	rspcdva 3625	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
89	77, 88	mpd 15	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)
90		2nn0 11915	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 ∈ ℕ0
91	90	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℕ0)
92	49	addid2d 10841	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) = 2)
93		0red 10644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℝ)
94	62, 64	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈ ℝ)
95	93, 94, 67, 48	leadd1dd 11254	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) ≤ ((2 · 𝑘) + 2))
96	92, 95	eqbrtrrd 5090	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ ((2 · 𝑘) + 2))
97	96, 58	breqtrrd 5094	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (♯‘𝑥))
98		nn0sub 11948	. . . . . . . . . . . . . . . . . . 19 ⊢ ((2 ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) → (2 ≤ (♯‘𝑥) ↔ ((♯‘𝑥) − 2) ∈ ℕ0))
99	98	biimpa 479	. . . . . . . . . . . . . . . . . 18 ⊢ (((2 ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) ∧ 2 ≤ (♯‘𝑥)) → ((♯‘𝑥) − 2) ∈ ℕ0)
100	91, 36, 97, 99	syl21anc 835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℕ0)
101	65	recnd 10669	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℂ)
102	101, 49, 52	subsubd 11025	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) = (((♯‘𝑥) − 2) + 1))
103		2m1e1 11764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (2 − 1) = 1
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 − 1) = 1)
105	104	oveq2d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) = ((♯‘𝑥) − 1))
106	102, 105	eqtr3d 2858	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 2) + 1) = ((♯‘𝑥) − 1))
107	65	lem1d 11573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ≤ (♯‘𝑥))
108	106, 107	eqbrtrd 5088	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 2) + 1) ≤ (♯‘𝑥))
109		nn0p1elfzo 13081	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑥) − 2) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧ (((♯‘𝑥) − 2) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥)))
110	100, 36, 108, 109	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥)))
111		wrdsymbcl 13876	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
112	33, 110, 111	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
113	112	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
114		nn0ge2m1nn0 11966	. . . . . . . . . . . . . . . . . 18 ⊢ (((♯‘𝑥) ∈ ℕ0 ∧ 2 ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈ ℕ0)
115	36, 97, 114	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈ ℕ0)
116	101, 52	npcand 11001	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 1) + 1) = (♯‘𝑥))
117	65	leidd 11206	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ≤ (♯‘𝑥))
118	116, 117	eqbrtrd 5088	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 1) + 1) ≤ (♯‘𝑥))
119		nn0p1elfzo 13081	. . . . . . . . . . . . . . . . 17 ⊢ ((((♯‘𝑥) − 1) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧ (((♯‘𝑥) − 1) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
120	115, 36, 118, 119	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
121		wrdsymbcl 13876	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
122	33, 120, 121	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
123	122	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
124		oveq1 7163	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝑦 ++ ⟨“𝑖𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩))
125	124	sbceq1d 3777	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑))
126	82, 125	imbi12d 347	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (([𝑦 / 𝑥]𝜑 → [(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑)))
127		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑖 = (𝑥‘((♯‘𝑥) − 2)))
128		eqidd 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑗 = 𝑗)
129	127, 128	s2eqd 14225	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ⟨“𝑖𝑗”⟩ = ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩)
130	129	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩))
131	130	sbceq1d 3777	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑))
132	131	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑)))
133		eqidd 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (𝑥‘((♯‘𝑥) − 2)) = (𝑥‘((♯‘𝑥) − 2)))
134		id 22	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → 𝑗 = (𝑥‘((♯‘𝑥) − 1)))
135	133, 134	s2eqd 14225	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩ = ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩)
136	135	oveq2d 7172	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
137	136	sbceq1d 3777	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
138	137	imbi2d 343	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑)))
139		wrdt2ind.6	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃))
140		ovex 7189	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ++ ⟨“𝑖𝑗”⟩) ∈ V
141		wrdt2ind.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑 ↔ 𝜃))
142	140, 141	sbcie 3812	. . . . . . . . . . . . . . . 16 ⊢ ([(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑 ↔ 𝜃)
143	139, 81, 142	3imtr4g 298	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → ([𝑦 / 𝑥]𝜑 → [(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑))
144	126, 132, 138, 143	vtocl3ga 3578	. . . . . . . . . . . . . 14 ⊢ (((𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵 ∧ (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵 ∧ (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
145	87, 113, 123, 144	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
146	89, 145	mpd 15	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑)
147		simprl 769	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵)
148		1red 10642	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈ ℝ)
149		simpll 765	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0)
150	149	nn0red 11957	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℝ)
151	150, 148	readdcld 10670	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑘 + 1) ∈ ℝ)
152	41	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℝ)
153	44	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 2)
154		0p1e1 11760	. . . . . . . . . . . . . . . . . 18 ⊢ (0 + 1) = 1
155		0red 10644	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℝ)
156	149	nn0ge0d 11959	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 𝑘)
157	148	leidd 11206	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ 1)
158	155, 148, 150, 148, 156, 157	le2addd 11259	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 1) ≤ (𝑘 + 1))
159	154, 158	eqbrtrrid 5102	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ (𝑘 + 1))
160	148, 151, 152, 153, 159	lemul2ad 11580	. . . . . . . . . . . . . . . 16 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) ≤ (2 · (𝑘 + 1)))
161	55, 160	eqbrtrrid 5102	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (2 · (𝑘 + 1)))
162		simprr 771	. . . . . . . . . . . . . . 15 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥))
163	161, 162	breqtrd 5092	. . . . . . . . . . . . . 14 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (♯‘𝑥))
164		eqid 2821	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘𝑥) = (♯‘𝑥)
165	164	pfxlsw2ccat 30626	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
166	165	eqcomd 2827	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) = 𝑥)
167	166	eqcomd 2827	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
168	147, 163, 167	syl2anc 586	. . . . . . . . . . . . 13 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
169		sbceq1a 3783	. . . . . . . . . . . . 13 ⊢ (𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
170	168, 169	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
171	146, 170	mpbird 259	. . . . . . . . . . 11 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝜑)
172	171	expr 459	. . . . . . . . . 10 ⊢ (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ 𝑥 ∈ Word 𝐵) → ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))
173	172	ralrimiva 3182	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))
174	173	ex 415	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ0 → (∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
175	32, 174	syl5bi 244	. . . . . . 7 ⊢ (𝑘 ∈ ℕ0 → (∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
176	4, 8, 12, 16, 27, 175	nn0ind 12078	. . . . . 6 ⊢ (𝑚 ∈ ℕ0 → ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑))
177	176	adantl 484	. . . . 5 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑))
178		simpl 485	. . . . . 6 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → 𝐴 ∈ Word 𝐵)
179		fveq2 6670	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
180	179	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((2 · 𝑚) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝐴)))
181		wrdt2ind.4	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
182	180, 181	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
183	182	adantl 484	. . . . . 6 ⊢ (((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) ∧ 𝑥 = 𝐴) → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
184	178, 183	rspcdv 3615	. . . . 5 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → (∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑) → ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
185	177, 184	mpd 15	. . . 4 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → ((2 · 𝑚) = (♯‘𝐴) → 𝜏))
186	185	imp 409	. . 3 ⊢ (((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) ∧ (2 · 𝑚) = (♯‘𝐴)) → 𝜏)
187	186	adantllr 717	. 2 ⊢ ((((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) ∧ 𝑚 ∈ ℕ0) ∧ (2 · 𝑚) = (♯‘𝐴)) → 𝜏)
188		lencl 13883	. . 3 ⊢ (𝐴 ∈ Word 𝐵 → (♯‘𝐴) ∈ ℕ0)
189		evennn02n 15699	. . . 4 ⊢ ((♯‘𝐴) ∈ ℕ0 → (2 ∥ (♯‘𝐴) ↔ ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴)))
190	189	biimpa 479	. . 3 ⊢ (((♯‘𝐴) ∈ ℕ0 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴))
191	188, 190	sylan 582	. 2 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴))
192	187, 191	r19.29a 3289	1 ⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  [wsbc 3772  ∅c0 4291   class class class wbr 5066  ‘cfv 6355  (class class class)co 7156  ℝcr 10536  0cc0 10537  1c1 10538   + caddc 10540   · cmul 10542   < clt 10675   ≤ cle 10676   − cmin 10870  2c2 11693  ℕ₀cn0 11898  ℤcz 11982  ...cfz 12893  ..^cfzo 13034  ♯chash 13691  Word cword 13862   ++ cconcat 13922   prefix cpfx 14032  ⟨“cs2 14203   ∥ cdvds 15607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-fin 8513  df-card 9368  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11639  df-2 11701  df-n0 11899  df-xnn0 11969  df-z 11983  df-uz 12245  df-rp 12391  df-fz 12894  df-fzo 13035  df-hash 13692  df-word 13863  df-lsw 13915  df-concat 13923  df-s1 13950  df-substr 14003  df-pfx 14033  df-s2 14210  df-dvds 15608

This theorem is referenced by:  cyc3genpm  30794