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