Step | Hyp | Ref
| Expression |
1 | | nn0readdcl 12484 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ โ) |
2 | 1 | rehalfcld 12405 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((๐ + ๐) / 2) โ โ) |
3 | | flle 13710 |
. . . . 5
โข (((๐ + ๐) / 2) โ โ โ
(โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2)) |
4 | 2, 3 | syl 17 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2)) |
5 | | reflcl 13707 |
. . . . . 6
โข (((๐ + ๐) / 2) โ โ โ
(โโ((๐ + ๐) / 2)) โ
โ) |
6 | 2, 5 | syl 17 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โ โ) |
7 | | nn0re 12427 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
8 | 7 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
9 | | letr 11254 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ โ
โง ((๐ + ๐) / 2) โ โ โง
๐ โ โ) โ
(((โโ((๐ +
๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
10 | 6, 2, 8, 9 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
11 | 4, 10 | mpand 694 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (โโ((๐ + ๐) / 2)) โค ๐)) |
12 | | nn0addcl 12453 |
. . . . . . 7
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (๐ + ๐) โ
โ0) |
13 | 12 | nn0ge0d 12481 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค (๐ + ๐)) |
14 | | halfnneg2 12389 |
. . . . . . 7
โข ((๐ + ๐) โ โ โ (0 โค (๐ + ๐) โ 0 โค ((๐ + ๐) / 2))) |
15 | 1, 14 | syl 17 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (0 โค (๐ + ๐) โ 0 โค ((๐ + ๐) / 2))) |
16 | 13, 15 | mpbid 231 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 0 โค ((๐ + ๐) / 2)) |
17 | | flge0nn0 13731 |
. . . . 5
โข ((((๐ + ๐) / 2) โ โ โง 0 โค ((๐ + ๐) / 2)) โ (โโ((๐ + ๐) / 2)) โ
โ0) |
18 | 2, 16, 17 | syl2anc 585 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (โโ((๐ + ๐) / 2)) โ
โ0) |
19 | | simpl 484 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ
โ0) |
20 | | facwordi 14195 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ
โ0 โง ๐
โ โ0 โง (โโ((๐ + ๐) / 2)) โค ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)) |
21 | 20 | 3exp 1120 |
. . . 4
โข
((โโ((๐
+ ๐) / 2)) โ
โ0 โ (๐ โ โ0 โ
((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)))) |
22 | 18, 19, 21 | sylc 65 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐))) |
23 | | faccl 14189 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
24 | 23 | nncnd 12174 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
25 | 24 | mulid1d 11177 |
. . . . . 6
โข (๐ โ โ0
โ ((!โ๐)
ยท 1) = (!โ๐)) |
26 | 25 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท 1) = (!โ๐)) |
27 | | faccl 14189 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
28 | 27 | nnred 12173 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
29 | 28 | adantl 483 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
30 | 23 | nnred 12173 |
. . . . . . . 8
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
31 | 23 | nnnn0d 12478 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ0) |
32 | 31 | nn0ge0d 12481 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
33 | 30, 32 | jca 513 |
. . . . . . 7
โข (๐ โ โ0
โ ((!โ๐) โ
โ โง 0 โค (!โ๐))) |
34 | 33 | adantr 482 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) โ โ โง 0 โค (!โ๐))) |
35 | 27 | nnge1d 12206 |
. . . . . . 7
โข (๐ โ โ0
โ 1 โค (!โ๐)) |
36 | 35 | adantl 483 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 1 โค (!โ๐)) |
37 | | 1re 11160 |
. . . . . . 7
โข 1 โ
โ |
38 | | lemul2a 12015 |
. . . . . . 7
โข (((1
โ โ โง (!โ๐) โ โ โง ((!โ๐) โ โ โง 0 โค
(!โ๐))) โง 1 โค
(!โ๐)) โ
((!โ๐) ยท 1)
โค ((!โ๐) ยท
(!โ๐))) |
39 | 37, 38 | mp3anl1 1456 |
. . . . . 6
โข
((((!โ๐)
โ โ โง ((!โ๐) โ โ โง 0 โค (!โ๐))) โง 1 โค (!โ๐)) โ ((!โ๐) ยท 1) โค
((!โ๐) ยท
(!โ๐))) |
40 | 29, 34, 36, 39 | syl21anc 837 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท 1) โค ((!โ๐) ยท (!โ๐))) |
41 | 26, 40 | eqbrtrrd 5130 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โค ((!โ๐) ยท (!โ๐))) |
42 | 18 | faccld 14190 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โ โ) |
43 | 42 | nnred 12173 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โ โ) |
44 | 30 | adantr 482 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โ โ) |
45 | | remulcl 11141 |
. . . . . 6
โข
(((!โ๐) โ
โ โง (!โ๐)
โ โ) โ ((!โ๐) ยท (!โ๐)) โ โ) |
46 | 30, 28, 45 | syl2an 597 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) ยท (!โ๐)) โ โ) |
47 | | letr 11254 |
. . . . 5
โข
(((!โ(โโ((๐ + ๐) / 2))) โ โ โง (!โ๐) โ โ โง
((!โ๐) ยท
(!โ๐)) โ
โ) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
48 | 43, 44, 46, 47 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
49 | 41, 48 | mpan2d 693 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
50 | 11, 22, 49 | 3syld 60 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
51 | | nn0re 12427 |
. . . . . 6
โข (๐ โ โ0
โ ๐ โ
โ) |
52 | 51 | adantl 483 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ โ) |
53 | | letr 11254 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ โ
โง ((๐ + ๐) / 2) โ โ โง
๐ โ โ) โ
(((โโ((๐ +
๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
54 | 6, 2, 52, 53 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((โโ((๐ + ๐) / 2)) โค ((๐ + ๐) / 2) โง ((๐ + ๐) / 2) โค ๐) โ (โโ((๐ + ๐) / 2)) โค ๐)) |
55 | 4, 54 | mpand 694 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (โโ((๐ + ๐) / 2)) โค ๐)) |
56 | | simpr 486 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ๐ โ
โ0) |
57 | | facwordi 14195 |
. . . . 5
โข
(((โโ((๐
+ ๐) / 2)) โ
โ0 โง ๐
โ โ0 โง (โโ((๐ + ๐) / 2)) โค ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)) |
58 | 57 | 3exp 1120 |
. . . 4
โข
((โโ((๐
+ ๐) / 2)) โ
โ0 โ (๐ โ โ0 โ
((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐)))) |
59 | 18, 56, 58 | sylc 65 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((โโ((๐ + ๐) / 2)) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค (!โ๐))) |
60 | 27 | nncnd 12174 |
. . . . . . 7
โข (๐ โ โ0
โ (!โ๐) โ
โ) |
61 | 60 | mulid2d 11178 |
. . . . . 6
โข (๐ โ โ0
โ (1 ยท (!โ๐)) = (!โ๐)) |
62 | 61 | adantl 483 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (1 ยท (!โ๐)) = (!โ๐)) |
63 | 27 | nnnn0d 12478 |
. . . . . . . . 9
โข (๐ โ โ0
โ (!โ๐) โ
โ0) |
64 | 63 | nn0ge0d 12481 |
. . . . . . . 8
โข (๐ โ โ0
โ 0 โค (!โ๐)) |
65 | 28, 64 | jca 513 |
. . . . . . 7
โข (๐ โ โ0
โ ((!โ๐) โ
โ โง 0 โค (!โ๐))) |
66 | 65 | adantl 483 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ๐) โ โ โง 0 โค (!โ๐))) |
67 | 23 | nnge1d 12206 |
. . . . . . 7
โข (๐ โ โ0
โ 1 โค (!โ๐)) |
68 | 67 | adantr 482 |
. . . . . 6
โข ((๐ โ โ0
โง ๐ โ
โ0) โ 1 โค (!โ๐)) |
69 | | lemul1a 12014 |
. . . . . . 7
โข (((1
โ โ โง (!โ๐) โ โ โง ((!โ๐) โ โ โง 0 โค
(!โ๐))) โง 1 โค
(!โ๐)) โ (1
ยท (!โ๐)) โค
((!โ๐) ยท
(!โ๐))) |
70 | 37, 69 | mp3anl1 1456 |
. . . . . 6
โข
((((!โ๐)
โ โ โง ((!โ๐) โ โ โง 0 โค (!โ๐))) โง 1 โค (!โ๐)) โ (1 ยท
(!โ๐)) โค
((!โ๐) ยท
(!โ๐))) |
71 | 44, 66, 68, 70 | syl21anc 837 |
. . . . 5
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (1 ยท (!โ๐)) โค ((!โ๐) ยท (!โ๐))) |
72 | 62, 71 | eqbrtrrd 5130 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ๐) โค ((!โ๐) ยท (!โ๐))) |
73 | | letr 11254 |
. . . . 5
โข
(((!โ(โโ((๐ + ๐) / 2))) โ โ โง (!โ๐) โ โ โง
((!โ๐) ยท
(!โ๐)) โ
โ) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
74 | 43, 29, 46, 73 | syl3anc 1372 |
. . . 4
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โง (!โ๐) โค ((!โ๐) ยท (!โ๐))) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
75 | 72, 74 | mpan2d 693 |
. . 3
โข ((๐ โ โ0
โง ๐ โ
โ0) โ ((!โ(โโ((๐ + ๐) / 2))) โค (!โ๐) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
76 | 55, 59, 75 | 3syld 60 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐)))) |
77 | | avgle 12400 |
. . 3
โข ((๐ โ โ โง ๐ โ โ) โ (((๐ + ๐) / 2) โค ๐ โจ ((๐ + ๐) / 2) โค ๐)) |
78 | 7, 51, 77 | syl2an 597 |
. 2
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (((๐ + ๐) / 2) โค ๐ โจ ((๐ + ๐) / 2) โค ๐)) |
79 | 50, 76, 78 | mpjaod 859 |
1
โข ((๐ โ โ0
โง ๐ โ
โ0) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐))) |