Step Hyp Ref
Expression 1 bitsval2 14075 . . . . . . 7
2 2z 10921 . . . . . . . . . 10
3 2 a1i 11 . . . . . . . . 9
4 simpl 457 . . . . . . . . . . . 12
5 4 zred 10994 . . . . . . . . . . 11
6 2nn 10718 . . . . . . . . . . . . 13
7 6 a1i 11 . . . . . . . . . . . 12
8 simpr 461 . . . . . . . . . . . 12
9 7 , 8 nnexpcld 12331 . . . . . . . . . . 11
10 5 , 9 nndivred 10609 . . . . . . . . . 10
11 10 flcld 11935 . . . . . . . . 9
12 dvdsnegb 14001 . . . . . . . . 9
13 3 , 11 , 12 syl2anc 661 . . . . . . . 8
14 13 notbid 294 . . . . . . 7
15 11 znegcld 10996 . . . . . . . . 9
16 oddm1even 14047 . . . . . . . . 9
17 15 , 16 syl 16 . . . . . . . 8
18 flltp1 11937 . . . . . . . . . . . . . . . 16
19 10 , 18 syl 16 . . . . . . . . . . . . . . 15
20 11 zred 10994 . . . . . . . . . . . . . . . . 17
21 1red 9632 . . . . . . . . . . . . . . . . 17
22 20 , 21 readdcld 9644 . . . . . . . . . . . . . . . 16
23 10 , 22 ltnegd 10155 . . . . . . . . . . . . . . 15
24 19 , 23 mpbid 210 . . . . . . . . . . . . . 14
25 20 recnd 9643 . . . . . . . . . . . . . . 15
26 21 recnd 9643 . . . . . . . . . . . . . . 15
27 25 , 26 negdi2d 9968 . . . . . . . . . . . . . 14
28 5 recnd 9643 . . . . . . . . . . . . . . 15
29 9 nncnd 10577 . . . . . . . . . . . . . . 15
30 9 nnne0d 10605 . . . . . . . . . . . . . . 15
31 28 , 29 , 30 divnegd 10358 . . . . . . . . . . . . . 14
32 24 , 27 , 31 3brtr3d 4481 . . . . . . . . . . . . 13
33 1zzd 10920 . . . . . . . . . . . . . . . 16
34 15 , 33 zsubcld 10999 . . . . . . . . . . . . . . 15
35 34 zred 10994 . . . . . . . . . . . . . 14
36 5 renegcld 10011 . . . . . . . . . . . . . 14
37 9 nnrpd 11284 . . . . . . . . . . . . . 14
38 35 , 36 , 37 ltmuldivd 11328 . . . . . . . . . . . . 13
39 32 , 38 mpbird 232 . . . . . . . . . . . 12
40 9 nnzd 10993 . . . . . . . . . . . . . 14
41 34 , 40 zmulcld 11000 . . . . . . . . . . . . 13
42 4 znegcld 10996 . . . . . . . . . . . . 13
43 zltlem1 10941 . . . . . . . . . . . . 13
44 41 , 42 , 43 syl2anc 661 . . . . . . . . . . . 12
45 39 , 44 mpbid 210 . . . . . . . . . . 11
46 36 , 21 resubcld 10012 . . . . . . . . . . . 12
47 35 , 46 , 37 lemuldivd 11330 . . . . . . . . . . 11
48 45 , 47 mpbid 210 . . . . . . . . . 10
49 flle 11936 . . . . . . . . . . . . . . . . 17
50 10 , 49 syl 16 . . . . . . . . . . . . . . . 16
51 20 , 10 lenegd 10156 . . . . . . . . . . . . . . . 16
52 50 , 51 mpbid 210 . . . . . . . . . . . . . . 15
53 31 , 52 eqbrtrrd 4474 . . . . . . . . . . . . . 14
54 20 renegcld 10011 . . . . . . . . . . . . . . 15
55 36 , 54 , 37 ledivmuld 11334 . . . . . . . . . . . . . 14
56 53 , 55 mpbid 210 . . . . . . . . . . . . 13
57 40 , 15 zmulcld 11000 . . . . . . . . . . . . . 14
58 zlem1lt 10940 . . . . . . . . . . . . . 14
59 42 , 57 , 58 syl2anc 661 . . . . . . . . . . . . 13
60 56 , 59 mpbid 210 . . . . . . . . . . . 12
61 46 , 54 , 37 ltdivmuld 11332 . . . . . . . . . . . 12
62 60 , 61 mpbird 232 . . . . . . . . . . 11
63 25 negcld 9941 . . . . . . . . . . . 12
64 63 , 26 npcand 9958 . . . . . . . . . . 11
65 62 , 64 breqtrrd 4478 . . . . . . . . . 10
66 46 , 9 nndivred 10609 . . . . . . . . . . 11
67 flbi 11952 . . . . . . . . . . 11
68 66 , 34 , 67 syl2anc 661 . . . . . . . . . 10
69 48 , 65 , 68 mpbir2and 922 . . . . . . . . 9
70 69 breq2d 4464 . . . . . . . 8
71 17 , 70 bitr4d 256 . . . . . . 7
72 1 , 14 , 71 3bitrd 279 . . . . . 6
73 72 notbid 294 . . . . 5
74 73 pm5.32da 641 . . . 4
75 znegcl 10924 . . . . . 6
76 1zzd 10920 . . . . . 6
77 75 , 76 zsubcld 10999 . . . . 5
78 77 biantrurd 508 . . . 4
79 74 , 78 bitrd 253 . . 3
80 eldif 3485 . . 3
81 bitsval 14074 . . . 4
82 3anass 977 . . . 4
83 81 , 82 bitri 249 . . 3
84 79 , 80 , 83 3bitr4g 288 . 2
85 84 eqrdv 2454 1
