Metamath Proof Explorer

Theorem sticksstones12a

Description: Establish bijective mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 11-Oct-2024)

Ref Expression
Hypotheses sticksstones12a.1 ⊢φ→N∈ℕ0
sticksstones12a.2 ⊢φ→K∈ℕ
sticksstones12a.3 ⊢F=a∈A⟼j∈1…K⟼j+∑l=1ja⁡l
sticksstones12a.4 ⊢G=b∈B⟼ifK=01Nk∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1
sticksstones12a.5 ⊢A=g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N
sticksstones12a.6 ⊢B=f|f:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y
Assertion sticksstones12a ⊢φ→∀d∈BF⁡G⁡d=d

Proof

Step Hyp Ref Expression
1 sticksstones12a.1 ⊢φ→N∈ℕ0
2 sticksstones12a.2 ⊢φ→K∈ℕ
3 sticksstones12a.3 ⊢F=a∈A⟼j∈1…K⟼j+∑l=1ja⁡l
4 sticksstones12a.4 ⊢G=b∈B⟼ifK=01Nk∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1
5 sticksstones12a.5 ⊢A=g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N
6 sticksstones12a.6 ⊢B=f|f:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y
7 4 a1i ⊢φ∧d∈B→G=b∈B⟼ifK=01Nk∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1
8 0red ⊢φ→0∈ℝ
9 2 nngt0d ⊢φ→0<K
10 8 9 ltned ⊢φ→0≠K
11 10 necomd ⊢φ→K≠0
12 11 neneqd ⊢φ→¬K=0
13 12 ad2antrr ⊢φ∧d∈B∧b=d→¬K=0
14 13 iffalsed ⊢φ∧d∈B∧b=d→ifK=01Nk∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1
15 fveq1 ⊢b=d→b⁡K=d⁡K
16 15 oveq2d ⊢b=d→N+K-b⁡K=N+K-d⁡K
17 fveq1 ⊢b=d→b⁡1=d⁡1
18 17 oveq1d ⊢b=d→b⁡1−1=d⁡1−1
19 fveq1 ⊢b=d→b⁡k=d⁡k
20 fveq1 ⊢b=d→b⁡k−1=d⁡k−1
21 19 20 oveq12d ⊢b=d→b⁡k−b⁡k−1=d⁡k−d⁡k−1
22 21 oveq1d ⊢b=d→b⁡k-b⁡k−1-1=d⁡k-d⁡k−1-1
23 18 22 ifeq12d ⊢b=d→ifk=1b⁡1−1b⁡k-b⁡k−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1
24 16 23 ifeq12d ⊢b=d→ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
25 24 adantl ⊢φ∧d∈B∧b=d→ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
26 25 adantr ⊢φ∧d∈B∧b=d∧k∈1…K+1→ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
27 26 mpteq2dva ⊢φ∧d∈B∧b=d→k∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
28 14 27 eqtrd ⊢φ∧d∈B∧b=d→ifK=01Nk∈1…K+1⟼ifk=K+1N+K-b⁡Kifk=1b⁡1−1b⁡k-b⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
29 simpr ⊢φ∧d∈B→d∈B
30 fzfid ⊢φ∧d∈B→1…K+1∈Fin
31 30 mptexd ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈V
32 7 28 29 31 fvmptd ⊢φ∧d∈B→G⁡d=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
33 32 fveq2d ⊢φ∧d∈B→F⁡G⁡d=F⁡k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
34 3 a1i ⊢φ∧d∈B→F=a∈A⟼j∈1…K⟼j+∑l=1ja⁡l
35 simpll ⊢a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧j∈1…K∧l∈1…j→a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
36 35 fveq1d ⊢a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧j∈1…K∧l∈1…j→a⁡l=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
37 36 sumeq2dv ⊢a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧j∈1…K→∑l=1ja⁡l=∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
38 37 oveq2d ⊢a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧j∈1…K→j+∑l=1ja⁡l=j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
39 38 mpteq2dva ⊢a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→j∈1…K⟼j+∑l=1ja⁡l=j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
40 39 adantl ⊢φ∧d∈B∧a=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→j∈1…K⟼j+∑l=1ja⁡l=j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
41 eleq1 ⊢N+K-d⁡K=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→N+K-d⁡K∈ℕ0↔ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
42 eleq1 ⊢ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0↔ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
43 6 eleq2i ⊢d∈B↔d∈f|f:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y
44 vex ⊢d∈V
45 feq1 ⊢f=d→f:1…K⟶1…N+K↔d:1…K⟶1…N+K
46 fveq1 ⊢f=d→f⁡x=d⁡x
47 fveq1 ⊢f=d→f⁡y=d⁡y
48 46 47 breq12d ⊢f=d→f⁡x<f⁡y↔d⁡x<d⁡y
49 48 imbi2d ⊢f=d→x<y→f⁡x<f⁡y↔x<y→d⁡x<d⁡y
50 49 2ralbidv ⊢f=d→∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y↔∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
51 45 50 anbi12d ⊢f=d→f:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y↔d:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
52 44 51 elab ⊢d∈f|f:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→f⁡x<f⁡y↔d:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
53 43 52 bitri ⊢d∈B↔d:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
54 53 biimpi ⊢d∈B→d:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
55 54 adantl ⊢φ∧d∈B→d:1…K⟶1…N+K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
56 55 simpld ⊢φ∧d∈B→d:1…K⟶1…N+K
57 1zzd ⊢φ→1∈ℤ
58 57 adantr ⊢φ∧d∈B→1∈ℤ
59 2 nnnn0d ⊢φ→K∈ℕ0
60 59 nn0zd ⊢φ→K∈ℤ
61 60 adantr ⊢φ∧d∈B→K∈ℤ
62 2 nnge1d ⊢φ→1≤K
63 62 adantr ⊢φ∧d∈B→1≤K
64 2 nnred ⊢φ→K∈ℝ
65 64 leidd ⊢φ→K≤K
66 65 adantr ⊢φ∧d∈B→K≤K
67 58 61 61 63 66 elfzd ⊢φ∧d∈B→K∈1…K
68 56 67 ffvelcdmd ⊢φ∧d∈B→d⁡K∈1…N+K
69 elfzle2 ⊢d⁡K∈1…N+K→d⁡K≤N+K
70 68 69 syl ⊢φ∧d∈B→d⁡K≤N+K
71 70 adantr ⊢φ∧d∈B∧k∈1…K+1→d⁡K≤N+K
72 71 adantr ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→d⁡K≤N+K
73 elfznn ⊢d⁡K∈1…N+K→d⁡K∈ℕ
74 73 nnnn0d ⊢d⁡K∈1…N+K→d⁡K∈ℕ0
75 68 74 syl ⊢φ∧d∈B→d⁡K∈ℕ0
76 75 adantr ⊢φ∧d∈B∧k∈1…K+1→d⁡K∈ℕ0
77 76 adantr ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→d⁡K∈ℕ0
78 1 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→N∈ℕ0
79 59 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→K∈ℕ0
80 78 79 nn0addcld ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→N+K∈ℕ0
81 nn0sub ⊢d⁡K∈ℕ0∧N+K∈ℕ0→d⁡K≤N+K↔N+K-d⁡K∈ℕ0
82 77 80 81 syl2anc ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→d⁡K≤N+K↔N+K-d⁡K∈ℕ0
83 72 82 mpbid ⊢φ∧d∈B∧k∈1…K+1∧k=K+1→N+K-d⁡K∈ℕ0
84 eleq1 ⊢d⁡1−1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡1−1∈ℕ0↔ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
85 eleq1 ⊢d⁡k-d⁡k−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡k-d⁡k−1-1∈ℕ0↔ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
86 1le1 ⊢1≤1
87 86 a1i ⊢φ∧d∈B→1≤1
88 58 61 58 87 63 elfzd ⊢φ∧d∈B→1∈1…K
89 56 88 ffvelcdmd ⊢φ∧d∈B→d⁡1∈1…N+K
90 elfznn ⊢d⁡1∈1…N+K→d⁡1∈ℕ
91 89 90 syl ⊢φ∧d∈B→d⁡1∈ℕ
92 nnm1nn0 ⊢d⁡1∈ℕ→d⁡1−1∈ℕ0
93 91 92 syl ⊢φ∧d∈B→d⁡1−1∈ℕ0
94 93 adantr ⊢φ∧d∈B∧k∈1…K+1→d⁡1−1∈ℕ0
95 94 adantr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→d⁡1−1∈ℕ0
96 95 adantr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧k=1→d⁡1−1∈ℕ0
97 56 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d:1…K⟶1…N+K
98 1zzd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→1∈ℤ
99 61 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→K∈ℤ
100 elfznn ⊢k∈1…K+1→k∈ℕ
101 100 nnzd ⊢k∈1…K+1→k∈ℤ
102 101 ad3antlr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k∈ℤ
103 elfzle1 ⊢k∈1…K+1→1≤k
104 103 ad3antlr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→1≤k
105 neqne ⊢¬k=K+1→k≠K+1
106 105 adantl ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k≠K+1
107 106 necomd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→K+1≠k
108 100 ad2antlr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k∈ℕ
109 108 nnred ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k∈ℝ
110 64 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→K∈ℝ
111 1red ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→1∈ℝ
112 110 111 readdcld ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→K+1∈ℝ
113 elfzle2 ⊢k∈1…K+1→k≤K+1
114 113 ad2antlr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k≤K+1
115 109 112 114 leltned ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k<K+1↔K+1≠k
116 107 115 mpbird ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k<K+1
117 101 ad2antlr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k∈ℤ
118 61 ad2antrr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→K∈ℤ
119 zleltp1 ⊢k∈ℤ∧K∈ℤ→k≤K↔k<K+1
120 117 118 119 syl2anc ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k≤K↔k<K+1
121 116 120 mpbird ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→k≤K
122 121 adantr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k≤K
123 98 99 102 104 122 elfzd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k∈1…K
124 97 123 ffvelcdmd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k∈1…N+K
125 elfznn ⊢d⁡k∈1…N+K→d⁡k∈ℕ
126 125 nnzd ⊢d⁡k∈1…N+K→d⁡k∈ℤ
127 124 126 syl ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k∈ℤ
128 1zzd ⊢φ∧k∈1…K+1∧¬k=1→1∈ℤ
129 60 ad2antrr ⊢φ∧k∈1…K+1∧¬k=1→K∈ℤ
130 129 3impa ⊢φ∧k∈1…K+1∧¬k=1→K∈ℤ
131 101 adantl ⊢φ∧k∈1…K+1→k∈ℤ
132 131 adantr ⊢φ∧k∈1…K+1∧¬k=1→k∈ℤ
133 132 3impa ⊢φ∧k∈1…K+1∧¬k=1→k∈ℤ
134 133 128 zsubcld ⊢φ∧k∈1…K+1∧¬k=1→k−1∈ℤ
135 neqne ⊢¬k=1→k≠1
136 135 3ad2ant3 ⊢φ∧k∈1…K+1∧¬k=1→k≠1
137 1red ⊢φ→1∈ℝ
138 137 3ad2ant1 ⊢φ∧k∈1…K+1∧¬k=1→1∈ℝ
139 133 zred ⊢φ∧k∈1…K+1∧¬k=1→k∈ℝ
140 simp2 ⊢φ∧k∈1…K+1∧¬k=1→k∈1…K+1
141 140 103 syl ⊢φ∧k∈1…K+1∧¬k=1→1≤k
142 138 139 141 leltned ⊢φ∧k∈1…K+1∧¬k=1→1<k↔k≠1
143 136 142 mpbird ⊢φ∧k∈1…K+1∧¬k=1→1<k
144 128 133 zltp1led ⊢φ∧k∈1…K+1∧¬k=1→1<k↔1+1≤k
145 143 144 mpbid ⊢φ∧k∈1…K+1∧¬k=1→1+1≤k
146 leaddsub ⊢1∈ℝ∧1∈ℝ∧k∈ℝ→1+1≤k↔1≤k−1
147 138 138 139 146 syl3anc ⊢φ∧k∈1…K+1∧¬k=1→1+1≤k↔1≤k−1
148 145 147 mpbid ⊢φ∧k∈1…K+1∧¬k=1→1≤k−1
149 134 zred ⊢φ∧k∈1…K+1∧¬k=1→k−1∈ℝ
150 64 3ad2ant1 ⊢φ∧k∈1…K+1∧¬k=1→K∈ℝ
151 1red ⊢φ∧k∈1…K+1∧¬k=1→1∈ℝ
152 150 151 readdcld ⊢φ∧k∈1…K+1∧¬k=1→K+1∈ℝ
153 152 151 resubcld ⊢φ∧k∈1…K+1∧¬k=1→K+1-1∈ℝ
154 113 3ad2ant2 ⊢φ∧k∈1…K+1∧¬k=1→k≤K+1
155 139 152 151 154 lesub1dd ⊢φ∧k∈1…K+1∧¬k=1→k−1≤K+1-1
156 64 recnd ⊢φ→K∈ℂ
157 156 3ad2ant1 ⊢φ∧k∈1…K+1∧¬k=1→K∈ℂ
158 1cnd ⊢φ∧k∈1…K+1∧¬k=1→1∈ℂ
159 157 158 pncand ⊢φ∧k∈1…K+1∧¬k=1→K+1-1=K
160 65 3ad2ant1 ⊢φ∧k∈1…K+1∧¬k=1→K≤K
161 159 160 eqbrtrd ⊢φ∧k∈1…K+1∧¬k=1→K+1-1≤K
162 149 153 150 155 161 letrd ⊢φ∧k∈1…K+1∧¬k=1→k−1≤K
163 128 130 134 148 162 elfzd ⊢φ∧k∈1…K+1∧¬k=1→k−1∈1…K
164 163 ad5ant135 ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k−1∈1…K
165 97 164 ffvelcdmd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1∈1…N+K
166 elfznn ⊢d⁡k−1∈1…N+K→d⁡k−1∈ℕ
167 165 166 syl ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1∈ℕ
168 167 nnzd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1∈ℤ
169 127 168 zsubcld ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−d⁡k−1∈ℤ
170 169 98 zsubcld ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k-d⁡k−1-1∈ℤ
171 108 adantr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k∈ℕ
172 171 nnred ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k∈ℝ
173 172 ltm1d ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k−1<k
174 164 123 jca ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k−1∈1…K∧k∈1…K
175 55 simprd ⊢φ∧d∈B→∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
176 175 ad3antrrr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y
177 breq1 ⊢x=k−1→x<y↔k−1<y
178 fveq2 ⊢x=k−1→d⁡x=d⁡k−1
179 178 breq1d ⊢x=k−1→d⁡x<d⁡y↔d⁡k−1<d⁡y
180 177 179 imbi12d ⊢x=k−1→x<y→d⁡x<d⁡y↔k−1<y→d⁡k−1<d⁡y
181 breq2 ⊢y=k→k−1<y↔k−1<k
182 fveq2 ⊢y=k→d⁡y=d⁡k
183 182 breq2d ⊢y=k→d⁡k−1<d⁡y↔d⁡k−1<d⁡k
184 181 183 imbi12d ⊢y=k→k−1<y→d⁡k−1<d⁡y↔k−1<k→d⁡k−1<d⁡k
185 180 184 rspc2va ⊢k−1∈1…K∧k∈1…K∧∀x∈1…K∀y∈1…Kx<y→d⁡x<d⁡y→k−1<k→d⁡k−1<d⁡k
186 174 176 185 syl2anc ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→k−1<k→d⁡k−1<d⁡k
187 173 186 mpd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1<d⁡k
188 167 nnred ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1∈ℝ
189 127 zred ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k∈ℝ
190 188 189 posdifd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k−1<d⁡k↔0<d⁡k−d⁡k−1
191 187 190 mpbid ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→0<d⁡k−d⁡k−1
192 0zd ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→0∈ℤ
193 192 169 zltlem1d ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→0<d⁡k−d⁡k−1↔0≤d⁡k-d⁡k−1-1
194 191 193 mpbid ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→0≤d⁡k-d⁡k−1-1
195 170 194 jca ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k-d⁡k−1-1∈ℤ∧0≤d⁡k-d⁡k−1-1
196 elnn0z ⊢d⁡k-d⁡k−1-1∈ℕ0↔d⁡k-d⁡k−1-1∈ℤ∧0≤d⁡k-d⁡k−1-1
197 195 196 sylibr ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1∧¬k=1→d⁡k-d⁡k−1-1∈ℕ0
198 84 85 96 197 ifbothda ⊢φ∧d∈B∧k∈1…K+1∧¬k=K+1→ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
199 41 42 83 198 ifbothda ⊢φ∧d∈B∧k∈1…K+1→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℕ0
200 eqid ⊢k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
201 199 200 fmptd ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0
202 eqidd ⊢φ∧d∈B∧i∈1…K+1→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
203 simpr ⊢φ∧d∈B∧i∈1…K+1∧k=i→k=i
204 203 eqeq1d ⊢φ∧d∈B∧i∈1…K+1∧k=i→k=K+1↔i=K+1
205 203 eqeq1d ⊢φ∧d∈B∧i∈1…K+1∧k=i→k=1↔i=1
206 203 fveq2d ⊢φ∧d∈B∧i∈1…K+1∧k=i→d⁡k=d⁡i
207 203 fvoveq1d ⊢φ∧d∈B∧i∈1…K+1∧k=i→d⁡k−1=d⁡i−1
208 206 207 oveq12d ⊢φ∧d∈B∧i∈1…K+1∧k=i→d⁡k−d⁡k−1=d⁡i−d⁡i−1
209 208 oveq1d ⊢φ∧d∈B∧i∈1…K+1∧k=i→d⁡k-d⁡k−1-1=d⁡i-d⁡i−1-1
210 205 209 ifbieq2d ⊢φ∧d∈B∧i∈1…K+1∧k=i→ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifi=1d⁡1−1d⁡i-d⁡i−1-1
211 204 210 ifbieq2d ⊢φ∧d∈B∧i∈1…K+1∧k=i→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1
212 simpr ⊢φ∧d∈B∧i∈1…K+1→i∈1…K+1
213 ovexd ⊢φ∧d∈B∧i∈1…K+1→N+K-d⁡K∈V
214 ovexd ⊢φ∧d∈B∧i∈1…K+1→d⁡1−1∈V
215 ovexd ⊢φ∧d∈B∧i∈1…K+1→d⁡i-d⁡i−1-1∈V
216 214 215 ifcld ⊢φ∧d∈B∧i∈1…K+1→ifi=1d⁡1−1d⁡i-d⁡i−1-1∈V
217 213 216 ifcld ⊢φ∧d∈B∧i∈1…K+1→ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1∈V
218 202 211 212 217 fvmptd ⊢φ∧d∈B∧i∈1…K+1→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1
219 218 sumeq2dv ⊢φ∧d∈B→∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=∑i=1K+1ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1
220 eqeq1 ⊢i=k→i=K+1↔k=K+1
221 eqeq1 ⊢i=k→i=1↔k=1
222 fveq2 ⊢i=k→d⁡i=d⁡k
223 fvoveq1 ⊢i=k→d⁡i−1=d⁡k−1
224 222 223 oveq12d ⊢i=k→d⁡i−d⁡i−1=d⁡k−d⁡k−1
225 224 oveq1d ⊢i=k→d⁡i-d⁡i−1-1=d⁡k-d⁡k−1-1
226 221 225 ifbieq2d ⊢i=k→ifi=1d⁡1−1d⁡i-d⁡i−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1
227 220 226 ifbieq2d ⊢i=k→ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1=ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
228 nfcv ⊢Ⅎ_k1…K+1
229 nfcv ⊢Ⅎ_i1…K+1
230 nfcv ⊢Ⅎ_kifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1
231 nfcv ⊢Ⅎ_iifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
232 227 228 229 230 231 cbvsum ⊢∑i=1K+1ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1=∑k=1K+1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
233 232 a1i ⊢φ∧d∈B→∑i=1K+1ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1=∑k=1K+1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
234 eqid ⊢1=1
235 1p0e1 ⊢1+0=1
236 234 235 eqtr4i ⊢1=1+0
237 236 a1i ⊢φ→1=1+0
238 0le1 ⊢0≤1
239 238 a1i ⊢φ→0≤1
240 137 8 64 137 62 239 le2addd ⊢φ→1+0≤K+1
241 237 240 eqbrtrd ⊢φ→1≤K+1
242 60 peano2zd ⊢φ→K+1∈ℤ
243 eluz ⊢1∈ℤ∧K+1∈ℤ→K+1∈ℤ≥1↔1≤K+1
244 57 242 243 syl2anc ⊢φ→K+1∈ℤ≥1↔1≤K+1
245 241 244 mpbird ⊢φ→K+1∈ℤ≥1
246 245 adantr ⊢φ∧d∈B→K+1∈ℤ≥1
247 199 nn0cnd ⊢φ∧d∈B∧k∈1…K+1→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℂ
248 eqeq1 ⊢k=K+1→k=K+1↔K+1=K+1
249 eqeq1 ⊢k=K+1→k=1↔K+1=1
250 fveq2 ⊢k=K+1→d⁡k=d⁡K+1
251 fvoveq1 ⊢k=K+1→d⁡k−1=d⁡K+1-1
252 250 251 oveq12d ⊢k=K+1→d⁡k−d⁡k−1=d⁡K+1−d⁡K+1-1
253 252 oveq1d ⊢k=K+1→d⁡k-d⁡k−1-1=d⁡K+1-d⁡K+1-1-1
254 249 253 ifbieq2d ⊢k=K+1→ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1
255 248 254 ifbieq2d ⊢k=K+1→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=ifK+1=K+1N+K-d⁡KifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1
256 246 247 255 fsumm1 ⊢φ∧d∈B→∑k=1K+1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=∑k=1K+1-1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+ifK+1=K+1N+K-d⁡KifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1
257 156 adantr ⊢φ∧d∈B→K∈ℂ
258 1cnd ⊢φ∧d∈B→1∈ℂ
259 257 258 pncand ⊢φ∧d∈B→K+1-1=K
260 259 oveq2d ⊢φ∧d∈B→1…K+1-1=1…K
261 260 sumeq1d ⊢φ∧d∈B→∑k=1K+1-1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
262 eqidd ⊢φ∧d∈B→K+1=K+1
263 262 iftrued ⊢φ∧d∈B→ifK+1=K+1N+K-d⁡KifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1=N+K-d⁡K
264 261 263 oveq12d ⊢φ∧d∈B→∑k=1K+1-1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+ifK+1=K+1N+K-d⁡KifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1=∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+N+K-d⁡K
265 elfzelz ⊢k∈1…K→k∈ℤ
266 265 adantl ⊢φ∧d∈B∧k∈1…K→k∈ℤ
267 266 zred ⊢φ∧d∈B∧k∈1…K→k∈ℝ
268 64 ad2antrr ⊢φ∧d∈B∧k∈1…K→K∈ℝ
269 1red ⊢φ∧d∈B∧k∈1…K→1∈ℝ
270 268 269 readdcld ⊢φ∧d∈B∧k∈1…K→K+1∈ℝ
271 elfzle2 ⊢k∈1…K→k≤K
272 271 adantl ⊢φ∧d∈B∧k∈1…K→k≤K
273 268 ltp1d ⊢φ∧d∈B∧k∈1…K→K<K+1
274 267 268 270 272 273 lelttrd ⊢φ∧d∈B∧k∈1…K→k<K+1
275 267 274 ltned ⊢φ∧d∈B∧k∈1…K→k≠K+1
276 275 neneqd ⊢φ∧d∈B∧k∈1…K→¬k=K+1
277 276 iffalsed ⊢φ∧d∈B∧k∈1…K→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1
278 277 sumeq2dv ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1
279 eqeq1 ⊢d⁡1−1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡1−1=ifk=1d⁡1d⁡k−d⁡k−1−1↔ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifk=1d⁡1d⁡k−d⁡k−1−1
280 eqeq1 ⊢d⁡k-d⁡k−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡k-d⁡k−1-1=ifk=1d⁡1d⁡k−d⁡k−1−1↔ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifk=1d⁡1d⁡k−d⁡k−1−1
281 simpr ⊢φ∧d∈B∧k∈1…K∧k=1→k=1
282 281 iftrued ⊢φ∧d∈B∧k∈1…K∧k=1→ifk=1d⁡1d⁡k−d⁡k−1=d⁡1
283 282 eqcomd ⊢φ∧d∈B∧k∈1…K∧k=1→d⁡1=ifk=1d⁡1d⁡k−d⁡k−1
284 283 oveq1d ⊢φ∧d∈B∧k∈1…K∧k=1→d⁡1−1=ifk=1d⁡1d⁡k−d⁡k−1−1
285 simpr ⊢φ∧d∈B∧k∈1…K∧¬k=1→¬k=1
286 285 iffalsed ⊢φ∧d∈B∧k∈1…K∧¬k=1→ifk=1d⁡1d⁡k−d⁡k−1=d⁡k−d⁡k−1
287 286 eqcomd ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k−d⁡k−1=ifk=1d⁡1d⁡k−d⁡k−1
288 287 oveq1d ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k-d⁡k−1-1=ifk=1d⁡1d⁡k−d⁡k−1−1
289 279 280 284 288 ifbothda ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifk=1d⁡1d⁡k−d⁡k−1−1
290 289 sumeq2dv ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=∑k=1Kifk=1d⁡1d⁡k−d⁡k−1−1
291 fzfid ⊢φ∧d∈B→1…K∈Fin
292 eleq1 ⊢d⁡1=ifk=1d⁡1d⁡k−d⁡k−1→d⁡1∈ℤ↔ifk=1d⁡1d⁡k−d⁡k−1∈ℤ
293 eleq1 ⊢d⁡k−d⁡k−1=ifk=1d⁡1d⁡k−d⁡k−1→d⁡k−d⁡k−1∈ℤ↔ifk=1d⁡1d⁡k−d⁡k−1∈ℤ
294 56 3adant3 ⊢φ∧d∈B∧k∈1…K→d:1…K⟶1…N+K
295 88 3adant3 ⊢φ∧d∈B∧k∈1…K→1∈1…K
296 294 295 ffvelcdmd ⊢φ∧d∈B∧k∈1…K→d⁡1∈1…N+K
297 90 nnzd ⊢d⁡1∈1…N+K→d⁡1∈ℤ
298 296 297 syl ⊢φ∧d∈B∧k∈1…K→d⁡1∈ℤ
299 298 adantr ⊢φ∧d∈B∧k∈1…K∧k=1→d⁡1∈ℤ
300 simp3 ⊢φ∧d∈B∧k∈1…K→k∈1…K
301 294 300 ffvelcdmd ⊢φ∧d∈B∧k∈1…K→d⁡k∈1…N+K
302 301 126 syl ⊢φ∧d∈B∧k∈1…K→d⁡k∈ℤ
303 302 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k∈ℤ
304 294 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→d:1…K⟶1…N+K
305 1zzd ⊢φ∧d∈B∧k∈1…K∧¬k=1→1∈ℤ
306 61 3adant3 ⊢φ∧d∈B∧k∈1…K→K∈ℤ
307 306 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→K∈ℤ
308 266 3impa ⊢φ∧d∈B∧k∈1…K→k∈ℤ
309 308 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→k∈ℤ
310 309 305 zsubcld ⊢φ∧d∈B∧k∈1…K∧¬k=1→k−1∈ℤ
311 elfzle1 ⊢k∈1…K→1≤k
312 300 311 syl ⊢φ∧d∈B∧k∈1…K→1≤k
313 312 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→1≤k
314 135 adantl ⊢φ∧d∈B∧k∈1…K∧¬k=1→k≠1
315 313 314 jca ⊢φ∧d∈B∧k∈1…K∧¬k=1→1≤k∧k≠1
316 1red ⊢φ∧d∈B∧k∈1…K∧¬k=1→1∈ℝ
317 309 zred ⊢φ∧d∈B∧k∈1…K∧¬k=1→k∈ℝ
318 316 317 ltlend ⊢φ∧d∈B∧k∈1…K∧¬k=1→1<k↔1≤k∧k≠1
319 315 318 mpbird ⊢φ∧d∈B∧k∈1…K∧¬k=1→1<k
320 305 309 zltlem1d ⊢φ∧d∈B∧k∈1…K∧¬k=1→1<k↔1≤k−1
321 319 320 mpbid ⊢φ∧d∈B∧k∈1…K∧¬k=1→1≤k−1
322 310 zred ⊢φ∧d∈B∧k∈1…K∧¬k=1→k−1∈ℝ
323 307 zred ⊢φ∧d∈B∧k∈1…K∧¬k=1→K∈ℝ
324 317 lem1d ⊢φ∧d∈B∧k∈1…K∧¬k=1→k−1≤k
325 300 271 syl ⊢φ∧d∈B∧k∈1…K→k≤K
326 325 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→k≤K
327 322 317 323 324 326 letrd ⊢φ∧d∈B∧k∈1…K∧¬k=1→k−1≤K
328 305 307 310 321 327 elfzd ⊢φ∧d∈B∧k∈1…K∧¬k=1→k−1∈1…K
329 304 328 ffvelcdmd ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k−1∈1…N+K
330 329 166 syl ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k−1∈ℕ
331 330 nnzd ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k−1∈ℤ
332 303 331 zsubcld ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k−d⁡k−1∈ℤ
333 292 293 299 332 ifbothda ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1d⁡k−d⁡k−1∈ℤ
334 333 3expa ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1d⁡k−d⁡k−1∈ℤ
335 334 zcnd ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1d⁡k−d⁡k−1∈ℂ
336 258 adantr ⊢φ∧d∈B∧k∈1…K→1∈ℂ
337 291 335 336 fsumsub ⊢φ∧d∈B→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1−1=∑k=1Kifk=1d⁡1d⁡k−d⁡k−1−∑k=1K1
338 simpr ⊢φ∧d∈B∧1=K→1=K
339 338 oveq2d ⊢φ∧d∈B∧1=K→1…1=1…K
340 339 eqcomd ⊢φ∧d∈B∧1=K→1…K=1…1
341 340 sumeq1d ⊢φ∧d∈B∧1=K→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=∑k=11ifk=1d⁡1d⁡k−d⁡k−1
342 1zzd ⊢φ∧d∈B→1∈ℤ
343 234 a1i ⊢φ∧d∈B→1=1
344 343 iftrued ⊢φ∧d∈B→if1=1d⁡1d⁡1−d⁡1−1=d⁡1
345 91 nncnd ⊢φ∧d∈B→d⁡1∈ℂ
346 344 345 eqeltrd ⊢φ∧d∈B→if1=1d⁡1d⁡1−d⁡1−1∈ℂ
347 eqeq1 ⊢k=1→k=1↔1=1
348 fveq2 ⊢k=1→d⁡k=d⁡1
349 fvoveq1 ⊢k=1→d⁡k−1=d⁡1−1
350 348 349 oveq12d ⊢k=1→d⁡k−d⁡k−1=d⁡1−d⁡1−1
351 347 350 ifbieq2d ⊢k=1→ifk=1d⁡1d⁡k−d⁡k−1=if1=1d⁡1d⁡1−d⁡1−1
352 351 fsum1 ⊢1∈ℤ∧if1=1d⁡1d⁡1−d⁡1−1∈ℂ→∑k=11ifk=1d⁡1d⁡k−d⁡k−1=if1=1d⁡1d⁡1−d⁡1−1
353 342 346 352 syl2anc ⊢φ∧d∈B→∑k=11ifk=1d⁡1d⁡k−d⁡k−1=if1=1d⁡1d⁡1−d⁡1−1
354 353 344 eqtrd ⊢φ∧d∈B→∑k=11ifk=1d⁡1d⁡k−d⁡k−1=d⁡1
355 354 adantr ⊢φ∧d∈B∧1=K→∑k=11ifk=1d⁡1d⁡k−d⁡k−1=d⁡1
356 fveq2 ⊢1=K→d⁡1=d⁡K
357 356 adantl ⊢φ∧d∈B∧1=K→d⁡1=d⁡K
358 341 355 357 3eqtrd ⊢φ∧d∈B∧1=K→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡K
359 2 3ad2ant1 ⊢φ∧d∈B∧1<K→K∈ℕ
360 nnuz ⊢ℕ=ℤ≥1
361 360 a1i ⊢φ∧d∈B∧1<K→ℕ=ℤ≥1
362 359 361 eleqtrd ⊢φ∧d∈B∧1<K→K∈ℤ≥1
363 335 3adantl3 ⊢φ∧d∈B∧1<K∧k∈1…K→ifk=1d⁡1d⁡k−d⁡k−1∈ℂ
364 iftrue ⊢k=1→ifk=1d⁡1d⁡k−d⁡k−1=d⁡1
365 362 363 364 fsum1p ⊢φ∧d∈B∧1<K→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡1+∑k=1+1Kifk=1d⁡1d⁡k−d⁡k−1
366 1red ⊢φ∧d∈B∧1<K∧k∈1+1…K→1∈ℝ
367 elfzle1 ⊢k∈1+1…K→1+1≤k
368 367 adantl ⊢φ∧d∈B∧1<K∧k∈1+1…K→1+1≤k
369 1zzd ⊢φ∧d∈B∧1<K∧k∈1+1…K→1∈ℤ
370 elfzelz ⊢k∈1+1…K→k∈ℤ
371 370 adantl ⊢φ∧d∈B∧1<K∧k∈1+1…K→k∈ℤ
372 369 371 zltp1led ⊢φ∧d∈B∧1<K∧k∈1+1…K→1<k↔1+1≤k
373 368 372 mpbird ⊢φ∧d∈B∧1<K∧k∈1+1…K→1<k
374 366 373 ltned ⊢φ∧d∈B∧1<K∧k∈1+1…K→1≠k
375 374 necomd ⊢φ∧d∈B∧1<K∧k∈1+1…K→k≠1
376 375 neneqd ⊢φ∧d∈B∧1<K∧k∈1+1…K→¬k=1
377 376 iffalsed ⊢φ∧d∈B∧1<K∧k∈1+1…K→ifk=1d⁡1d⁡k−d⁡k−1=d⁡k−d⁡k−1
378 377 sumeq2dv ⊢φ∧d∈B∧1<K→∑k=1+1Kifk=1d⁡1d⁡k−d⁡k−1=∑k=1+1Kd⁡k−d⁡k−1
379 378 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡1+∑k=1+1Kd⁡k−d⁡k−1
380 257 3adant3 ⊢φ∧d∈B∧1<K→K∈ℂ
381 1cnd ⊢φ∧d∈B∧1<K→1∈ℂ
382 380 381 npcand ⊢φ∧d∈B∧1<K→K-1+1=K
383 382 eqcomd ⊢φ∧d∈B∧1<K→K=K-1+1
384 383 oveq2d ⊢φ∧d∈B∧1<K→1+1…K=1+1…K-1+1
385 384 sumeq1d ⊢φ∧d∈B∧1<K→∑k=1+1Kd⁡k−d⁡k−1=∑k=1+1K-1+1d⁡k−d⁡k−1
386 385 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1Kd⁡k−d⁡k−1=d⁡1+∑k=1+1K-1+1d⁡k−d⁡k−1
387 elfzelz ⊢k∈1+1…K-1+1→k∈ℤ
388 387 adantl ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→k∈ℤ
389 388 zcnd ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→k∈ℂ
390 1cnd ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→1∈ℂ
391 389 390 npcand ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→k-1+1=k
392 391 eqcomd ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→k=k-1+1
393 392 fveq2d ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→d⁡k=d⁡k-1+1
394 393 oveq1d ⊢φ∧d∈B∧1<K∧k∈1+1…K-1+1→d⁡k−d⁡k−1=d⁡k-1+1−d⁡k−1
395 394 sumeq2dv ⊢φ∧d∈B∧1<K→∑k=1+1K-1+1d⁡k−d⁡k−1=∑k=1+1K-1+1d⁡k-1+1−d⁡k−1
396 395 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1K-1+1d⁡k−d⁡k−1=d⁡1+∑k=1+1K-1+1d⁡k-1+1−d⁡k−1
397 58 3adant3 ⊢φ∧d∈B∧1<K→1∈ℤ
398 61 3adant3 ⊢φ∧d∈B∧1<K→K∈ℤ
399 398 397 zsubcld ⊢φ∧d∈B∧1<K→K−1∈ℤ
400 56 3adant3 ⊢φ∧d∈B∧1<K→d:1…K⟶1…N+K
401 400 adantr ⊢φ∧d∈B∧1<K∧s∈1…K−1→d:1…K⟶1…N+K
402 1zzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→1∈ℤ
403 398 adantr ⊢φ∧d∈B∧1<K∧s∈1…K−1→K∈ℤ
404 elfznn ⊢s∈1…K−1→s∈ℕ
405 404 adantl ⊢φ∧d∈B∧1<K∧s∈1…K−1→s∈ℕ
406 405 nnzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→s∈ℤ
407 406 peano2zd ⊢φ∧d∈B∧1<K∧s∈1…K−1→s+1∈ℤ
408 1red ⊢φ∧d∈B∧1<K∧s∈1…K−1→1∈ℝ
409 405 nnred ⊢φ∧d∈B∧1<K∧s∈1…K−1→s∈ℝ
410 407 zred ⊢φ∧d∈B∧1<K∧s∈1…K−1→s+1∈ℝ
411 405 nnge1d ⊢φ∧d∈B∧1<K∧s∈1…K−1→1≤s
412 409 lep1d ⊢φ∧d∈B∧1<K∧s∈1…K−1→s≤s+1
413 408 409 410 411 412 letrd ⊢φ∧d∈B∧1<K∧s∈1…K−1→1≤s+1
414 elfzle2 ⊢s∈1…K−1→s≤K−1
415 414 adantl ⊢φ∧d∈B∧1<K∧s∈1…K−1→s≤K−1
416 403 zred ⊢φ∧d∈B∧1<K∧s∈1…K−1→K∈ℝ
417 leaddsub ⊢s∈ℝ∧1∈ℝ∧K∈ℝ→s+1≤K↔s≤K−1
418 409 408 416 417 syl3anc ⊢φ∧d∈B∧1<K∧s∈1…K−1→s+1≤K↔s≤K−1
419 415 418 mpbird ⊢φ∧d∈B∧1<K∧s∈1…K−1→s+1≤K
420 402 403 407 413 419 elfzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→s+1∈1…K
421 401 420 ffvelcdmd ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s+1∈1…N+K
422 elfznn ⊢d⁡s+1∈1…N+K→d⁡s+1∈ℕ
423 421 422 syl ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s+1∈ℕ
424 423 nnzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s+1∈ℤ
425 416 408 resubcld ⊢φ∧d∈B∧1<K∧s∈1…K−1→K−1∈ℝ
426 416 lem1d ⊢φ∧d∈B∧1<K∧s∈1…K−1→K−1≤K
427 409 425 416 415 426 letrd ⊢φ∧d∈B∧1<K∧s∈1…K−1→s≤K
428 402 403 406 411 427 elfzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→s∈1…K
429 401 ffvelcdmda ⊢φ∧d∈B∧1<K∧s∈1…K−1∧s∈1…K→d⁡s∈1…N+K
430 428 429 mpdan ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s∈1…N+K
431 elfznn ⊢d⁡s∈1…N+K→d⁡s∈ℕ
432 430 431 syl ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s∈ℕ
433 432 nnzd ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s∈ℤ
434 424 433 zsubcld ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s+1−d⁡s∈ℤ
435 434 zcnd ⊢φ∧d∈B∧1<K∧s∈1…K−1→d⁡s+1−d⁡s∈ℂ
436 fvoveq1 ⊢s=k−1→d⁡s+1=d⁡k-1+1
437 fveq2 ⊢s=k−1→d⁡s=d⁡k−1
438 436 437 oveq12d ⊢s=k−1→d⁡s+1−d⁡s=d⁡k-1+1−d⁡k−1
439 397 397 399 435 438 fsumshft ⊢φ∧d∈B∧1<K→∑s=1K−1d⁡s+1−d⁡s=∑k=1+1K-1+1d⁡k-1+1−d⁡k−1
440 439 eqcomd ⊢φ∧d∈B∧1<K→∑k=1+1K-1+1d⁡k-1+1−d⁡k−1=∑s=1K−1d⁡s+1−d⁡s
441 440 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1K-1+1d⁡k-1+1−d⁡k−1=d⁡1+∑s=1K−1d⁡s+1−d⁡s
442 fveq2 ⊢o=s→d⁡o=d⁡s
443 fveq2 ⊢o=s+1→d⁡o=d⁡s+1
444 fveq2 ⊢o=1→d⁡o=d⁡1
445 fveq2 ⊢o=K-1+1→d⁡o=d⁡K-1+1
446 382 362 eqeltrd ⊢φ∧d∈B∧1<K→K-1+1∈ℤ≥1
447 56 adantr ⊢φ∧d∈B∧1<K→d:1…K⟶1…N+K
448 447 3impa ⊢φ∧d∈B∧1<K→d:1…K⟶1…N+K
449 448 ffvelcdmda ⊢φ∧d∈B∧1<K∧o∈1…K→d⁡o∈1…N+K
450 449 ex ⊢φ∧d∈B∧1<K→o∈1…K→d⁡o∈1…N+K
451 382 oveq2d ⊢φ∧d∈B∧1<K→1…K-1+1=1…K
452 451 eleq2d ⊢φ∧d∈B∧1<K→o∈1…K-1+1↔o∈1…K
453 452 imbi1d ⊢φ∧d∈B∧1<K→o∈1…K-1+1→d⁡o∈1…N+K↔o∈1…K→d⁡o∈1…N+K
454 450 453 mpbird ⊢φ∧d∈B∧1<K→o∈1…K-1+1→d⁡o∈1…N+K
455 454 imp ⊢φ∧d∈B∧1<K∧o∈1…K-1+1→d⁡o∈1…N+K
456 elfznn ⊢d⁡o∈1…N+K→d⁡o∈ℕ
457 455 456 syl ⊢φ∧d∈B∧1<K∧o∈1…K-1+1→d⁡o∈ℕ
458 457 nncnd ⊢φ∧d∈B∧1<K∧o∈1…K-1+1→d⁡o∈ℂ
459 442 443 444 445 399 446 458 telfsum2 ⊢φ∧d∈B∧1<K→∑s=1K−1d⁡s+1−d⁡s=d⁡K-1+1−d⁡1
460 459 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+∑s=1K−1d⁡s+1−d⁡s=d⁡1+d⁡K-1+1-d⁡1
461 382 fveq2d ⊢φ∧d∈B∧1<K→d⁡K-1+1=d⁡K
462 461 oveq1d ⊢φ∧d∈B∧1<K→d⁡K-1+1−d⁡1=d⁡K−d⁡1
463 462 oveq2d ⊢φ∧d∈B∧1<K→d⁡1+d⁡K-1+1-d⁡1=d⁡1+d⁡K-d⁡1
464 345 3adant3 ⊢φ∧d∈B∧1<K→d⁡1∈ℂ
465 68 73 syl ⊢φ∧d∈B→d⁡K∈ℕ
466 465 nncnd ⊢φ∧d∈B→d⁡K∈ℂ
467 466 3adant3 ⊢φ∧d∈B∧1<K→d⁡K∈ℂ
468 464 467 pncan3d ⊢φ∧d∈B∧1<K→d⁡1+d⁡K-d⁡1=d⁡K
469 eqidd ⊢φ∧d∈B∧1<K→d⁡K=d⁡K
470 468 469 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+d⁡K-d⁡1=d⁡K
471 463 470 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+d⁡K-1+1-d⁡1=d⁡K
472 460 471 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+∑s=1K−1d⁡s+1−d⁡s=d⁡K
473 441 472 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1K-1+1d⁡k-1+1−d⁡k−1=d⁡K
474 396 473 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1K-1+1d⁡k−d⁡k−1=d⁡K
475 386 474 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1Kd⁡k−d⁡k−1=d⁡K
476 379 475 eqtrd ⊢φ∧d∈B∧1<K→d⁡1+∑k=1+1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡K
477 365 476 eqtrd ⊢φ∧d∈B∧1<K→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡K
478 477 3expa ⊢φ∧d∈B∧1<K→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡K
479 137 adantr ⊢φ∧d∈B→1∈ℝ
480 64 adantr ⊢φ∧d∈B→K∈ℝ
481 479 480 leloed ⊢φ∧d∈B→1≤K↔1<K∨1=K
482 63 481 mpbid ⊢φ∧d∈B→1<K∨1=K
483 482 orcomd ⊢φ∧d∈B→1=K∨1<K
484 358 478 483 mpjaodan ⊢φ∧d∈B→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1=d⁡K
485 fsumconst ⊢1…K∈Fin∧1∈ℂ→∑k=1K1=1…K⋅1
486 291 258 485 syl2anc ⊢φ∧d∈B→∑k=1K1=1…K⋅1
487 59 adantr ⊢φ∧d∈B→K∈ℕ0
488 hashfz1 ⊢K∈ℕ0→1…K=K
489 487 488 syl ⊢φ∧d∈B→1…K=K
490 489 oveq1d ⊢φ∧d∈B→1…K⋅1=K⋅1
491 257 mulridd ⊢φ∧d∈B→K⋅1=K
492 490 491 eqtrd ⊢φ∧d∈B→1…K⋅1=K
493 486 492 eqtrd ⊢φ∧d∈B→∑k=1K1=K
494 484 493 oveq12d ⊢φ∧d∈B→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1−∑k=1K1=d⁡K−K
495 337 494 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1d⁡k−d⁡k−1−1=d⁡K−K
496 290 495 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=d⁡K−K
497 466 257 subcld ⊢φ∧d∈B→d⁡K−K∈ℂ
498 497 addridd ⊢φ∧d∈B→d⁡K-K+0=d⁡K−K
499 498 eqcomd ⊢φ∧d∈B→d⁡K−K=d⁡K-K+0
500 0cnd ⊢φ∧d∈B→0∈ℂ
501 497 500 addcomd ⊢φ∧d∈B→d⁡K-K+0=0+d⁡K-K
502 499 501 eqtrd ⊢φ∧d∈B→d⁡K−K=0+d⁡K-K
503 496 502 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=0+d⁡K-K
504 500 257 466 subsub2d ⊢φ∧d∈B→0−K−d⁡K=0+d⁡K-K
505 504 eqcomd ⊢φ∧d∈B→0+d⁡K-K=0−K−d⁡K
506 503 505 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=0−K−d⁡K
507 1 nn0cnd ⊢φ→N∈ℂ
508 507 adantr ⊢φ∧d∈B→N∈ℂ
509 508 subidd ⊢φ∧d∈B→N−N=0
510 509 eqcomd ⊢φ∧d∈B→0=N−N
511 510 oveq1d ⊢φ∧d∈B→0−K−d⁡K=N-N-K−d⁡K
512 506 511 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N-N-K−d⁡K
513 257 466 subcld ⊢φ∧d∈B→K−d⁡K∈ℂ
514 508 508 513 subsub4d ⊢φ∧d∈B→N-N-K−d⁡K=N−N+K-d⁡K
515 512 514 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N−N+K-d⁡K
516 508 257 466 addsubassd ⊢φ∧d∈B→N+K-d⁡K=N+K-d⁡K
517 516 eqcomd ⊢φ∧d∈B→N+K-d⁡K=N+K-d⁡K
518 517 oveq2d ⊢φ∧d∈B→N−N+K-d⁡K=N−N+K-d⁡K
519 515 518 eqtrd ⊢φ∧d∈B→∑k=1Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N−N+K-d⁡K
520 278 519 eqtrd ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N−N+K-d⁡K
521 eleq1 ⊢d⁡1−1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡1−1∈ℤ↔ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
522 eleq1 ⊢d⁡k-d⁡k−1-1=ifk=1d⁡1−1d⁡k-d⁡k−1-1→d⁡k-d⁡k−1-1∈ℤ↔ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
523 1zzd ⊢φ∧d∈B∧k∈1…K→1∈ℤ
524 298 523 zsubcld ⊢φ∧d∈B∧k∈1…K→d⁡1−1∈ℤ
525 524 adantr ⊢φ∧d∈B∧k∈1…K∧k=1→d⁡1−1∈ℤ
526 523 adantr ⊢φ∧d∈B∧k∈1…K∧¬k=1→1∈ℤ
527 332 526 zsubcld ⊢φ∧d∈B∧k∈1…K∧¬k=1→d⁡k-d⁡k−1-1∈ℤ
528 521 522 525 527 ifbothda ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
529 528 3expa ⊢φ∧d∈B∧k∈1…K→ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
530 277 eleq1d ⊢φ∧d∈B∧k∈1…K→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ↔ifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
531 529 530 mpbird ⊢φ∧d∈B∧k∈1…K→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
532 291 531 fsumzcl ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℤ
533 532 zcnd ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈ℂ
534 508 257 addcld ⊢φ∧d∈B→N+K∈ℂ
535 534 466 subcld ⊢φ∧d∈B→N+K-d⁡K∈ℂ
536 533 535 508 addlsub ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+N+K-d⁡K=N↔∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N−N+K-d⁡K
537 520 536 mpbird ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+N+K-d⁡K=N
538 eqidd ⊢φ∧d∈B→N=N
539 537 538 eqtrd ⊢φ∧d∈B→∑k=1Kifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+N+K-d⁡K=N
540 264 539 eqtrd ⊢φ∧d∈B→∑k=1K+1-1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1+ifK+1=K+1N+K-d⁡KifK+1=1d⁡1−1d⁡K+1-d⁡K+1-1-1=N
541 256 540 eqtrd ⊢φ∧d∈B→∑k=1K+1ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=N
542 233 541 eqtrd ⊢φ∧d∈B→∑i=1K+1ifi=K+1N+K-d⁡Kifi=1d⁡1−1d⁡i-d⁡i−1-1=N
543 219 542 eqtrd ⊢φ∧d∈B→∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
544 201 543 jca ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0∧∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
545 ovex ⊢1…K+1∈V
546 545 mptex ⊢k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈V
547 feq1 ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→g:1…K+1⟶ℕ0↔k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0
548 simpl ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧i∈1…K+1→g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
549 548 fveq1d ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∧i∈1…K+1→g⁡i=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i
550 549 sumeq2dv ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→∑i=1K+1g⁡i=∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i
551 550 eqeq1d ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→∑i=1K+1g⁡i=N↔∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
552 547 551 anbi12d ⊢g=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1→g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N↔k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0∧∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
553 546 552 elab ⊢k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N↔k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0∧∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
554 553 a1i ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N↔k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1:1…K+1⟶ℕ0∧∑i=1K+1k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡i=N
555 544 554 mpbird ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N
556 5 a1i ⊢φ∧d∈B→A=g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N
557 556 eqcomd ⊢φ∧d∈B→g|g:1…K+1⟶ℕ0∧∑i=1K+1g⁡i=N=A
558 555 557 eleqtrd ⊢φ∧d∈B→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1∈A
559 291 mptexd ⊢φ∧d∈B→j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l∈V
560 34 40 558 559 fvmptd ⊢φ∧d∈B→F⁡k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l
561 eqidd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1
562 simpr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→k=l
563 562 eqeq1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→k=K+1↔l=K+1
564 562 eqeq1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→k=1↔l=1
565 562 fveq2d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→d⁡k=d⁡l
566 562 oveq1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→k−1=l−1
567 566 fveq2d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→d⁡k−1=d⁡l−1
568 565 567 oveq12d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→d⁡k−d⁡k−1=d⁡l−d⁡l−1
569 568 oveq1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→d⁡k-d⁡k−1-1=d⁡l-d⁡l−1-1
570 564 569 ifbieq2d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→ifk=1d⁡1−1d⁡k-d⁡k−1-1=ifl=1d⁡1−1d⁡l-d⁡l−1-1
571 563 570 ifbieq2d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧k=l→ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=ifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1
572 1zzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→1∈ℤ
573 60 3ad2ant1 ⊢φ∧d∈B∧j∈1…K→K∈ℤ
574 573 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K∈ℤ
575 574 peano2zd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K+1∈ℤ
576 elfzelz ⊢l∈1…j→l∈ℤ
577 576 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈ℤ
578 elfzle1 ⊢l∈1…j→1≤l
579 578 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j→1≤l
580 577 zred ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈ℝ
581 simp3 ⊢φ∧d∈B∧j∈1…K→j∈1…K
582 elfznn ⊢j∈1…K→j∈ℕ
583 581 582 syl ⊢φ∧d∈B∧j∈1…K→j∈ℕ
584 583 nnred ⊢φ∧d∈B∧j∈1…K→j∈ℝ
585 584 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→j∈ℝ
586 575 zred ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K+1∈ℝ
587 elfzle2 ⊢l∈1…j→l≤j
588 587 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l≤j
589 64 3ad2ant1 ⊢φ∧d∈B∧j∈1…K→K∈ℝ
590 1red ⊢φ∧d∈B∧j∈1…K→1∈ℝ
591 589 590 readdcld ⊢φ∧d∈B∧j∈1…K→K+1∈ℝ
592 elfzle2 ⊢j∈1…K→j≤K
593 581 592 syl ⊢φ∧d∈B∧j∈1…K→j≤K
594 589 lep1d ⊢φ∧d∈B∧j∈1…K→K≤K+1
595 584 589 591 593 594 letrd ⊢φ∧d∈B∧j∈1…K→j≤K+1
596 595 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→j≤K+1
597 580 585 586 588 596 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l≤K+1
598 572 575 577 579 597 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈1…K+1
599 ovexd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→N+K-d⁡K∈V
600 ovexd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d⁡1−1∈V
601 ovexd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d⁡l-d⁡l−1-1∈V
602 600 601 ifcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j→ifl=1d⁡1−1d⁡l-d⁡l−1-1∈V
603 599 602 ifcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j→ifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1∈V
604 561 571 598 603 fvmptd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=ifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1
605 604 sumeq2dv ⊢φ∧d∈B∧j∈1…K→∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=∑l=1jifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1
606 605 oveq2d ⊢φ∧d∈B∧j∈1…K→j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=j+∑l=1jifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1
607 elfznn ⊢l∈1…j→l∈ℕ
608 607 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈ℕ
609 608 nnred ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈ℝ
610 589 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K∈ℝ
611 1red ⊢φ∧d∈B∧j∈1…K∧l∈1…j→1∈ℝ
612 610 611 readdcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K+1∈ℝ
613 583 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→j∈ℕ
614 613 nnred ⊢φ∧d∈B∧j∈1…K∧l∈1…j→j∈ℝ
615 593 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→j≤K
616 609 614 610 588 615 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l≤K
617 610 ltp1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K<K+1
618 609 610 612 616 617 lelttrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l<K+1
619 609 618 ltned ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l≠K+1
620 619 neneqd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→¬l=K+1
621 620 iffalsed ⊢φ∧d∈B∧j∈1…K∧l∈1…j→ifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1=ifl=1d⁡1−1d⁡l-d⁡l−1-1
622 621 sumeq2dv ⊢φ∧d∈B∧j∈1…K→∑l=1jifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1=∑l=1jifl=1d⁡1−1d⁡l-d⁡l−1-1
623 622 oveq2d ⊢φ∧d∈B∧j∈1…K→j+∑l=1jifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1=j+∑l=1jifl=1d⁡1−1d⁡l-d⁡l−1-1
624 583 nnge1d ⊢φ∧d∈B∧j∈1…K→1≤j
625 57 3ad2ant1 ⊢φ∧d∈B∧j∈1…K→1∈ℤ
626 583 nnzd ⊢φ∧d∈B∧j∈1…K→j∈ℤ
627 eluz ⊢1∈ℤ∧j∈ℤ→j∈ℤ≥1↔1≤j
628 625 626 627 syl2anc ⊢φ∧d∈B∧j∈1…K→j∈ℤ≥1↔1≤j
629 624 628 mpbird ⊢φ∧d∈B∧j∈1…K→j∈ℤ≥1
630 eleq1 ⊢d⁡1−1=ifl=1d⁡1−1d⁡l-d⁡l−1-1→d⁡1−1∈ℂ↔ifl=1d⁡1−1d⁡l-d⁡l−1-1∈ℂ
631 eleq1 ⊢d⁡l-d⁡l−1-1=ifl=1d⁡1−1d⁡l-d⁡l−1-1→d⁡l-d⁡l−1-1∈ℂ↔ifl=1d⁡1−1d⁡l-d⁡l−1-1∈ℂ
632 56 3adant3 ⊢φ∧d∈B∧j∈1…K→d:1…K⟶1…N+K
633 simp1 ⊢φ∧d∈B∧j∈1…K→φ
634 633 62 syl ⊢φ∧d∈B∧j∈1…K→1≤K
635 633 60 syl ⊢φ∧d∈B∧j∈1…K→K∈ℤ
636 eluz ⊢1∈ℤ∧K∈ℤ→K∈ℤ≥1↔1≤K
637 625 635 636 syl2anc ⊢φ∧d∈B∧j∈1…K→K∈ℤ≥1↔1≤K
638 634 637 mpbird ⊢φ∧d∈B∧j∈1…K→K∈ℤ≥1
639 eluzfz1 ⊢K∈ℤ≥1→1∈1…K
640 638 639 syl ⊢φ∧d∈B∧j∈1…K→1∈1…K
641 632 640 ffvelcdmd ⊢φ∧d∈B∧j∈1…K→d⁡1∈1…N+K
642 641 90 syl ⊢φ∧d∈B∧j∈1…K→d⁡1∈ℕ
643 642 nnzd ⊢φ∧d∈B∧j∈1…K→d⁡1∈ℤ
644 643 625 zsubcld ⊢φ∧d∈B∧j∈1…K→d⁡1−1∈ℤ
645 644 zcnd ⊢φ∧d∈B∧j∈1…K→d⁡1−1∈ℂ
646 645 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d⁡1−1∈ℂ
647 646 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧l=1→d⁡1−1∈ℂ
648 632 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d:1…K⟶1…N+K
649 635 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j→K∈ℤ
650 608 nnzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈ℤ
651 608 nnge1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j→1≤l
652 572 649 650 651 616 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→l∈1…K
653 648 652 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d⁡l∈1…N+K
654 elfzelz ⊢d⁡l∈1…N+K→d⁡l∈ℤ
655 653 654 syl ⊢φ∧d∈B∧j∈1…K∧l∈1…j→d⁡l∈ℤ
656 655 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l∈ℤ
657 648 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d:1…K⟶1…N+K
658 1zzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1∈ℤ
659 649 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→K∈ℤ
660 650 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l∈ℤ
661 660 658 zsubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l−1∈ℤ
662 neqne ⊢¬l=1→l≠1
663 662 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l≠1
664 611 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1∈ℝ
665 609 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l∈ℝ
666 651 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1≤l
667 664 665 666 leltned ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1<l↔l≠1
668 663 667 mpbird ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1<l
669 658 660 zltlem1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1<l↔1≤l−1
670 668 669 mpbid ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→1≤l−1
671 661 zred ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l−1∈ℝ
672 610 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→K∈ℝ
673 665 lem1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l−1≤l
674 616 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l≤K
675 671 665 672 673 674 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l−1≤K
676 658 659 661 670 675 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→l−1∈1…K
677 657 676 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l−1∈1…N+K
678 elfzelz ⊢d⁡l−1∈1…N+K→d⁡l−1∈ℤ
679 677 678 syl ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l−1∈ℤ
680 656 679 zsubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l−d⁡l−1∈ℤ
681 680 658 zsubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l-d⁡l−1-1∈ℤ
682 681 zcnd ⊢φ∧d∈B∧j∈1…K∧l∈1…j∧¬l=1→d⁡l-d⁡l−1-1∈ℂ
683 630 631 647 682 ifbothda ⊢φ∧d∈B∧j∈1…K∧l∈1…j→ifl=1d⁡1−1d⁡l-d⁡l−1-1∈ℂ
684 iftrue ⊢l=1→ifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡1−1
685 629 683 684 fsum1p ⊢φ∧d∈B∧j∈1…K→∑l=1jifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡1-1+∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1
686 685 oveq2d ⊢φ∧d∈B∧j∈1…K→j+∑l=1jifl=1d⁡1−1d⁡l-d⁡l−1-1=j+d⁡1−1+∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1
687 633 137 syl ⊢φ∧d∈B∧j∈1…K→1∈ℝ
688 687 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1∈ℝ
689 688 688 readdcld ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1+1∈ℝ
690 elfzelz ⊢l∈1+1…j→l∈ℤ
691 690 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l∈ℤ
692 691 zred ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l∈ℝ
693 688 ltp1d ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1<1+1
694 elfzle1 ⊢l∈1+1…j→1+1≤l
695 694 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1+1≤l
696 688 689 692 693 695 ltletrd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1<l
697 688 696 ltned ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1≠l
698 697 necomd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l≠1
699 698 neneqd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→¬l=1
700 699 iffalsed ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→ifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡l-d⁡l−1-1
701 700 sumeq2dv ⊢φ∧d∈B∧j∈1…K→∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1=∑l=1+1jd⁡l-d⁡l−1-1
702 701 oveq2d ⊢φ∧d∈B∧j∈1…K→d⁡1-1+∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡1-1+∑l=1+1jd⁡l-d⁡l−1-1
703 702 oveq2d ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1=j+d⁡1−1+∑l=1+1jd⁡l-d⁡l−1-1
704 fzfid ⊢φ∧d∈B∧j∈1…K→1+1…j∈Fin
705 632 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d:1…K⟶1…N+K
706 1zzd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1∈ℤ
707 635 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→K∈ℤ
708 688 689 693 ltled ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1≤1+1
709 688 689 692 708 695 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1≤l
710 584 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→j∈ℝ
711 589 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→K∈ℝ
712 elfzle2 ⊢l∈1+1…j→l≤j
713 712 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l≤j
714 593 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→j≤K
715 692 710 711 713 714 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l≤K
716 706 707 691 709 715 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l∈1…K
717 705 716 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l∈1…N+K
718 717 654 syl ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l∈ℤ
719 718 zcnd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l∈ℂ
720 691 706 zsubcld ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l−1∈ℤ
721 leaddsub ⊢1∈ℝ∧1∈ℝ∧l∈ℝ→1+1≤l↔1≤l−1
722 688 688 692 721 syl3anc ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1+1≤l↔1≤l−1
723 695 722 mpbid ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1≤l−1
724 692 688 resubcld ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l−1∈ℝ
725 692 lem1d ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l−1≤l
726 724 692 711 725 715 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l−1≤K
727 706 707 720 723 726 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l−1∈1…K
728 705 727 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l−1∈1…N+K
729 678 zcnd ⊢d⁡l−1∈1…N+K→d⁡l−1∈ℂ
730 728 729 syl ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l−1∈ℂ
731 719 730 subcld ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l−d⁡l−1∈ℂ
732 1cnd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→1∈ℂ
733 704 731 732 fsumsub ⊢φ∧d∈B∧j∈1…K→∑l=1+1jd⁡l-d⁡l−1-1=∑l=1+1jd⁡l−d⁡l−1−∑l=1+1j1
734 733 oveq2d ⊢φ∧d∈B∧j∈1…K→d⁡1-1+∑l=1+1jd⁡l-d⁡l−1-1=d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-∑l=1+1j1
735 734 oveq2d ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l-d⁡l−1-1=j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−∑l=1+1j1
736 1cnd ⊢φ∧d∈B∧j∈1…K→1∈ℂ
737 fsumconst ⊢1+1…j∈Fin∧1∈ℂ→∑l=1+1j1=1+1…j⋅1
738 704 736 737 syl2anc ⊢φ∧d∈B∧j∈1…K→∑l=1+1j1=1+1…j⋅1
739 hashfzp1 ⊢j∈ℤ≥1→1+1…j=j−1
740 629 739 syl ⊢φ∧d∈B∧j∈1…K→1+1…j=j−1
741 740 oveq1d ⊢φ∧d∈B∧j∈1…K→1+1…j⋅1=j−1⋅1
742 583 nncnd ⊢φ∧d∈B∧j∈1…K→j∈ℂ
743 742 736 subcld ⊢φ∧d∈B∧j∈1…K→j−1∈ℂ
744 743 mulridd ⊢φ∧d∈B∧j∈1…K→j−1⋅1=j−1
745 741 744 eqtrd ⊢φ∧d∈B∧j∈1…K→1+1…j⋅1=j−1
746 738 745 eqtrd ⊢φ∧d∈B∧j∈1…K→∑l=1+1j1=j−1
747 746 oveq2d ⊢φ∧d∈B∧j∈1…K→∑l=1+1jd⁡l−d⁡l−1−∑l=1+1j1=∑l=1+1jd⁡l−d⁡l−1−j−1
748 747 oveq2d ⊢φ∧d∈B∧j∈1…K→d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-∑l=1+1j1=d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-j−1
749 748 oveq2d ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−∑l=1+1j1=j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−j−1
750 704 731 fsumcl ⊢φ∧d∈B∧j∈1…K→∑l=1+1jd⁡l−d⁡l−1∈ℂ
751 645 750 743 addsubassd ⊢φ∧d∈B∧j∈1…K→d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-j−1=d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-j−1
752 751 eqcomd ⊢φ∧d∈B∧j∈1…K→d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-j−1=d⁡1−1+∑l=1+1jd⁡l−d⁡l−1-j−1
753 752 oveq2d ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−j−1=j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1
754 645 750 addcld ⊢φ∧d∈B∧j∈1…K→d⁡1-1+∑l=1+1jd⁡l−d⁡l−1∈ℂ
755 742 754 743 addsubassd ⊢φ∧d∈B∧j∈1…K→j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1=j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1
756 755 eqcomd ⊢φ∧d∈B∧j∈1…K→j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1=j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1
757 742 754 743 addsubd ⊢φ∧d∈B∧j∈1…K→j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1=j−j−1+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1
758 742 736 nncand ⊢φ∧d∈B∧j∈1…K→j−j−1=1
759 1zzd ⊢φ∧d∈B∧j∈1…K→1∈ℤ
760 626 625 zsubcld ⊢φ∧d∈B∧j∈1…K→j−1∈ℤ
761 632 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d:1…K⟶1…N+K
762 1zzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→1∈ℤ
763 635 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→K∈ℤ
764 elfzelz ⊢l∈1…j−1→l∈ℤ
765 764 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l∈ℤ
766 765 peano2zd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l+1∈ℤ
767 1red ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→1∈ℝ
768 765 zred ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l∈ℝ
769 768 767 readdcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l+1∈ℝ
770 elfzle1 ⊢l∈1…j−1→1≤l
771 770 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→1≤l
772 768 lep1d ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l≤l+1
773 767 768 769 771 772 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→1≤l+1
774 584 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→j∈ℝ
775 774 767 resubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→j−1∈ℝ
776 589 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→K∈ℝ
777 776 767 resubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→K−1∈ℝ
778 elfzle2 ⊢l∈1…j−1→l≤j−1
779 778 adantl ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l≤j−1
780 593 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→j≤K
781 774 776 767 780 lesub1dd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→j−1≤K−1
782 768 775 777 779 781 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l≤K−1
783 leaddsub ⊢l∈ℝ∧1∈ℝ∧K∈ℝ→l+1≤K↔l≤K−1
784 768 767 776 783 syl3anc ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l+1≤K↔l≤K−1
785 782 784 mpbird ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l+1≤K
786 762 763 766 773 785 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l+1∈1…K
787 761 786 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l+1∈1…N+K
788 elfzelz ⊢d⁡l+1∈1…N+K→d⁡l+1∈ℤ
789 787 788 syl ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l+1∈ℤ
790 584 687 resubcld ⊢φ∧d∈B∧j∈1…K→j−1∈ℝ
791 584 lem1d ⊢φ∧d∈B∧j∈1…K→j−1≤j
792 790 584 589 791 593 letrd ⊢φ∧d∈B∧j∈1…K→j−1≤K
793 792 adantr ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→j−1≤K
794 768 775 776 779 793 letrd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l≤K
795 762 763 765 771 794 elfzd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→l∈1…K
796 761 795 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l∈1…N+K
797 796 654 syl ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l∈ℤ
798 789 797 zsubcld ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l+1−d⁡l∈ℤ
799 798 zcnd ⊢φ∧d∈B∧j∈1…K∧l∈1…j−1→d⁡l+1−d⁡l∈ℂ
800 fvoveq1 ⊢l=w−1→d⁡l+1=d⁡w-1+1
801 fveq2 ⊢l=w−1→d⁡l=d⁡w−1
802 800 801 oveq12d ⊢l=w−1→d⁡l+1−d⁡l=d⁡w-1+1−d⁡w−1
803 759 759 760 799 802 fsumshft ⊢φ∧d∈B∧j∈1…K→∑l=1j−1d⁡l+1−d⁡l=∑w=1+1j-1+1d⁡w-1+1−d⁡w−1
804 oveq1 ⊢w=l→w−1=l−1
805 804 fvoveq1d ⊢w=l→d⁡w-1+1=d⁡l-1+1
806 804 fveq2d ⊢w=l→d⁡w−1=d⁡l−1
807 805 806 oveq12d ⊢w=l→d⁡w-1+1−d⁡w−1=d⁡l-1+1−d⁡l−1
808 nfcv ⊢Ⅎ_l1+1…j-1+1
809 nfcv ⊢Ⅎ_w1+1…j-1+1
810 nfcv ⊢Ⅎ_ld⁡w-1+1−d⁡w−1
811 nfcv ⊢Ⅎ_wd⁡l-1+1−d⁡l−1
812 807 808 809 810 811 cbvsum ⊢∑w=1+1j-1+1d⁡w-1+1−d⁡w−1=∑l=1+1j-1+1d⁡l-1+1−d⁡l−1
813 812 a1i ⊢φ∧d∈B∧j∈1…K→∑w=1+1j-1+1d⁡w-1+1−d⁡w−1=∑l=1+1j-1+1d⁡l-1+1−d⁡l−1
814 803 813 eqtrd ⊢φ∧d∈B∧j∈1…K→∑l=1j−1d⁡l+1−d⁡l=∑l=1+1j-1+1d⁡l-1+1−d⁡l−1
815 742 736 npcand ⊢φ∧d∈B∧j∈1…K→j-1+1=j
816 815 oveq2d ⊢φ∧d∈B∧j∈1…K→1+1…j-1+1=1+1…j
817 816 sumeq1d ⊢φ∧d∈B∧j∈1…K→∑l=1+1j-1+1d⁡l-1+1−d⁡l−1=∑l=1+1jd⁡l-1+1−d⁡l−1
818 692 recnd ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l∈ℂ
819 818 732 npcand ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→l-1+1=l
820 819 fveq2d ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l-1+1=d⁡l
821 820 oveq1d ⊢φ∧d∈B∧j∈1…K∧l∈1+1…j→d⁡l-1+1−d⁡l−1=d⁡l−d⁡l−1
822 821 sumeq2dv ⊢φ∧d∈B∧j∈1…K→∑l=1+1jd⁡l-1+1−d⁡l−1=∑l=1+1jd⁡l−d⁡l−1
823 817 822 eqtrd ⊢φ∧d∈B∧j∈1…K→∑l=1+1j-1+1d⁡l-1+1−d⁡l−1=∑l=1+1jd⁡l−d⁡l−1
824 814 823 eqtrd ⊢φ∧d∈B∧j∈1…K→∑l=1j−1d⁡l+1−d⁡l=∑l=1+1jd⁡l−d⁡l−1
825 824 eqcomd ⊢φ∧d∈B∧j∈1…K→∑l=1+1jd⁡l−d⁡l−1=∑l=1j−1d⁡l+1−d⁡l
826 825 oveq2d ⊢φ∧d∈B∧j∈1…K→d⁡1-1+∑l=1+1jd⁡l−d⁡l−1=d⁡1-1+∑l=1j−1d⁡l+1−d⁡l
827 758 826 oveq12d ⊢φ∧d∈B∧j∈1…K→j−j−1+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1=1+d⁡1−1+∑l=1j−1d⁡l+1−d⁡l
828 fveq2 ⊢r=l→d⁡r=d⁡l
829 fveq2 ⊢r=l+1→d⁡r=d⁡l+1
830 fveq2 ⊢r=1→d⁡r=d⁡1
831 fveq2 ⊢r=j-1+1→d⁡r=d⁡j-1+1
832 815 629 eqeltrd ⊢φ∧d∈B∧j∈1…K→j-1+1∈ℤ≥1
833 632 adantr ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→d:1…K⟶1…N+K
834 1zzd ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→1∈ℤ
835 635 adantr ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→K∈ℤ
836 elfzelz ⊢r∈1…j-1+1→r∈ℤ
837 836 adantl ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→r∈ℤ
838 elfzle1 ⊢r∈1…j-1+1→1≤r
839 838 adantl ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→1≤r
840 837 zred ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→r∈ℝ
841 584 adantr ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→j∈ℝ
842 1red ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→1∈ℝ
843 841 842 resubcld ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→j−1∈ℝ
844 843 842 readdcld ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→j-1+1∈ℝ
845 589 adantr ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→K∈ℝ
846 elfzle2 ⊢r∈1…j-1+1→r≤j-1+1
847 846 adantl ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→r≤j-1+1
848 815 593 eqbrtrd ⊢φ∧d∈B∧j∈1…K→j-1+1≤K
849 848 adantr ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→j-1+1≤K
850 840 844 845 847 849 letrd ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→r≤K
851 834 835 837 839 850 elfzd ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→r∈1…K
852 833 851 ffvelcdmd ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→d⁡r∈1…N+K
853 elfzelz ⊢d⁡r∈1…N+K→d⁡r∈ℤ
854 852 853 syl ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→d⁡r∈ℤ
855 854 zcnd ⊢φ∧d∈B∧j∈1…K∧r∈1…j-1+1→d⁡r∈ℂ
856 828 829 830 831 760 832 855 telfsum2 ⊢φ∧d∈B∧j∈1…K→∑l=1j−1d⁡l+1−d⁡l=d⁡j-1+1−d⁡1
857 856 oveq2d ⊢φ∧d∈B∧j∈1…K→d⁡1-1+∑l=1j−1d⁡l+1−d⁡l=d⁡1−1+d⁡j-1+1-d⁡1
858 857 oveq2d ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+∑l=1j−1d⁡l+1−d⁡l=1+d⁡1−1+d⁡j-1+1−d⁡1
859 815 fveq2d ⊢φ∧d∈B∧j∈1…K→d⁡j-1+1=d⁡j
860 632 581 ffvelcdmd ⊢φ∧d∈B∧j∈1…K→d⁡j∈1…N+K
861 elfzelz ⊢d⁡j∈1…N+K→d⁡j∈ℤ
862 860 861 syl ⊢φ∧d∈B∧j∈1…K→d⁡j∈ℤ
863 859 862 eqeltrd ⊢φ∧d∈B∧j∈1…K→d⁡j-1+1∈ℤ
864 863 zcnd ⊢φ∧d∈B∧j∈1…K→d⁡j-1+1∈ℂ
865 642 nnred ⊢φ∧d∈B∧j∈1…K→d⁡1∈ℝ
866 865 recnd ⊢φ∧d∈B∧j∈1…K→d⁡1∈ℂ
867 864 866 subcld ⊢φ∧d∈B∧j∈1…K→d⁡j-1+1−d⁡1∈ℂ
868 736 645 867 addassd ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+d⁡j-1+1−d⁡1=1+d⁡1−1+d⁡j-1+1−d⁡1
869 868 eqcomd ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+d⁡j-1+1−d⁡1=1+d⁡1−1+d⁡j-1+1−d⁡1
870 736 866 pncan3d ⊢φ∧d∈B∧j∈1…K→1+d⁡1-1=d⁡1
871 870 oveq1d ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+d⁡j-1+1−d⁡1=d⁡1+d⁡j-1+1-d⁡1
872 866 864 pncan3d ⊢φ∧d∈B∧j∈1…K→d⁡1+d⁡j-1+1-d⁡1=d⁡j-1+1
873 872 859 eqtrd ⊢φ∧d∈B∧j∈1…K→d⁡1+d⁡j-1+1-d⁡1=d⁡j
874 871 873 eqtrd ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+d⁡j-1+1−d⁡1=d⁡j
875 869 874 eqtrd ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+d⁡j-1+1−d⁡1=d⁡j
876 858 875 eqtrd ⊢φ∧d∈B∧j∈1…K→1+d⁡1−1+∑l=1j−1d⁡l+1−d⁡l=d⁡j
877 827 876 eqtrd ⊢φ∧d∈B∧j∈1…K→j−j−1+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1=d⁡j
878 757 877 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1=d⁡j
879 756 878 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1-1+∑l=1+1jd⁡l−d⁡l−1-j−1=d⁡j
880 753 879 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−j−1=d⁡j
881 749 880 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l−d⁡l−1−∑l=1+1j1=d⁡j
882 735 881 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jd⁡l-d⁡l−1-1=d⁡j
883 703 882 eqtrd ⊢φ∧d∈B∧j∈1…K→j+d⁡1−1+∑l=1+1jifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡j
884 686 883 eqtrd ⊢φ∧d∈B∧j∈1…K→j+∑l=1jifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡j
885 623 884 eqtrd ⊢φ∧d∈B∧j∈1…K→j+∑l=1jifl=K+1N+K-d⁡Kifl=1d⁡1−1d⁡l-d⁡l−1-1=d⁡j
886 606 885 eqtrd ⊢φ∧d∈B∧j∈1…K→j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=d⁡j
887 886 3expa ⊢φ∧d∈B∧j∈1…K→j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=d⁡j
888 887 mpteq2dva ⊢φ∧d∈B→j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=j∈1…K⟼d⁡j
889 nfcv ⊢Ⅎ_qd⁡j
890 nfcv ⊢Ⅎ_jd⁡q
891 fveq2 ⊢j=q→d⁡j=d⁡q
892 889 890 891 cbvmpt ⊢j∈1…K⟼d⁡j=q∈1…K⟼d⁡q
893 892 a1i ⊢φ∧d∈B→j∈1…K⟼d⁡j=q∈1…K⟼d⁡q
894 888 893 eqtrd ⊢φ∧d∈B→j∈1…K⟼j+∑l=1jk∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1⁡l=q∈1…K⟼d⁡q
895 560 894 eqtrd ⊢φ∧d∈B→F⁡k∈1…K+1⟼ifk=K+1N+K-d⁡Kifk=1d⁡1−1d⁡k-d⁡k−1-1=q∈1…K⟼d⁡q
896 33 895 eqtrd ⊢φ∧d∈B→F⁡G⁡d=q∈1…K⟼d⁡q
897 56 ffnd ⊢φ∧d∈B→dFn1…K
898 dffn5 ⊢dFn1…K↔d=q∈1…K⟼d⁡q
899 898 biimpi ⊢dFn1…K→d=q∈1…K⟼d⁡q
900 897 899 syl ⊢φ∧d∈B→d=q∈1…K⟼d⁡q
901 900 eqcomd ⊢φ∧d∈B→q∈1…K⟼d⁡q=d
902 896 901 eqtrd ⊢φ∧d∈B→F⁡G⁡d=d
903 902 ralrimiva ⊢φ→∀d∈BF⁡G⁡d=d