Step | Hyp | Ref
| Expression |
1 | | fmulcl.2 |
. 2
โข ๐ = (seq1(๐, ๐)โ๐) |
2 | | fmulcl.4 |
. . . 4
โข (๐ โ ๐ โ (1...๐)) |
3 | | elfzuz 13438 |
. . . 4
โข (๐ โ (1...๐) โ ๐ โ
(โคโฅโ1)) |
4 | 2, 3 | syl 17 |
. . 3
โข (๐ โ ๐ โ
(โคโฅโ1)) |
5 | | elfzuz3 13439 |
. . . . . 6
โข (๐ โ (1...๐) โ ๐ โ (โคโฅโ๐)) |
6 | | fzss2 13482 |
. . . . . 6
โข (๐ โ
(โคโฅโ๐) โ (1...๐) โ (1...๐)) |
7 | 2, 5, 6 | 3syl 18 |
. . . . 5
โข (๐ โ (1...๐) โ (1...๐)) |
8 | 7 | sselda 3945 |
. . . 4
โข ((๐ โง โ โ (1...๐)) โ โ โ (1...๐)) |
9 | | fmulcl.5 |
. . . . 5
โข (๐ โ ๐:(1...๐)โถ๐) |
10 | 9 | ffvelcdmda 7036 |
. . . 4
โข ((๐ โง โ โ (1...๐)) โ (๐โโ) โ ๐) |
11 | 8, 10 | syldan 592 |
. . 3
โข ((๐ โง โ โ (1...๐)) โ (๐โโ) โ ๐) |
12 | | simprl 770 |
. . . . 5
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ โ โ ๐) |
13 | | simprr 772 |
. . . . 5
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ ๐ โ ๐) |
14 | | fmulcl.7 |
. . . . . . 7
โข (๐ โ ๐ โ V) |
15 | 14 | adantr 482 |
. . . . . 6
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ ๐ โ V) |
16 | | mptexg 7172 |
. . . . . 6
โข (๐ โ V โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ V) |
17 | 15, 16 | syl 17 |
. . . . 5
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ V) |
18 | | fveq1 6842 |
. . . . . . . 8
โข (๐ = โ โ (๐โ๐ก) = (โโ๐ก)) |
19 | | fveq1 6842 |
. . . . . . . 8
โข (๐ = ๐ โ (๐โ๐ก) = (๐โ๐ก)) |
20 | 18, 19 | oveqan12d 7377 |
. . . . . . 7
โข ((๐ = โ โง ๐ = ๐) โ ((๐โ๐ก) ยท (๐โ๐ก)) = ((โโ๐ก) ยท (๐โ๐ก))) |
21 | 20 | mpteq2dv 5208 |
. . . . . 6
โข ((๐ = โ โง ๐ = ๐) โ (๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก))) = (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก)))) |
22 | | fmulcl.1 |
. . . . . 6
โข ๐ = (๐ โ ๐, ๐ โ ๐ โฆ (๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก)))) |
23 | 21, 22 | ovmpoga 7510 |
. . . . 5
โข ((โ โ ๐ โง ๐ โ ๐ โง (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ V) โ (โ๐๐) = (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก)))) |
24 | 12, 13, 17, 23 | syl3anc 1372 |
. . . 4
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ (โ๐๐) = (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก)))) |
25 | | 3simpc 1151 |
. . . . . 6
โข ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (โ โ ๐ โง ๐ โ ๐)) |
26 | | eleq1w 2821 |
. . . . . . . . 9
โข (๐ = โ โ (๐ โ ๐ โ โ โ ๐)) |
27 | 26 | 3anbi2d 1442 |
. . . . . . . 8
โข (๐ = โ โ ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โง โ โ ๐ โง ๐ โ ๐))) |
28 | 18 | oveq1d 7373 |
. . . . . . . . . 10
โข (๐ = โ โ ((๐โ๐ก) ยท (๐โ๐ก)) = ((โโ๐ก) ยท (๐โ๐ก))) |
29 | 28 | mpteq2dv 5208 |
. . . . . . . . 9
โข (๐ = โ โ (๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก))) = (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก)))) |
30 | 29 | eleq1d 2823 |
. . . . . . . 8
โข (๐ = โ โ ((๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก))) โ ๐ โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐)) |
31 | 27, 30 | imbi12d 345 |
. . . . . . 7
โข (๐ = โ โ (((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก))) โ ๐) โ ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐))) |
32 | | eleq1w 2821 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ โ ๐ โ ๐ โ ๐)) |
33 | 32 | 3anbi3d 1443 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ โง โ โ ๐ โง ๐ โ ๐))) |
34 | 19 | oveq2d 7374 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((โโ๐ก) ยท (๐โ๐ก)) = ((โโ๐ก) ยท (๐โ๐ก))) |
35 | 34 | mpteq2dv 5208 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) = (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก)))) |
36 | 35 | eleq1d 2823 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐ โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐)) |
37 | 33, 36 | imbi12d 345 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐) โ ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐))) |
38 | | fmulcl.6 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((๐โ๐ก) ยท (๐โ๐ก))) โ ๐) |
39 | 31, 37, 38 | vtocl2g 3532 |
. . . . . 6
โข ((โ โ ๐ โง ๐ โ ๐) โ ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐)) |
40 | 25, 39 | mpcom 38 |
. . . . 5
โข ((๐ โง โ โ ๐ โง ๐ โ ๐) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐) |
41 | 40 | 3expb 1121 |
. . . 4
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ (๐ก โ ๐ โฆ ((โโ๐ก) ยท (๐โ๐ก))) โ ๐) |
42 | 24, 41 | eqeltrd 2838 |
. . 3
โข ((๐ โง (โ โ ๐ โง ๐ โ ๐)) โ (โ๐๐) โ ๐) |
43 | 4, 11, 42 | seqcl 13929 |
. 2
โข (๐ โ (seq1(๐, ๐)โ๐) โ ๐) |
44 | 1, 43 | eqeltrid 2842 |
1
โข (๐ โ ๐ โ ๐) |