Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . . 5
โข i โ
โ |
2 | | 0xr 11209 |
. . . . . . . 8
โข 0 โ
โ* |
3 | | 1re 11162 |
. . . . . . . 8
โข 1 โ
โ |
4 | | elioc2 13334 |
. . . . . . . 8
โข ((0
โ โ* โง 1 โ โ) โ (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 < ๐ด โง ๐ด โค 1))) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ (๐ด โ โ โง 0 <
๐ด โง ๐ด โค 1)) |
6 | 5 | simp1bi 1146 |
. . . . . 6
โข (๐ด โ (0(,]1) โ ๐ด โ
โ) |
7 | 6 | recnd 11190 |
. . . . 5
โข (๐ด โ (0(,]1) โ ๐ด โ
โ) |
8 | | mulcl 11142 |
. . . . 5
โข ((i
โ โ โง ๐ด
โ โ) โ (i ยท ๐ด) โ โ) |
9 | 1, 7, 8 | sylancr 588 |
. . . 4
โข (๐ด โ (0(,]1) โ (i
ยท ๐ด) โ
โ) |
10 | | 4nn0 12439 |
. . . 4
โข 4 โ
โ0 |
11 | | ef01bnd.1 |
. . . . 5
โข ๐น = (๐ โ โ0 โฆ (((i
ยท ๐ด)โ๐) / (!โ๐))) |
12 | 11 | eftlcl 15996 |
. . . 4
โข (((i
ยท ๐ด) โ โ
โง 4 โ โ0) โ ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐) โ โ) |
13 | 9, 10, 12 | sylancl 587 |
. . 3
โข (๐ด โ (0(,]1) โ
ฮฃ๐ โ
(โคโฅโ4)(๐นโ๐) โ โ) |
14 | 13 | abscld 15328 |
. 2
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)) โ โ) |
15 | | reexpcl 13991 |
. . . 4
โข ((๐ด โ โ โง 4 โ
โ0) โ (๐ดโ4) โ โ) |
16 | 6, 10, 15 | sylancl 587 |
. . 3
โข (๐ด โ (0(,]1) โ (๐ดโ4) โ
โ) |
17 | | 4re 12244 |
. . . . 5
โข 4 โ
โ |
18 | 17, 3 | readdcli 11177 |
. . . 4
โข (4 + 1)
โ โ |
19 | | faccl 14190 |
. . . . . 6
โข (4 โ
โ0 โ (!โ4) โ โ) |
20 | 10, 19 | ax-mp 5 |
. . . . 5
โข
(!โ4) โ โ |
21 | | 4nn 12243 |
. . . . 5
โข 4 โ
โ |
22 | 20, 21 | nnmulcli 12185 |
. . . 4
โข
((!โ4) ยท 4) โ โ |
23 | | nndivre 12201 |
. . . 4
โข (((4 + 1)
โ โ โง ((!โ4) ยท 4) โ โ) โ ((4 + 1) /
((!โ4) ยท 4)) โ โ) |
24 | 18, 22, 23 | mp2an 691 |
. . 3
โข ((4 + 1)
/ ((!โ4) ยท 4)) โ โ |
25 | | remulcl 11143 |
. . 3
โข (((๐ดโ4) โ โ โง
((4 + 1) / ((!โ4) ยท 4)) โ โ) โ ((๐ดโ4) ยท ((4 + 1) / ((!โ4)
ยท 4))) โ โ) |
26 | 16, 24, 25 | sylancl 587 |
. 2
โข (๐ด โ (0(,]1) โ ((๐ดโ4) ยท ((4 + 1) /
((!โ4) ยท 4))) โ โ) |
27 | | 6nn 12249 |
. . 3
โข 6 โ
โ |
28 | | nndivre 12201 |
. . 3
โข (((๐ดโ4) โ โ โง 6
โ โ) โ ((๐ดโ4) / 6) โ
โ) |
29 | 16, 27, 28 | sylancl 587 |
. 2
โข (๐ด โ (0(,]1) โ ((๐ดโ4) / 6) โ
โ) |
30 | | eqid 2737 |
. . . 4
โข (๐ โ โ0
โฆ (((absโ(i ยท ๐ด))โ๐) / (!โ๐))) = (๐ โ โ0 โฆ
(((absโ(i ยท ๐ด))โ๐) / (!โ๐))) |
31 | | eqid 2737 |
. . . 4
โข (๐ โ โ0
โฆ ((((absโ(i ยท ๐ด))โ4) / (!โ4)) ยท ((1 / (4
+ 1))โ๐))) = (๐ โ โ0
โฆ ((((absโ(i ยท ๐ด))โ4) / (!โ4)) ยท ((1 / (4
+ 1))โ๐))) |
32 | 21 | a1i 11 |
. . . 4
โข (๐ด โ (0(,]1) โ 4 โ
โ) |
33 | | absmul 15186 |
. . . . . . 7
โข ((i
โ โ โง ๐ด
โ โ) โ (absโ(i ยท ๐ด)) = ((absโi) ยท
(absโ๐ด))) |
34 | 1, 7, 33 | sylancr 588 |
. . . . . 6
โข (๐ด โ (0(,]1) โ
(absโ(i ยท ๐ด))
= ((absโi) ยท (absโ๐ด))) |
35 | | absi 15178 |
. . . . . . . 8
โข
(absโi) = 1 |
36 | 35 | oveq1i 7372 |
. . . . . . 7
โข
((absโi) ยท (absโ๐ด)) = (1 ยท (absโ๐ด)) |
37 | 5 | simp2bi 1147 |
. . . . . . . . . 10
โข (๐ด โ (0(,]1) โ 0 <
๐ด) |
38 | 6, 37 | elrpd 12961 |
. . . . . . . . 9
โข (๐ด โ (0(,]1) โ ๐ด โ
โ+) |
39 | | rpre 12930 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ ๐ด โ
โ) |
40 | | rpge0 12935 |
. . . . . . . . . 10
โข (๐ด โ โ+
โ 0 โค ๐ด) |
41 | 39, 40 | absidd 15314 |
. . . . . . . . 9
โข (๐ด โ โ+
โ (absโ๐ด) =
๐ด) |
42 | 38, 41 | syl 17 |
. . . . . . . 8
โข (๐ด โ (0(,]1) โ
(absโ๐ด) = ๐ด) |
43 | 42 | oveq2d 7378 |
. . . . . . 7
โข (๐ด โ (0(,]1) โ (1
ยท (absโ๐ด)) =
(1 ยท ๐ด)) |
44 | 36, 43 | eqtrid 2789 |
. . . . . 6
โข (๐ด โ (0(,]1) โ
((absโi) ยท (absโ๐ด)) = (1 ยท ๐ด)) |
45 | 7 | mulid2d 11180 |
. . . . . 6
โข (๐ด โ (0(,]1) โ (1
ยท ๐ด) = ๐ด) |
46 | 34, 44, 45 | 3eqtrd 2781 |
. . . . 5
โข (๐ด โ (0(,]1) โ
(absโ(i ยท ๐ด))
= ๐ด) |
47 | 5 | simp3bi 1148 |
. . . . 5
โข (๐ด โ (0(,]1) โ ๐ด โค 1) |
48 | 46, 47 | eqbrtrd 5132 |
. . . 4
โข (๐ด โ (0(,]1) โ
(absโ(i ยท ๐ด))
โค 1) |
49 | 11, 30, 31, 32, 9, 48 | eftlub 15998 |
. . 3
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)) โค (((absโ(i ยท ๐ด))โ4) ยท ((4 + 1) /
((!โ4) ยท 4)))) |
50 | 46 | oveq1d 7377 |
. . . 4
โข (๐ด โ (0(,]1) โ
((absโ(i ยท ๐ด))โ4) = (๐ดโ4)) |
51 | 50 | oveq1d 7377 |
. . 3
โข (๐ด โ (0(,]1) โ
(((absโ(i ยท ๐ด))โ4) ยท ((4 + 1) / ((!โ4)
ยท 4))) = ((๐ดโ4)
ยท ((4 + 1) / ((!โ4) ยท 4)))) |
52 | 49, 51 | breqtrd 5136 |
. 2
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)) โค ((๐ดโ4) ยท ((4 + 1) / ((!โ4)
ยท 4)))) |
53 | | 3pos 12265 |
. . . . . . . . 9
โข 0 <
3 |
54 | | 0re 11164 |
. . . . . . . . . 10
โข 0 โ
โ |
55 | | 3re 12240 |
. . . . . . . . . 10
โข 3 โ
โ |
56 | | 5re 12247 |
. . . . . . . . . 10
โข 5 โ
โ |
57 | 54, 55, 56 | ltadd1i 11716 |
. . . . . . . . 9
โข (0 < 3
โ (0 + 5) < (3 + 5)) |
58 | 53, 57 | mpbi 229 |
. . . . . . . 8
โข (0 + 5)
< (3 + 5) |
59 | | 5cn 12248 |
. . . . . . . . 9
โข 5 โ
โ |
60 | 59 | addid2i 11350 |
. . . . . . . 8
โข (0 + 5) =
5 |
61 | | cu2 14111 |
. . . . . . . . 9
โข
(2โ3) = 8 |
62 | | 5p3e8 12317 |
. . . . . . . . 9
โข (5 + 3) =
8 |
63 | | 3cn 12241 |
. . . . . . . . . 10
โข 3 โ
โ |
64 | 59, 63 | addcomi 11353 |
. . . . . . . . 9
โข (5 + 3) =
(3 + 5) |
65 | 61, 62, 64 | 3eqtr2ri 2772 |
. . . . . . . 8
โข (3 + 5) =
(2โ3) |
66 | 58, 60, 65 | 3brtr3i 5139 |
. . . . . . 7
โข 5 <
(2โ3) |
67 | | 2re 12234 |
. . . . . . . 8
โข 2 โ
โ |
68 | | 1le2 12369 |
. . . . . . . 8
โข 1 โค
2 |
69 | | 4z 12544 |
. . . . . . . . 9
โข 4 โ
โค |
70 | | 3lt4 12334 |
. . . . . . . . . 10
โข 3 <
4 |
71 | 55, 17, 70 | ltleii 11285 |
. . . . . . . . 9
โข 3 โค
4 |
72 | | 3z 12543 |
. . . . . . . . . 10
โข 3 โ
โค |
73 | 72 | eluz1i 12778 |
. . . . . . . . 9
โข (4 โ
(โคโฅโ3) โ (4 โ โค โง 3 โค
4)) |
74 | 69, 71, 73 | mpbir2an 710 |
. . . . . . . 8
โข 4 โ
(โคโฅโ3) |
75 | | leexp2a 14084 |
. . . . . . . 8
โข ((2
โ โ โง 1 โค 2 โง 4 โ (โคโฅโ3))
โ (2โ3) โค (2โ4)) |
76 | 67, 68, 74, 75 | mp3an 1462 |
. . . . . . 7
โข
(2โ3) โค (2โ4) |
77 | | 8re 12256 |
. . . . . . . . 9
โข 8 โ
โ |
78 | 61, 77 | eqeltri 2834 |
. . . . . . . 8
โข
(2โ3) โ โ |
79 | | 2nn 12233 |
. . . . . . . . . 10
โข 2 โ
โ |
80 | | nnexpcl 13987 |
. . . . . . . . . 10
โข ((2
โ โ โง 4 โ โ0) โ (2โ4) โ
โ) |
81 | 79, 10, 80 | mp2an 691 |
. . . . . . . . 9
โข
(2โ4) โ โ |
82 | 81 | nnrei 12169 |
. . . . . . . 8
โข
(2โ4) โ โ |
83 | 56, 78, 82 | ltletri 11290 |
. . . . . . 7
โข ((5 <
(2โ3) โง (2โ3) โค (2โ4)) โ 5 <
(2โ4)) |
84 | 66, 76, 83 | mp2an 691 |
. . . . . 6
โข 5 <
(2โ4) |
85 | | 6re 12250 |
. . . . . . . 8
โข 6 โ
โ |
86 | 85, 82 | remulcli 11178 |
. . . . . . 7
โข (6
ยท (2โ4)) โ โ |
87 | | 6pos 12270 |
. . . . . . . 8
โข 0 <
6 |
88 | 81 | nngt0i 12199 |
. . . . . . . 8
โข 0 <
(2โ4) |
89 | 85, 82, 87, 88 | mulgt0ii 11295 |
. . . . . . 7
โข 0 < (6
ยท (2โ4)) |
90 | 56, 82, 86, 89 | ltdiv1ii 12091 |
. . . . . 6
โข (5 <
(2โ4) โ (5 / (6 ยท (2โ4))) < ((2โ4) / (6 ยท
(2โ4)))) |
91 | 84, 90 | mpbi 229 |
. . . . 5
โข (5 / (6
ยท (2โ4))) < ((2โ4) / (6 ยท
(2โ4))) |
92 | | df-5 12226 |
. . . . . 6
โข 5 = (4 +
1) |
93 | | df-4 12225 |
. . . . . . . . . . 11
โข 4 = (3 +
1) |
94 | 93 | fveq2i 6850 |
. . . . . . . . . 10
โข
(!โ4) = (!โ(3 + 1)) |
95 | | 3nn0 12438 |
. . . . . . . . . . 11
โข 3 โ
โ0 |
96 | | facp1 14185 |
. . . . . . . . . . 11
โข (3 โ
โ0 โ (!โ(3 + 1)) = ((!โ3) ยท (3 +
1))) |
97 | 95, 96 | ax-mp 5 |
. . . . . . . . . 10
โข
(!โ(3 + 1)) = ((!โ3) ยท (3 + 1)) |
98 | | sq2 14108 |
. . . . . . . . . . . 12
โข
(2โ2) = 4 |
99 | 98, 93 | eqtr2i 2766 |
. . . . . . . . . . 11
โข (3 + 1) =
(2โ2) |
100 | 99 | oveq2i 7373 |
. . . . . . . . . 10
โข
((!โ3) ยท (3 + 1)) = ((!โ3) ยท
(2โ2)) |
101 | 94, 97, 100 | 3eqtri 2769 |
. . . . . . . . 9
โข
(!โ4) = ((!โ3) ยท (2โ2)) |
102 | 101 | oveq1i 7372 |
. . . . . . . 8
โข
((!โ4) ยท (2โ2)) = (((!โ3) ยท (2โ2))
ยท (2โ2)) |
103 | 98 | oveq2i 7373 |
. . . . . . . 8
โข
((!โ4) ยท (2โ2)) = ((!โ4) ยท
4) |
104 | | fac3 14187 |
. . . . . . . . . 10
โข
(!โ3) = 6 |
105 | | 6cn 12251 |
. . . . . . . . . 10
โข 6 โ
โ |
106 | 104, 105 | eqeltri 2834 |
. . . . . . . . 9
โข
(!โ3) โ โ |
107 | 17 | recni 11176 |
. . . . . . . . . 10
โข 4 โ
โ |
108 | 98, 107 | eqeltri 2834 |
. . . . . . . . 9
โข
(2โ2) โ โ |
109 | 106, 108,
108 | mulassi 11173 |
. . . . . . . 8
โข
(((!โ3) ยท (2โ2)) ยท (2โ2)) = ((!โ3)
ยท ((2โ2) ยท (2โ2))) |
110 | 102, 103,
109 | 3eqtr3i 2773 |
. . . . . . 7
โข
((!โ4) ยท 4) = ((!โ3) ยท ((2โ2) ยท
(2โ2))) |
111 | | 2p2e4 12295 |
. . . . . . . . . 10
โข (2 + 2) =
4 |
112 | 111 | oveq2i 7373 |
. . . . . . . . 9
โข
(2โ(2 + 2)) = (2โ4) |
113 | | 2cn 12235 |
. . . . . . . . . 10
โข 2 โ
โ |
114 | | 2nn0 12437 |
. . . . . . . . . 10
โข 2 โ
โ0 |
115 | | expadd 14017 |
. . . . . . . . . 10
โข ((2
โ โ โง 2 โ โ0 โง 2 โ
โ0) โ (2โ(2 + 2)) = ((2โ2) ยท
(2โ2))) |
116 | 113, 114,
114, 115 | mp3an 1462 |
. . . . . . . . 9
โข
(2โ(2 + 2)) = ((2โ2) ยท (2โ2)) |
117 | 112, 116 | eqtr3i 2767 |
. . . . . . . 8
โข
(2โ4) = ((2โ2) ยท (2โ2)) |
118 | 117 | oveq2i 7373 |
. . . . . . 7
โข
((!โ3) ยท (2โ4)) = ((!โ3) ยท ((2โ2)
ยท (2โ2))) |
119 | 104 | oveq1i 7372 |
. . . . . . 7
โข
((!โ3) ยท (2โ4)) = (6 ยท
(2โ4)) |
120 | 110, 118,
119 | 3eqtr2ri 2772 |
. . . . . 6
โข (6
ยท (2โ4)) = ((!โ4) ยท 4) |
121 | 92, 120 | oveq12i 7374 |
. . . . 5
โข (5 / (6
ยท (2โ4))) = ((4 + 1) / ((!โ4) ยท 4)) |
122 | 81 | nncni 12170 |
. . . . . . . 8
โข
(2โ4) โ โ |
123 | 122 | mulid2i 11167 |
. . . . . . 7
โข (1
ยท (2โ4)) = (2โ4) |
124 | 123 | oveq1i 7372 |
. . . . . 6
โข ((1
ยท (2โ4)) / (6 ยท (2โ4))) = ((2โ4) / (6 ยท
(2โ4))) |
125 | 81 | nnne0i 12200 |
. . . . . . . . 9
โข
(2โ4) โ 0 |
126 | 122, 125 | dividi 11895 |
. . . . . . . 8
โข
((2โ4) / (2โ4)) = 1 |
127 | 126 | oveq2i 7373 |
. . . . . . 7
โข ((1 / 6)
ยท ((2โ4) / (2โ4))) = ((1 / 6) ยท 1) |
128 | | ax-1cn 11116 |
. . . . . . . 8
โข 1 โ
โ |
129 | 85, 87 | gt0ne0ii 11698 |
. . . . . . . 8
โข 6 โ
0 |
130 | 128, 105,
122, 122, 129, 125 | divmuldivi 11922 |
. . . . . . 7
โข ((1 / 6)
ยท ((2โ4) / (2โ4))) = ((1 ยท (2โ4)) / (6 ยท
(2โ4))) |
131 | 85, 129 | rereccli 11927 |
. . . . . . . . 9
โข (1 / 6)
โ โ |
132 | 131 | recni 11176 |
. . . . . . . 8
โข (1 / 6)
โ โ |
133 | 132 | mulid1i 11166 |
. . . . . . 7
โข ((1 / 6)
ยท 1) = (1 / 6) |
134 | 127, 130,
133 | 3eqtr3i 2773 |
. . . . . 6
โข ((1
ยท (2โ4)) / (6 ยท (2โ4))) = (1 / 6) |
135 | 124, 134 | eqtr3i 2767 |
. . . . 5
โข
((2โ4) / (6 ยท (2โ4))) = (1 / 6) |
136 | 91, 121, 135 | 3brtr3i 5139 |
. . . 4
โข ((4 + 1)
/ ((!โ4) ยท 4)) < (1 / 6) |
137 | | rpexpcl 13993 |
. . . . . 6
โข ((๐ด โ โ+
โง 4 โ โค) โ (๐ดโ4) โ
โ+) |
138 | 38, 69, 137 | sylancl 587 |
. . . . 5
โข (๐ด โ (0(,]1) โ (๐ดโ4) โ
โ+) |
139 | | elrp 12924 |
. . . . . 6
โข ((๐ดโ4) โ
โ+ โ ((๐ดโ4) โ โ โง 0 < (๐ดโ4))) |
140 | | ltmul2 12013 |
. . . . . . 7
โข ((((4 +
1) / ((!โ4) ยท 4)) โ โ โง (1 / 6) โ โ
โง ((๐ดโ4) โ
โ โง 0 < (๐ดโ4))) โ (((4 + 1) / ((!โ4)
ยท 4)) < (1 / 6) โ ((๐ดโ4) ยท ((4 + 1) / ((!โ4)
ยท 4))) < ((๐ดโ4) ยท (1 /
6)))) |
141 | 24, 131, 140 | mp3an12 1452 |
. . . . . 6
โข (((๐ดโ4) โ โ โง 0
< (๐ดโ4)) โ
(((4 + 1) / ((!โ4) ยท 4)) < (1 / 6) โ ((๐ดโ4) ยท ((4 + 1) / ((!โ4)
ยท 4))) < ((๐ดโ4) ยท (1 /
6)))) |
142 | 139, 141 | sylbi 216 |
. . . . 5
โข ((๐ดโ4) โ
โ+ โ (((4 + 1) / ((!โ4) ยท 4)) < (1 / 6)
โ ((๐ดโ4) ยท
((4 + 1) / ((!โ4) ยท 4))) < ((๐ดโ4) ยท (1 /
6)))) |
143 | 138, 142 | syl 17 |
. . . 4
โข (๐ด โ (0(,]1) โ (((4 + 1)
/ ((!โ4) ยท 4)) < (1 / 6) โ ((๐ดโ4) ยท ((4 + 1) / ((!โ4)
ยท 4))) < ((๐ดโ4) ยท (1 /
6)))) |
144 | 136, 143 | mpbii 232 |
. . 3
โข (๐ด โ (0(,]1) โ ((๐ดโ4) ยท ((4 + 1) /
((!โ4) ยท 4))) < ((๐ดโ4) ยท (1 / 6))) |
145 | 16 | recnd 11190 |
. . . 4
โข (๐ด โ (0(,]1) โ (๐ดโ4) โ
โ) |
146 | | divrec 11836 |
. . . . 5
โข (((๐ดโ4) โ โ โง 6
โ โ โง 6 โ 0) โ ((๐ดโ4) / 6) = ((๐ดโ4) ยท (1 / 6))) |
147 | 105, 129,
146 | mp3an23 1454 |
. . . 4
โข ((๐ดโ4) โ โ โ
((๐ดโ4) / 6) = ((๐ดโ4) ยท (1 /
6))) |
148 | 145, 147 | syl 17 |
. . 3
โข (๐ด โ (0(,]1) โ ((๐ดโ4) / 6) = ((๐ดโ4) ยท (1 /
6))) |
149 | 144, 148 | breqtrrd 5138 |
. 2
โข (๐ด โ (0(,]1) โ ((๐ดโ4) ยท ((4 + 1) /
((!โ4) ยท 4))) < ((๐ดโ4) / 6)) |
150 | 14, 26, 29, 52, 149 | lelttrd 11320 |
1
โข (๐ด โ (0(,]1) โ
(absโฮฃ๐ โ
(โคโฅโ4)(๐นโ๐)) < ((๐ดโ4) / 6)) |