Step | Hyp | Ref
| Expression |
1 | | apdifflemf.a |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
2 | 1 | recnd 7986 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
3 | | apdifflemf.r |
. . . . . . 7
โข (๐ โ ๐
โ โ) |
4 | | qcn 9634 |
. . . . . . 7
โข (๐
โ โ โ ๐
โ
โ) |
5 | 3, 4 | syl 14 |
. . . . . 6
โข (๐ โ ๐
โ โ) |
6 | 2, 5 | subcld 8268 |
. . . . 5
โข (๐ โ (๐ด โ ๐
) โ โ) |
7 | 6 | adantr 276 |
. . . 4
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐ด โ ๐
) โ โ) |
8 | 7 | abscld 11190 |
. . 3
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (absโ(๐ด โ ๐
)) โ โ) |
9 | | apdifflemf.q |
. . . . . . 7
โข (๐ โ ๐ โ โ) |
10 | | qcn 9634 |
. . . . . . 7
โข (๐ โ โ โ ๐ โ
โ) |
11 | 9, 10 | syl 14 |
. . . . . 6
โข (๐ โ ๐ โ โ) |
12 | 2, 11 | subcld 8268 |
. . . . 5
โข (๐ โ (๐ด โ ๐) โ โ) |
13 | 12 | abscld 11190 |
. . . 4
โข (๐ โ (absโ(๐ด โ ๐)) โ โ) |
14 | 13 | adantr 276 |
. . 3
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (absโ(๐ด โ ๐)) โ โ) |
15 | | qre 9625 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
16 | 9, 15 | syl 14 |
. . . . . . . . 9
โข (๐ โ ๐ โ โ) |
17 | 16 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ โ โ) |
18 | 1 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ด โ โ) |
19 | | qaddcl 9635 |
. . . . . . . . . . . . . 14
โข ((๐ โ โ โง ๐
โ โ) โ (๐ + ๐
) โ โ) |
20 | 9, 3, 19 | syl2anc 411 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ + ๐
) โ โ) |
21 | | qre 9625 |
. . . . . . . . . . . . 13
โข ((๐ + ๐
) โ โ โ (๐ + ๐
) โ โ) |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . 12
โข (๐ โ (๐ + ๐
) โ โ) |
23 | 22 | rehalfcld 9165 |
. . . . . . . . . . 11
โข (๐ โ ((๐ + ๐
) / 2) โ โ) |
24 | 23 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ((๐ + ๐
) / 2) โ โ) |
25 | | apdifflemf.qr |
. . . . . . . . . . . 12
โข (๐ โ ๐ < ๐
) |
26 | | qre 9625 |
. . . . . . . . . . . . . 14
โข (๐
โ โ โ ๐
โ
โ) |
27 | 3, 26 | syl 14 |
. . . . . . . . . . . . 13
โข (๐ โ ๐
โ โ) |
28 | | avglt1 9157 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง ๐
โ โ) โ (๐ < ๐
โ ๐ < ((๐ + ๐
) / 2))) |
29 | 16, 27, 28 | syl2anc 411 |
. . . . . . . . . . . 12
โข (๐ โ (๐ < ๐
โ ๐ < ((๐ + ๐
) / 2))) |
30 | 25, 29 | mpbid 147 |
. . . . . . . . . . 11
โข (๐ โ ๐ < ((๐ + ๐
) / 2)) |
31 | 30 | adantr 276 |
. . . . . . . . . 10
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ < ((๐ + ๐
) / 2)) |
32 | | simpr 110 |
. . . . . . . . . 10
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ((๐ + ๐
) / 2) < ๐ด) |
33 | 17, 24, 18, 31, 32 | lttrd 8083 |
. . . . . . . . 9
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ < ๐ด) |
34 | 17, 18, 33 | ltled 8076 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ โค ๐ด) |
35 | 17, 18, 34 | abssubge0d 11185 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (absโ(๐ด โ ๐)) = (๐ด โ ๐)) |
36 | 35 | oveq2d 5891 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
โ (absโ(๐ด โ ๐))) = (๐
โ (๐ด โ ๐))) |
37 | 5 | adantr 276 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐
โ โ) |
38 | 2 | adantr 276 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ด โ โ) |
39 | 11 | adantr 276 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ โ โ) |
40 | 37, 38, 39 | subsub3d 8298 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
โ (๐ด โ ๐)) = ((๐
+ ๐) โ ๐ด)) |
41 | 37, 39 | addcomd 8108 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
+ ๐) = (๐ + ๐
)) |
42 | 41 | oveq1d 5890 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ((๐
+ ๐) โ ๐ด) = ((๐ + ๐
) โ ๐ด)) |
43 | 36, 40, 42 | 3eqtrd 2214 |
. . . . 5
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
โ (absโ(๐ด โ ๐))) = ((๐ + ๐
) โ ๐ด)) |
44 | 22 | adantr 276 |
. . . . . . . . 9
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐ + ๐
) โ โ) |
45 | | 2rp 9658 |
. . . . . . . . . 10
โข 2 โ
โ+ |
46 | 45 | a1i 9 |
. . . . . . . . 9
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ 2 โ
โ+) |
47 | 44, 18, 46 | ltdivmuld 9748 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (((๐ + ๐
) / 2) < ๐ด โ (๐ + ๐
) < (2 ยท ๐ด))) |
48 | 32, 47 | mpbid 147 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐ + ๐
) < (2 ยท ๐ด)) |
49 | 38 | 2timesd 9161 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (2 ยท ๐ด) = (๐ด + ๐ด)) |
50 | 48, 49 | breqtrd 4030 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐ + ๐
) < (๐ด + ๐ด)) |
51 | 44, 18, 18 | ltsubaddd 8498 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (((๐ + ๐
) โ ๐ด) < ๐ด โ (๐ + ๐
) < (๐ด + ๐ด))) |
52 | 50, 51 | mpbird 167 |
. . . . 5
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ((๐ + ๐
) โ ๐ด) < ๐ด) |
53 | 43, 52 | eqbrtrd 4026 |
. . . 4
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
โ (absโ(๐ด โ ๐))) < ๐ด) |
54 | 25 | adantr 276 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ < ๐
) |
55 | 27 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐
โ โ) |
56 | | difrp 9692 |
. . . . . . . 8
โข ((๐ โ โ โง ๐
โ โ) โ (๐ < ๐
โ (๐
โ ๐) โ
โ+)) |
57 | 17, 55, 56 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐ < ๐
โ (๐
โ ๐) โ
โ+)) |
58 | 54, 57 | mpbid 147 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
โ ๐) โ
โ+) |
59 | 18, 58 | ltaddrpd 9730 |
. . . . 5
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ด < (๐ด + (๐
โ ๐))) |
60 | 35 | oveq2d 5891 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
+ (absโ(๐ด โ ๐))) = (๐
+ (๐ด โ ๐))) |
61 | 37, 38, 39 | addsub12d 8291 |
. . . . . 6
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
+ (๐ด โ ๐)) = (๐ด + (๐
โ ๐))) |
62 | 60, 61 | eqtrd 2210 |
. . . . 5
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (๐
+ (absโ(๐ด โ ๐))) = (๐ด + (๐
โ ๐))) |
63 | 59, 62 | breqtrrd 4032 |
. . . 4
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ๐ด < (๐
+ (absโ(๐ด โ ๐)))) |
64 | 18, 55, 14 | absdifltd 11187 |
. . . 4
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ ((absโ(๐ด โ ๐
)) < (absโ(๐ด โ ๐)) โ ((๐
โ (absโ(๐ด โ ๐))) < ๐ด โง ๐ด < (๐
+ (absโ(๐ด โ ๐)))))) |
65 | 53, 63, 64 | mpbir2and 944 |
. . 3
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (absโ(๐ด โ ๐
)) < (absโ(๐ด โ ๐))) |
66 | 8, 14, 65 | gtapd 8594 |
. 2
โข ((๐ โง ((๐ + ๐
) / 2) < ๐ด) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐
))) |
67 | 13 | adantr 276 |
. . 3
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐)) โ โ) |
68 | 6 | adantr 276 |
. . . 4
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (๐ด โ ๐
) โ โ) |
69 | 68 | abscld 11190 |
. . 3
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐
)) โ โ) |
70 | 11, 5, 2 | subsubd 8296 |
. . . . . . 7
โข (๐ โ (๐ โ (๐
โ ๐ด)) = ((๐ โ ๐
) + ๐ด)) |
71 | 16, 27 | sublt0d 8527 |
. . . . . . . . 9
โข (๐ โ ((๐ โ ๐
) < 0 โ ๐ < ๐
)) |
72 | 25, 71 | mpbird 167 |
. . . . . . . 8
โข (๐ โ (๐ โ ๐
) < 0) |
73 | 16, 27 | resubcld 8338 |
. . . . . . . . 9
โข (๐ โ (๐ โ ๐
) โ โ) |
74 | | ltaddnegr 8382 |
. . . . . . . . 9
โข (((๐ โ ๐
) โ โ โง ๐ด โ โ) โ ((๐ โ ๐
) < 0 โ ((๐ โ ๐
) + ๐ด) < ๐ด)) |
75 | 73, 1, 74 | syl2anc 411 |
. . . . . . . 8
โข (๐ โ ((๐ โ ๐
) < 0 โ ((๐ โ ๐
) + ๐ด) < ๐ด)) |
76 | 72, 75 | mpbid 147 |
. . . . . . 7
โข (๐ โ ((๐ โ ๐
) + ๐ด) < ๐ด) |
77 | 70, 76 | eqbrtrd 4026 |
. . . . . 6
โข (๐ โ (๐ โ (๐
โ ๐ด)) < ๐ด) |
78 | 77 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (๐ โ (๐
โ ๐ด)) < ๐ด) |
79 | 1 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด โ โ) |
80 | 22 | adantr 276 |
. . . . . . . 8
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (๐ + ๐
) โ โ) |
81 | | simpr 110 |
. . . . . . . 8
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด < ((๐ + ๐
) / 2)) |
82 | 79, 79, 80, 81, 81 | lt2halvesd 9166 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (๐ด + ๐ด) < (๐ + ๐
)) |
83 | 79, 79, 80 | ltaddsub2d 8503 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ((๐ด + ๐ด) < (๐ + ๐
) โ ๐ด < ((๐ + ๐
) โ ๐ด))) |
84 | 82, 83 | mpbid 147 |
. . . . . 6
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด < ((๐ + ๐
) โ ๐ด)) |
85 | 11 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ โ โ) |
86 | 5 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐
โ โ) |
87 | 2 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด โ โ) |
88 | 85, 86, 87 | addsubassd 8288 |
. . . . . 6
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ((๐ + ๐
) โ ๐ด) = (๐ + (๐
โ ๐ด))) |
89 | 84, 88 | breqtrd 4030 |
. . . . 5
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด < (๐ + (๐
โ ๐ด))) |
90 | 16 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ โ โ) |
91 | 27 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐
โ โ) |
92 | 91, 79 | resubcld 8338 |
. . . . . 6
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (๐
โ ๐ด) โ โ) |
93 | 79, 90, 92 | absdifltd 11187 |
. . . . 5
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ((absโ(๐ด โ ๐)) < (๐
โ ๐ด) โ ((๐ โ (๐
โ ๐ด)) < ๐ด โง ๐ด < (๐ + (๐
โ ๐ด))))) |
94 | 78, 89, 93 | mpbir2and 944 |
. . . 4
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐)) < (๐
โ ๐ด)) |
95 | 23 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ((๐ + ๐
) / 2) โ โ) |
96 | | avglt2 9158 |
. . . . . . . . . 10
โข ((๐ โ โ โง ๐
โ โ) โ (๐ < ๐
โ ((๐ + ๐
) / 2) < ๐
)) |
97 | 16, 27, 96 | syl2anc 411 |
. . . . . . . . 9
โข (๐ โ (๐ < ๐
โ ((๐ + ๐
) / 2) < ๐
)) |
98 | 25, 97 | mpbid 147 |
. . . . . . . 8
โข (๐ โ ((๐ + ๐
) / 2) < ๐
) |
99 | 98 | adantr 276 |
. . . . . . 7
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ((๐ + ๐
) / 2) < ๐
) |
100 | 79, 95, 91, 81, 99 | lttrd 8083 |
. . . . . 6
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด < ๐
) |
101 | 79, 91, 100 | ltled 8076 |
. . . . 5
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ ๐ด โค ๐
) |
102 | 79, 91, 101 | abssuble0d 11186 |
. . . 4
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐
)) = (๐
โ ๐ด)) |
103 | 94, 102 | breqtrrd 4032 |
. . 3
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐)) < (absโ(๐ด โ ๐
))) |
104 | 67, 69, 103 | ltapd 8595 |
. 2
โข ((๐ โง ๐ด < ((๐ + ๐
) / 2)) โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐
))) |
105 | | apdifflemf.ap |
. . 3
โข (๐ โ ((๐ + ๐
) / 2) # ๐ด) |
106 | | reaplt 8545 |
. . . 4
โข ((((๐ + ๐
) / 2) โ โ โง ๐ด โ โ) โ (((๐ + ๐
) / 2) # ๐ด โ (((๐ + ๐
) / 2) < ๐ด โจ ๐ด < ((๐ + ๐
) / 2)))) |
107 | 23, 1, 106 | syl2anc 411 |
. . 3
โข (๐ โ (((๐ + ๐
) / 2) # ๐ด โ (((๐ + ๐
) / 2) < ๐ด โจ ๐ด < ((๐ + ๐
) / 2)))) |
108 | 105, 107 | mpbid 147 |
. 2
โข (๐ โ (((๐ + ๐
) / 2) < ๐ด โจ ๐ด < ((๐ + ๐
) / 2))) |
109 | 66, 104, 108 | mpjaodan 798 |
1
โข (๐ โ (absโ(๐ด โ ๐)) # (absโ(๐ด โ ๐
))) |