Step | Hyp | Ref
| Expression |
1 | | nn0addcl 9210 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
2 | 1 | nn0zd 9372 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ โค) |
3 | | 2nn 9079 |
. . . . . 6
โข 2 โ
โ |
4 | | znq 9623 |
. . . . . 6
โข (((๐ + ๐) โ โค โง 2 โ โ)
โ ((๐ + ๐) / 2) โ
โ) |
5 | 2, 3, 4 | sylancl 413 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + ๐) / 2) โ โ) |
6 | | flqle 10277 |
. . . . 5
โข (((๐ + ๐) / 2) โ โ โ
(โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2)) |
7 | 5, 6 | syl 14 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2)) |
8 | 5 | flqcld 10276 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โ โค) |
9 | 8 | zred 9374 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โ โ) |
10 | | nn0readdcl 9234 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ โ) |
11 | 10 | rehalfcld 9164 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + ๐) / 2) โ โ) |
12 | | nn0re 9184 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
13 | 12 | adantr 276 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
14 | | letr 8039 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ โ
โง ((๐ + ๐) / 2) โ โ โง
๐ โ โ) โ
(((โโ((๐ +
๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
15 | 9, 11, 13, 14 | syl3anc 1238 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
16 | 7, 15 | mpand 429 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (โโ((๐ + ๐) / 2)) โค ๐)) |
17 | 1 | nn0ge0d 9231 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค (๐ + ๐)) |
18 | | halfnneg2 9150 |
. . . . . . 7
โข ((๐ + ๐) โ โ โ (0 โค (๐ + ๐) โ 0 โค ((๐ + ๐) / 2))) |
19 | 10, 18 | syl 14 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0 โค (๐ + ๐) โ 0 โค ((๐ + ๐) / 2))) |
20 | 17, 19 | mpbid 147 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค ((๐ + ๐) / 2)) |
21 | | flqge0nn0 10292 |
. . . . 5
โข ((((๐ + ๐) / 2) โ โ โง 0 โค ((๐ + ๐) / 2)) โ (โโ((๐ + ๐) / 2)) โ
โ0) |
22 | 5, 20, 21 | syl2anc 411 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โ
โ0) |
23 | | simpl 109 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ
โ0) |
24 | | facwordi 10719 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ
โ0 โง ๐
โ โ0 โง (โโ((๐ + ๐) / 2)) โค ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)) |
25 | 24 | 3exp 1202 |
. . . 4
โข
((โโ((๐
+ ๐) / 2)) โ
โ0 โ (๐ โ โ0 โ
((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)))) |
26 | 22, 23, 25 | sylc 62 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐))) |
27 | | faccl 10714 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
28 | 27 | nncnd 8932 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
29 | 28 | mulridd 7973 |
. . . . . 6
โข (๐ โ โ0
โ ((!โ๐)
ยท 1) = (!โ๐)) |
30 | 29 | adantr 276 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท 1) = (!โ๐)) |
31 | | faccl 10714 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
32 | 31 | nnred 8931 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
33 | 32 | adantl 277 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
34 | 27 | nnred 8931 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
35 | 27 | nnnn0d 9228 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ0) |
36 | 35 | nn0ge0d 9231 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
37 | 34, 36 | jca 306 |
. . . . . . 7
โข (๐ โ โ0
โ ((!โ๐) โ
โ โง 0 โค (!โ๐))) |
38 | 37 | adantr 276 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) โ โ โง 0 โค (!โ๐))) |
39 | 31 | nnge1d 8961 |
. . . . . . 7
โข (๐ โ โ0
โ 1 โค (!โ๐)) |
40 | 39 | adantl 277 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 1 โค (!โ๐)) |
41 | | 1re 7955 |
. . . . . . 7
โข 1 โ
โ |
42 | | lemul2a 8815 |
. . . . . . 7
โข (((1
โ โ โง (!โ๐) โ โ โง ((!โ๐) โ โ โง 0 โค
(!โ๐))) โง 1 โค
(!โ๐)) โ
((!โ๐) ยท 1)
โค ((!โ๐) ยท
(!โ๐))) |
43 | 41, 42 | mp3anl1 1331 |
. . . . . 6
โข
((((!โ๐)
โ โ โง ((!โ๐) โ โ โง 0 โค (!โ๐))) โง 1 โค (!โ๐)) โ ((!โ๐) ยท 1) โค
((!โ๐) ยท
(!โ๐))) |
44 | 33, 38, 40, 43 | syl21anc 1237 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท 1) โค ((!โ๐) ยท (!โ๐))) |
45 | 30, 44 | eqbrtrrd 4027 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โค ((!โ๐) ยท (!โ๐))) |
46 | | faccl 10714 |
. . . . . . 7
โข
((โโ((๐
+ ๐) / 2)) โ
โ0 โ (!โ(โโ((๐ + ๐) / 2))) โ โ) |
47 | 22, 46 | syl 14 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โ โ) |
48 | 47 | nnred 8931 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โ โ) |
49 | 34 | adantr 276 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
50 | | remulcl 7938 |
. . . . . 6
โข
(((!โ๐) โ
โ โง (!โ๐)
โ โ) โ ((!โ๐) ยท (!โ๐)) โ โ) |
51 | 34, 32, 50 | syl2an 289 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท (!โ๐)) โ โ) |
52 | | letr 8039 |
. . . . 5
โข
(((!โ(โโ((๐ + ๐) / 2))) โ โ โง (!โ๐) โ โ โง
((!โ๐) ยท
(!โ๐)) โ
โ) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
53 | 48, 49, 51, 52 | syl3anc 1238 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
54 | 45, 53 | mpan2d 428 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
55 | 16, 26, 54 | 3syld 57 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
56 | | nn0re 9184 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
57 | 56 | adantl 277 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
58 | | letr 8039 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ โ
โง ((๐ + ๐) / 2) โ โ โง
๐ โ โ) โ
(((โโ((๐ +
๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
59 | 9, 11, 57, 58 | syl3anc 1238 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
60 | 7, 59 | mpand 429 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (โโ((๐ + ๐) / 2)) โค ๐)) |
61 | | simpr 110 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ
โ0) |
62 | | facwordi 10719 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ
โ0 โง ๐
โ โ0 โง (โโ((๐ + ๐) / 2)) โค ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)) |
63 | 62 | 3exp 1202 |
. . . 4
โข
((โโ((๐
+ ๐) / 2)) โ
โ0 โ (๐ โ โ0 โ
((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)))) |
64 | 22, 61, 63 | sylc 62 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐))) |
65 | 31 | nncnd 8932 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
66 | 65 | mulid2d 7975 |
. . . . . 6
โข (๐ โ โ0
โ (1 ยท (!โ๐)) = (!โ๐)) |
67 | 66 | adantl 277 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (1 ยท (!โ๐)) = (!โ๐)) |
68 | 31 | nnnn0d 9228 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ0) |
69 | 68 | nn0ge0d 9231 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
70 | 32, 69 | jca 306 |
. . . . . . 7
โข (๐ โ โ0
โ ((!โ๐) โ
โ โง 0 โค (!โ๐))) |
71 | 70 | adantl 277 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) โ โ โง 0 โค (!โ๐))) |
72 | 27 | nnge1d 8961 |
. . . . . . 7
โข (๐ โ โ0
โ 1 โค (!โ๐)) |
73 | 72 | adantr 276 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 1 โค (!โ๐)) |
74 | | lemul1a 8814 |
. . . . . . 7
โข (((1
โ โ โง (!โ๐) โ โ โง ((!โ๐) โ โ โง 0 โค
(!โ๐))) โง 1 โค
(!โ๐)) โ (1
ยท (!โ๐)) โค
((!โ๐) ยท
(!โ๐))) |
75 | 41, 74 | mp3anl1 1331 |
. . . . . 6
โข
((((!โ๐)
โ โ โง ((!โ๐) โ โ โง 0 โค (!โ๐))) โง 1 โค (!โ๐)) โ (1 ยท
(!โ๐)) โค
((!โ๐) ยท
(!โ๐))) |
76 | 49, 71, 73, 75 | syl21anc 1237 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (1 ยท (!โ๐)) โค ((!โ๐) ยท (!โ๐))) |
77 | 67, 76 | eqbrtrrd 4027 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โค ((!โ๐) ยท (!โ๐))) |
78 | | letr 8039 |
. . . . 5
โข
(((!โ(โโ((๐ + ๐) / 2))) โ โ โง (!โ๐) โ โ โง
((!โ๐) ยท
(!โ๐)) โ
โ) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
79 | 48, 33, 51, 78 | syl3anc 1238 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
80 | 77, 79 | mpan2d 428 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
81 | 60, 64, 80 | 3syld 57 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
82 | 23 | nn0zd 9372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โค) |
83 | | zq 9625 |
. . . 4
โข (๐ โ โค โ ๐ โ
โ) |
84 | 82, 83 | syl 14 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
85 | 61 | nn0zd 9372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โค) |
86 | | zq 9625 |
. . . 4
โข (๐ โ โค โ ๐ โ
โ) |
87 | 85, 86 | syl 14 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
88 | | qavgle 10258 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ + ๐) / 2) โค ๐ โจ ((๐ + ๐) / 2) โค ๐)) |
89 | 84, 87, 88 | syl2anc 411 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โจ ((๐ + ๐) / 2) โค ๐)) |
90 | 55, 81, 89 | mpjaod 718 |
1
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐))) |