Metamath Proof Explorer

Theorem clwlkclwwlklem2a1

Description: Lemma 1 for clwlkclwwlklem2a . (Contributed by Alexander van der Vekens, 21-Jun-2018) (Revised by AV, 11-Apr-2021)

Ref Expression
Assertion clwlkclwwlklem2a1 ⊢P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E

Proof

Step Hyp Ref Expression
1 lencl ⊢P∈WordV→P∈ℕ0
2 nn0cn ⊢P∈ℕ0→P∈ℂ
3 peano2cnm ⊢P∈ℂ→P−1∈ℂ
4 3 subid1d ⊢P∈ℂ→P-1-0=P−1
5 4 oveq1d ⊢P∈ℂ→P−1-0-1=P-1-1
6 sub1m1 ⊢P∈ℂ→P-1-1=P−2
7 5 6 eqtrd ⊢P∈ℂ→P−1-0-1=P−2
8 1 2 7 3syl ⊢P∈WordV→P−1-0-1=P−2
9 8 adantr ⊢P∈WordV∧2≤P→P−1-0-1=P−2
10 9 oveq2d ⊢P∈WordV∧2≤P→0..^P−1-0-1=0..^P−2
11 10 raleqdv ⊢P∈WordV∧2≤P→∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E↔∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E
12 11 biimpcd ⊢∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E→P∈WordV∧2≤P→∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E
13 12 adantr ⊢∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P∈WordV∧2≤P→∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E
14 13 adantl ⊢lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P∈WordV∧2≤P→∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E
15 14 impcom ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E
16 lsw ⊢P∈WordV→lastS⁡P=P⁡P−1
17 2m1e1 ⊢2−1=1
18 17 a1i ⊢P∈WordV→2−1=1
19 18 eqcomd ⊢P∈WordV→1=2−1
20 19 oveq2d ⊢P∈WordV→P−1=P−2−1
21 1 2 syl ⊢P∈WordV→P∈ℂ
22 2cnd ⊢P∈WordV→2∈ℂ
23 1cnd ⊢P∈WordV→1∈ℂ
24 21 22 23 subsubd ⊢P∈WordV→P−2−1=P-2+1
25 20 24 eqtrd ⊢P∈WordV→P−1=P-2+1
26 25 fveq2d ⊢P∈WordV→P⁡P−1=P⁡P-2+1
27 16 26 eqtrd ⊢P∈WordV→lastS⁡P=P⁡P-2+1
28 27 adantr ⊢P∈WordV∧2≤P→lastS⁡P=P⁡P-2+1
29 28 adantr ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→lastS⁡P=P⁡P-2+1
30 eqeq1 ⊢lastS⁡P=P⁡0→lastS⁡P=P⁡P-2+1↔P⁡0=P⁡P-2+1
31 30 adantl ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→lastS⁡P=P⁡P-2+1↔P⁡0=P⁡P-2+1
32 29 31 mpbid ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→P⁡0=P⁡P-2+1
33 32 preq2d ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→P⁡P−2P⁡0=P⁡P−2P⁡P-2+1
34 33 eleq1d ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→P⁡P−2P⁡0∈ran⁡E↔P⁡P−2P⁡P-2+1∈ran⁡E
35 34 biimpd ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0→P⁡P−2P⁡0∈ran⁡E→P⁡P−2P⁡P-2+1∈ran⁡E
36 35 ex ⊢P∈WordV∧2≤P→lastS⁡P=P⁡0→P⁡P−2P⁡0∈ran⁡E→P⁡P−2P⁡P-2+1∈ran⁡E
37 36 com13 ⊢P⁡P−2P⁡0∈ran⁡E→lastS⁡P=P⁡0→P∈WordV∧2≤P→P⁡P−2P⁡P-2+1∈ran⁡E
38 37 adantl ⊢∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→lastS⁡P=P⁡0→P∈WordV∧2≤P→P⁡P−2P⁡P-2+1∈ran⁡E
39 38 impcom ⊢lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P∈WordV∧2≤P→P⁡P−2P⁡P-2+1∈ran⁡E
40 39 impcom ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P⁡P−2P⁡P-2+1∈ran⁡E
41 ovexd ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→P−2∈V
42 fveq2 ⊢i=P−2→P⁡i=P⁡P−2
43 fvoveq1 ⊢i=P−2→P⁡i+1=P⁡P-2+1
44 42 43 preq12d ⊢i=P−2→P⁡iP⁡i+1=P⁡P−2P⁡P-2+1
45 44 eleq1d ⊢i=P−2→P⁡iP⁡i+1∈ran⁡E↔P⁡P−2P⁡P-2+1∈ran⁡E
46 45 ralunsn ⊢P−2∈V→∀i∈0..^P−2∪P−2P⁡iP⁡i+1∈ran⁡E↔∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡P-2+1∈ran⁡E
47 41 46 syl ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−2∪P−2P⁡iP⁡i+1∈ran⁡E↔∀i∈0..^P−2P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡P-2+1∈ran⁡E
48 15 40 47 mpbir2and ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−2∪P−2P⁡iP⁡i+1∈ran⁡E
49 1e2m1 ⊢1=2−1
50 49 a1i ⊢P∈WordV→1=2−1
51 50 oveq2d ⊢P∈WordV→P−1=P−2−1
52 51 24 eqtrd ⊢P∈WordV→P−1=P-2+1
53 52 oveq2d ⊢P∈WordV→0..^P−1=0..^P-2+1
54 53 adantr ⊢P∈WordV∧2≤P→0..^P−1=0..^P-2+1
55 nn0re ⊢P∈ℕ0→P∈ℝ
56 2re ⊢2∈ℝ
57 56 a1i ⊢P∈ℕ0→2∈ℝ
58 55 57 subge0d ⊢P∈ℕ0→0≤P−2↔2≤P
59 58 biimprd ⊢P∈ℕ0→2≤P→0≤P−2
60 nn0z ⊢P∈ℕ0→P∈ℤ
61 2z ⊢2∈ℤ
62 61 a1i ⊢P∈ℕ0→2∈ℤ
63 60 62 zsubcld ⊢P∈ℕ0→P−2∈ℤ
64 59 63 jctild ⊢P∈ℕ0→2≤P→P−2∈ℤ∧0≤P−2
65 1 64 syl ⊢P∈WordV→2≤P→P−2∈ℤ∧0≤P−2
66 65 imp ⊢P∈WordV∧2≤P→P−2∈ℤ∧0≤P−2
67 elnn0z ⊢P−2∈ℕ0↔P−2∈ℤ∧0≤P−2
68 66 67 sylibr ⊢P∈WordV∧2≤P→P−2∈ℕ0
69 elnn0uz ⊢P−2∈ℕ0↔P−2∈ℤ≥0
70 68 69 sylib ⊢P∈WordV∧2≤P→P−2∈ℤ≥0
71 fzosplitsn ⊢P−2∈ℤ≥0→0..^P-2+1=0..^P−2∪P−2
72 70 71 syl ⊢P∈WordV∧2≤P→0..^P-2+1=0..^P−2∪P−2
73 54 72 eqtrd ⊢P∈WordV∧2≤P→0..^P−1=0..^P−2∪P−2
74 73 adantr ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→0..^P−1=0..^P−2∪P−2
75 74 raleqdv ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E↔∀i∈0..^P−2∪P−2P⁡iP⁡i+1∈ran⁡E
76 48 75 mpbird ⊢P∈WordV∧2≤P∧lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E
77 76 ex ⊢P∈WordV∧2≤P→lastS⁡P=P⁡0∧∀i∈0..^P−1-0-1P⁡iP⁡i+1∈ran⁡E∧P⁡P−2P⁡0∈ran⁡E→∀i∈0..^P−1P⁡iP⁡i+1∈ran⁡E