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 = 1 j a ⁡ l
sticksstones12a.4 ⊢ G = b ∈ B ⟼ if K = 0 1 N k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1
sticksstones12a.5 ⊢ A = g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N
sticksstones12a.6 ⊢ B = f | f : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → f ⁡ x < f ⁡ y
Assertion sticksstones12a ⊢ φ → ∀ d ∈ B F ⁡ 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 = 1 j a ⁡ l
4 sticksstones12a.4 ⊢ G = b ∈ B ⟼ if K = 0 1 N k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1
5 sticksstones12a.5 ⊢ A = g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N
6 sticksstones12a.6 ⊢ B = f | f : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → f ⁡ x < f ⁡ y
7 4 a1i ⊢ φ ∧ d ∈ B → G = b ∈ B ⟼ if K = 0 1 N k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ 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 → if K = 0 1 N k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ 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 → if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
24 16 23 ifeq12d ⊢ b = d → if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
25 24 adantl ⊢ φ ∧ d ∈ B ∧ b = d → if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
26 25 adantr ⊢ φ ∧ d ∈ B ∧ b = d ∧ k ∈ 1 … K + 1 → if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
27 26 mpteq2dva ⊢ φ ∧ d ∈ B ∧ b = d → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
28 14 27 eqtrd ⊢ φ ∧ d ∈ B ∧ b = d → if K = 0 1 N k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - b ⁡ K if k = 1 b ⁡ 1 − 1 b ⁡ k - b ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ V
32 7 28 29 31 fvmptd ⊢ φ ∧ d ∈ B → G ⁡ d = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
33 32 fveq2d ⊢ φ ∧ d ∈ B → F ⁡ G ⁡ d = F ⁡ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
34 3 a1i ⊢ φ ∧ d ∈ B → F = a ∈ A ⟼ j ∈ 1 … K ⟼ j + ∑ l = 1 j a ⁡ l
35 simpll ⊢ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ j ∈ 1 … K ∧ l ∈ 1 … j → a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
36 35 fveq1d ⊢ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ j ∈ 1 … K ∧ l ∈ 1 … j → a ⁡ l = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
37 36 sumeq2dv ⊢ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ j ∈ 1 … K → ∑ l = 1 j a ⁡ l = ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
38 37 oveq2d ⊢ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ j ∈ 1 … K → j + ∑ l = 1 j a ⁡ l = j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
39 38 mpteq2dva ⊢ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → j ∈ 1 … K ⟼ j + ∑ l = 1 j a ⁡ l = j ∈ 1 … K ⟼ j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
40 39 adantl ⊢ φ ∧ d ∈ B ∧ a = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → j ∈ 1 … K ⟼ j + ∑ l = 1 j a ⁡ l = j ∈ 1 … K ⟼ j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
41 eleq1 ⊢ N + K - d ⁡ K = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → N + K - d ⁡ K ∈ ℕ 0 ↔ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0
42 eleq1 ⊢ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0 ↔ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0
43 6 eleq2i ⊢ d ∈ B ↔ d ∈ f | f : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < 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 … K x < y → f ⁡ x < f ⁡ y ↔ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → d ⁡ x < d ⁡ y
51 45 50 anbi12d ⊢ f = d → f : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → f ⁡ x < f ⁡ y ↔ d : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → d ⁡ x < d ⁡ y
52 44 51 elab ⊢ d ∈ f | f : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → f ⁡ x < f ⁡ y ↔ d : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → d ⁡ x < d ⁡ y
53 43 52 bitri ⊢ d ∈ B ↔ d : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → d ⁡ x < d ⁡ y
54 53 biimpi ⊢ d ∈ B → d : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < y → d ⁡ x < d ⁡ y
55 54 adantl ⊢ φ ∧ d ∈ B → d : 1 … K ⟶ 1 … N + K ∧ ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < 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 ffvelrnd ⊢ φ ∧ 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 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ 1 − 1 ∈ ℕ 0 ↔ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0
85 eleq1 ⊢ d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0 ↔ if k = 1 d ⁡ 1 − 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 … K x < y → d ⁡ x < d ⁡ y
176 175 ad3antrrr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K + 1 ∧ ¬ k = K + 1 ∧ ¬ k = 1 → ∀ x ∈ 1 … K ∀ y ∈ 1 … K x < 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 … K x < 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 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0
199 41 42 83 198 ifbothda ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K + 1 → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℕ 0
200 eqid ⊢ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
201 199 200 fmptd ⊢ φ ∧ d ∈ B → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0
202 eqidd ⊢ φ ∧ d ∈ B ∧ i ∈ 1 … K + 1 → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1
211 204 210 ifbieq2d ⊢ φ ∧ d ∈ B ∧ i ∈ 1 … K + 1 ∧ k = i → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ 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 → if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 ∈ V
217 213 216 ifcld ⊢ φ ∧ d ∈ B ∧ i ∈ 1 … K + 1 → if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 ∈ V
218 202 211 212 217 fvmptd ⊢ φ ∧ d ∈ B ∧ i ∈ 1 … K + 1 → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1
219 218 sumeq2dv ⊢ φ ∧ d ∈ B → ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = ∑ i = 1 K + 1 if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ 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 → if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
227 220 226 ifbieq2d ⊢ i = k → if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 = if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
228 nfcv ⊢ Ⅎ _ k 1 … K + 1
229 nfcv ⊢ Ⅎ _ i 1 … K + 1
230 nfcv ⊢ Ⅎ _ k if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1
231 nfcv ⊢ Ⅎ _ i if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
232 227 228 229 230 231 cbvsum ⊢ ∑ i = 1 K + 1 if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 = ∑ k = 1 K + 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
233 232 a1i ⊢ φ ∧ d ∈ B → ∑ i = 1 K + 1 if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 = ∑ k = 1 K + 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if K + 1 = 1 d ⁡ 1 − 1 d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1
255 248 254 ifbieq2d ⊢ k = K + 1 → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if K + 1 = K + 1 N + K - d ⁡ K if K + 1 = 1 d ⁡ 1 − 1 d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1
256 246 247 255 fsumm1 ⊢ φ ∧ d ∈ B → ∑ k = 1 K + 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = ∑ k = 1 K + 1 - 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + if K + 1 = K + 1 N + K - d ⁡ K if K + 1 = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K + 1 - 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
262 eqidd ⊢ φ ∧ d ∈ B → K + 1 = K + 1
263 262 iftrued ⊢ φ ∧ d ∈ B → if K + 1 = K + 1 N + K - d ⁡ K if K + 1 = 1 d ⁡ 1 − 1 d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1 = N + K - d ⁡ K
264 261 263 oveq12d ⊢ φ ∧ d ∈ B → ∑ k = 1 K + 1 - 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + if K + 1 = K + 1 N + K - d ⁡ K if K + 1 = 1 d ⁡ 1 − 1 d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1 = ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
278 277 sumeq2dv ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
279 eqeq1 ⊢ d ⁡ 1 − 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ 1 − 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1 ↔ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1
280 eqeq1 ⊢ d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1 ↔ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 d ⁡ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
283 282 eqcomd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1
284 283 oveq1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 − 1 = if k = 1 d ⁡ 1 d ⁡ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ k − d ⁡ k − 1
287 286 eqcomd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − d ⁡ k − 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1
288 287 oveq1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1
289 279 280 284 288 ifbothda ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1
290 289 sumeq2dv ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1
291 fzfid ⊢ φ ∧ d ∈ B → 1 … K ∈ Fin
292 eleq1 ⊢ d ⁡ 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 → d ⁡ 1 ∈ ℤ ↔ if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℤ
293 eleq1 ⊢ d ⁡ k − d ⁡ k − 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 → d ⁡ k − d ⁡ k − 1 ∈ ℤ ↔ if k = 1 d ⁡ 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℤ
334 333 3expa ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℤ
335 334 zcnd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℂ
336 258 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ∈ ℂ
337 291 335 336 fsumsub ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1 = ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − ∑ k = 1 K 1
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 = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1
342 1zzd ⊢ φ ∧ d ∈ B → 1 ∈ ℤ
343 234 a1i ⊢ φ ∧ d ∈ B → 1 = 1
344 343 iftrued ⊢ φ ∧ d ∈ B → if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1 = d ⁡ 1
345 91 nncnd ⊢ φ ∧ d ∈ B → d ⁡ 1 ∈ ℂ
346 344 345 eqeltrd ⊢ φ ∧ d ∈ B → if 1 = 1 d ⁡ 1 d ⁡ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1
352 351 fsum1 ⊢ 1 ∈ ℤ ∧ if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1 ∈ ℂ → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1
353 342 346 352 syl2anc ⊢ φ ∧ d ∈ B → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1
354 353 344 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
355 354 adantr ⊢ φ ∧ d ∈ B ∧ 1 = K → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 d ⁡ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℂ
364 iftrue ⊢ k = 1 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
365 362 363 364 fsum1p ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1 + ∑ k = 1 + 1 K if k = 1 d ⁡ 1 d ⁡ 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 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ k − d ⁡ k − 1
378 377 sumeq2dv ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 + 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = ∑ k = 1 + 1 K d ⁡ k − d ⁡ k − 1
379 378 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1 + ∑ k = 1 + 1 K d ⁡ 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 + 1 K d ⁡ k − d ⁡ k − 1 = ∑ k = 1 + 1 K - 1 + 1 d ⁡ k − d ⁡ k − 1
386 385 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K d ⁡ k − d ⁡ k − 1 = d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ 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 + 1 K - 1 + 1 d ⁡ k − d ⁡ k − 1 = ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1
396 395 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnda ⊢ φ ∧ 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 = 1 K − 1 d ⁡ s + 1 − d ⁡ s = ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1
440 439 eqcomd ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1 = ∑ s = 1 K − 1 d ⁡ s + 1 − d ⁡ s
441 440 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1 = d ⁡ 1 + ∑ s = 1 K − 1 d ⁡ 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 ffvelrnda ⊢ φ ∧ 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 = 1 K − 1 d ⁡ s + 1 − d ⁡ s = d ⁡ K - 1 + 1 − d ⁡ 1
460 459 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ s = 1 K − 1 d ⁡ 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 = 1 K − 1 d ⁡ s + 1 − d ⁡ s = d ⁡ K
473 441 472 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1 = d ⁡ K
474 396 473 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
475 386 474 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K d ⁡ k − d ⁡ k − 1 = d ⁡ K
476 379 475 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
477 365 476 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
478 477 3expa ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
485 fsumconst ⊢ 1 … K ∈ Fin ∧ 1 ∈ ℂ → ∑ k = 1 K 1 = 1 … K ⋅ 1
486 291 258 485 syl2anc ⊢ φ ∧ d ∈ B → ∑ k = 1 K 1 = 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 mulid1d ⊢ φ ∧ d ∈ B → K ⋅ 1 = K
492 490 491 eqtrd ⊢ φ ∧ d ∈ B → 1 … K ⋅ 1 = K
493 486 492 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K 1 = K
494 484 493 oveq12d ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − ∑ k = 1 K 1 = d ⁡ K − K
495 337 494 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1 = d ⁡ K − K
496 290 495 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = d ⁡ K − K
497 466 257 subcld ⊢ φ ∧ d ∈ B → d ⁡ K − K ∈ ℂ
498 497 addid1d ⊢ φ ∧ 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 = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N − N + K - d ⁡ K
520 278 519 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N − N + K - d ⁡ K
521 eleq1 ⊢ d ⁡ 1 − 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ 1 − 1 ∈ ℤ ↔ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
522 eleq1 ⊢ d ⁡ k - d ⁡ k − 1 - 1 = if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ ↔ if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
529 528 3expa ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
530 277 eleq1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ ↔ if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
531 529 530 mpbird ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
532 291 531 fsumzcl ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
533 532 zcnd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + N + K - d ⁡ K = N ↔ ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N − N + K - d ⁡ K
537 520 536 mpbird ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + N + K - d ⁡ K = N
538 eqidd ⊢ φ ∧ d ∈ B → N = N
539 537 538 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + N + K - d ⁡ K = N
540 264 539 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K + 1 - 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 + if K + 1 = K + 1 N + K - d ⁡ K if K + 1 = 1 d ⁡ 1 − 1 d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1 = N
541 256 540 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K + 1 if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N
542 233 541 eqtrd ⊢ φ ∧ d ∈ B → ∑ i = 1 K + 1 if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1 = N
543 219 542 eqtrd ⊢ φ ∧ d ∈ B → ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
544 201 543 jca ⊢ φ ∧ d ∈ B → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
545 ovex ⊢ 1 … K + 1 ∈ V
546 545 mptex ⊢ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ V
547 feq1 ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → g : 1 … K + 1 ⟶ ℕ 0 ↔ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0
548 simpl ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ i ∈ 1 … K + 1 → g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
549 548 fveq1d ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∧ i ∈ 1 … K + 1 → g ⁡ i = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i
550 549 sumeq2dv ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → ∑ i = 1 K + 1 g ⁡ i = ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i
551 550 eqeq1d ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → ∑ i = 1 K + 1 g ⁡ i = N ↔ ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
552 547 551 anbi12d ⊢ g = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 → g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N ↔ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
553 546 552 elab ⊢ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N ↔ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
554 553 a1i ⊢ φ ∧ d ∈ B → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N ↔ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ i = N
555 544 554 mpbird ⊢ φ ∧ d ∈ B → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N
556 5 a1i ⊢ φ ∧ d ∈ B → A = g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N
557 556 eqcomd ⊢ φ ∧ d ∈ B → g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N = A
558 555 557 eleqtrd ⊢ φ ∧ d ∈ B → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ A
559 291 mptexd ⊢ φ ∧ d ∈ B → j ∈ 1 … K ⟼ j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l ∈ V
560 34 40 558 559 fvmptd ⊢ φ ∧ d ∈ B → F ⁡ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = j ∈ 1 … K ⟼ j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l
561 eqidd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
571 563 570 ifbieq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ 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 → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ V
603 599 602 ifcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ V
604 561 571 598 603 fvmptd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
605 604 sumeq2dv ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = ∑ l = 1 j if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
606 605 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = j + ∑ l = 1 j if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ 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 → if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
622 621 sumeq2dv ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
623 622 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = j + ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ 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 = if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 → d ⁡ 1 − 1 ∈ ℂ ↔ if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ ℂ
631 eleq1 ⊢ d ⁡ l - d ⁡ l − 1 - 1 = if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 → d ⁡ l - d ⁡ l − 1 - 1 ∈ ℂ ↔ if l = 1 d ⁡ 1 − 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ ℂ
684 iftrue ⊢ l = 1 → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ 1 − 1
685 629 683 684 fsum1p ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ 1 - 1 + ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1
686 685 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ 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 → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ l - d ⁡ l − 1 - 1
701 700 sumeq2dv ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1
702 701 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1
703 702 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 + 1 j d ⁡ l - d ⁡ l − 1 - 1 = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − ∑ l = 1 + 1 j 1
734 733 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - ∑ l = 1 + 1 j 1
735 734 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1 = j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − ∑ l = 1 + 1 j 1
736 1cnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℂ
737 fsumconst ⊢ 1 + 1 … j ∈ Fin ∧ 1 ∈ ℂ → ∑ l = 1 + 1 j 1 = 1 + 1 … j ⋅ 1
738 704 736 737 syl2anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j 1 = 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 mulid1d ⊢ φ ∧ 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 + 1 j 1 = j − 1
747 746 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − ∑ l = 1 + 1 j 1 = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − j − 1
748 747 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - ∑ l = 1 + 1 j 1 = d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
749 748 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − ∑ l = 1 + 1 j 1 = j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − j − 1
750 704 731 fsumcl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 ∈ ℂ
751 645 750 743 addsubassd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
752 751 eqcomd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
753 752 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − j − 1 = j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
754 645 750 addcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 ∈ ℂ
755 742 754 743 addsubassd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
756 755 eqcomd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1
757 742 754 743 addsubd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = j − j − 1 + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 ffvelrnd ⊢ φ ∧ 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 = 1 j − 1 d ⁡ l + 1 − d ⁡ l = ∑ w = 1 + 1 j - 1 + 1 d ⁡ 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 ⊢ Ⅎ _ l 1 + 1 … j - 1 + 1
809 nfcv ⊢ Ⅎ _ w 1 + 1 … j - 1 + 1
810 nfcv ⊢ Ⅎ _ l d ⁡ w - 1 + 1 − d ⁡ w − 1
811 nfcv ⊢ Ⅎ _ w d ⁡ l - 1 + 1 − d ⁡ l − 1
812 807 808 809 810 811 cbvsum ⊢ ∑ w = 1 + 1 j - 1 + 1 d ⁡ w - 1 + 1 − d ⁡ w − 1 = ∑ l = 1 + 1 j - 1 + 1 d ⁡ l - 1 + 1 − d ⁡ l − 1
813 812 a1i ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ w = 1 + 1 j - 1 + 1 d ⁡ w - 1 + 1 − d ⁡ w − 1 = ∑ l = 1 + 1 j - 1 + 1 d ⁡ l - 1 + 1 − d ⁡ l − 1
814 803 813 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l = ∑ l = 1 + 1 j - 1 + 1 d ⁡ 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 + 1 j - 1 + 1 d ⁡ l - 1 + 1 − d ⁡ l − 1 = ∑ l = 1 + 1 j d ⁡ 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 + 1 j d ⁡ l - 1 + 1 − d ⁡ l − 1 = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1
823 817 822 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j - 1 + 1 d ⁡ l - 1 + 1 − d ⁡ l − 1 = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1
824 814 823 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1
825 824 eqcomd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l
826 825 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = d ⁡ 1 - 1 + ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l
827 758 826 oveq12d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − j − 1 + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = 1 + d ⁡ 1 − 1 + ∑ l = 1 j − 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 = 1 j − 1 d ⁡ l + 1 − d ⁡ l = d ⁡ j - 1 + 1 − d ⁡ 1
857 856 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 j − 1 d ⁡ 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 = 1 j − 1 d ⁡ 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 ffvelrnd ⊢ φ ∧ 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 = 1 j − 1 d ⁡ l + 1 − d ⁡ l = d ⁡ j
877 827 876 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − j − 1 + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = d ⁡ j
878 757 877 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ j
879 756 878 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ j
880 753 879 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − j − 1 = d ⁡ j
881 749 880 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − ∑ l = 1 + 1 j 1 = d ⁡ j
882 735 881 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
883 703 882 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
884 686 883 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
885 623 884 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j if l = K + 1 N + K - d ⁡ K if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
886 606 885 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = d ⁡ j
887 886 3expa ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = d ⁡ j
888 887 mpteq2dva ⊢ φ ∧ d ∈ B → j ∈ 1 … K ⟼ j + ∑ l = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = j ∈ 1 … K ⟼ d ⁡ j
889 nfcv ⊢ Ⅎ _ q d ⁡ j
890 nfcv ⊢ Ⅎ _ j d ⁡ 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 = 1 j k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ⁡ l = q ∈ 1 … K ⟼ d ⁡ q
895 560 894 eqtrd ⊢ φ ∧ d ∈ B → F ⁡ k ∈ 1 … K + 1 ⟼ if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ 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 → d Fn 1 … K
898 dffn5 ⊢ d Fn 1 … K ↔ d = q ∈ 1 … K ⟼ d ⁡ q
899 898 biimpi ⊢ d Fn 1 … 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 ∈ B F ⁡ G ⁡ d = d