Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wrdt2ind Structured version   Visualization version   GIF version

Theorem wrdt2ind 30541
 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.
StepHypRef Expression
1 oveq2 7159 . . . . . . . . . 10 (𝑛 = 0 → (2 · 𝑛) = (2 · 0))
21eqeq1d 2827 . . . . . . . . 9 (𝑛 = 0 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 0) = (♯‘𝑥)))
32imbi1d 343 . . . . . . . 8 (𝑛 = 0 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 0) = (♯‘𝑥) → 𝜑)))
43ralbidv 3201 . . . . . . 7 (𝑛 = 0 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 0) = (♯‘𝑥) → 𝜑)))
5 oveq2 7159 . . . . . . . . . 10 (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘))
65eqeq1d 2827 . . . . . . . . 9 (𝑛 = 𝑘 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑥)))
76imbi1d 343 . . . . . . . 8 (𝑛 = 𝑘 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑥) → 𝜑)))
87ralbidv 3201 . . . . . . 7 (𝑛 = 𝑘 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑)))
9 oveq2 7159 . . . . . . . . . 10 (𝑛 = (𝑘 + 1) → (2 · 𝑛) = (2 · (𝑘 + 1)))
109eqeq1d 2827 . . . . . . . . 9 (𝑛 = (𝑘 + 1) → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · (𝑘 + 1)) = (♯‘𝑥)))
1110imbi1d 343 . . . . . . . 8 (𝑛 = (𝑘 + 1) → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
1211ralbidv 3201 . . . . . . 7 (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
13 oveq2 7159 . . . . . . . . . 10 (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚))
1413eqeq1d 2827 . . . . . . . . 9 (𝑛 = 𝑚 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝑥)))
1514imbi1d 343 . . . . . . . 8 (𝑛 = 𝑚 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝑥) → 𝜑)))
1615ralbidv 3201 . . . . . . 7 (𝑛 = 𝑚 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑)))
17 2t0e0 11798 . . . . . . . . . . . 12 (2 · 0) = 0
1817eqeq1i 2830 . . . . . . . . . . 11 ((2 · 0) = (♯‘𝑥) ↔ 0 = (♯‘𝑥))
19 eqcom 2832 . . . . . . . . . . 11 (0 = (♯‘𝑥) ↔ (♯‘𝑥) = 0)
2018, 19bitri 276 . . . . . . . . . 10 ((2 · 0) = (♯‘𝑥) ↔ (♯‘𝑥) = 0)
21 hasheq0 13717 . . . . . . . . . 10 (𝑥 ∈ Word 𝐵 → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅))
2220, 21syl5bb 284 . . . . . . . . 9 (𝑥 ∈ Word 𝐵 → ((2 · 0) = (♯‘𝑥) ↔ 𝑥 = ∅))
23 wrdt2ind.5 . . . . . . . . . 10 𝜓
24 wrdt2ind.1 . . . . . . . . . 10 (𝑥 = ∅ → (𝜑𝜓))
2523, 24mpbiri 259 . . . . . . . . 9 (𝑥 = ∅ → 𝜑)
2622, 25syl6bi 254 . . . . . . . 8 (𝑥 ∈ Word 𝐵 → ((2 · 0) = (♯‘𝑥) → 𝜑))
2726rgen 3152 . . . . . . 7 𝑥 ∈ Word 𝐵((2 · 0) = (♯‘𝑥) → 𝜑)
28 fveq2 6666 . . . . . . . . . . 11 (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦))
2928eqeq2d 2836 . . . . . . . . . 10 (𝑥 = 𝑦 → ((2 · 𝑘) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑦)))
30 wrdt2ind.2 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝜑𝜒))
3129, 30imbi12d 346 . . . . . . . . 9 (𝑥 = 𝑦 → (((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑦) → 𝜒)))
3231cbvralv 3457 . . . . . . . 8 (∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒))
33 simprl 767 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵)
34 0zd 11985 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℤ)
35 lencl 13876 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ Word 𝐵 → (♯‘𝑥) ∈ ℕ0)
3633, 35syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℕ0)
3736nn0zd 12077 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℤ)
38 2z 12006 . . . . . . . . . . . . . . . . . . . 20 2 ∈ ℤ
3938a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℤ)
4037, 39zsubcld 12084 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℤ)
41 2re 11703 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℝ
4241a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → 2 ∈ ℝ)
43 nn0re 11898 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0𝑘 ∈ ℝ)
44 0le2 11731 . . . . . . . . . . . . . . . . . . . . . 22 0 ≤ 2
4544a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → 0 ≤ 2)
46 nn0ge0 11914 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ℕ0 → 0 ≤ 𝑘)
4742, 43, 45, 46mulge0d 11209 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → 0 ≤ (2 · 𝑘))
4847adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ (2 · 𝑘))
49 2cnd 11707 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℂ)
50 simpl 483 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0)
5150nn0cnd 11949 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℂ)
52 1cnd 10628 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈ ℂ)
5349, 51, 52adddid 10657 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
54 simprr 769 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥))
55 2t1e2 11792 . . . . . . . . . . . . . . . . . . . . . . . 24 (2 · 1) = 2
5655a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) = 2)
5756oveq2d 7167 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + 2))
5853, 54, 573eqtr3d 2868 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) = ((2 · 𝑘) + 2))
5958oveq1d 7166 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (((2 · 𝑘) + 2) − 2))
6049, 51mulcld 10653 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈ ℂ)
6160, 49pncand 10990 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((2 · 𝑘) + 2) − 2) = (2 · 𝑘))
6259, 61eqtrd 2860 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (2 · 𝑘))
6348, 62breqtrrd 5090 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ ((♯‘𝑥) − 2))
6440zred 12079 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℝ)
6536nn0red 11948 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℝ)
66 2pos 11732 . . . . . . . . . . . . . . . . . . . 20 0 < 2
6741a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℝ)
6867, 65ltsubposd 11218 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 < 2 ↔ ((♯‘𝑥) − 2) < (♯‘𝑥)))
6966, 68mpbii 234 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) < (♯‘𝑥))
7064, 65, 69ltled 10780 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ≤ (♯‘𝑥))
71 elfz2 12892 . . . . . . . . . . . . . . . . . . 19 (((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)) ↔ ((0 ∈ ℤ ∧ (♯‘𝑥) ∈ ℤ ∧ ((♯‘𝑥) − 2) ∈ ℤ) ∧ (0 ≤ ((♯‘𝑥) − 2) ∧ ((♯‘𝑥) − 2) ≤ (♯‘𝑥))))
7271biimpri 229 . . . . . . . . . . . . . . . . . 18 (((0 ∈ ℤ ∧ (♯‘𝑥) ∈ ℤ ∧ ((♯‘𝑥) − 2) ∈ ℤ) ∧ (0 ≤ ((♯‘𝑥) − 2) ∧ ((♯‘𝑥) − 2) ≤ (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)))
7334, 37, 40, 63, 70, 72syl32anc 1372 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥)))
74 pfxlen 14038 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) = ((♯‘𝑥) − 2))
7533, 73, 74syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) = ((♯‘𝑥) − 2))
7675, 62eqtr2d 2861 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
7776adantlr 711 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
78 fveq2 6666 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (♯‘𝑦) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))))
7978eqeq2d 2836 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ((2 · 𝑘) = (♯‘𝑦) ↔ (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2)))))
80 vex 3502 . . . . . . . . . . . . . . . . . 18 𝑦 ∈ V
8180, 30sbcie 3815 . . . . . . . . . . . . . . . . 17 ([𝑦 / 𝑥]𝜑𝜒)
82 dfsbcq 3777 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([𝑦 / 𝑥]𝜑[(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
8381, 82syl5bbr 286 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝜒[(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
8479, 83imbi12d 346 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (((2 · 𝑘) = (♯‘𝑦) → 𝜒) ↔ ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)))
85 simplr 765 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒))
86 pfxcl 14032 . . . . . . . . . . . . . . . 16 (𝑥 ∈ Word 𝐵 → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵)
8786ad2antrl 724 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵)
8884, 85, 87rspcdva 3628 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))
8977, 88mpd 15 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)
90 2nn0 11906 . . . . . . . . . . . . . . . . . . 19 2 ∈ ℕ0
9190a1i 11 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℕ0)
9249addid2d 10833 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) = 2)
93 0red 10636 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℝ)
9462, 64eqeltrrd 2918 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈ ℝ)
9593, 94, 67, 48leadd1dd 11246 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) ≤ ((2 · 𝑘) + 2))
9692, 95eqbrtrrd 5086 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ ((2 · 𝑘) + 2))
9796, 58breqtrrd 5090 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (♯‘𝑥))
98 nn0sub 11939 . . . . . . . . . . . . . . . . . . 19 ((2 ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) → (2 ≤ (♯‘𝑥) ↔ ((♯‘𝑥) − 2) ∈ ℕ0))
9998biimpa 477 . . . . . . . . . . . . . . . . . 18 (((2 ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) ∧ 2 ≤ (♯‘𝑥)) → ((♯‘𝑥) − 2) ∈ ℕ0)
10091, 36, 97, 99syl21anc 835 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ ℕ0)
10165recnd 10661 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈ ℂ)
102101, 49, 52subsubd 11017 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) = (((♯‘𝑥) − 2) + 1))
103 2m1e1 11755 . . . . . . . . . . . . . . . . . . . . 21 (2 − 1) = 1
104103a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 − 1) = 1)
105104oveq2d 7167 . . . . . . . . . . . . . . . . . . 19 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) = ((♯‘𝑥) − 1))
106102, 105eqtr3d 2862 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 2) + 1) = ((♯‘𝑥) − 1))
10765lem1d 11565 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ≤ (♯‘𝑥))
108106, 107eqbrtrd 5084 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 2) + 1) ≤ (♯‘𝑥))
109 nn0p1elfzo 13073 . . . . . . . . . . . . . . . . 17 ((((♯‘𝑥) − 2) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧ (((♯‘𝑥) − 2) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥)))
110100, 36, 108, 109syl3anc 1365 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥)))
111 wrdsymbcl 13868 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
11233, 110, 111syl2anc 584 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
113112adantlr 711 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵)
114 nn0ge2m1nn0 11957 . . . . . . . . . . . . . . . . . 18 (((♯‘𝑥) ∈ ℕ0 ∧ 2 ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈ ℕ0)
11536, 97, 114syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈ ℕ0)
116101, 52npcand 10993 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 1) + 1) = (♯‘𝑥))
11765leidd 11198 . . . . . . . . . . . . . . . . . 18 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ≤ (♯‘𝑥))
118116, 117eqbrtrd 5084 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((♯‘𝑥) − 1) + 1) ≤ (♯‘𝑥))
119 nn0p1elfzo 13073 . . . . . . . . . . . . . . . . 17 ((((♯‘𝑥) − 1) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧ (((♯‘𝑥) − 1) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
120115, 36, 118, 119syl3anc 1365 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥)))
121 wrdsymbcl 13868 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
12233, 120, 121syl2anc 584 . . . . . . . . . . . . . . 15 ((𝑘 ∈ ℕ0 ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
123122adantlr 711 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵)
124 oveq1 7158 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝑦 ++ ⟨“𝑖𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩))
125124sbceq1d 3780 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑))
12682, 125imbi12d 346 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (([𝑦 / 𝑥]𝜑[(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑)))
127 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑖 = (𝑥‘((♯‘𝑥) − 2)))
128 eqidd 2826 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑗 = 𝑗)
129127, 128s2eqd 14218 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ⟨“𝑖𝑗”⟩ = ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩)
130129oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩))
131130sbceq1d 3780 . . . . . . . . . . . . . . . 16 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑))
132131imbi2d 342 . . . . . . . . . . . . . . 15 (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑)))
133 eqidd 2826 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (𝑥‘((♯‘𝑥) − 2)) = (𝑥‘((♯‘𝑥) − 2)))
134 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → 𝑗 = (𝑥‘((♯‘𝑥) − 1)))
135133, 134s2eqd 14218 . . . . . . . . . . . . . . . . . 18 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩ = ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩)
136135oveq2d 7167 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
137136sbceq1d 3780 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
138137imbi2d 342 . . . . . . . . . . . . . . 15 (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))𝑗”⟩) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑)))
139 wrdt2ind.6 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ Word 𝐵𝑖𝐵𝑗𝐵) → (𝜒𝜃))
140 ovex 7184 . . . . . . . . . . . . . . . . 17 (𝑦 ++ ⟨“𝑖𝑗”⟩) ∈ V
141 wrdt2ind.3 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑦 ++ ⟨“𝑖𝑗”⟩) → (𝜑𝜃))
142140, 141sbcie 3815 . . . . . . . . . . . . . . . 16 ([(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑𝜃)
143139, 81, 1423imtr4g 297 . . . . . . . . . . . . . . 15 ((𝑦 ∈ Word 𝐵𝑖𝐵𝑗𝐵) → ([𝑦 / 𝑥]𝜑[(𝑦 ++ ⟨“𝑖𝑗”⟩) / 𝑥]𝜑))
144126, 132, 138, 143vtocl3ga 3582 . . . . . . . . . . . . . 14 (((𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵 ∧ (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵 ∧ (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
14587, 113, 123, 144syl3anc 1365 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
14689, 145mpd 15 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑)
147 simprl 767 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵)
148 1red 10634 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈ ℝ)
149 simpll 763 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0)
150149nn0red 11948 . . . . . . . . . . . . . . . . . 18 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℝ)
151150, 148readdcld 10662 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑘 + 1) ∈ ℝ)
15241a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℝ)
15344a1i 11 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 2)
154 0p1e1 11751 . . . . . . . . . . . . . . . . . 18 (0 + 1) = 1
155 0red 10636 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℝ)
156149nn0ge0d 11950 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 𝑘)
157148leidd 11198 . . . . . . . . . . . . . . . . . . 19 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ 1)
158155, 148, 150, 148, 156, 157le2addd 11251 . . . . . . . . . . . . . . . . . 18 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 1) ≤ (𝑘 + 1))
159154, 158eqbrtrrid 5098 . . . . . . . . . . . . . . . . 17 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ (𝑘 + 1))
160148, 151, 152, 153, 159lemul2ad 11572 . . . . . . . . . . . . . . . 16 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) ≤ (2 · (𝑘 + 1)))
16155, 160eqbrtrrid 5098 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (2 · (𝑘 + 1)))
162 simprr 769 . . . . . . . . . . . . . . 15 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥))
163161, 162breqtrd 5088 . . . . . . . . . . . . . 14 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (♯‘𝑥))
164 eqid 2825 . . . . . . . . . . . . . . . . 17 (♯‘𝑥) = (♯‘𝑥)
165164pfxlsw2ccat 30540 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
166165eqcomd 2831 . . . . . . . . . . . . . . 15 ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) = 𝑥)
167166eqcomd 2831 . . . . . . . . . . . . . 14 ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
168147, 163, 167syl2anc 584 . . . . . . . . . . . . 13 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩))
169 sbceq1a 3786 . . . . . . . . . . . . 13 (𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) → (𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
170168, 169syl 17 . . . . . . . . . . . 12 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝜑[((𝑥 prefix ((♯‘𝑥) − 2)) ++ ⟨“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”⟩) / 𝑥]𝜑))
171146, 170mpbird 258 . . . . . . . . . . 11 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝜑)
172171expr 457 . . . . . . . . . 10 (((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ 𝑥 ∈ Word 𝐵) → ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))
173172ralrimiva 3186 . . . . . . . . 9 ((𝑘 ∈ ℕ0 ∧ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))
174173ex 413 . . . . . . . 8 (𝑘 ∈ ℕ0 → (∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
17532, 174syl5bi 243 . . . . . . 7 (𝑘 ∈ ℕ0 → (∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)))
1764, 8, 12, 16, 27, 175nn0ind 12069 . . . . . 6 (𝑚 ∈ ℕ0 → ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑))
177176adantl 482 . . . . 5 ((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) → ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑))
178 simpl 483 . . . . . 6 ((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) → 𝐴 ∈ Word 𝐵)
179 fveq2 6666 . . . . . . . . 9 (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴))
180179eqeq2d 2836 . . . . . . . 8 (𝑥 = 𝐴 → ((2 · 𝑚) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝐴)))
181 wrdt2ind.4 . . . . . . . 8 (𝑥 = 𝐴 → (𝜑𝜏))
182180, 181imbi12d 346 . . . . . . 7 (𝑥 = 𝐴 → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
183182adantl 482 . . . . . 6 (((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) ∧ 𝑥 = 𝐴) → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
184178, 183rspcdv 3618 . . . . 5 ((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) → (∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑) → ((2 · 𝑚) = (♯‘𝐴) → 𝜏)))
185177, 184mpd 15 . . . 4 ((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) → ((2 · 𝑚) = (♯‘𝐴) → 𝜏))
186185imp 407 . . 3 (((𝐴 ∈ Word 𝐵𝑚 ∈ ℕ0) ∧ (2 · 𝑚) = (♯‘𝐴)) → 𝜏)
187186adantllr 715 . 2 ((((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) ∧ 𝑚 ∈ ℕ0) ∧ (2 · 𝑚) = (♯‘𝐴)) → 𝜏)
188 lencl 13876 . . 3 (𝐴 ∈ Word 𝐵 → (♯‘𝐴) ∈ ℕ0)
189 evennn02n 15691 . . . 4 ((♯‘𝐴) ∈ ℕ0 → (2 ∥ (♯‘𝐴) ↔ ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴)))
190189biimpa 477 . . 3 (((♯‘𝐴) ∈ ℕ0 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴))
191188, 190sylan 580 . 2 ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴))
192187, 191r19.29a 3293 1 ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ∀wral 3142  ∃wrex 3143  [wsbc 3775  ∅c0 4294   class class class wbr 5062  ‘cfv 6351  (class class class)co 7151  ℝcr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667   ≤ cle 10668   − cmin 10862  2c2 11684  ℕ0cn0 11889  ℤcz 11973  ...cfz 12885  ..^cfzo 13026  ♯chash 13683  Word cword 13854   ++ cconcat 13915   prefix cpfx 14025  ⟨“cs2 14196   ∥ cdvds 15599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-n0 11890  df-xnn0 11960  df-z 11974  df-uz 12236  df-rp 12383  df-fz 12886  df-fzo 13027  df-hash 13684  df-word 13855  df-lsw 13908  df-concat 13916  df-s1 13943  df-substr 13996  df-pfx 14026  df-s2 14203  df-dvds 15600 This theorem is referenced by:  cyc3genpm  30708
 Copyright terms: Public domain W3C validator