Step | Hyp | Ref
| Expression |
1 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = ๐พ โ ((๐พ + 1)...๐ฅ) = ((๐พ + 1)...๐พ)) |
2 | 1 | iuneq1d 4986 |
. . . . . 6
โข (๐ฅ = ๐พ โ โช
๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐) = โช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) |
3 | 2 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐พ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) = (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐))) |
4 | 1 | sumeq1d 15593 |
. . . . . 6
โข (๐ฅ = ๐พ โ ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0)) |
5 | 4 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐พ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0))) |
6 | 3, 5 | breq12d 5123 |
. . . 4
โข (๐ฅ = ๐พ โ ((โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0)))) |
7 | 6 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐พ โ ((๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0))) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0))))) |
8 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐พ + 1)...๐ฅ) = ((๐พ + 1)...๐)) |
9 | 8 | iuneq1d 4986 |
. . . . . 6
โข (๐ฅ = ๐ โ โช
๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐) = โช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) |
10 | 9 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) = (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
11 | 8 | sumeq1d 15593 |
. . . . . 6
โข (๐ฅ = ๐ โ ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) |
12 | 11 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))) |
13 | 10, 12 | breq12d 5123 |
. . . 4
โข (๐ฅ = ๐ โ ((โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
14 | 13 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ โ ((๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0))) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))))) |
15 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = (๐ + 1) โ ((๐พ + 1)...๐ฅ) = ((๐พ + 1)...(๐ + 1))) |
16 | 15 | iuneq1d 4986 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ โช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐) = โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) |
17 | 16 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) = (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐))) |
18 | 15 | sumeq1d 15593 |
. . . . . 6
โข (๐ฅ = (๐ + 1) โ ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) |
19 | 18 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = (๐ + 1) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))) |
20 | 17, 19 | breq12d 5123 |
. . . 4
โข (๐ฅ = (๐ + 1) โ ((โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
21 | 20 | imbi2d 341 |
. . 3
โข (๐ฅ = (๐ + 1) โ ((๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0))) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))))) |
22 | | oveq2 7370 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐พ + 1)...๐ฅ) = ((๐พ + 1)...๐)) |
23 | 22 | iuneq1d 4986 |
. . . . . 6
โข (๐ฅ = ๐ โ โช
๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐) = โช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) |
24 | 23 | fveq2d 6851 |
. . . . 5
โข (๐ฅ = ๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) = (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐))) |
25 | 22 | sumeq1d 15593 |
. . . . . 6
โข (๐ฅ = ๐ โ ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) |
26 | 25 | oveq2d 7378 |
. . . . 5
โข (๐ฅ = ๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))) |
27 | 24, 26 | breq12d 5123 |
. . . 4
โข (๐ฅ = ๐ โ ((โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
28 | 27 | imbi2d 341 |
. . 3
โข (๐ฅ = ๐ โ ((๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐ฅ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐ฅ)if(๐ โ โ, (1 / ๐), 0))) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))))) |
29 | | 0le0 12261 |
. . . . 5
โข 0 โค
0 |
30 | | prmrec.3 |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
31 | 30 | nncnd 12176 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
32 | 31 | mul01d 11361 |
. . . . 5
โข (๐ โ (๐ ยท 0) = 0) |
33 | 29, 32 | breqtrrid 5148 |
. . . 4
โข (๐ โ 0 โค (๐ ยท 0)) |
34 | | prmrec.2 |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ โ) |
35 | 34 | nnred 12175 |
. . . . . . . . . 10
โข (๐ โ ๐พ โ โ) |
36 | 35 | ltp1d 12092 |
. . . . . . . . 9
โข (๐ โ ๐พ < (๐พ + 1)) |
37 | 34 | nnzd 12533 |
. . . . . . . . . . 11
โข (๐ โ ๐พ โ โค) |
38 | 37 | peano2zd 12617 |
. . . . . . . . . 10
โข (๐ โ (๐พ + 1) โ โค) |
39 | | fzn 13464 |
. . . . . . . . . 10
โข (((๐พ + 1) โ โค โง ๐พ โ โค) โ (๐พ < (๐พ + 1) โ ((๐พ + 1)...๐พ) = โ
)) |
40 | 38, 37, 39 | syl2anc 585 |
. . . . . . . . 9
โข (๐ โ (๐พ < (๐พ + 1) โ ((๐พ + 1)...๐พ) = โ
)) |
41 | 36, 40 | mpbid 231 |
. . . . . . . 8
โข (๐ โ ((๐พ + 1)...๐พ) = โ
) |
42 | 41 | iuneq1d 4986 |
. . . . . . 7
โข (๐ โ โช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐) = โช ๐ โ โ
(๐โ๐)) |
43 | | 0iun 5028 |
. . . . . . 7
โข โช ๐ โ โ
(๐โ๐) = โ
|
44 | 42, 43 | eqtrdi 2793 |
. . . . . 6
โข (๐ โ โช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐) = โ
) |
45 | 44 | fveq2d 6851 |
. . . . 5
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) =
(โฏโโ
)) |
46 | | hash0 14274 |
. . . . 5
โข
(โฏโโ
) = 0 |
47 | 45, 46 | eqtrdi 2793 |
. . . 4
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) = 0) |
48 | 41 | sumeq1d 15593 |
. . . . . 6
โข (๐ โ ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ โ
if(๐ โ โ, (1 / ๐), 0)) |
49 | | sum0 15613 |
. . . . . 6
โข
ฮฃ๐ โ
โ
if(๐ โ
โ, (1 / ๐), 0) =
0 |
50 | 48, 49 | eqtrdi 2793 |
. . . . 5
โข (๐ โ ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0) = 0) |
51 | 50 | oveq2d 7378 |
. . . 4
โข (๐ โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท 0)) |
52 | 33, 47, 51 | 3brtr4d 5142 |
. . 3
โข (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐พ)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐พ)if(๐ โ โ, (1 / ๐), 0))) |
53 | | fzfi 13884 |
. . . . . . . . . . 11
โข
(1...๐) โ
Fin |
54 | | elfzuz 13444 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐พ + 1)...๐) โ ๐ โ (โคโฅโ(๐พ + 1))) |
55 | 34 | peano2nnd 12177 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (๐พ + 1) โ โ) |
56 | | eluznn 12850 |
. . . . . . . . . . . . . . . . 17
โข (((๐พ + 1) โ โ โง ๐ โ
(โคโฅโ(๐พ + 1))) โ ๐ โ โ) |
57 | 55, 56 | sylan 581 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ ๐ โ
โ) |
58 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (๐ โ โ โ ๐ โ โ)) |
59 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (๐ โฅ ๐ โ ๐ โฅ ๐)) |
60 | 58, 59 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = ๐ โ ((๐ โ โ โง ๐ โฅ ๐) โ (๐ โ โ โง ๐ โฅ ๐))) |
61 | 60 | rabbidv 3418 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = ๐ โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
62 | | prmrec.7 |
. . . . . . . . . . . . . . . . . . 19
โข ๐ = (๐ โ โ โฆ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
63 | | ovex 7395 |
. . . . . . . . . . . . . . . . . . . 20
โข
(1...๐) โ
V |
64 | 63 | rabex 5294 |
. . . . . . . . . . . . . . . . . . 19
โข {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ V |
65 | 61, 62, 64 | fvmpt 6953 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
66 | 65 | adantl 483 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โ) โ (๐โ๐) = {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)}) |
67 | | ssrab2 4042 |
. . . . . . . . . . . . . . . . 17
โข {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} โ (1...๐) |
68 | 66, 67 | eqsstrdi 4003 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ โ) โ (๐โ๐) โ (1...๐)) |
69 | 57, 68 | syldan 592 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ (๐โ๐) โ (1...๐)) |
70 | 54, 69 | sylan2 594 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐พ + 1)...๐)) โ (๐โ๐) โ (1...๐)) |
71 | 70 | ralrimiva 3144 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
72 | 71 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
73 | | iunss 5010 |
. . . . . . . . . . . 12
โข (โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐) โ โ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
74 | 72, 73 | sylibr 233 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) |
75 | | ssfi 9124 |
. . . . . . . . . . 11
โข
(((1...๐) โ Fin
โง โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ (1...๐)) โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin) |
76 | 53, 74, 75 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin) |
77 | | hashcl 14263 |
. . . . . . . . . 10
โข (โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ
โ0) |
78 | 76, 77 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ
โ0) |
79 | 78 | nn0red 12481 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โ โ) |
80 | 30 | nnred 12175 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
81 | 80 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ โ) |
82 | | fzfid 13885 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐พ + 1)...๐) โ Fin) |
83 | 55 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐พ + 1) โ โ) |
84 | 83, 54, 56 | syl2an 597 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ๐ โ ((๐พ + 1)...๐)) โ ๐ โ โ) |
85 | | nnrecre 12202 |
. . . . . . . . . . . 12
โข (๐ โ โ โ (1 /
๐) โ
โ) |
86 | | 0re 11164 |
. . . . . . . . . . . 12
โข 0 โ
โ |
87 | | ifcl 4536 |
. . . . . . . . . . . 12
โข (((1 /
๐) โ โ โง 0
โ โ) โ if(๐
โ โ, (1 / ๐), 0)
โ โ) |
88 | 85, 86, 87 | sylancl 587 |
. . . . . . . . . . 11
โข (๐ โ โ โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
89 | 84, 88 | syl 17 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ๐ โ ((๐พ + 1)...๐)) โ if(๐ โ โ, (1 / ๐), 0) โ โ) |
90 | 82, 89 | fsumrecl 15626 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) โ โ) |
91 | 81, 90 | remulcld 11192 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ โ) |
92 | | prmnn 16557 |
. . . . . . . . . . . 12
โข ((๐ + 1) โ โ โ
(๐ + 1) โ
โ) |
93 | 92 | nnrecred 12211 |
. . . . . . . . . . 11
โข ((๐ + 1) โ โ โ (1 /
(๐ + 1)) โ
โ) |
94 | 93 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ (1 / (๐ + 1)) โ
โ) |
95 | | 0red 11165 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ 0
โ โ) |
96 | 94, 95 | ifclda 4526 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ if((๐ + 1) โ โ, (1 / (๐ + 1)), 0) โ
โ) |
97 | 81, 96 | remulcld 11192 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)) โ
โ) |
98 | 79, 91, 97 | leadd1d 11756 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค ((๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))))) |
99 | | eluzp1p1 12798 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ๐พ) โ (๐ + 1) โ
(โคโฅโ(๐พ + 1))) |
100 | 99 | adantl 483 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ + 1) โ
(โคโฅโ(๐พ + 1))) |
101 | | simpl 484 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐) |
102 | | elfzuz 13444 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐พ + 1)...(๐ + 1)) โ ๐ โ (โคโฅโ(๐พ + 1))) |
103 | 88 | recnd 11190 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
104 | 57, 103 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
105 | 101, 102,
104 | syl2an 597 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ๐ โ ((๐พ + 1)...(๐ + 1))) โ if(๐ โ โ, (1 / ๐), 0) โ โ) |
106 | | eleq1 2826 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (๐ โ โ โ (๐ + 1) โ โ)) |
107 | | oveq2 7370 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ (1 / ๐) = (1 / (๐ + 1))) |
108 | 106, 107 | ifbieq1d 4515 |
. . . . . . . . . . . 12
โข (๐ = (๐ + 1) โ if(๐ โ โ, (1 / ๐), 0) = if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)) |
109 | 100, 105,
108 | fsumm1 15643 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0) = (ฮฃ๐ โ ((๐พ + 1)...((๐ + 1) โ 1))if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
110 | | eluzelz 12780 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ
(โคโฅโ๐พ) โ ๐ โ โค) |
111 | 110 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ โค) |
112 | 111 | zcnd 12615 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ โ) |
113 | | ax-1cn 11116 |
. . . . . . . . . . . . . . 15
โข 1 โ
โ |
114 | | pncan 11414 |
. . . . . . . . . . . . . . 15
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
115 | 112, 113,
114 | sylancl 587 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐ + 1) โ 1) = ๐) |
116 | 115 | oveq2d 7378 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐พ + 1)...((๐ + 1) โ 1)) = ((๐พ + 1)...๐)) |
117 | 116 | sumeq1d 15593 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...((๐ + 1) โ 1))if(๐ โ โ, (1 / ๐), 0) = ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) |
118 | 117 | oveq1d 7377 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (ฮฃ๐ โ ((๐พ + 1)...((๐ + 1) โ 1))if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)) = (ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
119 | 109, 118 | eqtrd 2777 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0) = (ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
120 | 119 | oveq2d 7378 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) = (๐ ยท (ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)))) |
121 | 31 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ โ) |
122 | 90 | recnd 11190 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) โ โ) |
123 | 96 | recnd 11190 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ if((๐ + 1) โ โ, (1 / (๐ + 1)), 0) โ
โ) |
124 | 121, 122,
123 | adddid 11186 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท (ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0) + if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) = ((๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)))) |
125 | 120, 124 | eqtrd 2777 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) = ((๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)))) |
126 | 125 | breq2d 5122 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) โ ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค ((๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))))) |
127 | 98, 126 | bitr4d 282 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
128 | 102, 69 | sylan2 594 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ ((๐พ + 1)...(๐ + 1))) โ (๐โ๐) โ (1...๐)) |
129 | 128 | ralrimiva 3144 |
. . . . . . . . . . . . 13
โข (๐ โ โ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐)) |
130 | 129 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐)) |
131 | | iunss 5010 |
. . . . . . . . . . . 12
โข (โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐) โ โ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐)) |
132 | 130, 131 | sylibr 233 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐)) |
133 | | ssfi 9124 |
. . . . . . . . . . 11
โข
(((1...๐) โ Fin
โง โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ (1...๐)) โ โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ Fin) |
134 | 53, 132, 133 | sylancr 588 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ Fin) |
135 | | hashcl 14263 |
. . . . . . . . . 10
โข (โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) โ Fin โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โ
โ0) |
136 | 134, 135 | syl 17 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โ
โ0) |
137 | 136 | nn0red 12481 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โ โ) |
138 | | fveq2 6847 |
. . . . . . . . . . . . . 14
โข (๐ = (๐ + 1) โ (๐โ๐) = (๐โ(๐ + 1))) |
139 | 138 | sseq1d 3980 |
. . . . . . . . . . . . 13
โข (๐ = (๐ + 1) โ ((๐โ๐) โ (1...๐) โ (๐โ(๐ + 1)) โ (1...๐))) |
140 | 68 | ralrimiva 3144 |
. . . . . . . . . . . . . 14
โข (๐ โ โ๐ โ โ (๐โ๐) โ (1...๐)) |
141 | 140 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โ๐ โ โ (๐โ๐) โ (1...๐)) |
142 | | eluznn 12850 |
. . . . . . . . . . . . . . 15
โข ((๐พ โ โ โง ๐ โ
(โคโฅโ๐พ)) โ ๐ โ โ) |
143 | 34, 142 | sylan 581 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ โ) |
144 | 143 | peano2nnd 12177 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ + 1) โ โ) |
145 | 139, 141,
144 | rspcdva 3585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐โ(๐ + 1)) โ (1...๐)) |
146 | | ssfi 9124 |
. . . . . . . . . . . 12
โข
(((1...๐) โ Fin
โง (๐โ(๐ + 1)) โ (1...๐)) โ (๐โ(๐ + 1)) โ Fin) |
147 | 53, 145, 146 | sylancr 588 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐โ(๐ + 1)) โ Fin) |
148 | | hashcl 14263 |
. . . . . . . . . . 11
โข ((๐โ(๐ + 1)) โ Fin โ
(โฏโ(๐โ(๐ + 1))) โ
โ0) |
149 | 147, 148 | syl 17 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ(๐โ(๐ + 1))) โ
โ0) |
150 | 149 | nn0red 12481 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ(๐โ(๐ + 1))) โ โ) |
151 | 79, 150 | readdcld 11191 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (โฏโ(๐โ(๐ + 1)))) โ โ) |
152 | 79, 97 | readdcld 11191 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โ
โ) |
153 | 38 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐พ + 1) โ โค) |
154 | | simpr 486 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ (โคโฅโ๐พ)) |
155 | 34 | nncnd 12176 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐พ โ โ) |
156 | 155 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐พ โ โ) |
157 | | pncan 11414 |
. . . . . . . . . . . . . . . 16
โข ((๐พ โ โ โง 1 โ
โ) โ ((๐พ + 1)
โ 1) = ๐พ) |
158 | 156, 113,
157 | sylancl 587 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐พ + 1) โ 1) = ๐พ) |
159 | 158 | fveq2d 6851 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โคโฅโ((๐พ + 1) โ 1)) =
(โคโฅโ๐พ)) |
160 | 154, 159 | eleqtrrd 2841 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ (โคโฅโ((๐พ + 1) โ
1))) |
161 | | fzsuc2 13506 |
. . . . . . . . . . . . 13
โข (((๐พ + 1) โ โค โง ๐ โ
(โคโฅโ((๐พ + 1) โ 1))) โ ((๐พ + 1)...(๐ + 1)) = (((๐พ + 1)...๐) โช {(๐ + 1)})) |
162 | 153, 160,
161 | syl2anc 585 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐พ + 1)...(๐ + 1)) = (((๐พ + 1)...๐) โช {(๐ + 1)})) |
163 | 162 | iuneq1d 4986 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) = โช ๐ โ (((๐พ + 1)...๐) โช {(๐ + 1)})(๐โ๐)) |
164 | | iunxun 5059 |
. . . . . . . . . . . 12
โข โช ๐ โ (((๐พ + 1)...๐) โช {(๐ + 1)})(๐โ๐) = (โช
๐ โ ((๐พ + 1)...๐)(๐โ๐) โช โช
๐ โ {(๐ + 1)} (๐โ๐)) |
165 | | ovex 7395 |
. . . . . . . . . . . . . 14
โข (๐ + 1) โ V |
166 | 165, 138 | iunxsn 5056 |
. . . . . . . . . . . . 13
โข โช ๐ โ {(๐ + 1)} (๐โ๐) = (๐โ(๐ + 1)) |
167 | 166 | uneq2i 4125 |
. . . . . . . . . . . 12
โข (โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โช โช
๐ โ {(๐ + 1)} (๐โ๐)) = (โช
๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1))) |
168 | 164, 167 | eqtri 2765 |
. . . . . . . . . . 11
โข โช ๐ โ (((๐พ + 1)...๐) โช {(๐ + 1)})(๐โ๐) = (โช
๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1))) |
169 | 163, 168 | eqtrdi 2793 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ โช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐) = (โช
๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1)))) |
170 | 169 | fveq2d 6851 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) = (โฏโ(โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1))))) |
171 | | hashun2 14290 |
. . . . . . . . . 10
โข
((โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โ Fin โง (๐โ(๐ + 1)) โ Fin) โ
(โฏโ(โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1)))) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (โฏโ(๐โ(๐ + 1))))) |
172 | 76, 147, 171 | syl2anc 585 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโ(โช ๐ โ ((๐พ + 1)...๐)(๐โ๐) โช (๐โ(๐ + 1)))) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (โฏโ(๐โ(๐ + 1))))) |
173 | 170, 172 | eqbrtrd 5132 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (โฏโ(๐โ(๐ + 1))))) |
174 | 81, 144 | nndivred 12214 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ / (๐ + 1)) โ โ) |
175 | | flle 13711 |
. . . . . . . . . . . . . 14
โข ((๐ / (๐ + 1)) โ โ โ
(โโ(๐ / (๐ + 1))) โค (๐ / (๐ + 1))) |
176 | 174, 175 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ(๐ / (๐ + 1))) โค (๐ / (๐ + 1))) |
177 | | elfznn 13477 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ (1...๐) โ ๐ โ โ) |
178 | 177 | nncnd 12176 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ (1...๐) โ ๐ โ โ) |
179 | 178 | subid1d 11508 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ (๐ โ 0) = ๐) |
180 | 179 | breq2d 5122 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (1...๐) โ ((๐ + 1) โฅ (๐ โ 0) โ (๐ + 1) โฅ ๐)) |
181 | 180 | rabbiia 3414 |
. . . . . . . . . . . . . . 15
โข {๐ โ (1...๐) โฃ (๐ + 1) โฅ (๐ โ 0)} = {๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐} |
182 | 181 | fveq2i 6850 |
. . . . . . . . . . . . . 14
โข
(โฏโ{๐
โ (1...๐) โฃ
(๐ + 1) โฅ (๐ โ 0)}) =
(โฏโ{๐ โ
(1...๐) โฃ (๐ + 1) โฅ ๐}) |
183 | | 1zzd 12541 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ 1 โ
โค) |
184 | 30 | nnnn0d 12480 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ ๐ โ
โ0) |
185 | | nn0uz 12812 |
. . . . . . . . . . . . . . . . . . 19
โข
โ0 = (โคโฅโ0) |
186 | | 1m1e0 12232 |
. . . . . . . . . . . . . . . . . . . 20
โข (1
โ 1) = 0 |
187 | 186 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . . 19
โข
(โคโฅโ(1 โ 1)) =
(โคโฅโ0) |
188 | 185, 187 | eqtr4i 2768 |
. . . . . . . . . . . . . . . . . 18
โข
โ0 = (โคโฅโ(1 โ
1)) |
189 | 184, 188 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ (โคโฅโ(1
โ 1))) |
190 | 189 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ๐ โ (โคโฅโ(1
โ 1))) |
191 | | 0zd 12518 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ 0 โ
โค) |
192 | 144, 183,
190, 191 | hashdvds 16654 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ{๐ โ (1...๐) โฃ (๐ + 1) โฅ (๐ โ 0)}) = ((โโ((๐ โ 0) / (๐ + 1))) โ
(โโ(((1 โ 1) โ 0) / (๐ + 1))))) |
193 | 121 | subid1d 11508 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ โ 0) = ๐) |
194 | 193 | fvoveq1d 7384 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ((๐ โ 0) / (๐ + 1))) = (โโ(๐ / (๐ + 1)))) |
195 | 186 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((1
โ 1) โ 0) = (0 โ 0) |
196 | | 0m0e0 12280 |
. . . . . . . . . . . . . . . . . . . . 21
โข (0
โ 0) = 0 |
197 | 195, 196 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
โข ((1
โ 1) โ 0) = 0 |
198 | 197 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . . 19
โข (((1
โ 1) โ 0) / (๐
+ 1)) = (0 / (๐ +
1)) |
199 | 144 | nncnd 12176 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ + 1) โ โ) |
200 | 144 | nnne0d 12210 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ + 1) โ 0) |
201 | 199, 200 | div0d 11937 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (0 / (๐ + 1)) = 0) |
202 | 198, 201 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (((1 โ 1)
โ 0) / (๐ + 1)) =
0) |
203 | 202 | fveq2d 6851 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ(((1
โ 1) โ 0) / (๐
+ 1))) = (โโ0)) |
204 | | 0z 12517 |
. . . . . . . . . . . . . . . . . 18
โข 0 โ
โค |
205 | | flid 13720 |
. . . . . . . . . . . . . . . . . 18
โข (0 โ
โค โ (โโ0) = 0) |
206 | 204, 205 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
(โโ0) = 0 |
207 | 203, 206 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ(((1
โ 1) โ 0) / (๐
+ 1))) = 0) |
208 | 194, 207 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โโ((๐ โ
0) / (๐ + 1))) โ
(โโ(((1 โ 1) โ 0) / (๐ + 1)))) = ((โโ(๐ / (๐ + 1))) โ 0)) |
209 | 174 | flcld 13710 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ(๐ / (๐ + 1))) โ โค) |
210 | 209 | zcnd 12615 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โโ(๐ / (๐ + 1))) โ โ) |
211 | 210 | subid1d 11508 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((โโ(๐ / (๐ + 1))) โ 0) = (โโ(๐ / (๐ + 1)))) |
212 | 192, 208,
211 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ{๐ โ (1...๐) โฃ (๐ + 1) โฅ (๐ โ 0)}) = (โโ(๐ / (๐ + 1)))) |
213 | 182, 212 | eqtr3id 2791 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ{๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐}) = (โโ(๐ / (๐ + 1)))) |
214 | 121, 199,
200 | divrecd 11941 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ / (๐ + 1)) = (๐ ยท (1 / (๐ + 1)))) |
215 | 214 | eqcomd 2743 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท (1 / (๐ + 1))) = (๐ / (๐ + 1))) |
216 | 176, 213,
215 | 3brtr4d 5142 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ{๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐}) โค (๐ ยท (1 / (๐ + 1)))) |
217 | 216 | adantr 482 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ
(โฏโ{๐ โ
(1...๐) โฃ (๐ + 1) โฅ ๐}) โค (๐ ยท (1 / (๐ + 1)))) |
218 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ + 1) โ (๐ โ โ โ (๐ + 1) โ โ)) |
219 | | breq1 5113 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ + 1) โ (๐ โฅ ๐ โ (๐ + 1) โฅ ๐)) |
220 | 218, 219 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ + 1) โ ((๐ โ โ โง ๐ โฅ ๐) โ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐))) |
221 | 220 | rabbidv 3418 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ + 1) โ {๐ โ (1...๐) โฃ (๐ โ โ โง ๐ โฅ ๐)} = {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)}) |
222 | 63 | rabex 5294 |
. . . . . . . . . . . . . . . 16
โข {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)} โ V |
223 | 221, 62, 222 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
โข ((๐ + 1) โ โ โ
(๐โ(๐ + 1)) = {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)}) |
224 | 144, 223 | syl 17 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐โ(๐ + 1)) = {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)}) |
225 | 224 | adantr 482 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ (๐โ(๐ + 1)) = {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)}) |
226 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ (๐ + 1) โ
โ) |
227 | 226 | biantrurd 534 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ ((๐ + 1) โฅ ๐ โ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐))) |
228 | 227 | rabbidv 3418 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ {๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐} = {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)}) |
229 | 225, 228 | eqtr4d 2780 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ (๐โ(๐ + 1)) = {๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐}) |
230 | 229 | fveq2d 6851 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ
(โฏโ(๐โ(๐ + 1))) = (โฏโ{๐ โ (1...๐) โฃ (๐ + 1) โฅ ๐})) |
231 | | iftrue 4497 |
. . . . . . . . . . . . 13
โข ((๐ + 1) โ โ โ
if((๐ + 1) โ โ,
(1 / (๐ + 1)), 0) = (1 /
(๐ + 1))) |
232 | 231 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ if((๐ + 1) โ โ, (1 /
(๐ + 1)), 0) = (1 / (๐ + 1))) |
233 | 232 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)) = (๐ ยท (1 / (๐ + 1)))) |
234 | 217, 230,
233 | 3brtr4d 5142 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง (๐ + 1) โ โ) โ
(โฏโ(๐โ(๐ + 1))) โค (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
235 | 29 | a1i 11 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ 0
โค 0) |
236 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
โข (((๐ + 1) โ โ โง
(๐ + 1) โฅ ๐) โ (๐ + 1) โ โ) |
237 | 236 | con3i 154 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
(๐ + 1) โ โ
โ ยฌ ((๐ + 1)
โ โ โง (๐ +
1) โฅ ๐)) |
238 | 237 | ralrimivw 3148 |
. . . . . . . . . . . . . . 15
โข (ยฌ
(๐ + 1) โ โ
โ โ๐ โ
(1...๐) ยฌ ((๐ + 1) โ โ โง
(๐ + 1) โฅ ๐)) |
239 | | rabeq0 4349 |
. . . . . . . . . . . . . . 15
โข ({๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)} = โ
โ โ๐ โ (1...๐) ยฌ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)) |
240 | 238, 239 | sylibr 233 |
. . . . . . . . . . . . . 14
โข (ยฌ
(๐ + 1) โ โ
โ {๐ โ (1...๐) โฃ ((๐ + 1) โ โ โง (๐ + 1) โฅ ๐)} = โ
) |
241 | 224, 240 | sylan9eq 2797 |
. . . . . . . . . . . . 13
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ
(๐โ(๐ + 1)) =
โ
) |
242 | 241 | fveq2d 6851 |
. . . . . . . . . . . 12
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ
(โฏโ(๐โ(๐ + 1))) =
(โฏโโ
)) |
243 | 242, 46 | eqtrdi 2793 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ
(โฏโ(๐โ(๐ + 1))) = 0) |
244 | | iffalse 4500 |
. . . . . . . . . . . . 13
โข (ยฌ
(๐ + 1) โ โ
โ if((๐ + 1) โ
โ, (1 / (๐ + 1)), 0)
= 0) |
245 | 244 | oveq2d 7378 |
. . . . . . . . . . . 12
โข (ยฌ
(๐ + 1) โ โ
โ (๐ ยท
if((๐ + 1) โ โ,
(1 / (๐ + 1)), 0)) = (๐ ยท 0)) |
246 | 32 | adantr 482 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท 0) = 0) |
247 | 245, 246 | sylan9eqr 2799 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ
(๐ ยท if((๐ + 1) โ โ, (1 /
(๐ + 1)), 0)) =
0) |
248 | 235, 243,
247 | 3brtr4d 5142 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ยฌ (๐ + 1) โ โ) โ
(โฏโ(๐โ(๐ + 1))) โค (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
249 | 234, 248 | pm2.61dan 812 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (โฏโ(๐โ(๐ + 1))) โค (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) |
250 | 150, 97, 79, 249 | leadd2dd 11777 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (โฏโ(๐โ(๐ + 1)))) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)))) |
251 | 137, 151,
152, 173, 250 | letrd 11319 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0)))) |
252 | | fzfid 13885 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ((๐พ + 1)...(๐ + 1)) โ Fin) |
253 | 57, 88 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ (โคโฅโ(๐พ + 1))) โ if(๐ โ โ, (1 / ๐), 0) โ
โ) |
254 | 101, 102,
253 | syl2an 597 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ (โคโฅโ๐พ)) โง ๐ โ ((๐พ + 1)...(๐ + 1))) โ if(๐ โ โ, (1 / ๐), 0) โ โ) |
255 | 252, 254 | fsumrecl 15626 |
. . . . . . . . 9
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0) โ โ) |
256 | 81, 255 | remulcld 11192 |
. . . . . . . 8
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) โ โ) |
257 | | letr 11256 |
. . . . . . . 8
โข
(((โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โ โ โง
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โ โ
โง (๐ ยท
ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) โ โ) โ
(((โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โง
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
258 | 137, 152,
256, 257 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(((โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โง
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
259 | 251, 258 | mpand 694 |
. . . . . 6
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
(((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) + (๐ ยท if((๐ + 1) โ โ, (1 / (๐ + 1)), 0))) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
260 | 127, 259 | sylbid 239 |
. . . . 5
โข ((๐ โง ๐ โ (โคโฅโ๐พ)) โ
((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0)))) |
261 | 260 | expcom 415 |
. . . 4
โข (๐ โ
(โคโฅโ๐พ) โ (๐ โ ((โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)) โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))))) |
262 | 261 | a2d 29 |
. . 3
โข (๐ โ
(โคโฅโ๐พ) โ ((๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0))) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...(๐ + 1))(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...(๐ + 1))if(๐ โ โ, (1 / ๐), 0))))) |
263 | 7, 14, 21, 28, 52, 262 | uzind4i 12842 |
. 2
โข (๐ โ
(โคโฅโ๐พ) โ (๐ โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |
264 | 263 | com12 32 |
1
โข (๐ โ (๐ โ (โคโฅโ๐พ) โ (โฏโโช ๐ โ ((๐พ + 1)...๐)(๐โ๐)) โค (๐ ยท ฮฃ๐ โ ((๐พ + 1)...๐)if(๐ โ โ, (1 / ๐), 0)))) |