Metamath Proof Explorer

Theorem 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 ⊢ ( 𝑥 = ∅ → ( 𝜑 ↔ 𝜓 ) )
wrdt2ind.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
wrdt2ind.3 ⊢ ( 𝑥 = ( 𝑦 ++ ⟨“ 𝑖 𝑗 ”⟩ ) → ( 𝜑 ↔ 𝜃 ) )
wrdt2ind.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
wrdt2ind.5 ⊢ 𝜓
wrdt2ind.6 ⊢ ( ( 𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵 ) → ( 𝜒 → 𝜃 ) )
Assertion wrdt2ind ( ( 𝐴 ∈ Word 𝐵 ∧ 2 ∥ ( ♯ ‘ 𝐴 ) ) → 𝜏 )

Proof

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