Metamath Proof Explorer

Theorem wlkdlem2

Description: Lemma 2 for wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses wlkd.p ⊢ φ → P ∈ Word V
wlkd.f ⊢ φ → F ∈ Word V
wlkd.l ⊢ φ → P = F + 1
wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
Assertion wlkdlem2 ⊢ φ → F ∈ ℕ → P ⁡ F ∈ I ⁡ F ⁡ F − 1 ∧ ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢ φ → P ∈ Word V
2 wlkd.f ⊢ φ → F ∈ Word V
3 wlkd.l ⊢ φ → P = F + 1
4 wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 fzo0end ⊢ F ∈ ℕ → F − 1 ∈ 0 ..^ F
6 fveq2 ⊢ k = F − 1 → P ⁡ k = P ⁡ F − 1
7 fvoveq1 ⊢ k = F − 1 → P ⁡ k + 1 = P ⁡ F - 1 + 1
8 6 7 preq12d ⊢ k = F − 1 → P ⁡ k P ⁡ k + 1 = P ⁡ F − 1 P ⁡ F - 1 + 1
9 2fveq3 ⊢ k = F − 1 → I ⁡ F ⁡ k = I ⁡ F ⁡ F − 1
10 8 9 sseq12d ⊢ k = F − 1 → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ↔ P ⁡ F − 1 P ⁡ F - 1 + 1 ⊆ I ⁡ F ⁡ F − 1
11 10 rspcv ⊢ F − 1 ∈ 0 ..^ F → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ F − 1 P ⁡ F - 1 + 1 ⊆ I ⁡ F ⁡ F − 1
12 5 11 syl ⊢ F ∈ ℕ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ F − 1 P ⁡ F - 1 + 1 ⊆ I ⁡ F ⁡ F − 1
13 fvex ⊢ P ⁡ F − 1 ∈ V
14 fvex ⊢ P ⁡ F - 1 + 1 ∈ V
15 13 14 prss ⊢ P ⁡ F − 1 ∈ I ⁡ F ⁡ F − 1 ∧ P ⁡ F - 1 + 1 ∈ I ⁡ F ⁡ F − 1 ↔ P ⁡ F − 1 P ⁡ F - 1 + 1 ⊆ I ⁡ F ⁡ F − 1
16 nncn ⊢ F ∈ ℕ → F ∈ ℂ
17 npcan1 ⊢ F ∈ ℂ → F - 1 + 1 = F
18 16 17 syl ⊢ F ∈ ℕ → F - 1 + 1 = F
19 18 fveq2d ⊢ F ∈ ℕ → P ⁡ F - 1 + 1 = P ⁡ F
20 19 eleq1d ⊢ F ∈ ℕ → P ⁡ F - 1 + 1 ∈ I ⁡ F ⁡ F − 1 ↔ P ⁡ F ∈ I ⁡ F ⁡ F − 1
21 20 biimpd ⊢ F ∈ ℕ → P ⁡ F - 1 + 1 ∈ I ⁡ F ⁡ F − 1 → P ⁡ F ∈ I ⁡ F ⁡ F − 1
22 21 adantld ⊢ F ∈ ℕ → P ⁡ F − 1 ∈ I ⁡ F ⁡ F − 1 ∧ P ⁡ F - 1 + 1 ∈ I ⁡ F ⁡ F − 1 → P ⁡ F ∈ I ⁡ F ⁡ F − 1
23 15 22 biimtrrid ⊢ F ∈ ℕ → P ⁡ F − 1 P ⁡ F - 1 + 1 ⊆ I ⁡ F ⁡ F − 1 → P ⁡ F ∈ I ⁡ F ⁡ F − 1
24 12 23 syld ⊢ F ∈ ℕ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ F ∈ I ⁡ F ⁡ F − 1
25 4 24 syl5com ⊢ φ → F ∈ ℕ → P ⁡ F ∈ I ⁡ F ⁡ F − 1
26 fvex ⊢ P ⁡ k ∈ V
27 fvex ⊢ P ⁡ k + 1 ∈ V
28 26 27 prss ⊢ P ⁡ k ∈ I ⁡ F ⁡ k ∧ P ⁡ k + 1 ∈ I ⁡ F ⁡ k ↔ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
29 simpl ⊢ P ⁡ k ∈ I ⁡ F ⁡ k ∧ P ⁡ k + 1 ∈ I ⁡ F ⁡ k → P ⁡ k ∈ I ⁡ F ⁡ k
30 28 29 sylbir ⊢ P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ∈ I ⁡ F ⁡ k
31 30 a1i ⊢ φ ∧ k ∈ 0 ..^ F → P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → P ⁡ k ∈ I ⁡ F ⁡ k
32 31 ralimdva ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k
33 4 32 mpd ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k
34 25 33 jca ⊢ φ → F ∈ ℕ → P ⁡ F ∈ I ⁡ F ⁡ F − 1 ∧ ∀ k ∈ 0 ..^ F P ⁡ k ∈ I ⁡ F ⁡ k