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 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 = 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 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 … 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 if i = K + 1 N + K - d ⁡ K if i = 1 d ⁡ 1 − 1 d ⁡ i - d ⁡ i − 1 - 1
229 nfcv ⊢ Ⅎ _ i if k = K + 1 N + K - d ⁡ K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1
230 227 228 229 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
231 230 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
232 eqid ⊢ 1 = 1
233 1p0e1 ⊢ 1 + 0 = 1
234 232 233 eqtr4i ⊢ 1 = 1 + 0
235 234 a1i ⊢ φ → 1 = 1 + 0
236 0le1 ⊢ 0 ≤ 1
237 236 a1i ⊢ φ → 0 ≤ 1
238 137 8 64 137 62 237 le2addd ⊢ φ → 1 + 0 ≤ K + 1
239 235 238 eqbrtrd ⊢ φ → 1 ≤ K + 1
240 60 peano2zd ⊢ φ → K + 1 ∈ ℤ
241 eluz ⊢ 1 ∈ ℤ ∧ K + 1 ∈ ℤ → K + 1 ∈ ℤ ≥ 1 ↔ 1 ≤ K + 1
242 57 240 241 syl2anc ⊢ φ → K + 1 ∈ ℤ ≥ 1 ↔ 1 ≤ K + 1
243 239 242 mpbird ⊢ φ → K + 1 ∈ ℤ ≥ 1
244 243 adantr ⊢ φ ∧ d ∈ B → K + 1 ∈ ℤ ≥ 1
245 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 ∈ ℂ
246 eqeq1 ⊢ k = K + 1 → k = K + 1 ↔ K + 1 = K + 1
247 eqeq1 ⊢ k = K + 1 → k = 1 ↔ K + 1 = 1
248 fveq2 ⊢ k = K + 1 → d ⁡ k = d ⁡ K + 1
249 fvoveq1 ⊢ k = K + 1 → d ⁡ k − 1 = d ⁡ K + 1 - 1
250 248 249 oveq12d ⊢ k = K + 1 → d ⁡ k − d ⁡ k − 1 = d ⁡ K + 1 − d ⁡ K + 1 - 1
251 250 oveq1d ⊢ k = K + 1 → d ⁡ k - d ⁡ k − 1 - 1 = d ⁡ K + 1 - d ⁡ K + 1 - 1 - 1
252 247 251 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
253 246 252 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
254 244 245 253 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
255 156 adantr ⊢ φ ∧ d ∈ B → K ∈ ℂ
256 1cnd ⊢ φ ∧ d ∈ B → 1 ∈ ℂ
257 255 256 pncand ⊢ φ ∧ d ∈ B → K + 1 - 1 = K
258 257 oveq2d ⊢ φ ∧ d ∈ B → 1 … K + 1 - 1 = 1 … K
259 258 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
260 eqidd ⊢ φ ∧ d ∈ B → K + 1 = K + 1
261 260 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
262 259 261 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
263 elfzelz ⊢ k ∈ 1 … K → k ∈ ℤ
264 263 adantl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ∈ ℤ
265 264 zred ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ∈ ℝ
266 64 ad2antrr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → K ∈ ℝ
267 1red ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ∈ ℝ
268 266 267 readdcld ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → K + 1 ∈ ℝ
269 elfzle2 ⊢ k ∈ 1 … K → k ≤ K
270 269 adantl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ≤ K
271 266 ltp1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → K < K + 1
272 265 266 268 270 271 lelttrd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k < K + 1
273 265 272 ltned ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ≠ K + 1
274 273 neneqd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → ¬ k = K + 1
275 274 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
276 275 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
277 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
278 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
279 simpr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → k = 1
280 279 iftrued ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
281 280 eqcomd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1
282 281 oveq1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 − 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1
283 simpr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → ¬ k = 1
284 283 iffalsed ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ k − d ⁡ k − 1
285 284 eqcomd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − d ⁡ k − 1 = if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1
286 285 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
287 277 278 282 286 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
288 287 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
289 fzfid ⊢ φ ∧ d ∈ B → 1 … K ∈ Fin
290 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 ∈ ℤ
291 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 ∈ ℤ
292 56 3adant3 ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d : 1 … K ⟶ 1 … N + K
293 88 3adant3 ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ∈ 1 … K
294 292 293 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d ⁡ 1 ∈ 1 … N + K
295 90 nnzd ⊢ d ⁡ 1 ∈ 1 … N + K → d ⁡ 1 ∈ ℤ
296 294 295 syl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d ⁡ 1 ∈ ℤ
297 296 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 ∈ ℤ
298 simp3 ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ∈ 1 … K
299 292 298 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d ⁡ k ∈ 1 … N + K
300 299 126 syl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d ⁡ k ∈ ℤ
301 300 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k ∈ ℤ
302 292 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d : 1 … K ⟶ 1 … N + K
303 1zzd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ∈ ℤ
304 61 3adant3 ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → K ∈ ℤ
305 304 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → K ∈ ℤ
306 264 3impa ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ∈ ℤ
307 306 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k ∈ ℤ
308 307 303 zsubcld ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k − 1 ∈ ℤ
309 elfzle1 ⊢ k ∈ 1 … K → 1 ≤ k
310 298 309 syl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ≤ k
311 310 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ≤ k
312 135 adantl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k ≠ 1
313 311 312 jca ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ≤ k ∧ k ≠ 1
314 1red ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ∈ ℝ
315 307 zred ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k ∈ ℝ
316 314 315 ltlend ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 < k ↔ 1 ≤ k ∧ k ≠ 1
317 313 316 mpbird ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 < k
318 303 307 zltlem1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 < k ↔ 1 ≤ k − 1
319 317 318 mpbid ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ≤ k − 1
320 308 zred ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k − 1 ∈ ℝ
321 305 zred ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → K ∈ ℝ
322 315 lem1d ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k − 1 ≤ k
323 298 269 syl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → k ≤ K
324 323 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k ≤ K
325 320 315 321 322 324 letrd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k − 1 ≤ K
326 303 305 308 319 325 elfzd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → k − 1 ∈ 1 … K
327 302 326 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − 1 ∈ 1 … N + K
328 327 166 syl ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − 1 ∈ ℕ
329 328 nnzd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − 1 ∈ ℤ
330 301 329 zsubcld ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k − d ⁡ k − 1 ∈ ℤ
331 290 291 297 330 ifbothda ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℤ
332 331 3expa ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℤ
333 332 zcnd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℂ
334 256 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ∈ ℂ
335 289 333 334 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
336 simpr ⊢ φ ∧ d ∈ B ∧ 1 = K → 1 = K
337 336 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 = K → 1 … 1 = 1 … K
338 337 eqcomd ⊢ φ ∧ d ∈ B ∧ 1 = K → 1 … K = 1 … 1
339 338 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
340 1zzd ⊢ φ ∧ d ∈ B → 1 ∈ ℤ
341 232 a1i ⊢ φ ∧ d ∈ B → 1 = 1
342 341 iftrued ⊢ φ ∧ d ∈ B → if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1 = d ⁡ 1
343 91 nncnd ⊢ φ ∧ d ∈ B → d ⁡ 1 ∈ ℂ
344 342 343 eqeltrd ⊢ φ ∧ d ∈ B → if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1 ∈ ℂ
345 eqeq1 ⊢ k = 1 → k = 1 ↔ 1 = 1
346 fveq2 ⊢ k = 1 → d ⁡ k = d ⁡ 1
347 fvoveq1 ⊢ k = 1 → d ⁡ k − 1 = d ⁡ 1 − 1
348 346 347 oveq12d ⊢ k = 1 → d ⁡ k − d ⁡ k − 1 = d ⁡ 1 − d ⁡ 1 − 1
349 345 348 ifbieq2d ⊢ k = 1 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = if 1 = 1 d ⁡ 1 d ⁡ 1 − d ⁡ 1 − 1
350 349 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
351 340 344 350 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
352 351 342 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
353 352 adantr ⊢ φ ∧ d ∈ B ∧ 1 = K → ∑ k = 1 1 if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
354 fveq2 ⊢ 1 = K → d ⁡ 1 = d ⁡ K
355 354 adantl ⊢ φ ∧ d ∈ B ∧ 1 = K → d ⁡ 1 = d ⁡ K
356 339 353 355 3eqtrd ⊢ φ ∧ d ∈ B ∧ 1 = K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
357 2 3ad2ant1 ⊢ φ ∧ d ∈ B ∧ 1 < K → K ∈ ℕ
358 nnuz ⊢ ℕ = ℤ ≥ 1
359 358 a1i ⊢ φ ∧ d ∈ B ∧ 1 < K → ℕ = ℤ ≥ 1
360 357 359 eleqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → K ∈ ℤ ≥ 1
361 333 3adantl3 ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 ∈ ℂ
362 iftrue ⊢ k = 1 → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ 1
363 360 361 362 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
364 1red ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 ∈ ℝ
365 elfzle1 ⊢ k ∈ 1 + 1 … K → 1 + 1 ≤ k
366 365 adantl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 + 1 ≤ k
367 1zzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 ∈ ℤ
368 elfzelz ⊢ k ∈ 1 + 1 … K → k ∈ ℤ
369 368 adantl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → k ∈ ℤ
370 367 369 zltp1led ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 < k ↔ 1 + 1 ≤ k
371 366 370 mpbird ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 < k
372 364 371 ltned ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → 1 ≠ k
373 372 necomd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → k ≠ 1
374 373 neneqd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → ¬ k = 1
375 374 iffalsed ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K → if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ k − d ⁡ k − 1
376 375 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
377 376 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
378 255 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → K ∈ ℂ
379 1cnd ⊢ φ ∧ d ∈ B ∧ 1 < K → 1 ∈ ℂ
380 378 379 npcand ⊢ φ ∧ d ∈ B ∧ 1 < K → K - 1 + 1 = K
381 380 eqcomd ⊢ φ ∧ d ∈ B ∧ 1 < K → K = K - 1 + 1
382 381 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → 1 + 1 … K = 1 + 1 … K - 1 + 1
383 382 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
384 383 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
385 elfzelz ⊢ k ∈ 1 + 1 … K - 1 + 1 → k ∈ ℤ
386 385 adantl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → k ∈ ℤ
387 386 zcnd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → k ∈ ℂ
388 1cnd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → 1 ∈ ℂ
389 387 388 npcand ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → k - 1 + 1 = k
390 389 eqcomd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → k = k - 1 + 1
391 390 fveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → d ⁡ k = d ⁡ k - 1 + 1
392 391 oveq1d ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ k ∈ 1 + 1 … K - 1 + 1 → d ⁡ k − d ⁡ k − 1 = d ⁡ k - 1 + 1 − d ⁡ k − 1
393 392 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
394 393 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
395 58 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → 1 ∈ ℤ
396 61 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → K ∈ ℤ
397 396 395 zsubcld ⊢ φ ∧ d ∈ B ∧ 1 < K → K − 1 ∈ ℤ
398 56 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → d : 1 … K ⟶ 1 … N + K
399 398 adantr ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d : 1 … K ⟶ 1 … N + K
400 1zzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → 1 ∈ ℤ
401 396 adantr ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → K ∈ ℤ
402 elfznn ⊢ s ∈ 1 … K − 1 → s ∈ ℕ
403 402 adantl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ∈ ℕ
404 403 nnzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ∈ ℤ
405 404 peano2zd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s + 1 ∈ ℤ
406 1red ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → 1 ∈ ℝ
407 403 nnred ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ∈ ℝ
408 405 zred ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s + 1 ∈ ℝ
409 403 nnge1d ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → 1 ≤ s
410 407 lep1d ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ≤ s + 1
411 406 407 408 409 410 letrd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → 1 ≤ s + 1
412 elfzle2 ⊢ s ∈ 1 … K − 1 → s ≤ K − 1
413 412 adantl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ≤ K − 1
414 401 zred ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → K ∈ ℝ
415 leaddsub ⊢ s ∈ ℝ ∧ 1 ∈ ℝ ∧ K ∈ ℝ → s + 1 ≤ K ↔ s ≤ K − 1
416 407 406 414 415 syl3anc ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s + 1 ≤ K ↔ s ≤ K − 1
417 413 416 mpbird ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s + 1 ≤ K
418 400 401 405 411 417 elfzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s + 1 ∈ 1 … K
419 399 418 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s + 1 ∈ 1 … N + K
420 elfznn ⊢ d ⁡ s + 1 ∈ 1 … N + K → d ⁡ s + 1 ∈ ℕ
421 419 420 syl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s + 1 ∈ ℕ
422 421 nnzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s + 1 ∈ ℤ
423 414 406 resubcld ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → K − 1 ∈ ℝ
424 414 lem1d ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → K − 1 ≤ K
425 407 423 414 413 424 letrd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ≤ K
426 400 401 404 409 425 elfzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → s ∈ 1 … K
427 399 ffvelcdmda ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 ∧ s ∈ 1 … K → d ⁡ s ∈ 1 … N + K
428 426 427 mpdan ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s ∈ 1 … N + K
429 elfznn ⊢ d ⁡ s ∈ 1 … N + K → d ⁡ s ∈ ℕ
430 428 429 syl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s ∈ ℕ
431 430 nnzd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s ∈ ℤ
432 422 431 zsubcld ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s + 1 − d ⁡ s ∈ ℤ
433 432 zcnd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ s ∈ 1 … K − 1 → d ⁡ s + 1 − d ⁡ s ∈ ℂ
434 fvoveq1 ⊢ s = k − 1 → d ⁡ s + 1 = d ⁡ k - 1 + 1
435 fveq2 ⊢ s = k − 1 → d ⁡ s = d ⁡ k − 1
436 434 435 oveq12d ⊢ s = k − 1 → d ⁡ s + 1 − d ⁡ s = d ⁡ k - 1 + 1 − d ⁡ k − 1
437 395 395 397 433 436 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
438 437 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
439 438 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
440 fveq2 ⊢ o = s → d ⁡ o = d ⁡ s
441 fveq2 ⊢ o = s + 1 → d ⁡ o = d ⁡ s + 1
442 fveq2 ⊢ o = 1 → d ⁡ o = d ⁡ 1
443 fveq2 ⊢ o = K - 1 + 1 → d ⁡ o = d ⁡ K - 1 + 1
444 380 360 eqeltrd ⊢ φ ∧ d ∈ B ∧ 1 < K → K - 1 + 1 ∈ ℤ ≥ 1
445 56 adantr ⊢ φ ∧ d ∈ B ∧ 1 < K → d : 1 … K ⟶ 1 … N + K
446 445 3impa ⊢ φ ∧ d ∈ B ∧ 1 < K → d : 1 … K ⟶ 1 … N + K
447 446 ffvelcdmda ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ o ∈ 1 … K → d ⁡ o ∈ 1 … N + K
448 447 ex ⊢ φ ∧ d ∈ B ∧ 1 < K → o ∈ 1 … K → d ⁡ o ∈ 1 … N + K
449 380 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → 1 … K - 1 + 1 = 1 … K
450 449 eleq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → o ∈ 1 … K - 1 + 1 ↔ o ∈ 1 … K
451 450 imbi1d ⊢ φ ∧ d ∈ B ∧ 1 < K → o ∈ 1 … K - 1 + 1 → d ⁡ o ∈ 1 … N + K ↔ o ∈ 1 … K → d ⁡ o ∈ 1 … N + K
452 448 451 mpbird ⊢ φ ∧ d ∈ B ∧ 1 < K → o ∈ 1 … K - 1 + 1 → d ⁡ o ∈ 1 … N + K
453 452 imp ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ o ∈ 1 … K - 1 + 1 → d ⁡ o ∈ 1 … N + K
454 elfznn ⊢ d ⁡ o ∈ 1 … N + K → d ⁡ o ∈ ℕ
455 453 454 syl ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ o ∈ 1 … K - 1 + 1 → d ⁡ o ∈ ℕ
456 455 nncnd ⊢ φ ∧ d ∈ B ∧ 1 < K ∧ o ∈ 1 … K - 1 + 1 → d ⁡ o ∈ ℂ
457 440 441 442 443 397 444 456 telfsum2 ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ s = 1 K − 1 d ⁡ s + 1 − d ⁡ s = d ⁡ K - 1 + 1 − d ⁡ 1
458 457 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ s = 1 K − 1 d ⁡ s + 1 − d ⁡ s = d ⁡ 1 + d ⁡ K - 1 + 1 - d ⁡ 1
459 380 fveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ K - 1 + 1 = d ⁡ K
460 459 oveq1d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ K - 1 + 1 − d ⁡ 1 = d ⁡ K − d ⁡ 1
461 460 oveq2d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + d ⁡ K - 1 + 1 - d ⁡ 1 = d ⁡ 1 + d ⁡ K - d ⁡ 1
462 343 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 ∈ ℂ
463 68 73 syl ⊢ φ ∧ d ∈ B → d ⁡ K ∈ ℕ
464 463 nncnd ⊢ φ ∧ d ∈ B → d ⁡ K ∈ ℂ
465 464 3adant3 ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ K ∈ ℂ
466 462 465 pncan3d ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + d ⁡ K - d ⁡ 1 = d ⁡ K
467 eqidd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ K = d ⁡ K
468 466 467 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + d ⁡ K - d ⁡ 1 = d ⁡ K
469 461 468 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + d ⁡ K - 1 + 1 - d ⁡ 1 = d ⁡ K
470 458 469 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ s = 1 K − 1 d ⁡ s + 1 − d ⁡ s = d ⁡ K
471 439 470 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k - 1 + 1 − d ⁡ k − 1 = d ⁡ K
472 394 471 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K - 1 + 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
473 384 472 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K d ⁡ k − d ⁡ k − 1 = d ⁡ K
474 377 473 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → d ⁡ 1 + ∑ k = 1 + 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
475 363 474 eqtrd ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
476 475 3expa ⊢ φ ∧ d ∈ B ∧ 1 < K → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
477 137 adantr ⊢ φ ∧ d ∈ B → 1 ∈ ℝ
478 64 adantr ⊢ φ ∧ d ∈ B → K ∈ ℝ
479 477 478 leloed ⊢ φ ∧ d ∈ B → 1 ≤ K ↔ 1 < K ∨ 1 = K
480 63 479 mpbid ⊢ φ ∧ d ∈ B → 1 < K ∨ 1 = K
481 480 orcomd ⊢ φ ∧ d ∈ B → 1 = K ∨ 1 < K
482 356 476 481 mpjaodan ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 = d ⁡ K
483 fsumconst ⊢ 1 … K ∈ Fin ∧ 1 ∈ ℂ → ∑ k = 1 K 1 = 1 … K ⋅ 1
484 289 256 483 syl2anc ⊢ φ ∧ d ∈ B → ∑ k = 1 K 1 = 1 … K ⋅ 1
485 59 adantr ⊢ φ ∧ d ∈ B → K ∈ ℕ 0
486 hashfz1 ⊢ K ∈ ℕ 0 → 1 … K = K
487 485 486 syl ⊢ φ ∧ d ∈ B → 1 … K = K
488 487 oveq1d ⊢ φ ∧ d ∈ B → 1 … K ⋅ 1 = K ⋅ 1
489 255 mulridd ⊢ φ ∧ d ∈ B → K ⋅ 1 = K
490 488 489 eqtrd ⊢ φ ∧ d ∈ B → 1 … K ⋅ 1 = K
491 484 490 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K 1 = K
492 482 491 oveq12d ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − ∑ k = 1 K 1 = d ⁡ K − K
493 335 492 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 d ⁡ k − d ⁡ k − 1 − 1 = d ⁡ K − K
494 288 493 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = d ⁡ K − K
495 464 255 subcld ⊢ φ ∧ d ∈ B → d ⁡ K − K ∈ ℂ
496 495 addridd ⊢ φ ∧ d ∈ B → d ⁡ K - K + 0 = d ⁡ K − K
497 496 eqcomd ⊢ φ ∧ d ∈ B → d ⁡ K − K = d ⁡ K - K + 0
498 0cnd ⊢ φ ∧ d ∈ B → 0 ∈ ℂ
499 495 498 addcomd ⊢ φ ∧ d ∈ B → d ⁡ K - K + 0 = 0 + d ⁡ K - K
500 497 499 eqtrd ⊢ φ ∧ d ∈ B → d ⁡ K − K = 0 + d ⁡ K - K
501 494 500 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = 0 + d ⁡ K - K
502 498 255 464 subsub2d ⊢ φ ∧ d ∈ B → 0 − K − d ⁡ K = 0 + d ⁡ K - K
503 502 eqcomd ⊢ φ ∧ d ∈ B → 0 + d ⁡ K - K = 0 − K − d ⁡ K
504 501 503 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = 0 − K − d ⁡ K
505 1 nn0cnd ⊢ φ → N ∈ ℂ
506 505 adantr ⊢ φ ∧ d ∈ B → N ∈ ℂ
507 506 subidd ⊢ φ ∧ d ∈ B → N − N = 0
508 507 eqcomd ⊢ φ ∧ d ∈ B → 0 = N − N
509 508 oveq1d ⊢ φ ∧ d ∈ B → 0 − K − d ⁡ K = N - N - K − d ⁡ K
510 504 509 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N - N - K − d ⁡ K
511 255 464 subcld ⊢ φ ∧ d ∈ B → K − d ⁡ K ∈ ℂ
512 506 506 511 subsub4d ⊢ φ ∧ d ∈ B → N - N - K − d ⁡ K = N − N + K - d ⁡ K
513 510 512 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N − N + K - d ⁡ K
514 506 255 464 addsubassd ⊢ φ ∧ d ∈ B → N + K - d ⁡ K = N + K - d ⁡ K
515 514 eqcomd ⊢ φ ∧ d ∈ B → N + K - d ⁡ K = N + K - d ⁡ K
516 515 oveq2d ⊢ φ ∧ d ∈ B → N − N + K - d ⁡ K = N − N + K - d ⁡ K
517 513 516 eqtrd ⊢ φ ∧ d ∈ B → ∑ k = 1 K if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 = N − N + K - d ⁡ K
518 276 517 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
519 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 ∈ ℤ
520 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 ∈ ℤ
521 1zzd ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → 1 ∈ ℤ
522 296 521 zsubcld ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → d ⁡ 1 − 1 ∈ ℤ
523 522 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ k = 1 → d ⁡ 1 − 1 ∈ ℤ
524 521 adantr ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → 1 ∈ ℤ
525 330 524 zsubcld ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K ∧ ¬ k = 1 → d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
526 519 520 523 525 ifbothda ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
527 526 3expa ⊢ φ ∧ d ∈ B ∧ k ∈ 1 … K → if k = 1 d ⁡ 1 − 1 d ⁡ k - d ⁡ k − 1 - 1 ∈ ℤ
528 275 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 ∈ ℤ
529 527 528 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 ∈ ℤ
530 289 529 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 ∈ ℤ
531 530 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 ∈ ℂ
532 506 255 addcld ⊢ φ ∧ d ∈ B → N + K ∈ ℂ
533 532 464 subcld ⊢ φ ∧ d ∈ B → N + K - d ⁡ K ∈ ℂ
534 531 533 506 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
535 518 534 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
536 eqidd ⊢ φ ∧ d ∈ B → N = N
537 535 536 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
538 262 537 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
539 254 538 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
540 231 539 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
541 219 540 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
542 201 541 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
543 ovex ⊢ 1 … K + 1 ∈ V
544 543 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
545 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
546 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
547 546 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
548 547 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
549 548 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
550 545 549 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
551 544 550 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
552 551 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
553 542 552 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
554 5 a1i ⊢ φ ∧ d ∈ B → A = g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N
555 554 eqcomd ⊢ φ ∧ d ∈ B → g | g : 1 … K + 1 ⟶ ℕ 0 ∧ ∑ i = 1 K + 1 g ⁡ i = N = A
556 553 555 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
557 289 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
558 34 40 556 557 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
559 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
560 simpr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → k = l
561 560 eqeq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → k = K + 1 ↔ l = K + 1
562 560 eqeq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → k = 1 ↔ l = 1
563 560 fveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → d ⁡ k = d ⁡ l
564 560 oveq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → k − 1 = l − 1
565 564 fveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → d ⁡ k − 1 = d ⁡ l − 1
566 563 565 oveq12d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → d ⁡ k − d ⁡ k − 1 = d ⁡ l − d ⁡ l − 1
567 566 oveq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ k = l → d ⁡ k - d ⁡ k − 1 - 1 = d ⁡ l - d ⁡ l − 1 - 1
568 562 567 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
569 561 568 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
570 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → 1 ∈ ℤ
571 60 3ad2ant1 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ∈ ℤ
572 571 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K ∈ ℤ
573 572 peano2zd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K + 1 ∈ ℤ
574 elfzelz ⊢ l ∈ 1 … j → l ∈ ℤ
575 574 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ ℤ
576 elfzle1 ⊢ l ∈ 1 … j → 1 ≤ l
577 576 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → 1 ≤ l
578 575 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ ℝ
579 simp3 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ 1 … K
580 elfznn ⊢ j ∈ 1 … K → j ∈ ℕ
581 579 580 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℕ
582 581 nnred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℝ
583 582 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → j ∈ ℝ
584 573 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K + 1 ∈ ℝ
585 elfzle2 ⊢ l ∈ 1 … j → l ≤ j
586 585 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ≤ j
587 64 3ad2ant1 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ∈ ℝ
588 1red ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℝ
589 587 588 readdcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K + 1 ∈ ℝ
590 elfzle2 ⊢ j ∈ 1 … K → j ≤ K
591 579 590 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ≤ K
592 587 lep1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ≤ K + 1
593 582 587 589 591 592 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ≤ K + 1
594 593 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → j ≤ K + 1
595 578 583 584 586 594 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ≤ K + 1
596 570 573 575 577 595 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ 1 … K + 1
597 ovexd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → N + K - d ⁡ K ∈ V
598 ovexd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d ⁡ 1 − 1 ∈ V
599 ovexd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d ⁡ l - d ⁡ l − 1 - 1 ∈ V
600 598 599 ifcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ V
601 597 600 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
602 559 569 596 601 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
603 602 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
604 603 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
605 elfznn ⊢ l ∈ 1 … j → l ∈ ℕ
606 605 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ ℕ
607 606 nnred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ ℝ
608 587 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K ∈ ℝ
609 1red ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → 1 ∈ ℝ
610 608 609 readdcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K + 1 ∈ ℝ
611 581 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → j ∈ ℕ
612 611 nnred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → j ∈ ℝ
613 591 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → j ≤ K
614 607 612 608 586 613 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ≤ K
615 608 ltp1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K < K + 1
616 607 608 610 614 615 lelttrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l < K + 1
617 607 616 ltned ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ≠ K + 1
618 617 neneqd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → ¬ l = K + 1
619 618 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
620 619 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
621 620 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
622 581 nnge1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ≤ j
623 57 3ad2ant1 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℤ
624 581 nnzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℤ
625 eluz ⊢ 1 ∈ ℤ ∧ j ∈ ℤ → j ∈ ℤ ≥ 1 ↔ 1 ≤ j
626 623 624 625 syl2anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℤ ≥ 1 ↔ 1 ≤ j
627 622 626 mpbird ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℤ ≥ 1
628 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 ∈ ℂ
629 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 ∈ ℂ
630 56 3adant3 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d : 1 … K ⟶ 1 … N + K
631 simp1 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → φ
632 631 62 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ≤ K
633 631 60 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ∈ ℤ
634 eluz ⊢ 1 ∈ ℤ ∧ K ∈ ℤ → K ∈ ℤ ≥ 1 ↔ 1 ≤ K
635 623 633 634 syl2anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ∈ ℤ ≥ 1 ↔ 1 ≤ K
636 632 635 mpbird ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → K ∈ ℤ ≥ 1
637 eluzfz1 ⊢ K ∈ ℤ ≥ 1 → 1 ∈ 1 … K
638 636 637 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ 1 … K
639 630 638 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 ∈ 1 … N + K
640 639 90 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 ∈ ℕ
641 640 nnzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 ∈ ℤ
642 641 623 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 − 1 ∈ ℤ
643 642 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 − 1 ∈ ℂ
644 643 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d ⁡ 1 − 1 ∈ ℂ
645 644 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ l = 1 → d ⁡ 1 − 1 ∈ ℂ
646 630 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d : 1 … K ⟶ 1 … N + K
647 633 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → K ∈ ℤ
648 606 nnzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ ℤ
649 606 nnge1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → 1 ≤ l
650 570 647 648 649 614 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → l ∈ 1 … K
651 646 650 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d ⁡ l ∈ 1 … N + K
652 elfzelz ⊢ d ⁡ l ∈ 1 … N + K → d ⁡ l ∈ ℤ
653 651 652 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → d ⁡ l ∈ ℤ
654 653 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l ∈ ℤ
655 646 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d : 1 … K ⟶ 1 … N + K
656 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 ∈ ℤ
657 647 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → K ∈ ℤ
658 648 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l ∈ ℤ
659 658 656 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l − 1 ∈ ℤ
660 neqne ⊢ ¬ l = 1 → l ≠ 1
661 660 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l ≠ 1
662 609 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 ∈ ℝ
663 607 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l ∈ ℝ
664 649 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 ≤ l
665 662 663 664 leltned ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 < l ↔ l ≠ 1
666 661 665 mpbird ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 < l
667 656 658 zltlem1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 < l ↔ 1 ≤ l − 1
668 666 667 mpbid ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → 1 ≤ l − 1
669 659 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l − 1 ∈ ℝ
670 608 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → K ∈ ℝ
671 663 lem1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l − 1 ≤ l
672 614 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l ≤ K
673 669 663 670 671 672 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l − 1 ≤ K
674 656 657 659 668 673 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → l − 1 ∈ 1 … K
675 655 674 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l − 1 ∈ 1 … N + K
676 elfzelz ⊢ d ⁡ l − 1 ∈ 1 … N + K → d ⁡ l − 1 ∈ ℤ
677 675 676 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l − 1 ∈ ℤ
678 654 677 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l − d ⁡ l − 1 ∈ ℤ
679 678 656 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l - d ⁡ l − 1 - 1 ∈ ℤ
680 679 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j ∧ ¬ l = 1 → d ⁡ l - d ⁡ l − 1 - 1 ∈ ℂ
681 628 629 645 680 ifbothda ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 ∈ ℂ
682 iftrue ⊢ l = 1 → if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ 1 − 1
683 627 681 682 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
684 683 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
685 631 137 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℝ
686 685 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ∈ ℝ
687 686 686 readdcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 + 1 ∈ ℝ
688 elfzelz ⊢ l ∈ 1 + 1 … j → l ∈ ℤ
689 688 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ∈ ℤ
690 689 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ∈ ℝ
691 686 ltp1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 < 1 + 1
692 elfzle1 ⊢ l ∈ 1 + 1 … j → 1 + 1 ≤ l
693 692 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 + 1 ≤ l
694 686 687 690 691 693 ltletrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 < l
695 686 694 ltned ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ≠ l
696 695 necomd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ≠ 1
697 696 neneqd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → ¬ l = 1
698 697 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
699 698 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
700 699 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
701 700 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
702 fzfid ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + 1 … j ∈ Fin
703 630 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d : 1 … K ⟶ 1 … N + K
704 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ∈ ℤ
705 633 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → K ∈ ℤ
706 686 687 691 ltled ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ≤ 1 + 1
707 686 687 690 706 693 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ≤ l
708 582 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → j ∈ ℝ
709 587 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → K ∈ ℝ
710 elfzle2 ⊢ l ∈ 1 + 1 … j → l ≤ j
711 710 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ≤ j
712 591 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → j ≤ K
713 690 708 709 711 712 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ≤ K
714 704 705 689 707 713 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ∈ 1 … K
715 703 714 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l ∈ 1 … N + K
716 715 652 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l ∈ ℤ
717 716 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l ∈ ℂ
718 689 704 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l − 1 ∈ ℤ
719 leaddsub ⊢ 1 ∈ ℝ ∧ 1 ∈ ℝ ∧ l ∈ ℝ → 1 + 1 ≤ l ↔ 1 ≤ l − 1
720 686 686 690 719 syl3anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 + 1 ≤ l ↔ 1 ≤ l − 1
721 693 720 mpbid ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ≤ l − 1
722 690 686 resubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l − 1 ∈ ℝ
723 690 lem1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l − 1 ≤ l
724 722 690 709 723 713 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l − 1 ≤ K
725 704 705 718 721 724 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l − 1 ∈ 1 … K
726 703 725 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l − 1 ∈ 1 … N + K
727 676 zcnd ⊢ d ⁡ l − 1 ∈ 1 … N + K → d ⁡ l − 1 ∈ ℂ
728 726 727 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l − 1 ∈ ℂ
729 717 728 subcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l − d ⁡ l − 1 ∈ ℂ
730 1cnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → 1 ∈ ℂ
731 702 729 730 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
732 731 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
733 732 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
734 1cnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℂ
735 fsumconst ⊢ 1 + 1 … j ∈ Fin ∧ 1 ∈ ℂ → ∑ l = 1 + 1 j 1 = 1 + 1 … j ⋅ 1
736 702 734 735 syl2anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j 1 = 1 + 1 … j ⋅ 1
737 hashfzp1 ⊢ j ∈ ℤ ≥ 1 → 1 + 1 … j = j − 1
738 627 737 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + 1 … j = j − 1
739 738 oveq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + 1 … j ⋅ 1 = j − 1 ⋅ 1
740 581 nncnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j ∈ ℂ
741 740 734 subcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ∈ ℂ
742 741 mulridd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ⋅ 1 = j − 1
743 739 742 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + 1 … j ⋅ 1 = j − 1
744 736 743 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j 1 = j − 1
745 744 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
746 745 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
747 746 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
748 702 729 fsumcl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 ∈ ℂ
749 643 748 741 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
750 749 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
751 750 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
752 643 748 addcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 ∈ ℂ
753 740 752 741 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
754 753 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
755 740 752 741 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
756 740 734 nncand ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − j − 1 = 1
757 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 ∈ ℤ
758 624 623 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ∈ ℤ
759 630 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d : 1 … K ⟶ 1 … N + K
760 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → 1 ∈ ℤ
761 633 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → K ∈ ℤ
762 elfzelz ⊢ l ∈ 1 … j − 1 → l ∈ ℤ
763 762 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ∈ ℤ
764 763 peano2zd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l + 1 ∈ ℤ
765 1red ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → 1 ∈ ℝ
766 763 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ∈ ℝ
767 766 765 readdcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l + 1 ∈ ℝ
768 elfzle1 ⊢ l ∈ 1 … j − 1 → 1 ≤ l
769 768 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → 1 ≤ l
770 766 lep1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ≤ l + 1
771 765 766 767 769 770 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → 1 ≤ l + 1
772 582 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → j ∈ ℝ
773 772 765 resubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → j − 1 ∈ ℝ
774 587 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → K ∈ ℝ
775 774 765 resubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → K − 1 ∈ ℝ
776 elfzle2 ⊢ l ∈ 1 … j − 1 → l ≤ j − 1
777 776 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ≤ j − 1
778 591 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → j ≤ K
779 772 774 765 778 lesub1dd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → j − 1 ≤ K − 1
780 766 773 775 777 779 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ≤ K − 1
781 leaddsub ⊢ l ∈ ℝ ∧ 1 ∈ ℝ ∧ K ∈ ℝ → l + 1 ≤ K ↔ l ≤ K − 1
782 766 765 774 781 syl3anc ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l + 1 ≤ K ↔ l ≤ K − 1
783 780 782 mpbird ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l + 1 ≤ K
784 760 761 764 771 783 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l + 1 ∈ 1 … K
785 759 784 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l + 1 ∈ 1 … N + K
786 elfzelz ⊢ d ⁡ l + 1 ∈ 1 … N + K → d ⁡ l + 1 ∈ ℤ
787 785 786 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l + 1 ∈ ℤ
788 582 685 resubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ∈ ℝ
789 582 lem1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ≤ j
790 788 582 587 789 591 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − 1 ≤ K
791 790 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → j − 1 ≤ K
792 766 773 774 777 791 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ≤ K
793 760 761 763 769 792 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → l ∈ 1 … K
794 759 793 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l ∈ 1 … N + K
795 794 652 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l ∈ ℤ
796 787 795 zsubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l + 1 − d ⁡ l ∈ ℤ
797 796 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 … j − 1 → d ⁡ l + 1 − d ⁡ l ∈ ℂ
798 fvoveq1 ⊢ l = w − 1 → d ⁡ l + 1 = d ⁡ w - 1 + 1
799 fveq2 ⊢ l = w − 1 → d ⁡ l = d ⁡ w − 1
800 798 799 oveq12d ⊢ l = w − 1 → d ⁡ l + 1 − d ⁡ l = d ⁡ w - 1 + 1 − d ⁡ w − 1
801 757 757 758 797 800 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
802 oveq1 ⊢ w = l → w − 1 = l − 1
803 802 fvoveq1d ⊢ w = l → d ⁡ w - 1 + 1 = d ⁡ l - 1 + 1
804 802 fveq2d ⊢ w = l → d ⁡ w − 1 = d ⁡ l − 1
805 803 804 oveq12d ⊢ w = l → d ⁡ w - 1 + 1 − d ⁡ w − 1 = d ⁡ l - 1 + 1 − d ⁡ l − 1
806 nfcv ⊢ Ⅎ _ l d ⁡ w - 1 + 1 − d ⁡ w − 1
807 nfcv ⊢ Ⅎ _ w d ⁡ l - 1 + 1 − d ⁡ l − 1
808 805 806 807 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
809 808 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
810 801 809 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
811 740 734 npcand ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j - 1 + 1 = j
812 811 oveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + 1 … j - 1 + 1 = 1 + 1 … j
813 812 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
814 690 recnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l ∈ ℂ
815 814 730 npcand ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → l - 1 + 1 = l
816 815 fveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l - 1 + 1 = d ⁡ l
817 816 oveq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ l ∈ 1 + 1 … j → d ⁡ l - 1 + 1 − d ⁡ l − 1 = d ⁡ l − d ⁡ l − 1
818 817 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
819 813 818 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
820 810 819 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l = ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1
821 820 eqcomd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l
822 821 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
823 756 822 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
824 fveq2 ⊢ r = l → d ⁡ r = d ⁡ l
825 fveq2 ⊢ r = l + 1 → d ⁡ r = d ⁡ l + 1
826 fveq2 ⊢ r = 1 → d ⁡ r = d ⁡ 1
827 fveq2 ⊢ r = j - 1 + 1 → d ⁡ r = d ⁡ j - 1 + 1
828 811 627 eqeltrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j - 1 + 1 ∈ ℤ ≥ 1
829 630 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → d : 1 … K ⟶ 1 … N + K
830 1zzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → 1 ∈ ℤ
831 633 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → K ∈ ℤ
832 elfzelz ⊢ r ∈ 1 … j - 1 + 1 → r ∈ ℤ
833 832 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → r ∈ ℤ
834 elfzle1 ⊢ r ∈ 1 … j - 1 + 1 → 1 ≤ r
835 834 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → 1 ≤ r
836 833 zred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → r ∈ ℝ
837 582 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → j ∈ ℝ
838 1red ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → 1 ∈ ℝ
839 837 838 resubcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → j − 1 ∈ ℝ
840 839 838 readdcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → j - 1 + 1 ∈ ℝ
841 587 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → K ∈ ℝ
842 elfzle2 ⊢ r ∈ 1 … j - 1 + 1 → r ≤ j - 1 + 1
843 842 adantl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → r ≤ j - 1 + 1
844 811 591 eqbrtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j - 1 + 1 ≤ K
845 844 adantr ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → j - 1 + 1 ≤ K
846 836 840 841 843 845 letrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → r ≤ K
847 830 831 833 835 846 elfzd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → r ∈ 1 … K
848 829 847 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → d ⁡ r ∈ 1 … N + K
849 elfzelz ⊢ d ⁡ r ∈ 1 … N + K → d ⁡ r ∈ ℤ
850 848 849 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → d ⁡ r ∈ ℤ
851 850 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K ∧ r ∈ 1 … j - 1 + 1 → d ⁡ r ∈ ℂ
852 824 825 826 827 758 828 851 telfsum2 ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l = d ⁡ j - 1 + 1 − d ⁡ 1
853 852 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
854 853 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
855 811 fveq2d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j - 1 + 1 = d ⁡ j
856 630 579 ffvelcdmd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j ∈ 1 … N + K
857 elfzelz ⊢ d ⁡ j ∈ 1 … N + K → d ⁡ j ∈ ℤ
858 856 857 syl ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j ∈ ℤ
859 855 858 eqeltrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j - 1 + 1 ∈ ℤ
860 859 zcnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j - 1 + 1 ∈ ℂ
861 640 nnred ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 ∈ ℝ
862 861 recnd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 ∈ ℂ
863 860 862 subcld ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ j - 1 + 1 − d ⁡ 1 ∈ ℂ
864 734 643 863 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
865 864 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
866 734 862 pncan3d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + d ⁡ 1 - 1 = d ⁡ 1
867 866 oveq1d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + d ⁡ 1 − 1 + d ⁡ j - 1 + 1 − d ⁡ 1 = d ⁡ 1 + d ⁡ j - 1 + 1 - d ⁡ 1
868 862 860 pncan3d ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 + d ⁡ j - 1 + 1 - d ⁡ 1 = d ⁡ j - 1 + 1
869 868 855 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → d ⁡ 1 + d ⁡ j - 1 + 1 - d ⁡ 1 = d ⁡ j
870 867 869 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + d ⁡ 1 − 1 + d ⁡ j - 1 + 1 − d ⁡ 1 = d ⁡ j
871 865 870 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + d ⁡ 1 − 1 + d ⁡ j - 1 + 1 − d ⁡ 1 = d ⁡ j
872 854 871 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → 1 + d ⁡ 1 − 1 + ∑ l = 1 j − 1 d ⁡ l + 1 − d ⁡ l = d ⁡ j
873 823 872 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j − j − 1 + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 = d ⁡ j
874 755 873 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ j
875 754 874 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 - 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 - j − 1 = d ⁡ j
876 751 875 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l − d ⁡ l − 1 − j − 1 = d ⁡ j
877 747 876 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
878 733 877 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + d ⁡ 1 − 1 + ∑ l = 1 + 1 j d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
879 701 878 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
880 684 879 eqtrd ⊢ φ ∧ d ∈ B ∧ j ∈ 1 … K → j + ∑ l = 1 j if l = 1 d ⁡ 1 − 1 d ⁡ l - d ⁡ l − 1 - 1 = d ⁡ j
881 621 880 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
882 604 881 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
883 882 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
884 883 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
885 nfcv ⊢ Ⅎ _ q d ⁡ j
886 nfcv ⊢ Ⅎ _ j d ⁡ q
887 fveq2 ⊢ j = q → d ⁡ j = d ⁡ q
888 885 886 887 cbvmpt ⊢ j ∈ 1 … K ⟼ d ⁡ j = q ∈ 1 … K ⟼ d ⁡ q
889 888 a1i ⊢ φ ∧ d ∈ B → j ∈ 1 … K ⟼ d ⁡ j = q ∈ 1 … K ⟼ d ⁡ q
890 884 889 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
891 558 890 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
892 33 891 eqtrd ⊢ φ ∧ d ∈ B → F ⁡ G ⁡ d = q ∈ 1 … K ⟼ d ⁡ q
893 56 ffnd ⊢ φ ∧ d ∈ B → d Fn 1 … K
894 dffn5 ⊢ d Fn 1 … K ↔ d = q ∈ 1 … K ⟼ d ⁡ q
895 894 biimpi ⊢ d Fn 1 … K → d = q ∈ 1 … K ⟼ d ⁡ q
896 893 895 syl ⊢ φ ∧ d ∈ B → d = q ∈ 1 … K ⟼ d ⁡ q
897 896 eqcomd ⊢ φ ∧ d ∈ B → q ∈ 1 … K ⟼ d ⁡ q = d
898 892 897 eqtrd ⊢ φ ∧ d ∈ B → F ⁡ G ⁡ d = d
899 898 ralrimiva ⊢ φ → ∀ d ∈ B F ⁡ G ⁡ d = d