Step | Hyp | Ref
| Expression |
1 | | fprodabs.2 |
. . 3
โข (๐ โ ๐ โ ๐) |
2 | | fprodabs.1 |
. . 3
โข ๐ =
(โคโฅโ๐) |
3 | 1, 2 | eleqtrdi 2844 |
. 2
โข (๐ โ ๐ โ (โคโฅโ๐)) |
4 | | oveq2 7414 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
5 | 4 | prodeq1d 15862 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
6 | 5 | fveq2d 6893 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
7 | 4 | prodeq1d 15862 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
8 | 6, 7 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
9 | 8 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
10 | | oveq2 7414 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
11 | 10 | prodeq1d 15862 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
12 | 11 | fveq2d 6893 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
13 | 10 | prodeq1d 15862 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
14 | 12, 13 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
15 | 14 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
16 | | oveq2 7414 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐...๐) = (๐...(๐ + 1))) |
17 | 16 | prodeq1d 15862 |
. . . . . 6
โข (๐ = (๐ + 1) โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...(๐ + 1))๐ด) |
18 | 17 | fveq2d 6893 |
. . . . 5
โข (๐ = (๐ + 1) โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...(๐ + 1))๐ด)) |
19 | 16 | prodeq1d 15862 |
. . . . 5
โข (๐ = (๐ + 1) โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)) |
20 | 18, 19 | eqeq12d 2749 |
. . . 4
โข (๐ = (๐ + 1) โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด))) |
21 | 20 | imbi2d 341 |
. . 3
โข (๐ = (๐ + 1) โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
22 | | oveq2 7414 |
. . . . . . 7
โข (๐ = ๐ โ (๐...๐) = (๐...๐)) |
23 | 22 | prodeq1d 15862 |
. . . . . 6
โข (๐ = ๐ โ โ๐ โ (๐...๐)๐ด = โ๐ โ (๐...๐)๐ด) |
24 | 23 | fveq2d 6893 |
. . . . 5
โข (๐ = ๐ โ (absโโ๐ โ (๐...๐)๐ด) = (absโโ๐ โ (๐...๐)๐ด)) |
25 | 22 | prodeq1d 15862 |
. . . . 5
โข (๐ = ๐ โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
26 | 24, 25 | eqeq12d 2749 |
. . . 4
โข (๐ = ๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
27 | 26 | imbi2d 341 |
. . 3
โข (๐ = ๐ โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)))) |
28 | | csbfv2g 6938 |
. . . . . 6
โข (๐ โ โค โ
โฆ๐ / ๐โฆ(absโ๐ด) =
(absโโฆ๐
/ ๐โฆ๐ด)) |
29 | 28 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ(absโ๐ด) = (absโโฆ๐ / ๐โฆ๐ด)) |
30 | | fzsn 13540 |
. . . . . . . 8
โข (๐ โ โค โ (๐...๐) = {๐}) |
31 | 30 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ (๐...๐) = {๐}) |
32 | 31 | prodeq1d 15862 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)(absโ๐ด) = โ๐ โ {๐} (absโ๐ด)) |
33 | | simpr 486 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ ๐ โ โค) |
34 | | uzid 12834 |
. . . . . . . . . . . 12
โข (๐ โ โค โ ๐ โ
(โคโฅโ๐)) |
35 | 34, 2 | eleqtrrdi 2845 |
. . . . . . . . . . 11
โข (๐ โ โค โ ๐ โ ๐) |
36 | | fprodabs.3 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐) โ ๐ด โ โ) |
37 | 36 | ralrimiva 3147 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ โ ๐ ๐ด โ โ) |
38 | | nfcsb1v 3918 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ๐ / ๐โฆ๐ด |
39 | 38 | nfel1 2920 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ๐ / ๐โฆ๐ด โ โ |
40 | | csbeq1a 3907 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ๐ด = โฆ๐ / ๐โฆ๐ด) |
41 | 40 | eleq1d 2819 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ด โ โ โ โฆ๐ / ๐โฆ๐ด โ โ)) |
42 | 39, 41 | rspc 3601 |
. . . . . . . . . . . 12
โข (๐ โ ๐ โ (โ๐ โ ๐ ๐ด โ โ โ โฆ๐ / ๐โฆ๐ด โ โ)) |
43 | 37, 42 | mpan9 508 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐) โ โฆ๐ / ๐โฆ๐ด โ โ) |
44 | 35, 43 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ๐ด โ โ) |
45 | 44 | abscld 15380 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โค) โ
(absโโฆ๐
/ ๐โฆ๐ด) โ
โ) |
46 | 45 | recnd 11239 |
. . . . . . . 8
โข ((๐ โง ๐ โ โค) โ
(absโโฆ๐
/ ๐โฆ๐ด) โ
โ) |
47 | 29, 46 | eqeltrd 2834 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โฆ๐ / ๐โฆ(absโ๐ด) โ โ) |
48 | | prodsns 15913 |
. . . . . . 7
โข ((๐ โ โค โง
โฆ๐ / ๐โฆ(absโ๐ด) โ โ) โ
โ๐ โ {๐} (absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
49 | 33, 47, 48 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ {๐} (absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
50 | 32, 49 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)(absโ๐ด) = โฆ๐ / ๐โฆ(absโ๐ด)) |
51 | 30 | prodeq1d 15862 |
. . . . . . . 8
โข (๐ โ โค โ
โ๐ โ (๐...๐)๐ด = โ๐ โ {๐}๐ด) |
52 | 51 | adantl 483 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)๐ด = โ๐ โ {๐}๐ด) |
53 | | prodsns 15913 |
. . . . . . . 8
โข ((๐ โ โค โง
โฆ๐ / ๐โฆ๐ด โ โ) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) |
54 | 33, 44, 53 | syl2anc 585 |
. . . . . . 7
โข ((๐ โง ๐ โ โค) โ โ๐ โ {๐}๐ด = โฆ๐ / ๐โฆ๐ด) |
55 | 52, 54 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ โ โค) โ โ๐ โ (๐...๐)๐ด = โฆ๐ / ๐โฆ๐ด) |
56 | 55 | fveq2d 6893 |
. . . . 5
โข ((๐ โง ๐ โ โค) โ
(absโโ๐ โ
(๐...๐)๐ด) = (absโโฆ๐ / ๐โฆ๐ด)) |
57 | 29, 50, 56 | 3eqtr4rd 2784 |
. . . 4
โข ((๐ โง ๐ โ โค) โ
(absโโ๐ โ
(๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
58 | 57 | expcom 415 |
. . 3
โข (๐ โ โค โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
59 | | simp3 1139 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |
60 | | ovex 7439 |
. . . . . . . . . . 11
โข (๐ + 1) โ V |
61 | | csbfv2g 6938 |
. . . . . . . . . . 11
โข ((๐ + 1) โ V โ
โฆ(๐ + 1) /
๐โฆ(absโ๐ด) = (absโโฆ(๐ + 1) / ๐โฆ๐ด)) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . 10
โข
โฆ(๐ +
1) / ๐โฆ(absโ๐ด) = (absโโฆ(๐ + 1) / ๐โฆ๐ด) |
63 | 62 | eqcomi 2742 |
. . . . . . . . 9
โข
(absโโฆ(๐ + 1) / ๐โฆ๐ด) = โฆ(๐ + 1) / ๐โฆ(absโ๐ด) |
64 | 63 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโฆ(๐ + 1) / ๐โฆ๐ด) = โฆ(๐ + 1) / ๐โฆ(absโ๐ด)) |
65 | 59, 64 | oveq12d 7424 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด)) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
66 | | simpr 486 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ ๐ โ (โคโฅโ๐)) |
67 | | elfzuz 13494 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐...(๐ + 1)) โ ๐ โ (โคโฅโ๐)) |
68 | 67, 2 | eleqtrrdi 2845 |
. . . . . . . . . . . . 13
โข (๐ โ (๐...(๐ + 1)) โ ๐ โ ๐) |
69 | 68, 36 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) |
70 | 69 | adantlr 714 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ ๐ด โ โ) |
71 | 66, 70 | fprodp1s 15912 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...(๐ + 1))๐ด = (โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) |
72 | 71 | fveq2d 6893 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโโ๐ โ
(๐...(๐ + 1))๐ด) = (absโ(โ๐ โ (๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด))) |
73 | | fzfid 13935 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ (๐...๐) โ Fin) |
74 | | elfzuz 13494 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐...๐) โ ๐ โ (โคโฅโ๐)) |
75 | 74, 2 | eleqtrrdi 2845 |
. . . . . . . . . . . . 13
โข (๐ โ (๐...๐) โ ๐ โ ๐) |
76 | 75, 36 | sylan2 594 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
77 | 76 | adantlr 714 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...๐)) โ ๐ด โ โ) |
78 | 73, 77 | fprodcl 15893 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...๐)๐ด โ โ) |
79 | | peano2uz 12882 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ
(โคโฅโ๐)) |
80 | 79, 2 | eleqtrrdi 2845 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ (๐ + 1) โ ๐) |
81 | | nfcsb1v 3918 |
. . . . . . . . . . . . . 14
โข
โฒ๐โฆ(๐ + 1) / ๐โฆ๐ด |
82 | 81 | nfel1 2920 |
. . . . . . . . . . . . 13
โข
โฒ๐โฆ(๐ + 1) / ๐โฆ๐ด โ โ |
83 | | csbeq1a 3907 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ ๐ด = โฆ(๐ + 1) / ๐โฆ๐ด) |
84 | 83 | eleq1d 2819 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (๐ด โ โ โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ)) |
85 | 82, 84 | rspc 3601 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ ๐ โ (โ๐ โ ๐ ๐ด โ โ โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ)) |
86 | 37, 85 | mpan9 508 |
. . . . . . . . . . 11
โข ((๐ โง (๐ + 1) โ ๐) โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ) |
87 | 80, 86 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โฆ(๐ + 1) / ๐โฆ๐ด โ โ) |
88 | 78, 87 | absmuld 15398 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโ(โ๐ โ
(๐...๐)๐ด ยท โฆ(๐ + 1) / ๐โฆ๐ด)) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
89 | 72, 88 | eqtrd 2773 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ
(absโโ๐ โ
(๐...(๐ + 1))๐ด) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
90 | 89 | 3adant3 1133 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = ((absโโ๐ โ (๐...๐)๐ด) ยท (absโโฆ(๐ + 1) / ๐โฆ๐ด))) |
91 | 70 | abscld 15380 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ (absโ๐ด) โ โ) |
92 | 91 | recnd 11239 |
. . . . . . . . 9
โข (((๐ โง ๐ โ (โคโฅโ๐)) โง ๐ โ (๐...(๐ + 1))) โ (absโ๐ด) โ โ) |
93 | 66, 92 | fprodp1s 15912 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐)) โ โ๐ โ (๐...(๐ + 1))(absโ๐ด) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
94 | 93 | 3adant3 1133 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ โ๐ โ (๐...(๐ + 1))(absโ๐ด) = (โ๐ โ (๐...๐)(absโ๐ด) ยท โฆ(๐ + 1) / ๐โฆ(absโ๐ด))) |
95 | 65, 90, 94 | 3eqtr4d 2783 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐) โง (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)) |
96 | 95 | 3exp 1120 |
. . . . 5
โข (๐ โ (๐ โ (โคโฅโ๐) โ
((absโโ๐ โ
(๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
97 | 96 | com12 32 |
. . . 4
โข (๐ โ
(โคโฅโ๐) โ (๐ โ ((absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด) โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
98 | 97 | a2d 29 |
. . 3
โข (๐ โ
(โคโฅโ๐) โ ((๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) โ (๐ โ (absโโ๐ โ (๐...(๐ + 1))๐ด) = โ๐ โ (๐...(๐ + 1))(absโ๐ด)))) |
99 | 9, 15, 21, 27, 58, 98 | uzind4 12887 |
. 2
โข (๐ โ
(โคโฅโ๐) โ (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด))) |
100 | 3, 99 | mpcom 38 |
1
โข (๐ โ (absโโ๐ โ (๐...๐)๐ด) = โ๐ โ (๐...๐)(absโ๐ด)) |