Step | Hyp | Ref
| Expression |
1 | | reccn2ap.t |
. . 3
โข ๐ = (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) ยท
((absโ๐ด) /
2)) |
2 | | 1red 7971 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ 1 โ
โ) |
3 | | simp1 997 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ ๐ด โ
โ) |
4 | | simp2 998 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ ๐ด # 0) |
5 | 3, 4 | absrpclapd 11196 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
(absโ๐ด) โ
โ+) |
6 | | simp3 999 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ ๐ต โ
โ+) |
7 | 5, 6 | rpmulcld 9712 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
((absโ๐ด) ยท
๐ต) โ
โ+) |
8 | 7 | rpred 9695 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
((absโ๐ด) ยท
๐ต) โ
โ) |
9 | | mincl 11238 |
. . . . . 6
โข ((1
โ โ โง ((absโ๐ด) ยท ๐ต) โ โ) โ inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โ
โ) |
10 | 2, 8, 9 | syl2anc 411 |
. . . . 5
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โ
โ) |
11 | 7 | rpgt0d 9698 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ 0 <
((absโ๐ด) ยท
๐ต)) |
12 | | 0lt1 8083 |
. . . . . . 7
โข 0 <
1 |
13 | 11, 12 | jctil 312 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ (0 <
1 โง 0 < ((absโ๐ด) ยท ๐ต))) |
14 | | 0red 7957 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ 0 โ
โ) |
15 | | ltmininf 11242 |
. . . . . . 7
โข ((0
โ โ โง 1 โ โ โง ((absโ๐ด) ยท ๐ต) โ โ) โ (0 < inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โ
(0 < 1 โง 0 < ((absโ๐ด) ยท ๐ต)))) |
16 | 14, 2, 8, 15 | syl3anc 1238 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ (0 <
inf({1, ((absโ๐ด)
ยท ๐ต)}, โ, <
) โ (0 < 1 โง 0 < ((absโ๐ด) ยท ๐ต)))) |
17 | 13, 16 | mpbird 167 |
. . . . 5
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ 0 <
inf({1, ((absโ๐ด)
ยท ๐ต)}, โ, <
)) |
18 | 10, 17 | elrpd 9692 |
. . . 4
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โ
โ+) |
19 | 5 | rphalfcld 9708 |
. . . 4
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
((absโ๐ด) / 2) โ
โ+) |
20 | 18, 19 | rpmulcld 9712 |
. . 3
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ (inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < )
ยท ((absโ๐ด) /
2)) โ โ+) |
21 | 1, 20 | eqeltrid 2264 |
. 2
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ ๐ โ
โ+) |
22 | 3 | adantr 276 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ด โ โ) |
23 | | simprl 529 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ง โ {๐ค โ โ โฃ ๐ค # 0}) |
24 | | breq1 4006 |
. . . . . . . . . . . 12
โข (๐ค = ๐ง โ (๐ค # 0 โ ๐ง # 0)) |
25 | 24 | elrab 2893 |
. . . . . . . . . . 11
โข (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โ (๐ง โ โ โง ๐ง # 0)) |
26 | 23, 25 | sylib 122 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ง โ โ โง ๐ง # 0)) |
27 | 26 | simpld 112 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ง โ โ) |
28 | 22, 27 | mulcld 7977 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ด ยท ๐ง) โ โ) |
29 | 4 | adantr 276 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ด # 0) |
30 | 26 | simprd 114 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ง # 0) |
31 | 22, 27, 29, 30 | mulap0d 8614 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ด ยท ๐ง) # 0) |
32 | 22, 27, 28, 31 | divsubdirapd 8786 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ด โ ๐ง) / (๐ด ยท ๐ง)) = ((๐ด / (๐ด ยท ๐ง)) โ (๐ง / (๐ด ยท ๐ง)))) |
33 | 22 | mulridd 7973 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ด ยท 1) = ๐ด) |
34 | 33 | oveq1d 5889 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ด ยท 1) / (๐ด ยท ๐ง)) = (๐ด / (๐ด ยท ๐ง))) |
35 | | 1cnd 7972 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ 1 โ โ) |
36 | 35, 27, 22, 30, 29 | divcanap5d 8773 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ด ยท 1) / (๐ด ยท ๐ง)) = (1 / ๐ง)) |
37 | 34, 36 | eqtr3d 2212 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ด / (๐ด ยท ๐ง)) = (1 / ๐ง)) |
38 | 27 | mulridd 7973 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ง ยท 1) = ๐ง) |
39 | 27, 22 | mulcomd 7978 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ง ยท ๐ด) = (๐ด ยท ๐ง)) |
40 | 38, 39 | oveq12d 5892 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ง ยท 1) / (๐ง ยท ๐ด)) = (๐ง / (๐ด ยท ๐ง))) |
41 | 35, 22, 27, 29, 30 | divcanap5d 8773 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ง ยท 1) / (๐ง ยท ๐ด)) = (1 / ๐ด)) |
42 | 40, 41 | eqtr3d 2212 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ง / (๐ด ยท ๐ง)) = (1 / ๐ด)) |
43 | 37, 42 | oveq12d 5892 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ด / (๐ด ยท ๐ง)) โ (๐ง / (๐ด ยท ๐ง))) = ((1 / ๐ง) โ (1 / ๐ด))) |
44 | 32, 43 | eqtrd 2210 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((๐ด โ ๐ง) / (๐ด ยท ๐ง)) = ((1 / ๐ง) โ (1 / ๐ด))) |
45 | 44 | fveq2d 5519 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ((๐ด โ ๐ง) / (๐ด ยท ๐ง))) = (absโ((1 / ๐ง) โ (1 / ๐ด)))) |
46 | 22, 27 | subcld 8267 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ด โ ๐ง) โ โ) |
47 | 46, 28, 31 | absdivapd 11203 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ((๐ด โ ๐ง) / (๐ด ยท ๐ง))) = ((absโ(๐ด โ ๐ง)) / (absโ(๐ด ยท ๐ง)))) |
48 | 45, 47 | eqtr3d 2212 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ((1 / ๐ง) โ (1 / ๐ด))) = ((absโ(๐ด โ ๐ง)) / (absโ(๐ด ยท ๐ง)))) |
49 | 46 | abscld 11189 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) โ โ) |
50 | 21 | adantr 276 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ โ
โ+) |
51 | 50 | rpred 9695 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ โ โ) |
52 | 28 | abscld 11189 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด ยท ๐ง)) โ โ) |
53 | 6 | rpred 9695 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ ๐ต โ
โ) |
54 | 53 | adantr 276 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ต โ โ) |
55 | 52, 54 | remulcld 7987 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ(๐ด ยท ๐ง)) ยท ๐ต) โ โ) |
56 | 22, 27 | abssubd 11201 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) = (absโ(๐ง โ ๐ด))) |
57 | | simprr 531 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ง โ ๐ด)) < ๐) |
58 | 56, 57 | eqbrtrd 4025 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) < ๐) |
59 | 7 | adantr 276 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) ยท ๐ต) โ
โ+) |
60 | 59 | rpred 9695 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) ยท ๐ต) โ โ) |
61 | 19 | adantr 276 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) / 2) โ
โ+) |
62 | 61 | rpred 9695 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) / 2) โ โ) |
63 | 60, 62 | remulcld 7987 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) ยท ๐ต) ยท ((absโ๐ด) / 2)) โ โ) |
64 | | 1re 7955 |
. . . . . . . . . . 11
โข 1 โ
โ |
65 | | min2inf 11240 |
. . . . . . . . . . 11
โข ((1
โ โ โง ((absโ๐ด) ยท ๐ต) โ โ) โ inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โค
((absโ๐ด) ยท
๐ต)) |
66 | 64, 60, 65 | sylancr 414 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) โค ((absโ๐ด) ยท ๐ต)) |
67 | 10 | adantr 276 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) โ
โ) |
68 | 67, 60, 61 | lemul1d 9739 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) โค ((absโ๐ด) ยท ๐ต) โ (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) ยท
((absโ๐ด) / 2)) โค
(((absโ๐ด) ยท
๐ต) ยท
((absโ๐ด) /
2)))) |
69 | 66, 68 | mpbid 147 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) ยท
((absโ๐ด) / 2)) โค
(((absโ๐ด) ยท
๐ต) ยท
((absโ๐ด) /
2))) |
70 | 1, 69 | eqbrtrid 4038 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ โค (((absโ๐ด) ยท ๐ต) ยท ((absโ๐ด) / 2))) |
71 | 27 | abscld 11189 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ๐ง) โ โ) |
72 | 22 | abscld 11189 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ๐ด) โ โ) |
73 | 72 | recnd 7985 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ๐ด) โ โ) |
74 | 73 | 2halvesd 9163 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) / 2) + ((absโ๐ด) / 2)) = (absโ๐ด)) |
75 | 72, 71 | resubcld 8337 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) โ (absโ๐ง)) โ โ) |
76 | 27, 22 | subcld 8267 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (๐ง โ ๐ด) โ โ) |
77 | 76 | abscld 11189 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ง โ ๐ด)) โ โ) |
78 | 56, 77 | eqeltrd 2254 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) โ โ) |
79 | 22, 27 | abs2difd 11205 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) โ (absโ๐ง)) โค (absโ(๐ด โ ๐ง))) |
80 | | min1inf 11239 |
. . . . . . . . . . . . . . . . . . 19
โข ((1
โ โ โง ((absโ๐ด) ยท ๐ต) โ โ) โ inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < ) โค
1) |
81 | 64, 60, 80 | sylancr 414 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) โค 1) |
82 | | 1red 7971 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ 1 โ โ) |
83 | 67, 82, 61 | lemul1d 9739 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) โค 1 โ (inf({1,
((absโ๐ด) ยท
๐ต)}, โ, < )
ยท ((absโ๐ด) /
2)) โค (1 ยท ((absโ๐ด) / 2)))) |
84 | 81, 83 | mpbid 147 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (inf({1, ((absโ๐ด) ยท ๐ต)}, โ, < ) ยท
((absโ๐ด) / 2)) โค
(1 ยท ((absโ๐ด)
/ 2))) |
85 | 1, 84 | eqbrtrid 4038 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ โค (1 ยท ((absโ๐ด) / 2))) |
86 | 62 | recnd 7985 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) / 2) โ โ) |
87 | 86 | mulid2d 7975 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (1 ยท ((absโ๐ด) / 2)) = ((absโ๐ด) / 2)) |
88 | 85, 87 | breqtrd 4029 |
. . . . . . . . . . . . . . 15
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ โค ((absโ๐ด) / 2)) |
89 | 78, 51, 62, 58, 88 | ltletrd 8379 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) < ((absโ๐ด) / 2)) |
90 | 75, 78, 62, 79, 89 | lelttrd 8081 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) โ (absโ๐ง)) < ((absโ๐ด) / 2)) |
91 | 72, 71, 62 | ltsubadd2d 8499 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) โ (absโ๐ง)) < ((absโ๐ด) / 2) โ (absโ๐ด) < ((absโ๐ง) + ((absโ๐ด) / 2)))) |
92 | 90, 91 | mpbid 147 |
. . . . . . . . . . . 12
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ๐ด) < ((absโ๐ง) + ((absโ๐ด) / 2))) |
93 | 74, 92 | eqbrtrd 4025 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) / 2) + ((absโ๐ด) / 2)) < ((absโ๐ง) + ((absโ๐ด) / 2))) |
94 | 62, 71, 62 | ltadd1d 8494 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) / 2) < (absโ๐ง) โ (((absโ๐ด) / 2) + ((absโ๐ด) / 2)) < ((absโ๐ง) + ((absโ๐ด) / 2)))) |
95 | 93, 94 | mpbird 167 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ๐ด) / 2) < (absโ๐ง)) |
96 | 62, 71, 59, 95 | ltmul2dd 9752 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) ยท ๐ต) ยท ((absโ๐ด) / 2)) < (((absโ๐ด) ยท ๐ต) ยท (absโ๐ง))) |
97 | 22, 27 | absmuld 11202 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด ยท ๐ง)) = ((absโ๐ด) ยท (absโ๐ง))) |
98 | 97 | oveq1d 5889 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ(๐ด ยท ๐ง)) ยท ๐ต) = (((absโ๐ด) ยท (absโ๐ง)) ยท ๐ต)) |
99 | 71 | recnd 7985 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ๐ง) โ โ) |
100 | 54 | recnd 7985 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ต โ โ) |
101 | 73, 99, 100 | mul32d 8109 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) ยท (absโ๐ง)) ยท ๐ต) = (((absโ๐ด) ยท ๐ต) ยท (absโ๐ง))) |
102 | 98, 101 | eqtrd 2210 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ(๐ด ยท ๐ง)) ยท ๐ต) = (((absโ๐ด) ยท ๐ต) ยท (absโ๐ง))) |
103 | 96, 102 | breqtrrd 4031 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ๐ด) ยท ๐ต) ยท ((absโ๐ด) / 2)) < ((absโ(๐ด ยท ๐ง)) ยท ๐ต)) |
104 | 51, 63, 55, 70, 103 | lelttrd 8081 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ๐ < ((absโ(๐ด ยท ๐ง)) ยท ๐ต)) |
105 | 49, 51, 55, 58, 104 | lttrd 8082 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด โ ๐ง)) < ((absโ(๐ด ยท ๐ง)) ยท ๐ต)) |
106 | 28, 31 | absrpclapd 11196 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ(๐ด ยท ๐ง)) โ
โ+) |
107 | 49, 54, 106 | ltdivmuld 9747 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (((absโ(๐ด โ ๐ง)) / (absโ(๐ด ยท ๐ง))) < ๐ต โ (absโ(๐ด โ ๐ง)) < ((absโ(๐ด ยท ๐ง)) ยท ๐ต))) |
108 | 105, 107 | mpbird 167 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ ((absโ(๐ด โ ๐ง)) / (absโ(๐ด ยท ๐ง))) < ๐ต) |
109 | 48, 108 | eqbrtrd 4025 |
. . . 4
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง (๐ง โ {๐ค โ โ โฃ ๐ค # 0} โง (absโ(๐ง โ ๐ด)) < ๐)) โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต) |
110 | 109 | expr 375 |
. . 3
โข (((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โง ๐ง โ {๐ค โ โ โฃ ๐ค # 0}) โ ((absโ(๐ง โ ๐ด)) < ๐ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต)) |
111 | 110 | ralrimiva 2550 |
. 2
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
โ๐ง โ {๐ค โ โ โฃ ๐ค # 0} ((absโ(๐ง โ ๐ด)) < ๐ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต)) |
112 | | breq2 4007 |
. . 3
โข (๐ฆ = ๐ โ ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ(๐ง โ ๐ด)) < ๐)) |
113 | 112 | rspceaimv 2849 |
. 2
โข ((๐ โ โ+
โง โ๐ง โ
{๐ค โ โ โฃ
๐ค # 0} ((absโ(๐ง โ ๐ด)) < ๐ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต)) โ โ๐ฆ โ โ+ โ๐ง โ {๐ค โ โ โฃ ๐ค # 0} ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต)) |
114 | 21, 111, 113 | syl2anc 411 |
1
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ต โ โ+) โ
โ๐ฆ โ
โ+ โ๐ง โ {๐ค โ โ โฃ ๐ค # 0} ((absโ(๐ง โ ๐ด)) < ๐ฆ โ (absโ((1 / ๐ง) โ (1 / ๐ด))) < ๐ต)) |