Step | Hyp | Ref
| Expression |
1 | | sticksstones12.1 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | sticksstones12.2 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ ℕ) |
3 | 2 | nnnn0d 12276 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
4 | | sticksstones12.3 |
. . 3
⊢ 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)))) |
5 | | sticksstones12.5 |
. . 3
⊢ 𝐴 = {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} |
6 | | sticksstones12.6 |
. . 3
⊢ 𝐵 = {𝑓 ∣ (𝑓:(1...𝐾)⟶(1...(𝑁 + 𝐾)) ∧ ∀𝑥 ∈ (1...𝐾)∀𝑦 ∈ (1...𝐾)(𝑥 < 𝑦 → (𝑓‘𝑥) < (𝑓‘𝑦)))} |
7 | 1, 3, 4, 5, 6 | sticksstones8 40089 |
. 2
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
8 | | sticksstones12.4 |
. . 3
⊢ 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) |
9 | 1, 2, 8, 5, 6 | sticksstones10 40091 |
. 2
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
10 | 8 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1))))))) |
11 | | 0red 10962 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
12 | 2 | nngt0d 12005 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝐾) |
13 | 11, 12 | ltned 11094 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≠ 𝐾) |
14 | 13 | necomd 3000 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ≠ 0) |
15 | 14 | neneqd 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐾 = 0) |
16 | 15 | iffalsed 4475 |
. . . . . . . . 9
⊢ (𝜑 → if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))))) |
18 | 17 | mpteq2dva 5178 |
. . . . . . 7
⊢ (𝜑 → (𝑏 ∈ 𝐵 ↦ if(𝐾 = 0, {〈1, 𝑁〉}, (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))))) = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) |
19 | 10, 18 | eqtrd 2779 |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) |
20 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐺 = (𝑏 ∈ 𝐵 ↦ (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) −
1)))))) |
21 | | fveq1 6767 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘𝐾) = ((𝐹‘𝑐)‘𝐾)) |
22 | 21 | oveq2d 7284 |
. . . . . . . . 9
⊢ (𝑏 = (𝐹‘𝑐) → ((𝑁 + 𝐾) − (𝑏‘𝐾)) = ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾))) |
23 | | fveq1 6767 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘1) = ((𝐹‘𝑐)‘1)) |
24 | 23 | oveq1d 7283 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑐) → ((𝑏‘1) − 1) = (((𝐹‘𝑐)‘1) − 1)) |
25 | | fveq1 6767 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘𝑘) = ((𝐹‘𝑐)‘𝑘)) |
26 | | fveq1 6767 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝐹‘𝑐) → (𝑏‘(𝑘 − 1)) = ((𝐹‘𝑐)‘(𝑘 − 1))) |
27 | 25, 26 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝐹‘𝑐) → ((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) = (((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1)))) |
28 | 27 | oveq1d 7283 |
. . . . . . . . . 10
⊢ (𝑏 = (𝐹‘𝑐) → (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1) = ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)) |
29 | 24, 28 | ifeq12d 4485 |
. . . . . . . . 9
⊢ (𝑏 = (𝐹‘𝑐) → if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)) = if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))) |
30 | 22, 29 | ifeq12d 4485 |
. . . . . . . 8
⊢ (𝑏 = (𝐹‘𝑐) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝑏 = (𝐹‘𝑐) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1))) = if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) |
32 | 31 | mpteq2dva 5178 |
. . . . . 6
⊢ (𝑏 = (𝐹‘𝑐) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))))) |
33 | 32 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑏 = (𝐹‘𝑐)) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − (𝑏‘𝐾)), if(𝑘 = 1, ((𝑏‘1) − 1), (((𝑏‘𝑘) − (𝑏‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))))) |
34 | 7 | ffvelrnda 6955 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) ∈ 𝐵) |
35 | | fzfid 13674 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...(𝐾 + 1)) ∈ Fin) |
36 | 35 | mptexd 7094 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) ∈
V) |
37 | 20, 33, 34, 36 | fvmptd 6876 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))))) |
38 | 4 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))) |
39 | | simpllr 772 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐) |
40 | 39 | fveq1d 6770 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎‘𝑙) = (𝑐‘𝑙)) |
41 | 40 | sumeq2dv 15396 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) |
42 | 41 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) |
43 | 42 | mpteq2dva 5178 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
44 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ 𝐴) |
45 | | fzfid 13674 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...𝐾) ∈ Fin) |
46 | 45 | mptexd 7094 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) ∈ V) |
47 | 38, 43, 44, 46 | fvmptd 6876 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐹‘𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
48 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → 𝑗 = 𝐾) |
49 | 48 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → (1...𝑗) = (1...𝐾)) |
50 | 49 | sumeq1d 15394 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) |
51 | 48, 50 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 𝐾) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) |
52 | | 1zzd 12334 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ∈
ℤ) |
53 | 3 | nn0zd 12406 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℤ) |
54 | 2 | nnge1d 12004 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 1 ≤ 𝐾) |
55 | 2 | nnred 11971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℝ) |
56 | 55 | leidd 11524 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ≤ 𝐾) |
57 | 52, 53, 53, 54, 56 | elfzd 13229 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐾 ∈ (1...𝐾)) |
58 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ (1...𝐾)) |
59 | | ovexd 7303 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) ∈ V) |
60 | 47, 51, 58, 59 | fvmptd 6876 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐹‘𝑐)‘𝐾) = (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) |
61 | 60 | oveq2d 7284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)))) |
62 | 1 | nn0cnd 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℂ) |
63 | 62 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑁 ∈ ℂ) |
64 | 55 | recnd 10987 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℂ) |
65 | 64 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℂ) |
66 | 63, 65 | addcomd 11160 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑁 + 𝐾) = (𝐾 + 𝑁)) |
67 | 66 | oveq1d 7283 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)))) |
68 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ∈ ℤ) |
69 | 53 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℤ) |
70 | 69 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℤ) |
71 | | elfzelz 13238 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...𝐾) → 𝑙 ∈ ℤ) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℤ) |
73 | | elfzle1 13241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...𝐾) → 1 ≤ 𝑙) |
74 | 73 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 1 ≤ 𝑙) |
75 | 72 | zred 12408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ ℝ) |
76 | 55 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ∈ ℝ) |
77 | 70 | zred 12408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝐾 + 1) ∈ ℝ) |
78 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ (1...𝐾) → 𝑙 ≤ 𝐾) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ 𝐾) |
80 | 76 | lep1d 11889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝐾 ≤ (𝐾 + 1)) |
81 | 75, 76, 77, 79, 80 | letrd 11115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ≤ (𝐾 + 1)) |
82 | 68, 70, 72, 74, 81 | elfzd 13229 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑙 ∈ (1...(𝐾 + 1))) |
83 | 5 | eleq2i 2831 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ 𝐴 ↔ 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
84 | 83 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑐 ∈ 𝐴 → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)}) |
86 | | vex 3434 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑐 ∈ V |
87 | | feq1 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔 = 𝑐 → (𝑔:(1...(𝐾 + 1))⟶ℕ0 ↔
𝑐:(1...(𝐾 +
1))⟶ℕ0)) |
88 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → 𝑔 = 𝑐) |
89 | 88 | fveq1d 6770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑔 = 𝑐 ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝑔‘𝑖) = (𝑐‘𝑖)) |
90 | 89 | sumeq2dv 15396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑔 = 𝑐 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖)) |
91 | 90 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑔 = 𝑐 → (Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁 ↔ Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)) |
92 | 87, 91 | anbi12d 630 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑔 = 𝑐 → ((𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁) ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))) |
93 | 86, 92 | elab 3610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)) |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} ↔ (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))) |
95 | 94 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐 ∈ {𝑔 ∣ (𝑔:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑔‘𝑖) = 𝑁)} → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁))) |
96 | 85, 95 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐:(1...(𝐾 + 1))⟶ℕ0 ∧
Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁)) |
97 | 96 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
98 | 97 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
99 | 98 | ffvelrnda 6955 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈
ℕ0) |
100 | 82, 99 | mpdan 683 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...𝐾)) → (𝑐‘𝑙) ∈
ℕ0) |
101 | 45, 100 | fsumnn0cl 15429 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) ∈
ℕ0) |
102 | 101 | nn0cnd 12278 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) ∈ ℂ) |
103 | 65, 63, 102 | pnpcand 11352 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) |
104 | | eqid 2739 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 =
1 |
105 | | 1p0e1 12080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 + 0) =
1 |
106 | 104, 105 | eqtr4i 2770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 = (1 +
0) |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 1 = (1 +
0)) |
108 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 ∈
ℝ) |
109 | | 0le1 11481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ≤
1 |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ 1) |
111 | 108, 11, 55, 108, 54, 110 | le2addd 11577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (1 + 0) ≤ (𝐾 + 1)) |
112 | 107, 111 | eqbrtrd 5100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 1 ≤ (𝐾 + 1)) |
113 | 53 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
114 | | eluz 12578 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℤ ∧ (𝐾 +
1) ∈ ℤ) → ((𝐾 + 1) ∈
(ℤ≥‘1) ↔ 1 ≤ (𝐾 + 1))) |
115 | 52, 113, 114 | syl2anc 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐾 + 1) ∈
(ℤ≥‘1) ↔ 1 ≤ (𝐾 + 1))) |
116 | 112, 115 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 + 1) ∈
(ℤ≥‘1)) |
117 | 116 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈
(ℤ≥‘1)) |
118 | 97 | ffvelrnda 6955 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈
ℕ0) |
119 | 118 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈ ℂ) |
120 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = (𝐾 + 1) → (𝑐‘𝑙) = (𝑐‘(𝐾 + 1))) |
121 | 117, 119,
120 | fsumm1 15444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) + (𝑐‘(𝐾 + 1)))) |
122 | | 1cnd 10954 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℂ) |
123 | 65, 122 | pncand 11316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 1) − 1) = 𝐾) |
124 | 123 | oveq2d 7284 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...((𝐾 + 1) − 1)) = (1...𝐾)) |
125 | 124 | sumeq1d 15394 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) |
126 | 125 | oveq1d 7283 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...((𝐾 + 1) − 1))(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1)))) |
127 | 121, 126 | eqtrd 2779 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1)))) |
128 | 127 | eqcomd 2745 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙)) |
129 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (𝑐‘𝑙) = (𝑐‘𝑖)) |
130 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖(1...(𝐾 + 1)) |
131 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑙(1...(𝐾 + 1)) |
132 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑖(𝑐‘𝑙) |
133 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑙(𝑐‘𝑖) |
134 | 129, 130,
131, 132, 133 | cbvsum 15388 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑙 ∈
(1...(𝐾 + 1))(𝑐‘𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖)) |
136 | 96 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑖 ∈ (1...(𝐾 + 1))(𝑐‘𝑖) = 𝑁) |
137 | 135, 136 | eqtrd 2779 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...(𝐾 + 1))(𝑐‘𝑙) = 𝑁) |
138 | 128, 137 | eqtrd 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁) |
139 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℤ) |
140 | 53 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℤ) |
141 | 140 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈ ℤ) |
142 | | 1e0p1 12461 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 = (0 +
1) |
143 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 = (0 + 1)) |
144 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ∈ ℝ) |
145 | 55 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝐾 ∈ ℝ) |
146 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ ℝ) |
147 | 11, 55, 12 | ltled 11106 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 0 ≤ 𝐾) |
148 | 147 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 0 ≤ 𝐾) |
149 | 144, 145,
146, 148 | leadd1dd 11572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (0 + 1) ≤ (𝐾 + 1)) |
150 | 143, 149 | eqbrtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ (𝐾 + 1)) |
151 | 55, 55, 108, 56 | leadd1dd 11572 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐾 + 1) ≤ (𝐾 + 1)) |
152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ≤ (𝐾 + 1)) |
153 | 139, 141,
141, 150, 152 | elfzd 13229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐾 + 1) ∈ (1...(𝐾 + 1))) |
154 | 97, 153 | ffvelrnd 6956 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘(𝐾 + 1)) ∈
ℕ0) |
155 | 154 | nn0cnd 12278 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘(𝐾 + 1)) ∈ ℂ) |
156 | 63, 102, 155 | subaddd 11333 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) = (𝑐‘(𝐾 + 1)) ↔ (Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙) + (𝑐‘(𝐾 + 1))) = 𝑁)) |
157 | 138, 156 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑁 − Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙)) = (𝑐‘(𝐾 + 1))) |
158 | 103, 157 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐾 + 𝑁) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑐‘(𝐾 + 1))) |
159 | 67, 158 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − (𝐾 + Σ𝑙 ∈ (1...𝐾)(𝑐‘𝑙))) = (𝑐‘(𝐾 + 1))) |
160 | 61, 159 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1))) |
161 | 160 | 3adant3 1130 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1))) |
162 | 161 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘(𝐾 + 1))) |
163 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → 𝑘 = (𝐾 + 1)) |
164 | 163 | fveq2d 6772 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘𝑘) = (𝑐‘(𝐾 + 1))) |
165 | 164 | eqcomd 2745 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → (𝑐‘(𝐾 + 1)) = (𝑐‘𝑘)) |
166 | 162, 165 | eqtrd 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ 𝑘 = (𝐾 + 1)) → ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)) = (𝑐‘𝑘)) |
167 | 47 | fveq1d 6770 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝐹‘𝑐)‘1) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1)) |
168 | 167 | oveq1d 7283 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝐹‘𝑐)‘1) − 1) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1)) |
169 | | eqidd 2740 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
170 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → 𝑗 = 1) |
171 | 170 | oveq2d 7284 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → (1...𝑗) = (1...1)) |
172 | 171 | sumeq1d 15394 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) |
173 | 170, 172 | oveq12d 7286 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑗 = 1) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙))) |
174 | 146 | leidd 11524 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ 1) |
175 | 54 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ≤ 𝐾) |
176 | 139, 140,
139, 174, 175 | elfzd 13229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (1...𝐾)) |
177 | | ovexd 7303 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) ∈ V) |
178 | 169, 173,
176, 177 | fvmptd 6876 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) = (1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙))) |
179 | 178 | oveq1d 7283 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1) = ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1)) |
180 | | fzfid 13674 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (1...1) ∈
Fin) |
181 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈
ℤ) |
182 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝐾 ∈ ℤ) |
183 | 182 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℤ) |
184 | | elfzelz 13238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ (1...1) → 𝑙 ∈
ℤ) |
185 | 184 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℤ) |
186 | | elfzle1 13241 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑙 ∈ (1...1) → 1 ≤
𝑙) |
187 | 186 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ≤ 𝑙) |
188 | 185 | zred 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ ℝ) |
189 | | 0red 10962 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 0 ∈
ℝ) |
190 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 ∈
ℝ) |
191 | 189, 190 | readdcld 10988 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ∈
ℝ) |
192 | 183 | zred 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝐾 + 1) ∈ ℝ) |
193 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑙 ∈ (1...1) → 𝑙 ≤ 1) |
194 | 193 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ 1) |
195 | 142 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 1 = (0 +
1)) |
196 | 194, 195 | breqtrd 5104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (0 + 1)) |
197 | 149 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (0 + 1) ≤ (𝐾 + 1)) |
198 | 188, 191,
192, 196, 197 | letrd 11115 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ≤ (𝐾 + 1)) |
199 | 181, 183,
185, 187, 198 | elfzd 13229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → 𝑙 ∈ (1...(𝐾 + 1))) |
200 | 118 | adantlr 711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈
ℕ0) |
201 | 199, 200 | mpdan 683 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑙 ∈ (1...1)) → (𝑐‘𝑙) ∈
ℕ0) |
202 | 180, 201 | fsumnn0cl 15429 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) ∈
ℕ0) |
203 | 202 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) ∈ ℂ) |
204 | 122, 203 | pncan2d 11317 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1) = Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) |
205 | 139, 141,
139, 174, 150 | elfzd 13229 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 1 ∈ (1...(𝐾 + 1))) |
206 | 97, 205 | ffvelrnd 6956 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈
ℕ0) |
207 | 206 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑐‘1) ∈ ℂ) |
208 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 1 → (𝑐‘𝑙) = (𝑐‘1)) |
209 | 208 | fsum1 15440 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℤ ∧ (𝑐‘1) ∈ ℂ) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) = (𝑐‘1)) |
210 | 139, 207,
209 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → Σ𝑙 ∈ (1...1)(𝑐‘𝑙) = (𝑐‘1)) |
211 | 204, 210 | eqtrd 2779 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → ((1 + Σ𝑙 ∈ (1...1)(𝑐‘𝑙)) − 1) = (𝑐‘1)) |
212 | 179, 211 | eqtrd 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘1) − 1) = (𝑐‘1)) |
213 | 168, 212 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1)) |
214 | 213 | 3adant3 1130 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1)) |
215 | 214 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1)) |
216 | 215 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘1)) |
217 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → 𝑘 = 1) |
218 | 217 | fveq2d 6772 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘𝑘) = (𝑐‘1)) |
219 | 218 | eqcomd 2745 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (𝑐‘1) = (𝑐‘𝑘)) |
220 | 216, 219 | eqtrd 2779 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ 𝑘 = 1) → (((𝐹‘𝑐)‘1) − 1) = (𝑐‘𝑘)) |
221 | 4 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐹 = (𝑎 ∈ 𝐴 ↦ (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))))) |
222 | | simpllr 772 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → 𝑎 = 𝑐) |
223 | 222 | fveq1d 6770 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) ∧ 𝑙 ∈ (1...𝑗)) → (𝑎‘𝑙) = (𝑐‘𝑙)) |
224 | 223 | sumeq2dv 15396 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙) = Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) |
225 | 224 | oveq2d 7284 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) ∧ 𝑗 ∈ (1...𝐾)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙)) = (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) |
226 | 225 | mpteq2dva 5178 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑎 = 𝑐) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑎‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
227 | | simpll2 1211 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐 ∈ 𝐴) |
228 | | fzfid 13674 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝐾) ∈ Fin) |
229 | 228 | mptexd 7094 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) ∈ V) |
230 | 221, 226,
227, 229 | fvmptd 6876 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐹‘𝑐) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
231 | 230 | fveq1d 6770 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹‘𝑐)‘𝑘) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘)) |
232 | 230 | fveq1d 6770 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐹‘𝑐)‘(𝑘 − 1)) = ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) |
233 | 231, 232 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) = (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1)))) |
234 | 233 | oveq1d 7283 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1) = ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1)) |
235 | | eqidd 2740 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙))) = (𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))) |
236 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → 𝑗 = 𝑘) |
237 | 236 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (1...𝑗) = (1...𝑘)) |
238 | 237 | sumeq1d 15394 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) |
239 | 236, 238 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = 𝑘) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙))) |
240 | | 1zzd 12334 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℤ) |
241 | 140 | 3adant3 1130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝐾 ∈ ℤ) |
242 | 241 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝐾 ∈ ℤ) |
243 | 242 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ) |
244 | | elfznn 13267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℕ) |
245 | 244 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℕ) |
246 | 245 | nnzd 12407 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ) |
247 | 246 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℤ) |
248 | 247 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ) |
249 | 245 | nnge1d 12004 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 1 ≤ 𝑘) |
250 | 249 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ≤ 𝑘) |
251 | 250 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘) |
252 | | simpl3 1191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ (1...(𝐾 + 1))) |
253 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 1 ∈
ℤ) |
254 | 242 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℤ) |
255 | | elfz 13227 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℤ ∧ 1 ∈
ℤ ∧ (𝐾 + 1)
∈ ℤ) → (𝑘
∈ (1...(𝐾 + 1)) ↔
(1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1)))) |
256 | 247, 253,
254, 255 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) ↔ (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1)))) |
257 | 256 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ∈ (1...(𝐾 + 1)) → (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1)))) |
258 | 252, 257 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (1 ≤ 𝑘 ∧ 𝑘 ≤ (𝐾 + 1))) |
259 | 258 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1)) |
260 | | neqne 2952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑘 = (𝐾 + 1) → 𝑘 ≠ (𝐾 + 1)) |
261 | 260 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≠ (𝐾 + 1)) |
262 | 261 | necomd 3000 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ≠ 𝑘) |
263 | 259, 262 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘)) |
264 | 247 | zred 12408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈ ℝ) |
265 | 254 | zred 12408 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝐾 + 1) ∈ ℝ) |
266 | 264, 265 | ltlend 11103 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 < (𝐾 + 1) ↔ (𝑘 ≤ (𝐾 + 1) ∧ (𝐾 + 1) ≠ 𝑘))) |
267 | 263, 266 | mpbird 256 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 < (𝐾 + 1)) |
268 | | zleltp1 12354 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑘 ≤ 𝐾 ↔ 𝑘 < (𝐾 + 1))) |
269 | 247, 242,
268 | syl2anc 583 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑘 ≤ 𝐾 ↔ 𝑘 < (𝐾 + 1))) |
270 | 267, 269 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ≤ 𝐾) |
271 | 270 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ 𝐾) |
272 | 240, 243,
248, 251, 271 | elfzd 13229 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...𝐾)) |
273 | | ovexd 7303 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) ∈ V) |
274 | 235, 239,
272, 273 | fvmptd 6876 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) = (𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙))) |
275 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → 𝑗 = (𝑘 − 1)) |
276 | 275 | oveq2d 7284 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (1...𝑗) = (1...(𝑘 − 1))) |
277 | 276 | sumeq1d 15394 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙) = Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) |
278 | 275, 277 | oveq12d 7286 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑗 = (𝑘 − 1)) → (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) |
279 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℤ) |
280 | 53 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ) |
281 | 280 | 3impa 1108 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℤ) |
282 | 244 | nnzd 12407 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ∈ ℤ) |
283 | 282 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ ℤ) |
284 | 283 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ) |
285 | 284 | 3impa 1108 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℤ) |
286 | 285, 279 | zsubcld 12413 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℤ) |
287 | | neqne 2952 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑘 = 1 → 𝑘 ≠ 1) |
288 | 287 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≠ 1) |
289 | 108 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℝ) |
290 | 285 | zred 12408 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℝ) |
291 | | simp2 1135 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ (1...(𝐾 + 1))) |
292 | | elfzle1 13241 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 1 ≤ 𝑘) |
293 | 291, 292 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ 𝑘) |
294 | 289, 290,
293 | leltned 11111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ 𝑘 ≠ 1)) |
295 | 288, 294 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 < 𝑘) |
296 | 279, 285 | zltp1led 39968 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 < 𝑘 ↔ (1 + 1) ≤ 𝑘)) |
297 | 295, 296 | mpbid 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1 + 1) ≤ 𝑘) |
298 | | leaddsub 11434 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑘 ∈ ℝ) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1))) |
299 | 289, 289,
290, 298 | syl3anc 1369 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + 1) ≤ 𝑘 ↔ 1 ≤ (𝑘 − 1))) |
300 | 297, 299 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ≤ (𝑘 − 1)) |
301 | 286 | zred 12408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℝ) |
302 | 55 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℝ) |
303 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℝ) |
304 | 302, 303 | readdcld 10988 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝐾 + 1) ∈ ℝ) |
305 | 304, 303 | resubcld 11386 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ∈
ℝ) |
306 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ (1...(𝐾 + 1)) → 𝑘 ≤ (𝐾 + 1)) |
307 | 306 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ≤ (𝐾 + 1)) |
308 | 290, 304,
303, 307 | lesub1dd 11574 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ ((𝐾 + 1) − 1)) |
309 | 64 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ∈ ℂ) |
310 | | 1cnd 10954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℂ) |
311 | 309, 310 | pncand 11316 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) = 𝐾) |
312 | 56 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝐾 ≤ 𝐾) |
313 | 311, 312 | eqbrtrd 5100 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝐾 + 1) − 1) ≤ 𝐾) |
314 | 301, 305,
302, 308, 313 | letrd 11115 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ≤ 𝐾) |
315 | 279, 281,
286, 300, 314 | elfzd 13229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾)) |
316 | 315 | 3expa 1116 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾)) |
317 | 316 | 3adantl2 1165 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾)) |
318 | 317 | adantlr 711 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ (1...𝐾)) |
319 | | ovexd 7303 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) ∈ V) |
320 | 235, 278,
318, 319 | fvmptd 6876 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1)) = ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) |
321 | 274, 320 | oveq12d 7286 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) = ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))) |
322 | 321 | oveq1d 7283 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1) = (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1)) |
323 | 248 | zcnd 12409 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈ ℂ) |
324 | | fzfid 13674 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...𝑘) ∈ Fin) |
325 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ∈ ℤ) |
326 | 243 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝐾 ∈ ℤ) |
327 | 326 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℤ) |
328 | | elfznn 13267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ∈ ℕ) |
329 | 328 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℕ) |
330 | 329 | nnzd 12407 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℤ) |
331 | 329 | nnge1d 12004 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 1 ≤ 𝑙) |
332 | 329 | nnred 11971 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ ℝ) |
333 | 264 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ∈ ℝ) |
334 | 265 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝐾 + 1) ∈ ℝ) |
335 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...𝑘) → 𝑙 ≤ 𝑘) |
336 | 335 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ 𝑘) |
337 | 259 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑘 ≤ (𝐾 + 1)) |
338 | 332, 333,
334, 336, 337 | letrd 11115 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ≤ (𝐾 + 1)) |
339 | 325, 327,
330, 331, 338 | elfzd 13229 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑙 ∈ (1...(𝐾 + 1))) |
340 | 97 | 3adant3 1130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
341 | 340 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
342 | 341 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
343 | 342 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
344 | 343 | ffvelrnda 6955 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈
ℕ0) |
345 | 339, 344 | mpdan 683 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐‘𝑙) ∈
ℕ0) |
346 | 324, 345 | fsumnn0cl 15429 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) ∈
ℕ0) |
347 | 346 | nn0cnd 12278 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) ∈ ℂ) |
348 | | 1cnd 10954 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 1 ∈
ℂ) |
349 | 323, 348 | subcld 11315 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − 1) ∈ ℂ) |
350 | | fzfid 13674 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (1...(𝑘 − 1)) ∈ Fin) |
351 | | 1zzd 12334 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈
ℤ) |
352 | 243 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝐾 ∈ ℤ) |
353 | 352 | peano2zd 12411 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℤ) |
354 | | elfznn 13267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ∈ ℕ) |
355 | 354 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℕ) |
356 | 355 | nnzd 12407 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℤ) |
357 | 355 | nnge1d 12004 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ≤ 𝑙) |
358 | 355 | nnred 11971 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ ℝ) |
359 | 264 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ∈ ℝ) |
360 | | 1red 10960 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 1 ∈
ℝ) |
361 | 359, 360 | resubcld 11386 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ∈ ℝ) |
362 | 265 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝐾 + 1) ∈ ℝ) |
363 | | elfzle2 13242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈ (1...(𝑘 − 1)) → 𝑙 ≤ (𝑘 − 1)) |
364 | 363 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝑘 − 1)) |
365 | 359 | lem1d 11891 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ 𝑘) |
366 | 259 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑘 ≤ (𝐾 + 1)) |
367 | 361, 359,
362, 365, 366 | letrd 11115 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑘 − 1) ≤ (𝐾 + 1)) |
368 | 358, 361,
362, 364, 367 | letrd 11115 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ≤ (𝐾 + 1)) |
369 | 351, 353,
356, 357, 368 | elfzd 13229 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑙 ∈ (1...(𝐾 + 1))) |
370 | 342 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → 𝑐:(1...(𝐾 +
1))⟶ℕ0) |
371 | 370 | ffvelrnda 6955 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) ∧ 𝑙 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑙) ∈
ℕ0) |
372 | 369, 371 | mpdan 683 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...(𝑘 − 1))) → (𝑐‘𝑙) ∈
ℕ0) |
373 | 350, 372 | fsumnn0cl 15429 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) ∈
ℕ0) |
374 | 373 | nn0cnd 12278 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) ∈ ℂ) |
375 | 323, 347,
349, 374 | addsub4d 11362 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) = ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))) |
376 | 375 | oveq1d 7283 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1)) |
377 | 323, 348 | nncand 11320 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑘 − (𝑘 − 1)) = 1) |
378 | 377 | oveq1d 7283 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) = (1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)))) |
379 | 378 | oveq1d 7283 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1)) |
380 | 347, 374 | subcld 11315 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) ∈ ℂ) |
381 | 348, 380 | pncan2d 11317 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) |
382 | 139 | 3adant3 1130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 1 ∈
ℤ) |
383 | 382, 246,
249 | 3jca 1126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤
𝑘)) |
384 | | eluz2 12570 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 1 ≤
𝑘)) |
385 | 383, 384 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈
(ℤ≥‘1)) |
386 | 385 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → 𝑘 ∈
(ℤ≥‘1)) |
387 | 386 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → 𝑘 ∈
(ℤ≥‘1)) |
388 | 345 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) ∧ 𝑙 ∈ (1...𝑘)) → (𝑐‘𝑙) ∈ ℂ) |
389 | | fveq2 6768 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑘 → (𝑐‘𝑙) = (𝑐‘𝑘)) |
390 | 387, 388,
389 | fsumm1 15444 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) = (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘))) |
391 | 390 | eqcomd 2745 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) |
392 | | simp3 1136 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → 𝑘 ∈ (1...(𝐾 + 1))) |
393 | 340, 392 | ffvelrnd 6956 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑘) ∈
ℕ0) |
394 | 393 | nn0cnd 12278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → (𝑐‘𝑘) ∈ ℂ) |
395 | 394 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → (𝑐‘𝑘) ∈ ℂ) |
396 | 395 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (𝑐‘𝑘) ∈ ℂ) |
397 | 347, 374,
396 | subaddd 11333 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) = (𝑐‘𝑘) ↔ (Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙) + (𝑐‘𝑘)) = Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙))) |
398 | 391, 397 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙)) = (𝑐‘𝑘)) |
399 | 381, 398 | eqtrd 2779 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((1 + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘)) |
400 | 379, 399 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 − (𝑘 − 1)) + (Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙) − Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘)) |
401 | 376, 400 | eqtrd 2779 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → (((𝑘 + Σ𝑙 ∈ (1...𝑘)(𝑐‘𝑙)) − ((𝑘 − 1) + Σ𝑙 ∈ (1...(𝑘 − 1))(𝑐‘𝑙))) − 1) = (𝑐‘𝑘)) |
402 | 322, 401 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘𝑘) − ((𝑗 ∈ (1...𝐾) ↦ (𝑗 + Σ𝑙 ∈ (1...𝑗)(𝑐‘𝑙)))‘(𝑘 − 1))) − 1) = (𝑐‘𝑘)) |
403 | 234, 402 | eqtrd 2779 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) ∧ ¬ 𝑘 = 1) → ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1) = (𝑐‘𝑘)) |
404 | 220, 403 | ifeqda 4500 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) ∧ ¬ 𝑘 = (𝐾 + 1)) → if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)) = (𝑐‘𝑘)) |
405 | 166, 404 | ifeqda 4500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴 ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))) = (𝑐‘𝑘)) |
406 | 405 | 3expa 1116 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑘 ∈ (1...(𝐾 + 1))) → if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1))) = (𝑐‘𝑘)) |
407 | 406 | mpteq2dva 5178 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘))) |
408 | 97 | ffnd 6597 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 Fn (1...(𝐾 + 1))) |
409 | | dffn5 6822 |
. . . . . . . 8
⊢ (𝑐 Fn (1...(𝐾 + 1)) ↔ 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘))) |
410 | 409 | biimpi 215 |
. . . . . . 7
⊢ (𝑐 Fn (1...(𝐾 + 1)) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘))) |
411 | 408, 410 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → 𝑐 = (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘))) |
412 | 411 | eqcomd 2745 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ (𝑐‘𝑘)) = 𝑐) |
413 | 407, 412 | eqtrd 2779 |
. . . 4
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝑘 ∈ (1...(𝐾 + 1)) ↦ if(𝑘 = (𝐾 + 1), ((𝑁 + 𝐾) − ((𝐹‘𝑐)‘𝐾)), if(𝑘 = 1, (((𝐹‘𝑐)‘1) − 1), ((((𝐹‘𝑐)‘𝑘) − ((𝐹‘𝑐)‘(𝑘 − 1))) − 1)))) = 𝑐) |
414 | 37, 413 | eqtrd 2779 |
. . 3
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐴) → (𝐺‘(𝐹‘𝑐)) = 𝑐) |
415 | 414 | ralrimiva 3109 |
. 2
⊢ (𝜑 → ∀𝑐 ∈ 𝐴 (𝐺‘(𝐹‘𝑐)) = 𝑐) |
416 | 1, 2, 4, 8, 5, 6 | sticksstones12a 40093 |
. 2
⊢ (𝜑 → ∀𝑑 ∈ 𝐵 (𝐹‘(𝐺‘𝑑)) = 𝑑) |
417 | 7, 9, 415, 416 | 2fvidf1od 7163 |
1
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |