Step | Hyp | Ref
| Expression |
1 | | prodfc 14514 |
. 2
⊢
∏𝑗 ∈
(𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ∏𝑘 ∈ (𝑀...𝑁)𝐴 |
2 | | fveq2 6103 |
. . . 4
⊢ (𝑗 = ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚))) |
3 | | fprodser.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
4 | | eluzelz 11573 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℤ) |
6 | 5 | zcnd 11359 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
7 | | eluzel2 11568 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ∈ ℤ) |
8 | 3, 7 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
9 | 8 | zcnd 11359 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℂ) |
10 | | 1cnd 9935 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℂ) |
11 | 6, 9, 10 | subadd23d 10293 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 𝑀) + 1) = (𝑁 + (1 − 𝑀))) |
12 | 11 | eqcomd 2616 |
. . . . 5
⊢ (𝜑 → (𝑁 + (1 − 𝑀)) = ((𝑁 − 𝑀) + 1)) |
13 | | uznn0sub 11595 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → (𝑁 − 𝑀) ∈
ℕ0) |
14 | 3, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑁 − 𝑀) ∈
ℕ0) |
15 | | nn0p1nn 11209 |
. . . . . 6
⊢ ((𝑁 − 𝑀) ∈ ℕ0 → ((𝑁 − 𝑀) + 1) ∈ ℕ) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℕ) |
17 | 12, 16 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℕ) |
18 | 10, 9 | pncan3d 10274 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 + (𝑀 − 1)) = 𝑀) |
19 | 6, 10, 9 | pnpncand 10331 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑁 + (1 − 𝑀)) + (𝑀 − 1)) = 𝑁) |
20 | 18, 19 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝜑 → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁)) |
21 | 20 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝜑 → (𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) ↔ 𝑝 ∈ (𝑀...𝑁))) |
22 | 21 | biimpa 500 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → 𝑝 ∈ (𝑀...𝑁)) |
23 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℤ) |
24 | 23 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (𝑀...𝑁) → 𝑝 ∈ ℂ) |
25 | 24 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℂ) |
26 | | peano2zm 11297 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℤ → (𝑀 − 1) ∈
ℤ) |
27 | 8, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑀 − 1) ∈ ℤ) |
28 | 27 | zcnd 11359 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑀 − 1) ∈ ℂ) |
29 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℂ) |
30 | 25, 29 | npcand 10275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) = 𝑝) |
31 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ (𝑀...𝑁)) |
32 | 30, 31 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
33 | | ovex 6577 |
. . . . . . . . . 10
⊢ (𝑝 − (𝑀 − 1)) ∈ V |
34 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑛 + (𝑀 − 1)) = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) |
35 | 34 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → ((𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁))) |
36 | 33, 35 | sbcie 3437 |
. . . . . . . . 9
⊢
([(𝑝 −
(𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
37 | 32, 36 | sylibr 223 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
38 | 22, 37 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) → [(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
39 | 38 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
40 | | 1zzd 11285 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
41 | 17 | nnzd 11357 |
. . . . . . 7
⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈ ℤ) |
42 | | fzshftral 12297 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ (𝑁 +
(1 − 𝑀)) ∈
ℤ ∧ (𝑀 − 1)
∈ ℤ) → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))) |
43 | 40, 41, 27, 42 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ↔ ∀𝑝 ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))[(𝑝 − (𝑀 − 1)) / 𝑛](𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁))) |
44 | 39, 43 | mpbird 246 |
. . . . 5
⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
45 | 8 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
46 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑁 ∈ ℤ) |
47 | 23 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 ∈ ℤ) |
48 | 27 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑀 − 1) ∈ ℤ) |
49 | | fzsubel 12248 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑝 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ))
→ (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))))) |
50 | 45, 46, 47, 48, 49 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 ∈ (𝑀...𝑁) ↔ (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))))) |
51 | 31, 50 | mpbid 221 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1)))) |
52 | 9, 10 | nncand 10276 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑀 − (𝑀 − 1)) = 1) |
53 | 6, 9, 10 | subsub2d 10300 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁 − (𝑀 − 1)) = (𝑁 + (1 − 𝑀))) |
54 | 52, 53 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀)))) |
55 | 54 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ((𝑀 − (𝑀 − 1))...(𝑁 − (𝑀 − 1))) = (1...(𝑁 + (1 − 𝑀)))) |
56 | 51, 55 | eleqtrd 2690 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → (𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀)))) |
57 | 30 | eqcomd 2616 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) |
58 | 34 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑛 = (𝑝 − (𝑀 − 1)) → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1)))) |
59 | 58 | rspcev 3282 |
. . . . . . . 8
⊢ (((𝑝 − (𝑀 − 1)) ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑝 = ((𝑝 − (𝑀 − 1)) + (𝑀 − 1))) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))) |
60 | 56, 57, 59 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))) |
61 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℤ) |
62 | 61 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑛 ∈ ℂ) |
63 | | elfzelz 12213 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℤ) |
64 | 63 | zcnd 11359 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → 𝑚 ∈ ℂ) |
65 | 62, 64 | anim12i 588 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) |
66 | | eqtr2 2630 |
. . . . . . . . . . 11
⊢ ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1))) |
67 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑛 ∈ ℂ) |
68 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → 𝑚 ∈ ℂ) |
69 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → (𝑀 − 1) ∈ ℂ) |
70 | 67, 68, 69 | addcan2d 10119 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1)) ↔ 𝑛 = 𝑚)) |
71 | 66, 70 | syl5ib 233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ ℂ ∧ 𝑚 ∈ ℂ)) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)) |
72 | 65, 71 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀))))) → ((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)) |
73 | 72 | ralrimivva 2954 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)) |
74 | 73 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚)) |
75 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑛 + (𝑀 − 1)) = (𝑚 + (𝑀 − 1))) |
76 | 75 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑝 = (𝑛 + (𝑀 − 1)) ↔ 𝑝 = (𝑚 + (𝑀 − 1)))) |
77 | 76 | reu4 3367 |
. . . . . . 7
⊢
(∃!𝑛 ∈
(1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ↔ (∃𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)) ∧ ∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))∀𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))((𝑝 = (𝑛 + (𝑀 − 1)) ∧ 𝑝 = (𝑚 + (𝑀 − 1))) → 𝑛 = 𝑚))) |
78 | 60, 74, 77 | sylanbrc 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ (𝑀...𝑁)) → ∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))) |
79 | 78 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1))) |
80 | | eqid 2610 |
. . . . . 6
⊢ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) = (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))) |
81 | 80 | f1ompt 6290 |
. . . . 5
⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) ↔ (∀𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))(𝑛 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ∀𝑝 ∈ (𝑀...𝑁)∃!𝑛 ∈ (1...(𝑁 + (1 − 𝑀)))𝑝 = (𝑛 + (𝑀 − 1)))) |
82 | 44, 79, 81 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁)) |
83 | | fprodser.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
84 | | eqid 2610 |
. . . . . 6
⊢ (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) = (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴) |
85 | 83, 84 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑁) ↦ 𝐴):(𝑀...𝑁)⟶ℂ) |
86 | 85 | ffvelrnda 6267 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) ∈ ℂ) |
87 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) |
88 | | 1zzd 11285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 1 ∈
ℤ) |
89 | 41 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑁 + (1 − 𝑀)) ∈ ℤ) |
90 | 63 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → 𝑚 ∈ ℤ) |
91 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑀 − 1) ∈ ℤ) |
92 | | fzaddel 12246 |
. . . . . . . . 9
⊢ (((1
∈ ℤ ∧ (𝑁 +
(1 − 𝑀)) ∈
ℤ) ∧ (𝑚 ∈
ℤ ∧ (𝑀 − 1)
∈ ℤ)) → (𝑚
∈ (1...(𝑁 + (1 −
𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))) |
93 | 88, 89, 90, 91, 92 | syl22anc 1319 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) ↔ (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))))) |
94 | 87, 93 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) |
95 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((1 + (𝑀 − 1))...((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (𝑀...𝑁)) |
96 | 94, 95 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) |
97 | | fprodser.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑁)) → (𝐹‘𝑘) = 𝐴) |
98 | 97 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴) |
99 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 |
100 | 99 | nfeq2 2766 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 |
101 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐹‘𝑘) = (𝐹‘(𝑚 + (𝑀 − 1)))) |
102 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → 𝐴 = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
103 | 101, 102 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → ((𝐹‘𝑘) = 𝐴 ↔ (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)) |
104 | 100, 103 | rspc 3276 |
. . . . . . 7
⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)(𝐹‘𝑘) = 𝐴 → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴)) |
105 | 98, 104 | mpan9 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
106 | 96, 105 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
107 | | f1of 6050 |
. . . . . . . 8
⊢ ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))–1-1-onto→(𝑀...𝑁) → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁)) |
108 | 82, 107 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁)) |
109 | | fvco3 6185 |
. . . . . . 7
⊢ (((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))):(1...(𝑁 + (1 − 𝑀)))⟶(𝑀...𝑁) ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚))) |
110 | 108, 109 | sylan 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚))) |
111 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑚 + (𝑀 − 1)) ∈ V |
112 | 75, 80, 111 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑚 ∈ (1...(𝑁 + (1 − 𝑀))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1))) |
113 | 112 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚) = (𝑚 + (𝑀 − 1))) |
114 | 113 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → (𝐹‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = (𝐹‘(𝑚 + (𝑀 − 1)))) |
115 | 110, 114 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = (𝐹‘(𝑚 + (𝑀 − 1)))) |
116 | 113 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1)))) |
117 | 83 | ralrimiva 2949 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ) |
118 | 99 | nfel1 2765 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ |
119 | 102 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑚 + (𝑀 − 1)) → (𝐴 ∈ ℂ ↔ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)) |
120 | 118, 119 | rspc 3276 |
. . . . . . . . 9
⊢ ((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) → (∀𝑘 ∈ (𝑀...𝑁)𝐴 ∈ ℂ → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ)) |
121 | 117, 120 | mpan9 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁)) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) |
122 | 96, 121 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) |
123 | 84 | fvmpts 6194 |
. . . . . . 7
⊢ (((𝑚 + (𝑀 − 1)) ∈ (𝑀...𝑁) ∧ ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴 ∈ ℂ) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
124 | 96, 122, 123 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘(𝑚 + (𝑀 − 1))) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
125 | 116, 124 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚)) = ⦋(𝑚 + (𝑀 − 1)) / 𝑘⦌𝐴) |
126 | 106, 115,
125 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1...(𝑁 + (1 − 𝑀)))) → ((𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1))))‘𝑚) = ((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘((𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))‘𝑚))) |
127 | 2, 17, 82, 86, 126 | fprod 14510 |
. . 3
⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀)))) |
128 | | nnuz 11599 |
. . . . 5
⊢ ℕ =
(ℤ≥‘1) |
129 | 17, 128 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → (𝑁 + (1 − 𝑀)) ∈
(ℤ≥‘1)) |
130 | 129, 27, 115 | seqshft2 12689 |
. . 3
⊢ (𝜑 → (seq1( · , (𝐹 ∘ (𝑛 ∈ (1...(𝑁 + (1 − 𝑀))) ↦ (𝑛 + (𝑀 − 1)))))‘(𝑁 + (1 − 𝑀))) = (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1)))) |
131 | 18 | seqeq1d 12669 |
. . . 4
⊢ (𝜑 → seq(1 + (𝑀 − 1))( · , 𝐹) = seq𝑀( · , 𝐹)) |
132 | 131, 19 | fveq12d 6109 |
. . 3
⊢ (𝜑 → (seq(1 + (𝑀 − 1))( · , 𝐹)‘((𝑁 + (1 − 𝑀)) + (𝑀 − 1))) = (seq𝑀( · , 𝐹)‘𝑁)) |
133 | 127, 130,
132 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ∏𝑗 ∈ (𝑀...𝑁)((𝑘 ∈ (𝑀...𝑁) ↦ 𝐴)‘𝑗) = (seq𝑀( · , 𝐹)‘𝑁)) |
134 | 1, 133 | syl5eqr 2658 |
1
⊢ (𝜑 → ∏𝑘 ∈ (𝑀...𝑁)𝐴 = (seq𝑀( · , 𝐹)‘𝑁)) |