Step | Hyp | Ref
| Expression |
1 | | bitsf 15149 |
. 2
bits |
2 | | simpl 473 |
. . . . . . . 8
|
3 | 2 | zcnd 11483 |
. . . . . . 7
|
4 | 3 | adantr 481 |
. . . . . 6
bits bits |
5 | | simpr 477 |
. . . . . . . 8
|
6 | 5 | zcnd 11483 |
. . . . . . 7
|
7 | 6 | adantr 481 |
. . . . . 6
bits bits |
8 | 4 | negcld 10379 |
. . . . . . 7
bits bits |
9 | 7 | negcld 10379 |
. . . . . . 7
bits bits |
10 | | 1cnd 10056 |
. . . . . . 7
bits bits |
11 | | simprr 796 |
. . . . . . . . . . 11
bits bits bits bits |
12 | 11 | difeq2d 3728 |
. . . . . . . . . 10
bits bits bits bits |
13 | | bitscmp 15160 |
. . . . . . . . . . 11
bits bits |
14 | 13 | ad2antrr 762 |
. . . . . . . . . 10
bits bits bits bits |
15 | | bitscmp 15160 |
. . . . . . . . . . 11
bits bits |
16 | 15 | ad2antlr 763 |
. . . . . . . . . 10
bits bits bits bits |
17 | 12, 14, 16 | 3eqtr3d 2664 |
. . . . . . . . 9
bits bits bits bits |
18 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
19 | 18 | ad2antrl 764 |
. . . . . . . . . 10
bits bits |
20 | | fvres 6207 |
. . . . . . . . . 10
bits bits |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
bits bits bits bits |
22 | | ominf 8172 |
. . . . . . . . . . . . . . . . 17
|
23 | | nn0ennn 12778 |
. . . . . . . . . . . . . . . . . . 19
|
24 | | nnenom 12779 |
. . . . . . . . . . . . . . . . . . 19
|
25 | 23, 24 | entr2i 8011 |
. . . . . . . . . . . . . . . . . 18
|
26 | | enfii 8177 |
. . . . . . . . . . . . . . . . . 18
|
27 | 25, 26 | mpan2 707 |
. . . . . . . . . . . . . . . . 17
|
28 | 22, 27 | mto 188 |
. . . . . . . . . . . . . . . 16
|
29 | | difinf 8230 |
. . . . . . . . . . . . . . . 16
bits bits |
30 | 28, 29 | mpan 706 |
. . . . . . . . . . . . . . 15
bits bits |
31 | | bitsfi 15159 |
. . . . . . . . . . . . . . . . 17
bits |
32 | 19, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
bits bits bits |
33 | 14, 32 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
bits bits bits |
34 | 30, 33 | nsyl3 133 |
. . . . . . . . . . . . . 14
bits bits
bits |
35 | 11, 34 | eqneltrrd 2721 |
. . . . . . . . . . . . 13
bits bits
bits |
36 | | bitsfi 15159 |
. . . . . . . . . . . . 13
bits |
37 | 35, 36 | nsyl 135 |
. . . . . . . . . . . 12
bits bits
|
38 | 5 | znegcld 11484 |
. . . . . . . . . . . . . . . 16
|
39 | | elznn 11393 |
. . . . . . . . . . . . . . . . 17
|
40 | 39 | simprbi 480 |
. . . . . . . . . . . . . . . 16
|
41 | 38, 40 | syl 17 |
. . . . . . . . . . . . . . 15
|
42 | 6 | negnegd 10383 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | orbi2d 738 |
. . . . . . . . . . . . . . 15
|
45 | 41, 44 | mpbid 222 |
. . . . . . . . . . . . . 14
|
46 | 45 | adantr 481 |
. . . . . . . . . . . . 13
bits bits |
47 | 46 | ord 392 |
. . . . . . . . . . . 12
bits bits
|
48 | 37, 47 | mt3d 140 |
. . . . . . . . . . 11
bits bits |
49 | | nnm1nn0 11334 |
. . . . . . . . . . 11
|
50 | 48, 49 | syl 17 |
. . . . . . . . . 10
bits bits |
51 | | fvres 6207 |
. . . . . . . . . 10
bits bits |
52 | 50, 51 | syl 17 |
. . . . . . . . 9
bits bits bits bits |
53 | 17, 21, 52 | 3eqtr4d 2666 |
. . . . . . . 8
bits bits bits bits |
54 | | bitsf1o 15167 |
. . . . . . . . . . 11
bits |
55 | | f1of1 6136 |
. . . . . . . . . . 11
bits bits |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . 10
bits |
57 | | f1fveq 6519 |
. . . . . . . . . 10
bits
bits bits
|
58 | 56, 57 | mpan 706 |
. . . . . . . . 9
bits bits |
59 | 19, 50, 58 | syl2anc 693 |
. . . . . . . 8
bits bits bits bits |
60 | 53, 59 | mpbid 222 |
. . . . . . 7
bits bits |
61 | 8, 9, 10, 60 | subcan2d 10434 |
. . . . . 6
bits bits |
62 | 4, 7, 61 | neg11d 10404 |
. . . . 5
bits bits |
63 | 62 | expr 643 |
. . . 4
bits bits |
64 | 3 | negnegd 10383 |
. . . . . . 7
|
65 | 64 | eleq1d 2686 |
. . . . . 6
|
66 | 65 | biimpa 501 |
. . . . 5
|
67 | | simprr 796 |
. . . . . . . 8
bits bits bits bits |
68 | | fvres 6207 |
. . . . . . . . 9
bits bits |
69 | 68 | ad2antrl 764 |
. . . . . . . 8
bits bits bits bits |
70 | 15 | ad2antlr 763 |
. . . . . . . . . . . . 13
bits bits bits bits |
71 | | bitsfi 15159 |
. . . . . . . . . . . . . . . 16
bits |
72 | 71 | ad2antrl 764 |
. . . . . . . . . . . . . . 15
bits bits bits |
73 | 67, 72 | eqeltrrd 2702 |
. . . . . . . . . . . . . 14
bits bits bits |
74 | | difinf 8230 |
. . . . . . . . . . . . . 14
bits bits |
75 | 28, 73, 74 | sylancr 695 |
. . . . . . . . . . . . 13
bits bits
bits |
76 | 70, 75 | eqneltrrd 2721 |
. . . . . . . . . . . 12
bits bits
bits |
77 | | bitsfi 15159 |
. . . . . . . . . . . 12
bits |
78 | 76, 77 | nsyl 135 |
. . . . . . . . . . 11
bits bits
|
79 | 78, 49 | nsyl 135 |
. . . . . . . . . 10
bits bits
|
80 | 45 | adantr 481 |
. . . . . . . . . . 11
bits bits |
81 | 80 | ord 392 |
. . . . . . . . . 10
bits bits
|
82 | 79, 81 | mpd 15 |
. . . . . . . . 9
bits bits |
83 | | fvres 6207 |
. . . . . . . . 9
bits bits |
84 | 82, 83 | syl 17 |
. . . . . . . 8
bits bits bits bits |
85 | 67, 69, 84 | 3eqtr4d 2666 |
. . . . . . 7
bits bits bits bits |
86 | | simprl 794 |
. . . . . . . 8
bits bits |
87 | | f1fveq 6519 |
. . . . . . . . 9
bits
bits bits
|
88 | 56, 87 | mpan 706 |
. . . . . . . 8
bits bits
|
89 | 86, 82, 88 | syl2anc 693 |
. . . . . . 7
bits bits bits bits
|
90 | 85, 89 | mpbid 222 |
. . . . . 6
bits bits |
91 | 90 | expr 643 |
. . . . 5
bits bits |
92 | 66, 91 | syldan 487 |
. . . 4
bits bits |
93 | 2 | znegcld 11484 |
. . . . 5
|
94 | | elznn 11393 |
. . . . . 6
|
95 | 94 | simprbi 480 |
. . . . 5
|
96 | 93, 95 | syl 17 |
. . . 4
|
97 | 63, 92, 96 | mpjaodan 827 |
. . 3
bits bits |
98 | 97 | rgen2a 2977 |
. 2
bits bits |
99 | | dff13 6512 |
. 2
bits
bits
bits bits |
100 | 1, 98, 99 | mpbir2an 955 |
1
bits |