Step | Hyp | Ref
| Expression |
1 | | zre 12499 |
. . . . . . . . 9
โข (๐ด โ โค โ ๐ด โ
โ) |
2 | 1 | rehalfcld 12396 |
. . . . . . . 8
โข (๐ด โ โค โ (๐ด / 2) โ
โ) |
3 | 2 | flcld 13695 |
. . . . . . 7
โข (๐ด โ โค โ
(โโ(๐ด / 2))
โ โค) |
4 | 3 | zred 12603 |
. . . . . 6
โข (๐ด โ โค โ
(โโ(๐ด / 2))
โ โ) |
5 | 4 | 3ad2ant1 1133 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / 2)) โ โ) |
6 | | 2re 12223 |
. . . . . . . 8
โข 2 โ
โ |
7 | 6 | a1i 11 |
. . . . . . 7
โข (๐ โ โ0
โ 2 โ โ) |
8 | | id 22 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โ0) |
9 | 7, 8 | reexpcld 14060 |
. . . . . 6
โข (๐ โ โ0
โ (2โ๐) โ
โ) |
10 | 9 | 3ad2ant3 1135 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ๐) โ โ) |
11 | | 2cnd 12227 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 2 โ โ) |
12 | | 2ne0 12253 |
. . . . . . 7
โข 2 โ
0 |
13 | 12 | a1i 11 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 2 โ 0) |
14 | | nn0z 12520 |
. . . . . . 7
โข (๐ โ โ0
โ ๐ โ
โค) |
15 | 14 | 3ad2ant3 1135 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ๐ โ โค) |
16 | 11, 13, 15 | expne0d 14049 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ๐) โ 0) |
17 | 5, 10, 16 | redivcld 11979 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((โโ(๐ด / 2)) / (2โ๐)) โ โ) |
18 | 17 | flcld 13695 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) โ โค) |
19 | 1 | 3ad2ant1 1133 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ๐ด โ โ) |
20 | 6 | a1i 11 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 2 โ โ) |
21 | | simp3 1138 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ๐ โ
โ0) |
22 | | 1nn0 12425 |
. . . . . . . 8
โข 1 โ
โ0 |
23 | 22 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 1 โ โ0) |
24 | 21, 23 | nn0addcld 12473 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ + 1) โ
โ0) |
25 | 20, 24 | reexpcld 14060 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ(๐ + 1)) โ โ) |
26 | 15 | peano2zd 12606 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ + 1) โ โค) |
27 | 11, 13, 26 | expne0d 14049 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ(๐ + 1)) โ 0) |
28 | 19, 25, 27 | redivcld 11979 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ด / (2โ(๐ + 1))) โ โ) |
29 | 28 | flcld 13695 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / (2โ(๐ + 1)))) โ โค) |
30 | | nn0p1nn 12448 |
. . . . 5
โข (๐ โ โ0
โ (๐ + 1) โ
โ) |
31 | | dignn0flhalflem1 46633 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง (๐ + 1) โ
โ) โ (โโ((๐ด / (2โ(๐ + 1))) โ 1)) <
(โโ((๐ด โ
1) / (2โ(๐ +
1))))) |
32 | 30, 31 | syl3an3 1165 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((๐ด / (2โ(๐ + 1))) โ 1)) <
(โโ((๐ด โ
1) / (2โ(๐ +
1))))) |
33 | | 1zzd 12530 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 1 โ โค) |
34 | | flsubz 46535 |
. . . . . 6
โข (((๐ด / (2โ(๐ + 1))) โ โ โง 1 โ
โค) โ (โโ((๐ด / (2โ(๐ + 1))) โ 1)) = ((โโ(๐ด / (2โ(๐ + 1)))) โ 1)) |
35 | 28, 33, 34 | syl2anc 584 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((๐ด / (2โ(๐ + 1))) โ 1)) = ((โโ(๐ด / (2โ(๐ + 1)))) โ 1)) |
36 | 35 | eqcomd 2742 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((โโ(๐ด / (2โ(๐ + 1)))) โ 1) = (โโ((๐ด / (2โ(๐ + 1))) โ 1))) |
37 | | nnz 12516 |
. . . . . . . . . 10
โข (((๐ด โ 1) / 2) โ โ
โ ((๐ด โ 1) / 2)
โ โค) |
38 | | zob 16233 |
. . . . . . . . . 10
โข (๐ด โ โค โ (((๐ด + 1) / 2) โ โค โ
((๐ด โ 1) / 2) โ
โค)) |
39 | 37, 38 | syl5ibr 245 |
. . . . . . . . 9
โข (๐ด โ โค โ (((๐ด โ 1) / 2) โ โ
โ ((๐ด + 1) / 2) โ
โค)) |
40 | 39 | imp 407 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ)
โ ((๐ด + 1) / 2) โ
โค) |
41 | | zofldiv2 46549 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด + 1) / 2) โ โค)
โ (โโ(๐ด /
2)) = ((๐ด โ 1) /
2)) |
42 | 40, 41 | syldan 591 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ)
โ (โโ(๐ด /
2)) = ((๐ด โ 1) /
2)) |
43 | 42 | 3adant3 1132 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / 2)) = ((๐ด โ 1) / 2)) |
44 | 43 | fvoveq1d 7375 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) = (โโ(((๐ด โ 1) / 2) / (2โ๐)))) |
45 | | zcn 12500 |
. . . . . . . . 9
โข (๐ด โ โค โ ๐ด โ
โ) |
46 | | 1cnd 11146 |
. . . . . . . . 9
โข (๐ด โ โค โ 1 โ
โ) |
47 | 45, 46 | subcld 11508 |
. . . . . . . 8
โข (๐ด โ โค โ (๐ด โ 1) โ
โ) |
48 | | 2rp 12912 |
. . . . . . . . . 10
โข 2 โ
โ+ |
49 | 48 | a1i 11 |
. . . . . . . . 9
โข (((๐ด โ 1) / 2) โ โ
โ 2 โ โ+) |
50 | 49 | rpcnne0d 12958 |
. . . . . . . 8
โข (((๐ด โ 1) / 2) โ โ
โ (2 โ โ โง 2 โ 0)) |
51 | 48 | a1i 11 |
. . . . . . . . . 10
โข (๐ โ โ0
โ 2 โ โ+) |
52 | 51, 14 | rpexpcld 14142 |
. . . . . . . . 9
โข (๐ โ โ0
โ (2โ๐) โ
โ+) |
53 | 52 | rpcnne0d 12958 |
. . . . . . . 8
โข (๐ โ โ0
โ ((2โ๐) โ
โ โง (2โ๐)
โ 0)) |
54 | | divdiv1 11862 |
. . . . . . . 8
โข (((๐ด โ 1) โ โ โง
(2 โ โ โง 2 โ 0) โง ((2โ๐) โ โ โง (2โ๐) โ 0)) โ (((๐ด โ 1) / 2) / (2โ๐)) = ((๐ด โ 1) / (2 ยท (2โ๐)))) |
55 | 47, 50, 53, 54 | syl3an 1160 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (((๐ด โ 1) / 2) / (2โ๐)) = ((๐ด โ 1) / (2 ยท (2โ๐)))) |
56 | 10 | recnd 11179 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ๐) โ โ) |
57 | 11, 56 | mulcomd 11172 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2 ยท (2โ๐)) = ((2โ๐) ยท 2)) |
58 | 11, 21 | expp1d 14044 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ(๐ + 1)) = ((2โ๐) ยท 2)) |
59 | 57, 58 | eqtr4d 2779 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2 ยท (2โ๐)) = (2โ(๐ + 1))) |
60 | 59 | oveq2d 7369 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((๐ด โ 1) / (2 ยท (2โ๐))) = ((๐ด โ 1) / (2โ(๐ + 1)))) |
61 | 55, 60 | eqtrd 2776 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (((๐ด โ 1) / 2) / (2โ๐)) = ((๐ด โ 1) / (2โ(๐ + 1)))) |
62 | 61 | fveq2d 6843 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(((๐ด โ 1) / 2) / (2โ๐))) = (โโ((๐ด โ 1) / (2โ(๐ + 1))))) |
63 | 44, 62 | eqtrd 2776 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) = (โโ((๐ด โ 1) / (2โ(๐ + 1))))) |
64 | 32, 36, 63 | 3brtr4d 5135 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((โโ(๐ด / (2โ(๐ + 1)))) โ 1) <
(โโ((โโ(๐ด / 2)) / (2โ๐)))) |
65 | 19 | rehalfcld 12396 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ด / 2) โ โ) |
66 | 65, 10, 16 | redivcld 11979 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((๐ด / 2) / (2โ๐)) โ โ) |
67 | | reflcl 13693 |
. . . . . . 7
โข ((๐ด / 2) โ โ โ
(โโ(๐ด / 2))
โ โ) |
68 | 65, 67 | syl 17 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / 2)) โ โ) |
69 | 48 | a1i 11 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ 2 โ โ+) |
70 | 69, 15 | rpexpcld 14142 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ๐) โ
โ+) |
71 | | flle 13696 |
. . . . . . 7
โข ((๐ด / 2) โ โ โ
(โโ(๐ด / 2))
โค (๐ด /
2)) |
72 | 65, 71 | syl 17 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / 2)) โค (๐ด / 2)) |
73 | 68, 65, 70, 72 | lediv1dd 13007 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((โโ(๐ด / 2)) / (2โ๐)) โค ((๐ด / 2) / (2โ๐))) |
74 | | flwordi 13709 |
. . . . 5
โข
((((โโ(๐ด
/ 2)) / (2โ๐)) โ
โ โง ((๐ด / 2) /
(2โ๐)) โ โ
โง ((โโ(๐ด /
2)) / (2โ๐)) โค
((๐ด / 2) / (2โ๐))) โ
(โโ((โโ(๐ด / 2)) / (2โ๐))) โค (โโ((๐ด / 2) / (2โ๐)))) |
75 | 17, 66, 73, 74 | syl3anc 1371 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) โค (โโ((๐ด / 2) / (2โ๐)))) |
76 | | divdiv1 11862 |
. . . . . . . 8
โข ((๐ด โ โ โง (2 โ
โ โง 2 โ 0) โง ((2โ๐) โ โ โง (2โ๐) โ 0)) โ ((๐ด / 2) / (2โ๐)) = (๐ด / (2 ยท (2โ๐)))) |
77 | 45, 50, 53, 76 | syl3an 1160 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((๐ด / 2) / (2โ๐)) = (๐ด / (2 ยท (2โ๐)))) |
78 | 52 | rpcnd 12951 |
. . . . . . . . . . 11
โข (๐ โ โ0
โ (2โ๐) โ
โ) |
79 | 78 | 3ad2ant3 1135 |
. . . . . . . . . 10
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ๐) โ โ) |
80 | 11, 79 | mulcomd 11172 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2 ยท (2โ๐)) = ((2โ๐) ยท 2)) |
81 | 11, 13, 15 | expp1zd 14052 |
. . . . . . . . 9
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2โ(๐ + 1)) = ((2โ๐) ยท 2)) |
82 | 80, 81 | eqtr4d 2779 |
. . . . . . . 8
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (2 ยท (2โ๐)) = (2โ(๐ + 1))) |
83 | 82 | oveq2d 7369 |
. . . . . . 7
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ด / (2 ยท (2โ๐))) = (๐ด / (2โ(๐ + 1)))) |
84 | 77, 83 | eqtrd 2776 |
. . . . . 6
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ ((๐ด / 2) / (2โ๐)) = (๐ด / (2โ(๐ + 1)))) |
85 | 84 | eqcomd 2742 |
. . . . 5
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (๐ด / (2โ(๐ + 1))) = ((๐ด / 2) / (2โ๐))) |
86 | 85 | fveq2d 6843 |
. . . 4
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / (2โ(๐ + 1)))) = (โโ((๐ด / 2) / (2โ๐)))) |
87 | 75, 86 | breqtrrd 5131 |
. . 3
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) โค (โโ(๐ด / (2โ(๐ + 1))))) |
88 | | zgtp1leeq 46534 |
. . . 4
โข
(((โโ((โโ(๐ด / 2)) / (2โ๐))) โ โค โง
(โโ(๐ด /
(2โ(๐ + 1)))) โ
โค) โ ((((โโ(๐ด / (2โ(๐ + 1)))) โ 1) <
(โโ((โโ(๐ด / 2)) / (2โ๐))) โง
(โโ((โโ(๐ด / 2)) / (2โ๐))) โค (โโ(๐ด / (2โ(๐ + 1))))) โ
(โโ((โโ(๐ด / 2)) / (2โ๐))) = (โโ(๐ด / (2โ(๐ + 1)))))) |
89 | 88 | imp 407 |
. . 3
โข
((((โโ((โโ(๐ด / 2)) / (2โ๐))) โ โค โง
(โโ(๐ด /
(2โ(๐ + 1)))) โ
โค) โง (((โโ(๐ด / (2โ(๐ + 1)))) โ 1) <
(โโ((โโ(๐ด / 2)) / (2โ๐))) โง
(โโ((โโ(๐ด / 2)) / (2โ๐))) โค (โโ(๐ด / (2โ(๐ + 1)))))) โ
(โโ((โโ(๐ด / 2)) / (2โ๐))) = (โโ(๐ด / (2โ(๐ + 1))))) |
90 | 18, 29, 64, 87, 89 | syl22anc 837 |
. 2
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ((โโ(๐ด / 2)) / (2โ๐))) = (โโ(๐ด / (2โ(๐ + 1))))) |
91 | 90 | eqcomd 2742 |
1
โข ((๐ด โ โค โง ((๐ด โ 1) / 2) โ โ
โง ๐ โ
โ0) โ (โโ(๐ด / (2โ(๐ + 1)))) =
(โโ((โโ(๐ด / 2)) / (2โ๐)))) |