Step | Hyp | Ref
| Expression |
1 | | fprodabs.2 |
. . 3
โข (๐ โ ๐ โ ๐) |
2 | | fprodabs.1 |
. . 3
โข ๐ =
(โคโฅโ๐) |
3 | 1, 2 | eleqtrdi 2270 |
. 2
โข (๐ โ ๐ โ (โคโฅโ๐)) |
4 | | oveq2 5885 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
5 | 4 | prodeq1d 11574 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
6 | 5 | fveq2d 5521 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
7 | 4 | prodeq1d 11574 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
8 | 6, 7 | eqeq12d 2192 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
9 | 8 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
10 | | oveq2 5885 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
11 | 10 | prodeq1d 11574 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
12 | 11 | fveq2d 5521 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
13 | 10 | prodeq1d 11574 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
14 | 12, 13 | eqeq12d 2192 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
15 | 14 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
16 | | oveq2 5885 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐...๐) = (๐...(๐ + 1))) |
17 | 16 | prodeq1d 11574 |
. . . . . 6
โข (๐ = (๐ + 1) โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...(๐ + 1))๐ด) |
18 | 17 | fveq2d 5521 |
. . . . 5
โข (๐ = (๐ + 1) โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...(๐ + 1))๐ด)) |
19 | 16 | prodeq1d 11574 |
. . . . 5
โข (๐ = (๐ + 1) โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)) |
20 | 18, 19 | eqeq12d 2192 |
. . . 4
โข (๐ = (๐ + 1) โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด))) |
21 | 20 | imbi2d 230 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
22 | | oveq2 5885 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
23 | 22 | prodeq1d 11574 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
24 | 23 | fveq2d 5521 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
25 | 22 | prodeq1d 11574 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
26 | 24, 25 | eqeq12d 2192 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
27 | 26 | imbi2d 230 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
28 | | csbfv2g 5554 |
. . . . . 6
โข (๐ โ โค โ
โฆ๐ / ๐โฆ(absโ๐ด) =
(absโโฆ๐
/ ๐โฆ๐ด)) |
29 | 28 | adantl 277 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ(absโ๐ด) = (absโโฆ๐ / ๐โฆ๐ด)) |
30 | | fzsn 10068 |
. . . . . . . 8
โข (๐ โ โค โ (๐...๐) = {๐}) |
31 | 30 | adantl 277 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ (๐...๐) = {๐}) |
32 | 31 | prodeq1d 11574 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ {๐} (absโ๐ด)) |
33 | | simpr 110 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ ๐ โ โค) |
34 | | uzid 9544 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
35 | 34, 2 | eleqtrrdi 2271 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ ๐) |
36 | | fprodabs.3 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) |
37 | 36 | ralrimiva 2550 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ ๐ ๐ด โ โ) |
38 | | nfcsb1v 3092 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ๐ / ๐โฆ๐ด |
39 | 38 | nfel1 2330 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ๐ / ๐โฆ๐ด โ โ |
40 | | csbeq1a 3068 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ๐ด = โฆ๐ / ๐โฆ๐ด) |
41 | 40 | eleq1d 2246 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ด โ โ โ โฆ๐ / ๐โฆ๐ด โ โ)) |
42 | 39, 41 | rspc 2837 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (โ๐ โ ๐ ๐ด โ โ โ โฆ๐ / ๐โฆ๐ด โ โ)) |
43 | 37, 42 | mpan9 281 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ด โ โ) |
44 | 35, 43 | sylan2 286 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ๐ด โ โ) |
45 | 44 | abscld 11192 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โค) โ
(absโโฆ๐
/ ๐โฆ๐ด) โ
โ) |
46 | 45 | recnd 7988 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ
(absโโฆ๐
/ ๐โฆ๐ด) โ
โ) |
47 | 29, 46 | eqeltrd 2254 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ(absโ๐ด) โ โ) |
48 | | prodsns 11613 |
. . . . . . 7
โข ((๐ โ โค โง
โฆ๐ / ๐โฆ(absโ๐ด) โ โ) โ
โ๐ โ {๐} (absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
49 | 33, 47, 48 | syl2anc 411 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ {๐} (absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
50 | 32, 49 | eqtrd 2210 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)(absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
51 | 30 | prodeq1d 11574 |
. . . . . . . 8
โข (๐ โ โค โ
โ๐ โ (๐...๐)๐ด = โ๐ โ {๐}๐ด) |
52 | 51 | adantl 277 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)๐ด = โ๐ โ {๐}๐ด) |
53 | | prodsns 11613 |
. . . . . . . 8
โข ((๐ โ โค โง
โฆ๐ / ๐โฆ๐ด โ โ) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) |
54 | 33, 44, 53 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) |
55 | 52, 54 | eqtrd 2210 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)๐ด = โฆ๐ / ๐โฆ๐ด) |
56 | 55 | fveq2d 5521 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ
(absโโ๐ โ
(๐...๐)๐ด) = (absโโฆ๐ / ๐โฆ๐ด)) |
57 | 29, 50, 56 | 3eqtr4rd 2221 |
. . . 4
โข ((๐ โง ๐ โ โค) โ
(absโโ๐ โ
(๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
58 | 57 | expcom 116 |
. . 3
โข (๐ โ โค โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
59 | | simp3 999 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
60 | | peano2uz 9585 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
61 | | csbfv2g 5554 |
. . . . . . . . . . 11
โข ((๐ + 1) โ
(โคโฅโ๐) โ โฆ(๐ + 1) / ๐โฆ(absโ๐ด) = (absโโฆ(๐ + 1) / ๐โฆ๐ด)) |
62 | 60, 61 | syl 14 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ๐) โ โฆ(๐ + 1) / ๐โฆ(absโ๐ด) = (absโโฆ(๐ + 1) / ๐โฆ๐ด)) |
63 | 62 | eqcomd 2183 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ๐) โ (absโโฆ(๐ + 1) / ๐โฆ๐ด) = โฆ(๐ + 1) / ๐โฆ(absโ๐ด)) |
64 | 63 | 3ad2ant2 1019 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโฆ(๐ + 1) / ๐โฆ๐ด) = โฆ(๐ + 1) / ๐โฆ(absโ๐ด)) |
65 | 59, 64 | oveq12d 5895 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด)) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
66 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ (โคโฅโ๐)) |
67 | | elfzuz 10023 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐...(๐ + 1)) โ ๐ โ (โคโฅโ๐)) |
68 | 67, 2 | eleqtrrdi 2271 |
. . . . . . . . . . . . 13
โข (๐ โ (๐...(๐ + 1)) โ ๐ โ ๐) |
69 | 68, 36 | sylan2 286 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) |
70 | 69 | adantlr 477 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) |
71 | 66, 70 | fprodp1s 11612 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) |
72 | 71 | fveq2d 5521 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโโ๐ โ
(๐...(๐ + 1))๐ด) = (absโ(โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด))) |
73 | | eluzel2 9535 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
74 | 73 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
75 | | eluzelz 9539 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
76 | 75 | adantl 277 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
77 | 74, 76 | fzfigd 10433 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐...๐) โ Fin) |
78 | | elfzuz 10023 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐...๐) โ ๐ โ (โคโฅโ๐)) |
79 | 78, 2 | eleqtrrdi 2271 |
. . . . . . . . . . . . 13
โข (๐ โ (๐...๐) โ ๐ โ ๐) |
80 | 79, 36 | sylan2 286 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
81 | 80 | adantlr 477 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
82 | 77, 81 | fprodcl 11617 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐)๐ด โ โ) |
83 | 60, 2 | eleqtrrdi 2271 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ ๐) |
84 | | nfcsb1v 3092 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ(๐ + 1) / ๐โฆ๐ด |
85 | 84 | nfel1 2330 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ(๐ + 1) / ๐โฆ๐ด โ โ |
86 | | csbeq1a 3068 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ ๐ด = โฆ(๐ + 1) / ๐โฆ๐ด) |
87 | 86 | eleq1d 2246 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (๐ด โ โ โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ)) |
88 | 85, 87 | rspc 2837 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ ๐ โ (โ๐ โ ๐ ๐ด โ โ โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ)) |
89 | 37, 88 | mpan9 281 |
. . . . . . . . . . 11
โข ((๐ โง (๐ + 1) โ ๐) โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ) |
90 | 83, 89 | sylan2 286 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ) |
91 | 82, 90 | absmuld 11205 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโ(โ๐ โ
(๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
92 | 72, 91 | eqtrd 2210 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโโ๐ โ
(๐...(๐ + 1))๐ด) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
93 | 92 | 3adant3 1017 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
94 | 70 | abscld 11192 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ (absโ๐ด) โ โ) |
95 | 94 | recnd 7988 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ (absโ๐ด) โ โ) |
96 | 66, 95 | fprodp1s 11612 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...(๐ + 1))(absโ๐ด) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
97 | 96 | 3adant3 1017 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ โ๐ โ (๐...(๐ + 1))(absโ๐ด) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
98 | 65, 93, 97 | 3eqtr4d 2220 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)) |
99 | 98 | 3exp 1202 |
. . . . 5
โข (๐ โ (๐ โ (โคโฅโ๐) โ
((absโโ๐ โ
(๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
100 | 99 | com12 30 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
101 | 100 | a2d 26 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
102 | 9, 15, 21, 27, 58, 101 | uzind4 9590 |
. 2
โข (๐ โ
(โคโฅโ๐) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
103 | 3, 102 | mpcom 36 |
1
โข (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |