Step | Hyp | Ref
| Expression |
1 | | mbfi1fseq.1 |
. . 3
โข (๐ โ ๐น โ MblFn) |
2 | | mbfi1fseq.2 |
. . 3
โข (๐ โ ๐น:โโถ(0[,)+โ)) |
3 | | mbfi1fseq.3 |
. . 3
โข ๐ฝ = (๐ โ โ, ๐ฆ โ โ โฆ
((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐))) |
4 | | mbfi1fseq.4 |
. . 3
โข ๐บ = (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))) |
5 | 1, 2, 3, 4 | mbfi1fseqlem4 25106 |
. 2
โข (๐ โ ๐บ:โโถdom
โซ1) |
6 | 1, 2, 3, 4 | mbfi1fseqlem5 25107 |
. . 3
โข ((๐ โง ๐ โ โ) โ
(0๐ โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1)))) |
7 | 6 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ โ โ (0๐
โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1)))) |
8 | | simpr 486 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
9 | 8 | recnd 11191 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ๐ฅ โ โ) |
10 | 9 | abscld 15330 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ (absโ๐ฅ) โ
โ) |
11 | 2 | ffvelcdmda 7039 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐นโ๐ฅ) โ (0[,)+โ)) |
12 | | elrege0 13380 |
. . . . . . . 8
โข ((๐นโ๐ฅ) โ (0[,)+โ) โ ((๐นโ๐ฅ) โ โ โง 0 โค (๐นโ๐ฅ))) |
13 | 11, 12 | sylib 217 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ((๐นโ๐ฅ) โ โ โง 0 โค (๐นโ๐ฅ))) |
14 | 13 | simpld 496 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ (๐นโ๐ฅ) โ โ) |
15 | 10, 14 | readdcld 11192 |
. . . . 5
โข ((๐ โง ๐ฅ โ โ) โ ((absโ๐ฅ) + (๐นโ๐ฅ)) โ โ) |
16 | | arch 12418 |
. . . . 5
โข
(((absโ๐ฅ) +
(๐นโ๐ฅ)) โ โ โ โ๐ โ โ
((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐) |
17 | 15, 16 | syl 17 |
. . . 4
โข ((๐ โง ๐ฅ โ โ) โ โ๐ โ โ
((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐) |
18 | | eqid 2733 |
. . . . 5
โข
(โคโฅโ๐) = (โคโฅโ๐) |
19 | | nnz 12528 |
. . . . . 6
โข (๐ โ โ โ ๐ โ
โค) |
20 | 19 | ad2antrl 727 |
. . . . 5
โข (((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โ ๐ โ โค) |
21 | | nnuz 12814 |
. . . . . . . 8
โข โ =
(โคโฅโ1) |
22 | | 1zzd 12542 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ 1 โ
โค) |
23 | | halfcn 12376 |
. . . . . . . . . 10
โข (1 / 2)
โ โ |
24 | 23 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ (1 / 2) โ
โ) |
25 | | halfre 12375 |
. . . . . . . . . . . 12
โข (1 / 2)
โ โ |
26 | | halfge0 12378 |
. . . . . . . . . . . 12
โข 0 โค (1
/ 2) |
27 | | absid 15190 |
. . . . . . . . . . . 12
โข (((1 / 2)
โ โ โง 0 โค (1 / 2)) โ (absโ(1 / 2)) = (1 /
2)) |
28 | 25, 26, 27 | mp2an 691 |
. . . . . . . . . . 11
โข
(absโ(1 / 2)) = (1 / 2) |
29 | | halflt1 12379 |
. . . . . . . . . . 11
โข (1 / 2)
< 1 |
30 | 28, 29 | eqbrtri 5130 |
. . . . . . . . . 10
โข
(absโ(1 / 2)) < 1 |
31 | 30 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ๐ฅ โ โ) โ (absโ(1 / 2))
< 1) |
32 | 24, 31 | expcnv 15757 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ โ0 โฆ ((1 /
2)โ๐)) โ
0) |
33 | 14 | recnd 11191 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐นโ๐ฅ) โ โ) |
34 | | nnex 12167 |
. . . . . . . . . 10
โข โ
โ V |
35 | 34 | mptex 7177 |
. . . . . . . . 9
โข (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) โ V |
36 | 35 | a1i 11 |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) โ V) |
37 | | nnnn0 12428 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ๐ โ โ0) |
39 | | oveq2 7369 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((1 / 2)โ๐) = ((1 / 2)โ๐)) |
40 | | eqid 2733 |
. . . . . . . . . . 11
โข (๐ โ โ0
โฆ ((1 / 2)โ๐)) =
(๐ โ
โ0 โฆ ((1 / 2)โ๐)) |
41 | | ovex 7394 |
. . . . . . . . . . 11
โข ((1 /
2)โ๐) โ
V |
42 | 39, 40, 41 | fvmpt 6952 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ((๐ โ
โ0 โฆ ((1 / 2)โ๐))โ๐) = ((1 / 2)โ๐)) |
43 | 38, 42 | syl 17 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) = ((1 / 2)โ๐)) |
44 | | expcl 13994 |
. . . . . . . . . 10
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
45 | 23, 38, 44 | sylancr 588 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((1 / 2)โ๐) โ
โ) |
46 | 43, 45 | eqeltrd 2834 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐) โ
โ) |
47 | 39 | oveq2d 7377 |
. . . . . . . . . . 11
โข (๐ = ๐ โ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) = ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
48 | | eqid 2733 |
. . . . . . . . . . 11
โข (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) = (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
49 | | ovex 7394 |
. . . . . . . . . . 11
โข ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) โ V |
50 | 47, 48, 49 | fvmpt 6952 |
. . . . . . . . . 10
โข (๐ โ โ โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) = ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
51 | 50 | adantl 483 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) = ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
52 | 43 | oveq2d 7377 |
. . . . . . . . 9
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((๐นโ๐ฅ) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐)) = ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
53 | 51, 52 | eqtr4d 2776 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง ๐ โ โ) โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) = ((๐นโ๐ฅ) โ ((๐ โ โ0 โฆ ((1 /
2)โ๐))โ๐))) |
54 | 21, 22, 32, 33, 36, 46, 53 | climsubc2 15530 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) โ ((๐นโ๐ฅ) โ 0)) |
55 | 33 | subid1d 11509 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ โ) โ ((๐นโ๐ฅ) โ 0) = (๐นโ๐ฅ)) |
56 | 54, 55 | breqtrd 5135 |
. . . . . 6
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) โ (๐นโ๐ฅ)) |
57 | 56 | adantr 482 |
. . . . 5
โข (((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โ (๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) โ (๐นโ๐ฅ)) |
58 | 34 | mptex 7177 |
. . . . . 6
โข (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ V |
59 | 58 | a1i 11 |
. . . . 5
โข (((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ V) |
60 | | simprl 770 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โ ๐ โ โ) |
61 | | eluznn 12851 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ โ
(โคโฅโ๐)) โ ๐ โ โ) |
62 | 60, 61 | sylan 581 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
63 | 62, 50 | syl 17 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) = ((๐นโ๐ฅ) โ ((1 / 2)โ๐))) |
64 | 14 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โ โ) |
65 | 62, 37 | syl 17 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ0) |
66 | | reexpcl 13993 |
. . . . . . . 8
โข (((1 / 2)
โ โ โง ๐
โ โ0) โ ((1 / 2)โ๐) โ โ) |
67 | 25, 65, 66 | sylancr 588 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((1 / 2)โ๐) โ
โ) |
68 | 64, 67 | resubcld 11591 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) โ โ) |
69 | 63, 68 | eqeltrd 2834 |
. . . . 5
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) โ โ) |
70 | | fveq2 6846 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐บโ๐) = (๐บโ๐)) |
71 | 70 | fveq1d 6848 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐บโ๐)โ๐ฅ) = ((๐บโ๐)โ๐ฅ)) |
72 | | eqid 2733 |
. . . . . . . 8
โข (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) = (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) |
73 | | fvex 6859 |
. . . . . . . 8
โข ((๐บโ๐)โ๐ฅ) โ V |
74 | 71, 72, 73 | fvmpt 6952 |
. . . . . . 7
โข (๐ โ โ โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) = ((๐บโ๐)โ๐ฅ)) |
75 | 62, 74 | syl 17 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) = ((๐บโ๐)โ๐ฅ)) |
76 | 5 | ad3antrrr 729 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐บ:โโถdom
โซ1) |
77 | 76, 62 | ffvelcdmd 7040 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) โ dom
โซ1) |
78 | | i1ff 25063 |
. . . . . . . 8
โข ((๐บโ๐) โ dom โซ1 โ (๐บโ๐):โโถโ) |
79 | 77, 78 | syl 17 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐):โโถโ) |
80 | 8 | ad2antrr 725 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ฅ โ โ) |
81 | 79, 80 | ffvelcdmd 7040 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐บโ๐)โ๐ฅ) โ โ) |
82 | 75, 81 | eqeltrd 2834 |
. . . . 5
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) โ โ) |
83 | 33 | ad2antrr 725 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โ โ) |
84 | | 2nn 12234 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
85 | | nnexpcl 13989 |
. . . . . . . . . . . . . 14
โข ((2
โ โ โง ๐
โ โ0) โ (2โ๐) โ โ) |
86 | 84, 65, 85 | sylancr 588 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (2โ๐) โ
โ) |
87 | 86 | nnred 12176 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (2โ๐) โ
โ) |
88 | 87 | recnd 11191 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (2โ๐) โ
โ) |
89 | 86 | nnne0d 12211 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (2โ๐) โ 0) |
90 | 83, 88, 89 | divcan4d 11945 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (((๐นโ๐ฅ) ยท (2โ๐)) / (2โ๐)) = (๐นโ๐ฅ)) |
91 | 90 | eqcomd 2739 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) = (((๐นโ๐ฅ) ยท (2โ๐)) / (2โ๐))) |
92 | | 2cnd 12239 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 2 โ
โ) |
93 | | 2ne0 12265 |
. . . . . . . . . . 11
โข 2 โ
0 |
94 | 93 | a1i 11 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 2 โ
0) |
95 | | eluzelz 12781 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ๐) โ ๐ โ โค) |
96 | 95 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โค) |
97 | 92, 94, 96 | exprecd 14068 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((1 / 2)โ๐) = (1 / (2โ๐))) |
98 | 91, 97 | oveq12d 7379 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) = ((((๐นโ๐ฅ) ยท (2โ๐)) / (2โ๐)) โ (1 / (2โ๐)))) |
99 | 64, 87 | remulcld 11193 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) ยท (2โ๐)) โ โ) |
100 | 99 | recnd 11191 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) ยท (2โ๐)) โ โ) |
101 | | 1cnd 11158 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 1 โ
โ) |
102 | 100, 101,
88, 89 | divsubdird 11978 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) / (2โ๐)) = ((((๐นโ๐ฅ) ยท (2โ๐)) / (2โ๐)) โ (1 / (2โ๐)))) |
103 | 98, 102 | eqtr4d 2776 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) = ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) / (2โ๐))) |
104 | | fllep1 13715 |
. . . . . . . . . 10
โข (((๐นโ๐ฅ) ยท (2โ๐)) โ โ โ ((๐นโ๐ฅ) ยท (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) + 1)) |
105 | 99, 104 | syl 17 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) ยท (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) + 1)) |
106 | | 1red 11164 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 1 โ
โ) |
107 | | reflcl 13710 |
. . . . . . . . . . 11
โข (((๐นโ๐ฅ) ยท (2โ๐)) โ โ โ
(โโ((๐นโ๐ฅ) ยท (2โ๐))) โ โ) |
108 | 99, 107 | syl 17 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (โโ((๐นโ๐ฅ) ยท (2โ๐))) โ โ) |
109 | 99, 106, 108 | lesubaddd 11760 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โค (โโ((๐นโ๐ฅ) ยท (2โ๐))) โ ((๐นโ๐ฅ) ยท (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) + 1))) |
110 | 105, 109 | mpbird 257 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โค (โโ((๐นโ๐ฅ) ยท (2โ๐)))) |
111 | | peano2rem 11476 |
. . . . . . . . . 10
โข (((๐นโ๐ฅ) ยท (2โ๐)) โ โ โ (((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โ
โ) |
112 | 99, 111 | syl 17 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โ
โ) |
113 | 86 | nngt0d 12210 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 0 < (2โ๐)) |
114 | | lediv1 12028 |
. . . . . . . . 9
โข
(((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โ โ
โง (โโ((๐นโ๐ฅ) ยท (2โ๐))) โ โ โง ((2โ๐) โ โ โง 0 <
(2โ๐))) โ
((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โค
(โโ((๐นโ๐ฅ) ยท (2โ๐))) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) / (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)))) |
115 | 112, 108,
87, 113, 114 | syl112anc 1375 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) โค (โโ((๐นโ๐ฅ) ยท (2โ๐))) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) / (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)))) |
116 | 110, 115 | mpbid 231 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((((๐นโ๐ฅ) ยท (2โ๐)) โ 1) / (2โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
117 | 103, 116 | eqbrtrd 5131 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)) โค ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
118 | 1, 2, 3, 4 | mbfi1fseqlem2 25104 |
. . . . . . . . . 10
โข (๐ โ โ โ (๐บโ๐) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))) |
119 | 62, 118 | syl 17 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐บโ๐) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))) |
120 | 119 | fveq1d 6848 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐บโ๐)โ๐ฅ) = ((๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))โ๐ฅ)) |
121 | | ovex 7394 |
. . . . . . . . . . 11
โข (๐๐ฝ๐ฅ) โ V |
122 | | vex 3451 |
. . . . . . . . . . 11
โข ๐ โ V |
123 | 121, 122 | ifex 4540 |
. . . . . . . . . 10
โข if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐) โ V |
124 | | c0ex 11157 |
. . . . . . . . . 10
โข 0 โ
V |
125 | 123, 124 | ifex 4540 |
. . . . . . . . 9
โข if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0) โ V |
126 | | eqid 2733 |
. . . . . . . . . 10
โข (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0)) |
127 | 126 | fvmpt2 6963 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0) โ V) โ ((๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))โ๐ฅ) = if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0)) |
128 | 80, 125, 127 | sylancl 587 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))โ๐ฅ) = if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0)) |
129 | 75, 120, 128 | 3eqtrd 2777 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) = if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0)) |
130 | 10 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (absโ๐ฅ) โ
โ) |
131 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ฅ) + (๐นโ๐ฅ)) โ โ) |
132 | 62 | nnred 12176 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
133 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โ (0[,)+โ)) |
134 | 133, 12 | sylib 217 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐นโ๐ฅ) โ โ โง 0 โค (๐นโ๐ฅ))) |
135 | 134 | simprd 497 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 0 โค (๐นโ๐ฅ)) |
136 | 130, 64 | addge01d 11751 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (0 โค (๐นโ๐ฅ) โ (absโ๐ฅ) โค ((absโ๐ฅ) + (๐นโ๐ฅ)))) |
137 | 135, 136 | mpbid 231 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (absโ๐ฅ) โค ((absโ๐ฅ) + (๐นโ๐ฅ))) |
138 | 60 | adantr 482 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
139 | 138 | nnred 12176 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) |
140 | | simplrr 777 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐) |
141 | 131, 139,
140 | ltled 11311 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ฅ) + (๐นโ๐ฅ)) โค ๐) |
142 | | eluzle 12784 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ๐) โ ๐ โค ๐) |
143 | 142 | adantl 483 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ โค ๐) |
144 | 131, 139,
132, 141, 143 | letrd 11320 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ฅ) + (๐นโ๐ฅ)) โค ๐) |
145 | 130, 131,
132, 137, 144 | letrd 11320 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (absโ๐ฅ) โค ๐) |
146 | 80, 132 | absled 15324 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((absโ๐ฅ) โค ๐ โ (-๐ โค ๐ฅ โง ๐ฅ โค ๐))) |
147 | 145, 146 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (-๐ โค ๐ฅ โง ๐ฅ โค ๐)) |
148 | 147 | simpld 496 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ -๐ โค ๐ฅ) |
149 | 147 | simprd 497 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ฅ โค ๐) |
150 | 132 | renegcld 11590 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ -๐ โ โ) |
151 | | elicc2 13338 |
. . . . . . . . . 10
โข ((-๐ โ โ โง ๐ โ โ) โ (๐ฅ โ (-๐[,]๐) โ (๐ฅ โ โ โง -๐ โค ๐ฅ โง ๐ฅ โค ๐))) |
152 | 150, 132,
151 | syl2anc 585 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐ฅ โ (-๐[,]๐) โ (๐ฅ โ โ โง -๐ โค ๐ฅ โง ๐ฅ โค ๐))) |
153 | 80, 148, 149, 152 | mpbir3and 1343 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ฅ โ (-๐[,]๐)) |
154 | 153 | iftrued 4498 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0) = if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐)) |
155 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ ๐ฆ = ๐ฅ) |
156 | 155 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ (๐นโ๐ฆ) = (๐นโ๐ฅ)) |
157 | | simpl 484 |
. . . . . . . . . . . . . . . 16
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ ๐ = ๐) |
158 | 157 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ (2โ๐) = (2โ๐)) |
159 | 156, 158 | oveq12d 7379 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ ((๐นโ๐ฆ) ยท (2โ๐)) = ((๐นโ๐ฅ) ยท (2โ๐))) |
160 | 159 | fveq2d 6850 |
. . . . . . . . . . . . 13
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ (โโ((๐นโ๐ฆ) ยท (2โ๐))) = (โโ((๐นโ๐ฅ) ยท (2โ๐)))) |
161 | 160, 158 | oveq12d 7379 |
. . . . . . . . . . . 12
โข ((๐ = ๐ โง ๐ฆ = ๐ฅ) โ ((โโ((๐นโ๐ฆ) ยท (2โ๐))) / (2โ๐)) = ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
162 | | ovex 7394 |
. . . . . . . . . . . 12
โข
((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โ V |
163 | 161, 3, 162 | ovmpoa 7514 |
. . . . . . . . . . 11
โข ((๐ โ โ โง ๐ฅ โ โ) โ (๐๐ฝ๐ฅ) = ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
164 | 62, 80, 163 | syl2anc 585 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐๐ฝ๐ฅ) = ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
165 | 108, 86 | nndivred 12215 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ
((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โ โ) |
166 | | flle 13713 |
. . . . . . . . . . . . 13
โข (((๐นโ๐ฅ) ยท (2โ๐)) โ โ โ
(โโ((๐นโ๐ฅ) ยท (2โ๐))) โค ((๐นโ๐ฅ) ยท (2โ๐))) |
167 | 99, 166 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (โโ((๐นโ๐ฅ) ยท (2โ๐))) โค ((๐นโ๐ฅ) ยท (2โ๐))) |
168 | | ledivmul2 12042 |
. . . . . . . . . . . . 13
โข
(((โโ((๐นโ๐ฅ) ยท (2โ๐))) โ โ โง (๐นโ๐ฅ) โ โ โง ((2โ๐) โ โ โง 0 <
(2โ๐))) โ
(((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โค (๐นโ๐ฅ) โ (โโ((๐นโ๐ฅ) ยท (2โ๐))) โค ((๐นโ๐ฅ) ยท (2โ๐)))) |
169 | 108, 64, 87, 113, 168 | syl112anc 1375 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ
(((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โค (๐นโ๐ฅ) โ (โโ((๐นโ๐ฅ) ยท (2โ๐))) โค ((๐นโ๐ฅ) ยท (2โ๐)))) |
170 | 167, 169 | mpbird 257 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ
((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โค (๐นโ๐ฅ)) |
171 | 9 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ๐ฅ โ โ) |
172 | 171 | absge0d 15338 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ 0 โค
(absโ๐ฅ)) |
173 | 64, 130 | addge02d 11752 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (0 โค
(absโ๐ฅ) โ (๐นโ๐ฅ) โค ((absโ๐ฅ) + (๐นโ๐ฅ)))) |
174 | 172, 173 | mpbid 231 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โค ((absโ๐ฅ) + (๐นโ๐ฅ))) |
175 | 64, 131, 132, 174, 144 | letrd 11320 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐นโ๐ฅ) โค ๐) |
176 | 165, 64, 132, 170, 175 | letrd 11320 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ
((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐)) โค ๐) |
177 | 164, 176 | eqbrtrd 5131 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ (๐๐ฝ๐ฅ) โค ๐) |
178 | 177 | iftrued 4498 |
. . . . . . . 8
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐) = (๐๐ฝ๐ฅ)) |
179 | 178, 164 | eqtrd 2773 |
. . . . . . 7
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐) = ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
180 | 129, 154,
179 | 3eqtrd 2777 |
. . . . . 6
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) = ((โโ((๐นโ๐ฅ) ยท (2โ๐))) / (2โ๐))) |
181 | 117, 63, 180 | 3brtr4d 5141 |
. . . . 5
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐นโ๐ฅ) โ ((1 / 2)โ๐)))โ๐) โค ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐)) |
182 | 180, 170 | eqbrtrd 5131 |
. . . . 5
โข ((((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โง ๐ โ (โคโฅโ๐)) โ ((๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))โ๐) โค (๐นโ๐ฅ)) |
183 | 18, 20, 57, 59, 69, 82, 181, 182 | climsqz 15532 |
. . . 4
โข (((๐ โง ๐ฅ โ โ) โง (๐ โ โ โง ((absโ๐ฅ) + (๐นโ๐ฅ)) < ๐)) โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ)) |
184 | 17, 183 | rexlimddv 3155 |
. . 3
โข ((๐ โง ๐ฅ โ โ) โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ)) |
185 | 184 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ฅ โ โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ)) |
186 | 34 | mptex 7177 |
. . . 4
โข (๐ โ โ โฆ (๐ฅ โ โ โฆ if(๐ฅ โ (-๐[,]๐), if((๐๐ฝ๐ฅ) โค ๐, (๐๐ฝ๐ฅ), ๐), 0))) โ V |
187 | 4, 186 | eqeltri 2830 |
. . 3
โข ๐บ โ V |
188 | | feq1 6653 |
. . . 4
โข (๐ = ๐บ โ (๐:โโถdom โซ1 โ
๐บ:โโถdom
โซ1)) |
189 | | fveq1 6845 |
. . . . . . 7
โข (๐ = ๐บ โ (๐โ๐) = (๐บโ๐)) |
190 | 189 | breq2d 5121 |
. . . . . 6
โข (๐ = ๐บ โ (0๐
โr โค (๐โ๐) โ 0๐
โr โค (๐บโ๐))) |
191 | | fveq1 6845 |
. . . . . . 7
โข (๐ = ๐บ โ (๐โ(๐ + 1)) = (๐บโ(๐ + 1))) |
192 | 189, 191 | breq12d 5122 |
. . . . . 6
โข (๐ = ๐บ โ ((๐โ๐) โr โค (๐โ(๐ + 1)) โ (๐บโ๐) โr โค (๐บโ(๐ + 1)))) |
193 | 190, 192 | anbi12d 632 |
. . . . 5
โข (๐ = ๐บ โ ((0๐
โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โ (0๐
โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1))))) |
194 | 193 | ralbidv 3171 |
. . . 4
โข (๐ = ๐บ โ (โ๐ โ โ (0๐
โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โ โ๐ โ โ (0๐
โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1))))) |
195 | 189 | fveq1d 6848 |
. . . . . . 7
โข (๐ = ๐บ โ ((๐โ๐)โ๐ฅ) = ((๐บโ๐)โ๐ฅ)) |
196 | 195 | mpteq2dv 5211 |
. . . . . 6
โข (๐ = ๐บ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) = (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ))) |
197 | 196 | breq1d 5119 |
. . . . 5
โข (๐ = ๐บ โ ((๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ) โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ))) |
198 | 197 | ralbidv 3171 |
. . . 4
โข (๐ = ๐บ โ (โ๐ฅ โ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ) โ โ๐ฅ โ โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ))) |
199 | 188, 194,
198 | 3anbi123d 1437 |
. . 3
โข (๐ = ๐บ โ ((๐:โโถdom โซ1 โง
โ๐ โ โ
(0๐ โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ)) โ (๐บ:โโถdom โซ1 โง
โ๐ โ โ
(0๐ โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ)))) |
200 | 187, 199 | spcev 3567 |
. 2
โข ((๐บ:โโถdom
โซ1 โง โ๐ โ โ (0๐
โr โค (๐บโ๐) โง (๐บโ๐) โr โค (๐บโ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐บโ๐)โ๐ฅ)) โ (๐นโ๐ฅ)) โ โ๐(๐:โโถdom โซ1 โง
โ๐ โ โ
(0๐ โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ))) |
201 | 5, 7, 185, 200 | syl3anc 1372 |
1
โข (๐ โ โ๐(๐:โโถdom โซ1 โง
โ๐ โ โ
(0๐ โr โค (๐โ๐) โง (๐โ๐) โr โค (๐โ(๐ + 1))) โง โ๐ฅ โ โ (๐ โ โ โฆ ((๐โ๐)โ๐ฅ)) โ (๐นโ๐ฅ))) |