Step | Hyp | Ref
| Expression |
1 | | odd2np1 10272 |
. . 3
|
2 | | halfre 8244 |
. . . . . . . . . . . . . . . 16
|
3 | 2 | a1i 9 |
. . . . . . . . . . . . . . 15
|
4 | | 1red 7134 |
. . . . . . . . . . . . . . 15
|
5 | | zre 8355 |
. . . . . . . . . . . . . . 15
|
6 | 3, 4, 5 | 3jca 1118 |
. . . . . . . . . . . . . 14
|
7 | 6 | adantr 270 |
. . . . . . . . . . . . 13
|
8 | | halflt1 8248 |
. . . . . . . . . . . . 13
|
9 | | axltadd 7182 |
. . . . . . . . . . . . 13
|
10 | 7, 8, 9 | mpisyl 1375 |
. . . . . . . . . . . 12
|
11 | | zre 8355 |
. . . . . . . . . . . . . 14
|
12 | 11 | adantl 271 |
. . . . . . . . . . . . 13
|
13 | 5, 3 | readdcld 7148 |
. . . . . . . . . . . . . 14
|
14 | 13 | adantr 270 |
. . . . . . . . . . . . 13
|
15 | | peano2z 8387 |
. . . . . . . . . . . . . . 15
|
16 | 15 | zred 8469 |
. . . . . . . . . . . . . 14
|
17 | 16 | adantr 270 |
. . . . . . . . . . . . 13
|
18 | | lttr 7185 |
. . . . . . . . . . . . 13
|
19 | 12, 14, 17, 18 | syl3anc 1169 |
. . . . . . . . . . . 12
|
20 | 10, 19 | mpan2d 418 |
. . . . . . . . . . 11
|
21 | | zleltp1 8406 |
. . . . . . . . . . . 12
|
22 | 21 | ancoms 264 |
. . . . . . . . . . 11
|
23 | 20, 22 | sylibrd 167 |
. . . . . . . . . 10
|
24 | | halfgt0 8246 |
. . . . . . . . . . . 12
|
25 | 3, 5 | jca 300 |
. . . . . . . . . . . . . 14
|
26 | 25 | adantr 270 |
. . . . . . . . . . . . 13
|
27 | | ltaddpos 7556 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | syl 14 |
. . . . . . . . . . . 12
|
29 | 24, 28 | mpbii 146 |
. . . . . . . . . . 11
|
30 | 5 | adantr 270 |
. . . . . . . . . . . 12
|
31 | | lelttr 7199 |
. . . . . . . . . . . 12
|
32 | 12, 30, 14, 31 | syl3anc 1169 |
. . . . . . . . . . 11
|
33 | 29, 32 | mpan2d 418 |
. . . . . . . . . 10
|
34 | 23, 33 | impbid 127 |
. . . . . . . . 9
|
35 | | zcn 8356 |
. . . . . . . . . . . 12
|
36 | | 1cnd 7135 |
. . . . . . . . . . . 12
|
37 | | 2cn 8110 |
. . . . . . . . . . . . . 14
|
38 | | 2ap0 8132 |
. . . . . . . . . . . . . 14
# |
39 | 37, 38 | pm3.2i 266 |
. . . . . . . . . . . . 13
# |
40 | 39 | a1i 9 |
. . . . . . . . . . . 12
# |
41 | | muldivdirap 7795 |
. . . . . . . . . . . 12
# |
42 | 35, 36, 40, 41 | syl3anc 1169 |
. . . . . . . . . . 11
|
43 | 42 | breq2d 3797 |
. . . . . . . . . 10
|
44 | 43 | adantr 270 |
. . . . . . . . 9
|
45 | | 2z 8379 |
. . . . . . . . . . . . . . . . 17
|
46 | 45 | a1i 9 |
. . . . . . . . . . . . . . . 16
|
47 | | id 19 |
. . . . . . . . . . . . . . . 16
|
48 | 46, 47 | zmulcld 8475 |
. . . . . . . . . . . . . . 15
|
49 | 48 | zcnd 8470 |
. . . . . . . . . . . . . 14
|
50 | 49 | adantr 270 |
. . . . . . . . . . . . 13
|
51 | | pncan1 7481 |
. . . . . . . . . . . . 13
|
52 | 50, 51 | syl 14 |
. . . . . . . . . . . 12
|
53 | 52 | oveq1d 5547 |
. . . . . . . . . . 11
|
54 | | 2cnd 8112 |
. . . . . . . . . . . . 13
|
55 | 38 | a1i 9 |
. . . . . . . . . . . . 13
# |
56 | 35, 54, 55 | divcanap3d 7882 |
. . . . . . . . . . . 12
|
57 | 56 | adantr 270 |
. . . . . . . . . . 11
|
58 | 53, 57 | eqtrd 2113 |
. . . . . . . . . 10
|
59 | 58 | breq2d 3797 |
. . . . . . . . 9
|
60 | 34, 44, 59 | 3bitr4d 218 |
. . . . . . . 8
|
61 | | oveq1 5539 |
. . . . . . . . . 10
|
62 | 61 | breq2d 3797 |
. . . . . . . . 9
|
63 | | oveq1 5539 |
. . . . . . . . . . 11
|
64 | 63 | oveq1d 5547 |
. . . . . . . . . 10
|
65 | 64 | breq2d 3797 |
. . . . . . . . 9
|
66 | 62, 65 | bibi12d 233 |
. . . . . . . 8
|
67 | 60, 66 | syl5ibcom 153 |
. . . . . . 7
|
68 | 67 | ex 113 |
. . . . . 6
|
69 | 68 | adantl 271 |
. . . . 5
|
70 | 69 | com23 77 |
. . . 4
|
71 | 70 | rexlimdva 2477 |
. . 3
|
72 | 1, 71 | sylbid 148 |
. 2
|
73 | 72 | 3imp 1132 |
1
|