Step | Hyp | Ref
| Expression |
1 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑛 = 0 → (2 · 𝑛) = (2 ·
0)) |
2 | 1 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑛 = 0 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 0) =
(♯‘𝑥))) |
3 | 2 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑛 = 0 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 0) =
(♯‘𝑥) →
𝜑))) |
4 | 3 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑛 = 0 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 0) = (♯‘𝑥) → 𝜑))) |
5 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (2 · 𝑛) = (2 · 𝑘)) |
6 | 5 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑥))) |
7 | 6 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑥) → 𝜑))) |
8 | 7 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑛 = 𝑘 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑))) |
9 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑘 + 1) → (2 · 𝑛) = (2 · (𝑘 + 1))) |
10 | 9 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑛 = (𝑘 + 1) → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · (𝑘 + 1)) = (♯‘𝑥))) |
11 | 10 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑛 = (𝑘 + 1) → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))) |
12 | 11 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑛 = (𝑘 + 1) → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))) |
13 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (2 · 𝑛) = (2 · 𝑚)) |
14 | 13 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → ((2 · 𝑛) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝑥))) |
15 | 14 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝑥) → 𝜑))) |
16 | 15 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∀𝑥 ∈ Word 𝐵((2 · 𝑛) = (♯‘𝑥) → 𝜑) ↔ ∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑))) |
17 | | 2t0e0 11885 |
. . . . . . . . . . . 12
⊢ (2
· 0) = 0 |
18 | 17 | eqeq1i 2743 |
. . . . . . . . . . 11
⊢ ((2
· 0) = (♯‘𝑥) ↔ 0 = (♯‘𝑥)) |
19 | | eqcom 2745 |
. . . . . . . . . . 11
⊢ (0 =
(♯‘𝑥) ↔
(♯‘𝑥) =
0) |
20 | 18, 19 | bitri 278 |
. . . . . . . . . 10
⊢ ((2
· 0) = (♯‘𝑥) ↔ (♯‘𝑥) = 0) |
21 | | hasheq0 13816 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Word 𝐵 → ((♯‘𝑥) = 0 ↔ 𝑥 = ∅)) |
22 | 20, 21 | syl5bb 286 |
. . . . . . . . 9
⊢ (𝑥 ∈ Word 𝐵 → ((2 · 0) =
(♯‘𝑥) ↔
𝑥 =
∅)) |
23 | | wrdt2ind.5 |
. . . . . . . . . 10
⊢ 𝜓 |
24 | | wrdt2ind.1 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝜑 ↔ 𝜓)) |
25 | 23, 24 | mpbiri 261 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → 𝜑) |
26 | 22, 25 | syl6bi 256 |
. . . . . . . 8
⊢ (𝑥 ∈ Word 𝐵 → ((2 · 0) =
(♯‘𝑥) →
𝜑)) |
27 | 26 | rgen 3063 |
. . . . . . 7
⊢
∀𝑥 ∈
Word 𝐵((2 · 0) =
(♯‘𝑥) →
𝜑) |
28 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
29 | 28 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((2 · 𝑘) = (♯‘𝑥) ↔ (2 · 𝑘) = (♯‘𝑦))) |
30 | | wrdt2ind.2 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) |
31 | 29, 30 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑘) = (♯‘𝑦) → 𝜒))) |
32 | 31 | cbvralvw 3349 |
. . . . . . . 8
⊢
(∀𝑥 ∈
Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) ↔ ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) |
33 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵) |
34 | | 0zd 12074 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈
ℤ) |
35 | | lencl 13974 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ Word 𝐵 → (♯‘𝑥) ∈
ℕ0) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈
ℕ0) |
37 | 36 | nn0zd 12166 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈
ℤ) |
38 | | 2z 12095 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
ℤ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈
ℤ) |
40 | 37, 39 | zsubcld 12173 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈
ℤ) |
41 | | 2re 11790 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℝ |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 2 ∈ ℝ) |
43 | | nn0re 11985 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℝ) |
44 | | 0le2 11818 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 0 ≤
2 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 2) |
46 | | nn0ge0 12001 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ 𝑘) |
47 | 42, 43, 45, 46 | mulge0d 11295 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ 0 ≤ (2 · 𝑘)) |
48 | 47 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ (2 ·
𝑘)) |
49 | | 2cnd 11794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈
ℂ) |
50 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0) |
51 | 50 | nn0cnd 12038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℂ) |
52 | | 1cnd 10714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈
ℂ) |
53 | 49, 51, 52 | adddid 10743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 ·
1))) |
54 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥)) |
55 | | 2t1e2 11879 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (2
· 1) = 2 |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) =
2) |
57 | 56 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) + (2 · 1)) = ((2
· 𝑘) +
2)) |
58 | 53, 54, 57 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) = ((2 · 𝑘) + 2)) |
59 | 58 | oveq1d 7185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (((2 ·
𝑘) + 2) −
2)) |
60 | 49, 51 | mulcld 10739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈
ℂ) |
61 | 60, 49 | pncand 11076 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (((2 · 𝑘) + 2) − 2) = (2 ·
𝑘)) |
62 | 59, 61 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) = (2 · 𝑘)) |
63 | 48, 62 | breqtrrd 5058 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤
((♯‘𝑥) −
2)) |
64 | 40 | zred 12168 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈
ℝ) |
65 | 36 | nn0red 12037 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈
ℝ) |
66 | | 2pos 11819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
67 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈
ℝ) |
68 | 67, 65 | ltsubposd 11304 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 < 2 ↔
((♯‘𝑥) −
2) < (♯‘𝑥))) |
69 | 66, 68 | mpbii 236 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) <
(♯‘𝑥)) |
70 | 64, 65, 69 | ltled 10866 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ≤
(♯‘𝑥)) |
71 | 34, 37, 40, 63, 70 | elfzd 12989 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈
(0...(♯‘𝑥))) |
72 | | pfxlen 14134 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0...(♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) =
((♯‘𝑥) −
2)) |
73 | 33, 71, 72 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) =
((♯‘𝑥) −
2)) |
74 | 73, 62 | eqtr2d 2774 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2)))) |
75 | 74 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2)))) |
76 | | fveq2 6674 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (♯‘𝑦) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2)))) |
77 | 76 | eqeq2d 2749 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ((2 · 𝑘) = (♯‘𝑦) ↔ (2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) −
2))))) |
78 | | vex 3402 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
79 | 78, 30 | sbcie 3722 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑦 / 𝑥]𝜑 ↔ 𝜒) |
80 | | dfsbcq 3682 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([𝑦 / 𝑥]𝜑 ↔ [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)) |
81 | 79, 80 | bitr3id 288 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝜒 ↔ [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)) |
82 | 77, 81 | imbi12d 348 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (((2 · 𝑘) = (♯‘𝑦) → 𝜒) ↔ ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑))) |
83 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ∀𝑦 ∈ Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) |
84 | | pfxcl 14128 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ Word 𝐵 → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵) |
85 | 84 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵) |
86 | 82, 83, 85 | rspcdva 3528 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((2 · 𝑘) = (♯‘(𝑥 prefix ((♯‘𝑥) − 2))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑)) |
87 | 75, 86 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑) |
88 | | 2nn0 11993 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℕ0 |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈
ℕ0) |
90 | 49 | addid2d 10919 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) =
2) |
91 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈
ℝ) |
92 | 62, 64 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 𝑘) ∈
ℝ) |
93 | 91, 92, 67, 48 | leadd1dd 11332 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 2) ≤ ((2
· 𝑘) +
2)) |
94 | 90, 93 | eqbrtrrd 5054 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ ((2 ·
𝑘) + 2)) |
95 | 94, 58 | breqtrrd 5058 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤
(♯‘𝑥)) |
96 | | nn0sub 12026 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) → (2 ≤
(♯‘𝑥) ↔
((♯‘𝑥) −
2) ∈ ℕ0)) |
97 | 96 | biimpa 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0) ∧ 2 ≤
(♯‘𝑥)) →
((♯‘𝑥) −
2) ∈ ℕ0) |
98 | 89, 36, 95, 97 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈
ℕ0) |
99 | 65 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ∈
ℂ) |
100 | 99, 49, 52 | subsubd 11103 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) =
(((♯‘𝑥) −
2) + 1)) |
101 | | 2m1e1 11842 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
− 1) = 1 |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 − 1) =
1) |
103 | 102 | oveq2d 7186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − (2 − 1)) =
((♯‘𝑥) −
1)) |
104 | 100, 103 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) →
(((♯‘𝑥) −
2) + 1) = ((♯‘𝑥) − 1)) |
105 | 65 | lem1d 11651 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ≤
(♯‘𝑥)) |
106 | 104, 105 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) →
(((♯‘𝑥) −
2) + 1) ≤ (♯‘𝑥)) |
107 | | nn0p1elfzo 13171 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑥)
− 2) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧
(((♯‘𝑥) −
2) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥))) |
108 | 98, 36, 106, 107 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 2) ∈
(0..^(♯‘𝑥))) |
109 | | wrdsymbcl 13968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 2) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵) |
110 | 33, 108, 109 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵) |
111 | 110 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵) |
112 | | nn0ge2m1nn0 12046 |
. . . . . . . . . . . . . . . . . 18
⊢
(((♯‘𝑥)
∈ ℕ0 ∧ 2 ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈
ℕ0) |
113 | 36, 95, 112 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈
ℕ0) |
114 | 99, 52 | npcand 11079 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) →
(((♯‘𝑥) −
1) + 1) = (♯‘𝑥)) |
115 | 65 | leidd 11284 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (♯‘𝑥) ≤ (♯‘𝑥)) |
116 | 114, 115 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) →
(((♯‘𝑥) −
1) + 1) ≤ (♯‘𝑥)) |
117 | | nn0p1elfzo 13171 |
. . . . . . . . . . . . . . . . 17
⊢
((((♯‘𝑥)
− 1) ∈ ℕ0 ∧ (♯‘𝑥) ∈ ℕ0 ∧
(((♯‘𝑥) −
1) + 1) ≤ (♯‘𝑥)) → ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥))) |
118 | 113, 36, 116, 117 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ((♯‘𝑥) − 1) ∈
(0..^(♯‘𝑥))) |
119 | | wrdsymbcl 13968 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝐵 ∧ ((♯‘𝑥) − 1) ∈ (0..^(♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) |
120 | 33, 118, 119 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) |
121 | 120 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) |
122 | | oveq1 7177 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (𝑦 ++ 〈“𝑖𝑗”〉) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“𝑖𝑗”〉)) |
123 | 122 | sbceq1d 3685 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → ([(𝑦 ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑)) |
124 | 80, 123 | imbi12d 348 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 prefix ((♯‘𝑥) − 2)) → (([𝑦 / 𝑥]𝜑 → [(𝑦 ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑))) |
125 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑖 = (𝑥‘((♯‘𝑥) − 2))) |
126 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 𝑗 = 𝑗) |
127 | 125, 126 | s2eqd 14314 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → 〈“𝑖𝑗”〉 = 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) |
128 | 127 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“𝑖𝑗”〉) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉)) |
129 | 128 | sbceq1d 3685 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++
〈“𝑖𝑗”〉) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) / 𝑥]𝜑)) |
130 | 129 | imbi2d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑥‘((♯‘𝑥) − 2)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) / 𝑥]𝜑))) |
131 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (𝑥‘((♯‘𝑥) − 2)) = (𝑥‘((♯‘𝑥) − 2))) |
132 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → 𝑗 = (𝑥‘((♯‘𝑥) − 1))) |
133 | 131, 132 | s2eqd 14314 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉 = 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) |
134 | 133 | oveq2d 7186 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉)) |
135 | 134 | sbceq1d 3685 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → ([((𝑥 prefix ((♯‘𝑥) − 2)) ++
〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) / 𝑥]𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑)) |
136 | 135 | imbi2d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = (𝑥‘((♯‘𝑥) − 1)) → (([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))𝑗”〉) / 𝑥]𝜑) ↔ ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑))) |
137 | | wrdt2ind.6 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝜒 → 𝜃)) |
138 | | ovex 7203 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ++ 〈“𝑖𝑗”〉) ∈ V |
139 | | wrdt2ind.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑦 ++ 〈“𝑖𝑗”〉) → (𝜑 ↔ 𝜃)) |
140 | 138, 139 | sbcie 3722 |
. . . . . . . . . . . . . . . 16
⊢
([(𝑦 ++
〈“𝑖𝑗”〉) / 𝑥]𝜑 ↔ 𝜃) |
141 | 137, 79, 140 | 3imtr4g 299 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ Word 𝐵 ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → ([𝑦 / 𝑥]𝜑 → [(𝑦 ++ 〈“𝑖𝑗”〉) / 𝑥]𝜑)) |
142 | 124, 130,
136, 141 | vtocl3ga 3482 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 prefix ((♯‘𝑥) − 2)) ∈ Word 𝐵 ∧ (𝑥‘((♯‘𝑥) − 2)) ∈ 𝐵 ∧ (𝑥‘((♯‘𝑥) − 1)) ∈ 𝐵) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑)) |
143 | 85, 111, 121, 142 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → ([(𝑥 prefix ((♯‘𝑥) − 2)) / 𝑥]𝜑 → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑)) |
144 | 87, 143 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑) |
145 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 ∈ Word 𝐵) |
146 | | 1red 10720 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ∈ ℝ) |
147 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℕ0) |
148 | 147 | nn0red 12037 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑘 ∈ ℝ) |
149 | 148, 146 | readdcld 10748 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝑘 + 1) ∈ ℝ) |
150 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ∈ ℝ) |
151 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 2) |
152 | | 0p1e1 11838 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 + 1) =
1 |
153 | | 0red 10722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ∈ ℝ) |
154 | 147 | nn0ge0d 12039 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 0 ≤ 𝑘) |
155 | 146 | leidd 11284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ 1) |
156 | 153, 146,
148, 146, 154, 155 | le2addd 11337 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (0 + 1) ≤ (𝑘 + 1)) |
157 | 152, 156 | eqbrtrrid 5066 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 1 ≤ (𝑘 + 1)) |
158 | 146, 149,
150, 151, 157 | lemul2ad 11658 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · 1) ≤ (2 ·
(𝑘 + 1))) |
159 | 55, 158 | eqbrtrrid 5066 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (2 · (𝑘 + 1))) |
160 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (2 · (𝑘 + 1)) = (♯‘𝑥)) |
161 | 159, 160 | breqtrd 5056 |
. . . . . . . . . . . . . 14
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 2 ≤ (♯‘𝑥)) |
162 | | eqid 2738 |
. . . . . . . . . . . . . . . . 17
⊢
(♯‘𝑥) =
(♯‘𝑥) |
163 | 162 | pfxlsw2ccat 30799 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉)) |
164 | 163 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) = 𝑥) |
165 | 164 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ Word 𝐵 ∧ 2 ≤ (♯‘𝑥)) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉)) |
166 | 145, 161,
165 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉)) |
167 | | sbceq1a 3691 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++
〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑)) |
168 | 166, 167 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → (𝜑 ↔ [((𝑥 prefix ((♯‘𝑥) − 2)) ++ 〈“(𝑥‘((♯‘𝑥) − 2))(𝑥‘((♯‘𝑥) − 1))”〉) / 𝑥]𝜑)) |
169 | 144, 168 | mpbird 260 |
. . . . . . . . . . 11
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ (𝑥 ∈ Word 𝐵 ∧ (2 · (𝑘 + 1)) = (♯‘𝑥))) → 𝜑) |
170 | 169 | expr 460 |
. . . . . . . . . 10
⊢ (((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) ∧ 𝑥 ∈ Word 𝐵) → ((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)) |
171 | 170 | ralrimiva 3096 |
. . . . . . . . 9
⊢ ((𝑘 ∈ ℕ0
∧ ∀𝑦 ∈ Word
𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒)) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑)) |
172 | 171 | ex 416 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (∀𝑦 ∈
Word 𝐵((2 · 𝑘) = (♯‘𝑦) → 𝜒) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))) |
173 | 32, 172 | syl5bi 245 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (∀𝑥 ∈
Word 𝐵((2 · 𝑘) = (♯‘𝑥) → 𝜑) → ∀𝑥 ∈ Word 𝐵((2 · (𝑘 + 1)) = (♯‘𝑥) → 𝜑))) |
174 | 4, 8, 12, 16, 27, 173 | nn0ind 12158 |
. . . . . 6
⊢ (𝑚 ∈ ℕ0
→ ∀𝑥 ∈
Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑)) |
175 | 174 | adantl 485 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) →
∀𝑥 ∈ Word 𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑)) |
176 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → 𝐴 ∈ Word 𝐵) |
177 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (♯‘𝑥) = (♯‘𝐴)) |
178 | 177 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((2 · 𝑚) = (♯‘𝑥) ↔ (2 · 𝑚) = (♯‘𝐴))) |
179 | | wrdt2ind.4 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏)) |
180 | 178, 179 | imbi12d 348 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏))) |
181 | 180 | adantl 485 |
. . . . . 6
⊢ (((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) ∧ 𝑥 = 𝐴) → (((2 · 𝑚) = (♯‘𝑥) → 𝜑) ↔ ((2 · 𝑚) = (♯‘𝐴) → 𝜏))) |
182 | 176, 181 | rspcdv 3518 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) →
(∀𝑥 ∈ Word
𝐵((2 · 𝑚) = (♯‘𝑥) → 𝜑) → ((2 · 𝑚) = (♯‘𝐴) → 𝜏))) |
183 | 175, 182 | mpd 15 |
. . . 4
⊢ ((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) → ((2
· 𝑚) =
(♯‘𝐴) →
𝜏)) |
184 | 183 | imp 410 |
. . 3
⊢ (((𝐴 ∈ Word 𝐵 ∧ 𝑚 ∈ ℕ0) ∧ (2
· 𝑚) =
(♯‘𝐴)) →
𝜏) |
185 | 184 | adantllr 719 |
. 2
⊢ ((((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) ∧ 𝑚 ∈ ℕ0) ∧ (2
· 𝑚) =
(♯‘𝐴)) →
𝜏) |
186 | | lencl 13974 |
. . 3
⊢ (𝐴 ∈ Word 𝐵 → (♯‘𝐴) ∈
ℕ0) |
187 | | evennn02n 15795 |
. . . 4
⊢
((♯‘𝐴)
∈ ℕ0 → (2 ∥ (♯‘𝐴) ↔ ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴))) |
188 | 187 | biimpa 480 |
. . 3
⊢
(((♯‘𝐴)
∈ ℕ0 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2 · 𝑚) = (♯‘𝐴)) |
189 | 186, 188 | sylan 583 |
. 2
⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → ∃𝑚 ∈ ℕ0 (2
· 𝑚) =
(♯‘𝐴)) |
190 | 185, 189 | r19.29a 3199 |
1
⊢ ((𝐴 ∈ Word 𝐵 ∧ 2 ∥ (♯‘𝐴)) → 𝜏) |