Metamath Proof Explorer

Theorem clwwlkccatlem

Description: Lemma for clwwlkccat : index j is shifted up by ( #A ) , and the case i = ( ( #A ) - 1 ) is covered by the "bridge" { ( lastSA ) , ( B0 ) } = { ( lastSA ) , ( A0 ) } e. ( EdgG ) . (Contributed by AV, 23-Apr-2022)

Ref Expression
Assertion clwwlkccatlem ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A++B−1A++B⁡iA++B⁡i+1∈Edg⁡G

Proof

Step Hyp Ref Expression
1 simplll ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A∈WordVtx⁡G
2 simplr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→B∈WordVtx⁡G
3 lencl ⊢A∈WordVtx⁡G→A∈ℕ0
4 3 nn0zd ⊢A∈WordVtx⁡G→A∈ℤ
5 fzossrbm1 ⊢A∈ℤ→0..^A−1⊆0..^A
6 4 5 syl ⊢A∈WordVtx⁡G→0..^A−1⊆0..^A
7 6 ad2antrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G→0..^A−1⊆0..^A
8 7 sselda ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→i∈0..^A
9 ccatval1 ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧i∈0..^A→A++B⁡i=A⁡i
10 1 2 8 9 syl3anc ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A++B⁡i=A⁡i
11 4 ad2antrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G→A∈ℤ
12 elfzom1elp1fzo ⊢A∈ℤ∧i∈0..^A−1→i+1∈0..^A
13 11 12 sylan ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→i+1∈0..^A
14 ccatval1 ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧i+1∈0..^A→A++B⁡i+1=A⁡i+1
15 1 2 13 14 syl3anc ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A++B⁡i+1=A⁡i+1
16 10 15 preq12d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A++B⁡iA++B⁡i+1=A⁡iA⁡i+1
17 16 eleq1d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A++B⁡iA++B⁡i+1∈Edg⁡G↔A⁡iA⁡i+1∈Edg⁡G
18 17 biimprd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧i∈0..^A−1→A⁡iA⁡i+1∈Edg⁡G→A++B⁡iA++B⁡i+1∈Edg⁡G
19 18 ralimdva ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G→∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
20 19 impancom ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G→B∈WordVtx⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
21 20 3adant3 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→B∈WordVtx⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
22 21 com12 ⊢B∈WordVtx⁡G→A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
23 22 adantr ⊢B∈WordVtx⁡G∧B≠∅→A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
24 23 3ad2ant1 ⊢B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
25 24 impcom ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
26 25 3adant3 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G
27 simprl ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A∈WordVtx⁡G
28 simpll ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→B∈WordVtx⁡G
29 simprr ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A≠∅
30 ccatval1lsw ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧A≠∅→A++B⁡A−1=lastS⁡A
31 27 28 29 30 syl3anc ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A++B⁡A−1=lastS⁡A
32 31 adantr ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A++B⁡A−1=lastS⁡A
33 3 nn0cnd ⊢A∈WordVtx⁡G→A∈ℂ
34 npcan1 ⊢A∈ℂ→A-1+1=A
35 33 34 syl ⊢A∈WordVtx⁡G→A-1+1=A
36 35 ad2antrl ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A-1+1=A
37 36 fveq2d ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A++B⁡A-1+1=A++B⁡A
38 simplr ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→B≠∅
39 ccatval21sw ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧B≠∅→A++B⁡A=B⁡0
40 27 28 38 39 syl3anc ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A++B⁡A=B⁡0
41 37 40 eqtrd ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A++B⁡A-1+1=B⁡0
42 41 adantr ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A++B⁡A-1+1=B⁡0
43 simpr ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A⁡0=B⁡0
44 42 43 eqtr4d ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A++B⁡A-1+1=A⁡0
45 32 44 preq12d ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1=lastS⁡AA⁡0
46 45 eleq1d ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅∧A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G↔lastS⁡AA⁡0∈Edg⁡G
47 46 exbiri ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→A⁡0=B⁡0→lastS⁡AA⁡0∈Edg⁡G→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
48 47 com23 ⊢B∈WordVtx⁡G∧B≠∅∧A∈WordVtx⁡G∧A≠∅→lastS⁡AA⁡0∈Edg⁡G→A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
49 48 expimpd ⊢B∈WordVtx⁡G∧B≠∅→A∈WordVtx⁡G∧A≠∅∧lastS⁡AA⁡0∈Edg⁡G→A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
50 49 3ad2ant1 ⊢B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A∈WordVtx⁡G∧A≠∅∧lastS⁡AA⁡0∈Edg⁡G→A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
51 50 com12 ⊢A∈WordVtx⁡G∧A≠∅∧lastS⁡AA⁡0∈Edg⁡G→B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
52 51 3adant2 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
53 52 3imp ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
54 ralunb ⊢∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G∧∀i∈A−1A++B⁡iA++B⁡i+1∈Edg⁡G
55 ovex ⊢A−1∈V
56 fveq2 ⊢i=A−1→A++B⁡i=A++B⁡A−1
57 fvoveq1 ⊢i=A−1→A++B⁡i+1=A++B⁡A-1+1
58 56 57 preq12d ⊢i=A−1→A++B⁡iA++B⁡i+1=A++B⁡A−1A++B⁡A-1+1
59 58 eleq1d ⊢i=A−1→A++B⁡iA++B⁡i+1∈Edg⁡G↔A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
60 55 59 ralsn ⊢∀i∈A−1A++B⁡iA++B⁡i+1∈Edg⁡G↔A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
61 60 anbi2i ⊢∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G∧∀i∈A−1A++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G∧A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
62 54 61 bitri ⊢∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1A++B⁡iA++B⁡i+1∈Edg⁡G∧A++B⁡A−1A++B⁡A-1+1∈Edg⁡G
63 26 53 62 sylanbrc ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G
64 0z ⊢0∈ℤ
65 lennncl ⊢A∈WordVtx⁡G∧A≠∅→A∈ℕ
66 0p1e1 ⊢0+1=1
67 66 fveq2i ⊢ℤ≥0+1=ℤ≥1
68 67 eleq2i ⊢A∈ℤ≥0+1↔A∈ℤ≥1
69 elnnuz ⊢A∈ℕ↔A∈ℤ≥1
70 68 69 bitr4i ⊢A∈ℤ≥0+1↔A∈ℕ
71 65 70 sylibr ⊢A∈WordVtx⁡G∧A≠∅→A∈ℤ≥0+1
72 fzosplitsnm1 ⊢0∈ℤ∧A∈ℤ≥0+1→0..^A=0..^A−1∪A−1
73 64 71 72 sylancr ⊢A∈WordVtx⁡G∧A≠∅→0..^A=0..^A−1∪A−1
74 73 raleqdv ⊢A∈WordVtx⁡G∧A≠∅→∀i∈0..^AA++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G
75 74 3ad2ant1 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→∀i∈0..^AA++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G
76 75 3ad2ant1 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^AA++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A−1∪A−1A++B⁡iA++B⁡i+1∈Edg⁡G
77 63 76 mpbird ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^AA++B⁡iA++B⁡i+1∈Edg⁡G
78 lencl ⊢B∈WordVtx⁡G→B∈ℕ0
79 78 nn0zd ⊢B∈WordVtx⁡G→B∈ℤ
80 peano2zm ⊢B∈ℤ→B−1∈ℤ
81 79 80 syl ⊢B∈WordVtx⁡G→B−1∈ℤ
82 81 ad2antrl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→B−1∈ℤ
83 82 adantr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→B−1∈ℤ
84 83 anim1ci ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i∈A..^A+B-1∧B−1∈ℤ
85 fzosubel3 ⊢i∈A..^A+B-1∧B−1∈ℤ→i−A∈0..^B−1
86 fveq2 ⊢j=i−A→B⁡j=B⁡i−A
87 fvoveq1 ⊢j=i−A→B⁡j+1=B⁡i-A+1
88 86 87 preq12d ⊢j=i−A→B⁡jB⁡j+1=B⁡i−AB⁡i-A+1
89 88 eleq1d ⊢j=i−A→B⁡jB⁡j+1∈Edg⁡G↔B⁡i−AB⁡i-A+1∈Edg⁡G
90 89 rspcv ⊢i−A∈0..^B−1→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→B⁡i−AB⁡i-A+1∈Edg⁡G
91 84 85 90 3syl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→B⁡i−AB⁡i-A+1∈Edg⁡G
92 simp-4l ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A∈WordVtx⁡G
93 simprl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→B∈WordVtx⁡G
94 93 ad2antrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→B∈WordVtx⁡G
95 3 adantr ⊢A∈WordVtx⁡G∧A≠∅→A∈ℕ0
96 78 adantr ⊢B∈WordVtx⁡G∧B≠∅→B∈ℕ0
97 nn0addcl ⊢A∈ℕ0∧B∈ℕ0→A+B∈ℕ0
98 97 nn0zd ⊢A∈ℕ0∧B∈ℕ0→A+B∈ℤ
99 95 96 98 syl2an ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A+B∈ℤ
100 1nn0 ⊢1∈ℕ0
101 eluzmn ⊢A+B∈ℤ∧1∈ℕ0→A+B∈ℤ≥A+B-1
102 99 100 101 sylancl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A+B∈ℤ≥A+B-1
103 33 ad2antrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A∈ℂ
104 78 nn0cnd ⊢B∈WordVtx⁡G→B∈ℂ
105 104 ad2antrl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→B∈ℂ
106 1cnd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→1∈ℂ
107 103 105 106 addsubassd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A+B-1=A+B-1
108 107 fveq2d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→ℤ≥A+B-1=ℤ≥A+B-1
109 102 108 eleqtrd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A+B∈ℤ≥A+B-1
110 fzoss2 ⊢A+B∈ℤ≥A+B-1→A..^A+B-1⊆A..^A+B
111 109 110 syl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A..^A+B-1⊆A..^A+B
112 111 adantr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→A..^A+B-1⊆A..^A+B
113 112 sselda ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i∈A..^A+B
114 ccatval2 ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧i∈A..^A+B→A++B⁡i=B⁡i−A
115 92 94 113 114 syl3anc ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A++B⁡i=B⁡i−A
116 107 oveq2d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A..^A+B-1=A..^A+B-1
117 116 eleq2d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→i∈A..^A+B-1↔i∈A..^A+B-1
118 117 adantr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→i∈A..^A+B-1↔i∈A..^A+B-1
119 eluzmn ⊢A∈ℤ∧1∈ℕ0→A∈ℤ≥A−1
120 4 100 119 sylancl ⊢A∈WordVtx⁡G→A∈ℤ≥A−1
121 120 ad3antrrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→A∈ℤ≥A−1
122 fzoss1 ⊢A∈ℤ≥A−1→A..^A+B-1⊆A−1..^A+B-1
123 121 122 syl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→A..^A+B-1⊆A−1..^A+B-1
124 123 sseld ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→i∈A..^A+B-1→i∈A−1..^A+B-1
125 118 124 sylbird ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→i∈A..^A+B-1→i∈A−1..^A+B-1
126 125 imp ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i∈A−1..^A+B-1
127 4 adantr ⊢A∈WordVtx⁡G∧A≠∅→A∈ℤ
128 79 adantr ⊢B∈WordVtx⁡G∧B≠∅→B∈ℤ
129 simpl ⊢A∈ℤ∧B∈ℤ→A∈ℤ
130 zaddcl ⊢A∈ℤ∧B∈ℤ→A+B∈ℤ
131 129 130 jca ⊢A∈ℤ∧B∈ℤ→A∈ℤ∧A+B∈ℤ
132 127 128 131 syl2an ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A∈ℤ∧A+B∈ℤ
133 132 adantr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0→A∈ℤ∧A+B∈ℤ
134 elfzoelz ⊢i∈A..^A+B-1→i∈ℤ
135 1zzd ⊢i∈A..^A+B-1→1∈ℤ
136 134 135 jca ⊢i∈A..^A+B-1→i∈ℤ∧1∈ℤ
137 elfzomelpfzo ⊢A∈ℤ∧A+B∈ℤ∧i∈ℤ∧1∈ℤ→i∈A−1..^A+B-1↔i+1∈A..^A+B
138 133 136 137 syl2an ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i∈A−1..^A+B-1↔i+1∈A..^A+B
139 126 138 mpbid ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i+1∈A..^A+B
140 ccatval2 ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G∧i+1∈A..^A+B→A++B⁡i+1=B⁡i+1-A
141 92 94 139 140 syl3anc ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A++B⁡i+1=B⁡i+1-A
142 134 zcnd ⊢i∈A..^A+B-1→i∈ℂ
143 142 adantl ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i∈ℂ
144 1cnd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→1∈ℂ
145 103 ad2antrr ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A∈ℂ
146 143 144 145 addsubd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→i+1-A=i-A+1
147 146 fveq2d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→B⁡i+1-A=B⁡i-A+1
148 141 147 eqtrd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A++B⁡i+1=B⁡i-A+1
149 115 148 preq12d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A++B⁡iA++B⁡i+1=B⁡i−AB⁡i-A+1
150 149 eleq1d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→A++B⁡iA++B⁡i+1∈Edg⁡G↔B⁡i−AB⁡i-A+1∈Edg⁡G
151 91 150 sylibrd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧i∈A..^A+B-1→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→A++B⁡iA++B⁡i+1∈Edg⁡G
152 151 impancom ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→i∈A..^A+B-1→A++B⁡iA++B⁡i+1∈Edg⁡G
153 152 ralrimiv ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧A⁡0=B⁡0∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
154 153 exp31 ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A⁡0=B⁡0→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
155 154 expcom ⊢B∈WordVtx⁡G∧B≠∅→A∈WordVtx⁡G∧A≠∅→A⁡0=B⁡0→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
156 155 com23 ⊢B∈WordVtx⁡G∧B≠∅→A⁡0=B⁡0→A∈WordVtx⁡G∧A≠∅→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
157 156 com24 ⊢B∈WordVtx⁡G∧B≠∅→∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→A∈WordVtx⁡G∧A≠∅→A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
158 157 imp ⊢B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G→A∈WordVtx⁡G∧A≠∅→A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
159 158 3adant3 ⊢B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A∈WordVtx⁡G∧A≠∅→A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
160 159 com12 ⊢A∈WordVtx⁡G∧A≠∅→B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
161 160 3ad2ant1 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G→B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
162 161 3imp ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
163 ralunb ⊢∀i∈0..^A∪A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^AA++B⁡iA++B⁡i+1∈Edg⁡G∧∀i∈A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
164 77 162 163 sylanbrc ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A∪A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
165 ccatlen ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G→A++B=A+B
166 165 oveq1d ⊢A∈WordVtx⁡G∧B∈WordVtx⁡G→A++B−1=A+B-1
167 166 ad2ant2r ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A++B−1=A+B-1
168 167 107 eqtrd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→A++B−1=A+B-1
169 168 oveq2d ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→0..^A++B−1=0..^A+B-1
170 elnn0uz ⊢A∈ℕ0↔A∈ℤ≥0
171 3 170 sylib ⊢A∈WordVtx⁡G→A∈ℤ≥0
172 171 adantr ⊢A∈WordVtx⁡G∧A≠∅→A∈ℤ≥0
173 lennncl ⊢B∈WordVtx⁡G∧B≠∅→B∈ℕ
174 nnm1nn0 ⊢B∈ℕ→B−1∈ℕ0
175 173 174 syl ⊢B∈WordVtx⁡G∧B≠∅→B−1∈ℕ0
176 fzoun ⊢A∈ℤ≥0∧B−1∈ℕ0→0..^A+B-1=0..^A∪A..^A+B-1
177 172 175 176 syl2an ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→0..^A+B-1=0..^A∪A..^A+B-1
178 169 177 eqtrd ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅→0..^A++B−1=0..^A∪A..^A+B-1
179 178 3ad2antr1 ⊢A∈WordVtx⁡G∧A≠∅∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→0..^A++B−1=0..^A∪A..^A+B-1
180 179 3ad2antl1 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G→0..^A++B−1=0..^A∪A..^A+B-1
181 180 3adant3 ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→0..^A++B−1=0..^A∪A..^A+B-1
182 181 raleqdv ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A++B−1A++B⁡iA++B⁡i+1∈Edg⁡G↔∀i∈0..^A∪A..^A+B-1A++B⁡iA++B⁡i+1∈Edg⁡G
183 164 182 mpbird ⊢A∈WordVtx⁡G∧A≠∅∧∀i∈0..^A−1A⁡iA⁡i+1∈Edg⁡G∧lastS⁡AA⁡0∈Edg⁡G∧B∈WordVtx⁡G∧B≠∅∧∀j∈0..^B−1B⁡jB⁡j+1∈Edg⁡G∧lastS⁡BB⁡0∈Edg⁡G∧A⁡0=B⁡0→∀i∈0..^A++B−1A++B⁡iA++B⁡i+1∈Edg⁡G