Step | Hyp | Ref
| Expression |
1 | | odd2np1 15065 |
. . 3
|
2 | | halfre 11246 |
. . . . . . . . . . . . . . . 16
|
3 | 2 | a1i 11 |
. . . . . . . . . . . . . . 15
|
4 | | 1red 10055 |
. . . . . . . . . . . . . . 15
|
5 | | zre 11381 |
. . . . . . . . . . . . . . 15
|
6 | 3, 4, 5 | 3jca 1242 |
. . . . . . . . . . . . . 14
|
7 | 6 | adantr 481 |
. . . . . . . . . . . . 13
|
8 | | halflt1 11250 |
. . . . . . . . . . . . 13
|
9 | | axltadd 10111 |
. . . . . . . . . . . . 13
|
10 | 7, 8, 9 | mpisyl 21 |
. . . . . . . . . . . 12
|
11 | | zre 11381 |
. . . . . . . . . . . . . 14
|
12 | 11 | adantl 482 |
. . . . . . . . . . . . 13
|
13 | 5, 3 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
14 | 13 | adantr 481 |
. . . . . . . . . . . . 13
|
15 | | peano2z 11418 |
. . . . . . . . . . . . . . 15
|
16 | 15 | zred 11482 |
. . . . . . . . . . . . . 14
|
17 | 16 | adantr 481 |
. . . . . . . . . . . . 13
|
18 | | lttr 10114 |
. . . . . . . . . . . . 13
|
19 | 12, 14, 17, 18 | syl3anc 1326 |
. . . . . . . . . . . 12
|
20 | 10, 19 | mpan2d 710 |
. . . . . . . . . . 11
|
21 | | zleltp1 11428 |
. . . . . . . . . . . 12
|
22 | 21 | ancoms 469 |
. . . . . . . . . . 11
|
23 | 20, 22 | sylibrd 249 |
. . . . . . . . . 10
|
24 | | halfgt0 11248 |
. . . . . . . . . . . 12
|
25 | 3, 5 | jca 554 |
. . . . . . . . . . . . . 14
|
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
|
27 | | ltaddpos 10518 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
|
29 | 24, 28 | mpbii 223 |
. . . . . . . . . . 11
|
30 | 5 | adantr 481 |
. . . . . . . . . . . 12
|
31 | | lelttr 10128 |
. . . . . . . . . . . 12
|
32 | 12, 30, 14, 31 | syl3anc 1326 |
. . . . . . . . . . 11
|
33 | 29, 32 | mpan2d 710 |
. . . . . . . . . 10
|
34 | 23, 33 | impbid 202 |
. . . . . . . . 9
|
35 | | zcn 11382 |
. . . . . . . . . . . 12
|
36 | | 1cnd 10056 |
. . . . . . . . . . . 12
|
37 | | 2cnne0 11242 |
. . . . . . . . . . . . 13
|
38 | 37 | a1i 11 |
. . . . . . . . . . . 12
|
39 | | muldivdir 10720 |
. . . . . . . . . . . 12
|
40 | 35, 36, 38, 39 | syl3anc 1326 |
. . . . . . . . . . 11
|
41 | 40 | breq2d 4665 |
. . . . . . . . . 10
|
42 | 41 | adantr 481 |
. . . . . . . . 9
|
43 | | 2z 11409 |
. . . . . . . . . . . . . . . . 17
|
44 | 43 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
45 | | id 22 |
. . . . . . . . . . . . . . . 16
|
46 | 44, 45 | zmulcld 11488 |
. . . . . . . . . . . . . . 15
|
47 | 46 | zcnd 11483 |
. . . . . . . . . . . . . 14
|
48 | 47 | adantr 481 |
. . . . . . . . . . . . 13
|
49 | | pncan1 10454 |
. . . . . . . . . . . . 13
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . 12
|
51 | 50 | oveq1d 6665 |
. . . . . . . . . . 11
|
52 | | 2cnd 11093 |
. . . . . . . . . . . . 13
|
53 | | 2ne0 11113 |
. . . . . . . . . . . . . 14
|
54 | 53 | a1i 11 |
. . . . . . . . . . . . 13
|
55 | 35, 52, 54 | divcan3d 10806 |
. . . . . . . . . . . 12
|
56 | 55 | adantr 481 |
. . . . . . . . . . 11
|
57 | 51, 56 | eqtrd 2656 |
. . . . . . . . . 10
|
58 | 57 | breq2d 4665 |
. . . . . . . . 9
|
59 | 34, 42, 58 | 3bitr4d 300 |
. . . . . . . 8
|
60 | | oveq1 6657 |
. . . . . . . . . 10
|
61 | 60 | breq2d 4665 |
. . . . . . . . 9
|
62 | | oveq1 6657 |
. . . . . . . . . . 11
|
63 | 62 | oveq1d 6665 |
. . . . . . . . . 10
|
64 | 63 | breq2d 4665 |
. . . . . . . . 9
|
65 | 61, 64 | bibi12d 335 |
. . . . . . . 8
|
66 | 59, 65 | syl5ibcom 235 |
. . . . . . 7
|
67 | 66 | ex 450 |
. . . . . 6
|
68 | 67 | adantl 482 |
. . . . 5
|
69 | 68 | com23 86 |
. . . 4
|
70 | 69 | rexlimdva 3031 |
. . 3
|
71 | 1, 70 | sylbid 230 |
. 2
|
72 | 71 | 3imp 1256 |
1
|