Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . 5
โข (๐ = ๐ด โ (1...๐) = (1...๐ด)) |
2 | 1 | sumeq1d 15593 |
. . . 4
โข (๐ = ๐ด โ ฮฃ๐ โ (1...๐)(๐นโ๐) = ฮฃ๐ โ (1...๐ด)(๐นโ๐)) |
3 | | aaliou3lem.e |
. . . 4
โข ๐ป = (๐ โ โ โฆ ฮฃ๐ โ (1...๐)(๐นโ๐)) |
4 | | sumex 15579 |
. . . 4
โข
ฮฃ๐ โ
(1...๐ด)(๐นโ๐) โ V |
5 | 2, 3, 4 | fvmpt 6953 |
. . 3
โข (๐ด โ โ โ (๐ปโ๐ด) = ฮฃ๐ โ (1...๐ด)(๐นโ๐)) |
6 | 5 | oveq1d 7377 |
. 2
โข (๐ด โ โ โ ((๐ปโ๐ด) ยท (2โ(!โ๐ด))) = (ฮฃ๐ โ (1...๐ด)(๐นโ๐) ยท (2โ(!โ๐ด)))) |
7 | | fzfid 13885 |
. . . 4
โข (๐ด โ โ โ
(1...๐ด) โ
Fin) |
8 | | 2rp 12927 |
. . . . . 6
โข 2 โ
โ+ |
9 | | nnnn0 12427 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ0) |
10 | 9 | faccld 14191 |
. . . . . . 7
โข (๐ด โ โ โ
(!โ๐ด) โ
โ) |
11 | 10 | nnzd 12533 |
. . . . . 6
โข (๐ด โ โ โ
(!โ๐ด) โ
โค) |
12 | | rpexpcl 13993 |
. . . . . 6
โข ((2
โ โ+ โง (!โ๐ด) โ โค) โ
(2โ(!โ๐ด)) โ
โ+) |
13 | 8, 11, 12 | sylancr 588 |
. . . . 5
โข (๐ด โ โ โ
(2โ(!โ๐ด)) โ
โ+) |
14 | 13 | rpcnd 12966 |
. . . 4
โข (๐ด โ โ โ
(2โ(!โ๐ด)) โ
โ) |
15 | | elfznn 13477 |
. . . . . . 7
โข (๐ โ (1...๐ด) โ ๐ โ โ) |
16 | | fveq2 6847 |
. . . . . . . . . 10
โข (๐ = ๐ โ (!โ๐) = (!โ๐)) |
17 | 16 | negeqd 11402 |
. . . . . . . . 9
โข (๐ = ๐ โ -(!โ๐) = -(!โ๐)) |
18 | 17 | oveq2d 7378 |
. . . . . . . 8
โข (๐ = ๐ โ (2โ-(!โ๐)) = (2โ-(!โ๐))) |
19 | | aaliou3lem.c |
. . . . . . . 8
โข ๐น = (๐ โ โ โฆ
(2โ-(!โ๐))) |
20 | | ovex 7395 |
. . . . . . . 8
โข
(2โ-(!โ๐)) โ V |
21 | 18, 19, 20 | fvmpt 6953 |
. . . . . . 7
โข (๐ โ โ โ (๐นโ๐) = (2โ-(!โ๐))) |
22 | 15, 21 | syl 17 |
. . . . . 6
โข (๐ โ (1...๐ด) โ (๐นโ๐) = (2โ-(!โ๐))) |
23 | 22 | adantl 483 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (๐นโ๐) = (2โ-(!โ๐))) |
24 | 15 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ๐ โ โ) |
25 | 24 | nnnn0d 12480 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ๐ โ โ0) |
26 | 25 | faccld 14191 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐) โ โ) |
27 | 26 | nnzd 12533 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐) โ โค) |
28 | 27 | znegcld 12616 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ -(!โ๐) โ โค) |
29 | | rpexpcl 13993 |
. . . . . . 7
โข ((2
โ โ+ โง -(!โ๐) โ โค) โ
(2โ-(!โ๐))
โ โ+) |
30 | 8, 28, 29 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (2โ-(!โ๐)) โ
โ+) |
31 | 30 | rpcnd 12966 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (2โ-(!โ๐)) โ
โ) |
32 | 23, 31 | eqeltrd 2838 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (๐นโ๐) โ โ) |
33 | 7, 14, 32 | fsummulc1 15677 |
. . 3
โข (๐ด โ โ โ
(ฮฃ๐ โ (1...๐ด)(๐นโ๐) ยท (2โ(!โ๐ด))) = ฮฃ๐ โ (1...๐ด)((๐นโ๐) ยท (2โ(!โ๐ด)))) |
34 | 23 | oveq1d 7377 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((๐นโ๐) ยท (2โ(!โ๐ด))) = ((2โ-(!โ๐)) ยท (2โ(!โ๐ด)))) |
35 | 11 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐ด) โ โค) |
36 | | 2cnne0 12370 |
. . . . . . . 8
โข (2 โ
โ โง 2 โ 0) |
37 | | expaddz 14019 |
. . . . . . . 8
โข (((2
โ โ โง 2 โ 0) โง (-(!โ๐) โ โค โง (!โ๐ด) โ โค)) โ
(2โ(-(!โ๐) +
(!โ๐ด))) =
((2โ-(!โ๐))
ยท (2โ(!โ๐ด)))) |
38 | 36, 37 | mpan 689 |
. . . . . . 7
โข
((-(!โ๐)
โ โค โง (!โ๐ด) โ โค) โ
(2โ(-(!โ๐) +
(!โ๐ด))) =
((2โ-(!โ๐))
ยท (2โ(!โ๐ด)))) |
39 | 28, 35, 38 | syl2anc 585 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (2โ(-(!โ๐) + (!โ๐ด))) = ((2โ-(!โ๐)) ยท (2โ(!โ๐ด)))) |
40 | | 2z 12542 |
. . . . . . 7
โข 2 โ
โค |
41 | 28 | zcnd 12615 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ -(!โ๐) โ โ) |
42 | 35 | zcnd 12615 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐ด) โ โ) |
43 | 41, 42 | addcomd 11364 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (-(!โ๐) + (!โ๐ด)) = ((!โ๐ด) + -(!โ๐))) |
44 | 26 | nncnd 12176 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐) โ โ) |
45 | 42, 44 | negsubd 11525 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((!โ๐ด) + -(!โ๐)) = ((!โ๐ด) โ (!โ๐))) |
46 | 43, 45 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (-(!โ๐) + (!โ๐ด)) = ((!โ๐ด) โ (!โ๐))) |
47 | 9 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ๐ด โ
โ0) |
48 | | elfzle2 13452 |
. . . . . . . . . . 11
โข (๐ โ (1...๐ด) โ ๐ โค ๐ด) |
49 | 48 | adantl 483 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ๐ โค ๐ด) |
50 | | facwordi 14196 |
. . . . . . . . . 10
โข ((๐ โ โ0
โง ๐ด โ
โ0 โง ๐
โค ๐ด) โ
(!โ๐) โค
(!โ๐ด)) |
51 | 25, 47, 49, 50 | syl3anc 1372 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐) โค (!โ๐ด)) |
52 | 26 | nnnn0d 12480 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐) โ
โ0) |
53 | 47 | faccld 14191 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐ด) โ โ) |
54 | 53 | nnnn0d 12480 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (!โ๐ด) โ
โ0) |
55 | | nn0sub 12470 |
. . . . . . . . . 10
โข
(((!โ๐) โ
โ0 โง (!โ๐ด) โ โ0) โ
((!โ๐) โค
(!โ๐ด) โ
((!โ๐ด) โ
(!โ๐)) โ
โ0)) |
56 | 52, 54, 55 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((!โ๐) โค (!โ๐ด) โ ((!โ๐ด) โ (!โ๐)) โ
โ0)) |
57 | 51, 56 | mpbid 231 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((!โ๐ด) โ (!โ๐)) โ
โ0) |
58 | 46, 57 | eqeltrd 2838 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (-(!โ๐) + (!โ๐ด)) โ
โ0) |
59 | | zexpcl 13989 |
. . . . . . 7
โข ((2
โ โค โง (-(!โ๐) + (!โ๐ด)) โ โ0) โ
(2โ(-(!โ๐) +
(!โ๐ด))) โ
โค) |
60 | 40, 58, 59 | sylancr 588 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ (2โ(-(!โ๐) + (!โ๐ด))) โ โค) |
61 | 39, 60 | eqeltrrd 2839 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((2โ-(!โ๐)) ยท
(2โ(!โ๐ด)))
โ โค) |
62 | 34, 61 | eqeltrd 2838 |
. . . 4
โข ((๐ด โ โ โง ๐ โ (1...๐ด)) โ ((๐นโ๐) ยท (2โ(!โ๐ด))) โ โค) |
63 | 7, 62 | fsumzcl 15627 |
. . 3
โข (๐ด โ โ โ
ฮฃ๐ โ (1...๐ด)((๐นโ๐) ยท (2โ(!โ๐ด))) โ โค) |
64 | 33, 63 | eqeltrd 2838 |
. 2
โข (๐ด โ โ โ
(ฮฃ๐ โ (1...๐ด)(๐นโ๐) ยท (2โ(!โ๐ด))) โ โค) |
65 | 6, 64 | eqeltrd 2838 |
1
โข (๐ด โ โ โ ((๐ปโ๐ด) ยท (2โ(!โ๐ด))) โ
โค) |