Step Hyp Ref
Expression 1 bitsf 14077 . 2
2 simpl 457 . . . . . . . 8
3 2 zcnd 10995 . . . . . . 7
4 3 adantr 465 . . . . . 6
5 simpr 461 . . . . . . . 8
6 5 zcnd 10995 . . . . . . 7
7 6 adantr 465 . . . . . 6
8 4 negcld 9941 . . . . . . 7
9 7 negcld 9941 . . . . . . 7
10 1cnd 9633 . . . . . . 7
11 simprr 757 . . . . . . . . . . 11
12 11 difeq2d 3621 . . . . . . . . . 10
13 bitscmp 14088 . . . . . . . . . . 11
14 13 ad2antrr 725 . . . . . . . . . 10
15 bitscmp 14088 . . . . . . . . . . 11
16 15 ad2antlr 726 . . . . . . . . . 10
17 12 , 14 , 16 3eqtr3d 2506 . . . . . . . . 9
18 nnm1nn0 10862 . . . . . . . . . . 11
19 18 ad2antrl 727 . . . . . . . . . 10
20 fvres 5885 . . . . . . . . . 10
21 19 , 20 syl 16 . . . . . . . . 9
22 ominf 7752 . . . . . . . . . . . . . . . . 17
23 nn0ennn 12089 . . . . . . . . . . . . . . . . . . 19
24 nnenom 12090 . . . . . . . . . . . . . . . . . . 19
25 23 , 24 entr2i 7590 . . . . . . . . . . . . . . . . . 18
26 enfii 7757 . . . . . . . . . . . . . . . . . 18
27 25 , 26 mpan2 671 . . . . . . . . . . . . . . . . 17
28 22 , 27 mto 176 . . . . . . . . . . . . . . . 16
29 difinf 7810 . . . . . . . . . . . . . . . 16
30 28 , 29 mpan 670 . . . . . . . . . . . . . . 15
31 bitsfi 14087 . . . . . . . . . . . . . . . . 17
32 19 , 31 syl 16 . . . . . . . . . . . . . . . 16
33 14 , 32 eqeltrd 2545 . . . . . . . . . . . . . . 15
34 30 , 33 nsyl3 119 . . . . . . . . . . . . . 14
35 11 , 34 eqneltrrd 2567 . . . . . . . . . . . . 13
36 bitsfi 14087 . . . . . . . . . . . . 13
37 35 , 36 nsyl 121 . . . . . . . . . . . 12
38 5 znegcld 10996 . . . . . . . . . . . . . . . 16
39 elznn 10905 . . . . . . . . . . . . . . . . 17
40 39 simprbi 464 . . . . . . . . . . . . . . . 16
41 38 , 40 syl 16 . . . . . . . . . . . . . . 15
42 6 negnegd 9945 . . . . . . . . . . . . . . . . 17
43 42 eleq1d 2526 . . . . . . . . . . . . . . . 16
44 43 orbi2d 701 . . . . . . . . . . . . . . 15
45 41 , 44 mpbid 210 . . . . . . . . . . . . . 14
46 45 adantr 465 . . . . . . . . . . . . 13
47 46 ord 377 . . . . . . . . . . . 12
48 37 , 47 mt3d 125 . . . . . . . . . . 11
49 nnm1nn0 10862 . . . . . . . . . . 11
50 48 , 49 syl 16 . . . . . . . . . 10
51 fvres 5885 . . . . . . . . . 10
52 50 , 51 syl 16 . . . . . . . . 9
53 17 , 21 , 52 3eqtr4d 2508 . . . . . . . 8
54 bitsf1o 14095 . . . . . . . . . . 11
55 f1of1 5820 . . . . . . . . . . 11
56 54 , 55 ax-mp 5 . . . . . . . . . 10
57 f1fveq 6170 . . . . . . . . . 10
58 56 , 57 mpan 670 . . . . . . . . 9
59 19 , 50 , 58 syl2anc 661 . . . . . . . 8
60 53 , 59 mpbid 210 . . . . . . 7
61 8 , 9 , 10 , 60 subcan2d 9996 . . . . . 6
62 4 , 7 , 61 neg11d 9966 . . . . 5
63 62 expr 615 . . . 4
64 3 negnegd 9945 . . . . . . 7
65 64 eleq1d 2526 . . . . . 6
66 65 biimpa 484 . . . . 5
67 simprr 757 . . . . . . . 8
68 fvres 5885 . . . . . . . . 9
69 68 ad2antrl 727 . . . . . . . 8
70 15 ad2antlr 726 . . . . . . . . . . . . 13
71 bitsfi 14087 . . . . . . . . . . . . . . . 16
72 71 ad2antrl 727 . . . . . . . . . . . . . . 15
73 67 , 72 eqeltrrd 2546 . . . . . . . . . . . . . 14
74 difinf 7810 . . . . . . . . . . . . . 14
75 28 , 73 , 74 sylancr 663 . . . . . . . . . . . . 13
76 70 , 75 eqneltrrd 2567 . . . . . . . . . . . 12
77 bitsfi 14087 . . . . . . . . . . . 12
78 76 , 77 nsyl 121 . . . . . . . . . . 11
79 78 , 49 nsyl 121 . . . . . . . . . 10
80 45 adantr 465 . . . . . . . . . . 11
81 80 ord 377 . . . . . . . . . 10
82 79 , 81 mpd 15 . . . . . . . . 9
83 fvres 5885 . . . . . . . . 9
84 82 , 83 syl 16 . . . . . . . 8
85 67 , 69 , 84 3eqtr4d 2508 . . . . . . 7
86 simprl 756 . . . . . . . 8
87 f1fveq 6170 . . . . . . . . 9
88 56 , 87 mpan 670 . . . . . . . 8
89 86 , 82 , 88 syl2anc 661 . . . . . . 7
90 85 , 89 mpbid 210 . . . . . 6
91 90 expr 615 . . . . 5
92 66 , 91 syldan 470 . . . 4
93 2 znegcld 10996 . . . . 5
94 elznn 10905 . . . . . 6
95 94 simprbi 464 . . . . 5
96 93 , 95 syl 16 . . . 4
97 63 , 92 , 96 mpjaodan 786 . . 3
98 97 rgen2a 2884 . 2
99 dff13 6166 . 2
100 1 , 98 , 99 mpbir2an 920 1
