Nearby theorems
|
|
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > ILE Home > Th. List > bitsfzo | Unicode version | ||
Description: The bits of a number are
all at positions less than  iff the number
is nonnegative and less than   . (Contributed by Mario
Carneiro, 5-Sep-2016.) (Proof shortened by AV,
1-Oct-2020.) |
| Ref | Expression |
|---|---|
| bitsfzo |
     ![/\](wedge.gif "/\"){kind=small}
    ..^ 
bits 
..^ |
are mutually distinct and distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitsval 12298 |
. . . 4
bits
    | |
| 2 | simp32 1037 |
. . . . . . 7
..^
| |
| 3 | nn0uz 9690 |
. . . . . . 7
  | |
| 4 | 2, 3 | eleqtrdi 2299 |
. . . . . 6
..^
|
| 5 | simp1r 1025 |
. . . . . . 7
..^
| |
| 6 | 5 | nn0zd 9500 |
. . . . . 6
..^
|
| 7 | 2re 9113 |
. . . . . . . . . 10
 | |
| 8 | 7 | a1i 9 |
. . . . . . . . 9
..^
|
| 9 | 8, 2 | reexpcld 10842 |
. . . . . . . 8
..^
|
| 10 | simp1l 1024 |
. . . . . . . . 9
..^
| |
| 11 | 10 | zred 9502 |
. . . . . . . 8
..^
|
| 12 | 8, 5 | reexpcld 10842 |
. . . . . . . 8
..^
|
| 13 | 9 | recnd 8108 |
. . . . . . . . . 10
..^
 |
| 14 | 13 | mullidd 8097 |
. . . . . . . . 9
..^
  |
| 15 | 1z 9405 |
. . . . . . . . . . . . . 14
| |
| 16 | zq 9754 |
. . . . . . . . . . . . . 14
 | |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
|
| 18 | 17 | a1i 9 |
. . . . . . . . . . . 12
..^
|
| 19 | 2nn 9205 |
. . . . . . . . . . . . . . 15
 | |
| 20 | 19 | a1i 9 |
. . . . . . . . . . . . . 14
..^
|
| 21 | 20, 2 | nnexpcld 10847 |
. . . . . . . . . . . . 13
..^
|
| 22 | znq 9752 |
. . . . . . . . . . . . 13
| |
| 23 | 10, 21, 22 | syl2anc 411 |
. . . . . . . . . . . 12
..^
|
| 24 | qdcle 10396 |
. . . . . . . . . . . 12
DECID 
| |
| 25 | 18, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
..^
DECID
|
| 26 | simp33 1038 |
. . . . . . . . . . . 12
..^
| |
| 27 | qltnle 10393 |
. . . . . . . . . . . . . 14
| |
| 28 | 23, 18, 27 | syl2anc 411 |
. . . . . . . . . . . . 13
..^
|
| 29 | 0p1e1 9157 |
. . . . . . . . . . . . . . 15
 | |
| 30 | 29 | breq2i 4055 |
. . . . . . . . . . . . . 14
|
| 31 | 2rp 9787 |
. . . . . . . . . . . . . . . . . 18
 | |
| 32 | 31 | a1i 9 |
. . . . . . . . . . . . . . . . 17
..^
|
| 33 | 2 | nn0zd 9500 |
. . . . . . . . . . . . . . . . 17
..^
|
| 34 | 32, 33 | rpexpcld 10849 |
. . . . . . . . . . . . . . . 16
..^
|
| 35 | elfzole1 10285 |
. . . . . . . . . . . . . . . . 17
..^
| |
| 36 | 35 | 3ad2ant2 1022 |
. . . . . . . . . . . . . . . 16
..^
|
| 37 | 11, 34, 36 | divge0d 9866 |
. . . . . . . . . . . . . . 15
..^
|
| 38 | 0z 9390 |
. . . . . . . . . . . . . . . . 17
| |
| 39 | flqbi 10440 |
. . . . . . . . . . . . . . . . 17
| |
| 40 | 23, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
..^
|
| 41 | z0even 12266 |
. . . . . . . . . . . . . . . . 17
| |
| 42 | id 19 |
. . . . . . . . . . . . . . . . 17
| |
| 43 | 41, 42 | breqtrrid 4085 |
. . . . . . . . . . . . . . . 16
|
| 44 | 40, 43 | biimtrrdi 164 |
. . . . . . . . . . . . . . 15
..^
|
| 45 | 37, 44 | mpand 429 |
. . . . . . . . . . . . . 14
..^
|
| 46 | 30, 45 | biimtrrid 153 |
. . . . . . . . . . . . 13
..^
|
| 47 | 28, 46 | sylbird 170 |
. . . . . . . . . . . 12
..^
|
| 48 | 26, 47 | mtod 665 |
. . . . . . . . . . 11
..^
|
| 49 | notnotrdc 845 |
. . . . . . . . . . 11
DECID
| |
| 50 | 25, 48, 49 | sylc 62 |
. . . . . . . . . 10
..^
|
| 51 | 1red 8094 |
. . . . . . . . . . 11
..^
| |
| 52 | 51, 11, 34 | lemuldivd 9875 |
. . . . . . . . . 10
..^
|
| 53 | 50, 52 | mpbird 167 |
. . . . . . . . 9
..^
|
| 54 | 14, 53 | eqbrtrrd 4071 |
. . . . . . . 8
..^
|
| 55 | elfzolt2 10286 |
. . . . . . . . 9
..^
| |
| 56 | 55 | 3ad2ant2 1022 |
. . . . . . . 8
..^
|
| 57 | 9, 11, 12, 54, 56 | lelttrd 8204 |
. . . . . . 7
..^
|
| 58 | 1lt2 9213 |
. . . . . . . . 9
| |
| 59 | 58 | a1i 9 |
. . . . . . . 8
..^
|
| 60 | nn0ltexp2 10861 |
. . . . . . . 8
| |
| 61 | 8, 2, 5, 59, 60 | syl31anc 1253 |
. . . . . . 7
..^
|
| 62 | 57, 61 | mpbird 167 |
. . . . . 6
..^
|
| 63 | elfzo2 10279 |
. . . . . 6
..^
| |
| 64 | 4, 6, 62, 63 | syl3anbrc 1184 |
. . . . 5
..^
..^ |
| 65 | 64 | 3expia 1208 |
. . . 4
..^
..^ |
| 66 | 1, 65 | biimtrid 152 |
. . 3
..^ bits ..^ |
| 67 | 66 | ssrdv 3200 |
. 2
..^ bits
..^ |
| 68 | simpr 110 |
. . . . . . . 8
bits ..^  | |
| 69 | 68 | nnred 9056 |
. . . . . . 7
bits ..^ |
| 70 | simpllr 534 |
. . . . . . . 8
bits ..^ | |
| 71 | 70 | nn0red 9356 |
. . . . . . 7
bits ..^ |
| 72 | maxle2 11567 |
. . . . . . 7
    | |
| 73 | 69, 71, 72 | syl2anc 411 |
. . . . . 6
bits ..^ |
| 74 | simplr 528 |
. . . . . . . . 9
bits ..^ bits
..^ | |
| 75 | n2dvdsm1 12268 |
. . . . . . . . . . 11
| |
| 76 | simplll 533 |
. . . . . . . . . . . . . . . 16
bits ..^ | |
| 77 | 76 | zred 9502 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 78 | 19 | a1i 9 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 79 | 68 | nnnn0d 9355 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 80 | nn0maxcl 11580 |
. . . . . . . . . . . . . . . . 17
| |
| 81 | 79, 70, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 82 | 78, 81 | nnexpcld 10847 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 83 | 77, 82 | nndivred 9093 |
. . . . . . . . . . . . . 14
bits ..^ |
| 84 | 1red 8094 |
. . . . . . . . . . . . . 14
bits ..^ | |
| 85 | 76 | zcnd 9503 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 86 | 82 | nncnd 9057 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 87 | 82 | nnap0d 9089 |
. . . . . . . . . . . . . . . 16
bits ..^
# |
| 88 | 85, 86, 87 | divnegapd 8883 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 89 | 81 | nn0red 9356 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 90 | 82 | nnred 9056 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 91 | maxle1 11566 |
. . . . . . . . . . . . . . . . . . 19
| |
| 92 | 69, 71, 91 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
| 93 | 2z 9407 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 94 | uzid 9669 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 96 | bernneq3 10814 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 97 | 95, 81, 96 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
bits ..^
|
| 98 | 89, 90, 97 | ltled 8198 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 99 | 69, 89, 90, 92, 98 | letrd 8203 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 100 | 86 | mulridd 8096 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 101 | 99, 100 | breqtrrd 4075 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 102 | 82 | nnrpd 9823 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 103 | 69, 84, 102 | ledivmuld 9879 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 104 | 101, 103 | mpbird 167 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 105 | 88, 104 | eqbrtrd 4069 |
. . . . . . . . . . . . . 14
bits ..^ |
| 106 | 83, 84, 105 | lenegcon1d 8607 |
. . . . . . . . . . . . 13
bits ..^
|
| 107 | 68 | nngt0d 9087 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 108 | 82 | nngt0d 9087 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 109 | 69, 90, 107, 108 | divgt0d 9015 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 110 | 109, 88 | breqtrrd 4075 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 111 | 83 | lt0neg1d 8595 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 112 | 110, 111 | mpbird 167 |
. . . . . . . . . . . . . 14
bits ..^ |
| 113 | ax-1cn 8025 |
. . . . . . . . . . . . . . 15
| |
| 114 | neg1cn 9148 |
. . . . . . . . . . . . . . 15
| |
| 115 | 1pneg1e0 9154 |
. . . . . . . . . . . . . . 15
| |
| 116 | 113, 114, 115 | addcomli 8224 |
. . . . . . . . . . . . . 14
|
| 117 | 112, 116 | breqtrrdi 4089 |
. . . . . . . . . . . . 13
bits ..^ |
| 118 | znq 9752 |
. . . . . . . . . . . . . . 15
| |
| 119 | 76, 82, 118 | syl2anc 411 |
. . . . . . . . . . . . . 14
bits ..^ |
| 120 | neg1z 9411 |
. . . . . . . . . . . . . 14
| |
| 121 | flqbi 10440 |
. . . . . . . . . . . . . 14
| |
| 122 | 119, 120, 121 | sylancl 413 |
. . . . . . . . . . . . 13
bits ..^
|
| 123 | 106, 117, 122 | mpbir2and 947 |
. . . . . . . . . . . 12
bits ..^
|
| 124 | 123 | breq2d 4059 |
. . . . . . . . . . 11
bits ..^
|
| 125 | 75, 124 | mtbiri 677 |
. . . . . . . . . 10
bits ..^
|
| 126 | bitsval2 12299 |
. . . . . . . . . . 11
bits
| |
| 127 | 76, 81, 126 | syl2anc 411 |
. . . . . . . . . 10
bits ..^
bits
|
| 128 | 125, 127 | mpbird 167 |
. . . . . . . . 9
bits ..^
bits |
| 129 | 74, 128 | sseldd 3195 |
. . . . . . . 8
bits ..^
..^ |
| 130 | elfzolt2 10286 |
. . . . . . . 8
..^ | |
| 131 | 129, 130 | syl 14 |
. . . . . . 7
bits ..^
|
| 132 | 81 | nn0zd 9500 |
. . . . . . . 8
bits ..^
|
| 133 | 70 | nn0zd 9500 |
. . . . . . . 8
bits ..^ |
| 134 | zltnle 9425 |
. . . . . . . 8
| |
| 135 | 132, 133, 134 | syl2anc 411 |
. . . . . . 7
bits ..^
|
| 136 | 131, 135 | mpbid 147 |
. . . . . 6
bits ..^
|
| 137 | 73, 136 | pm2.65da 663 |
. . . . 5
bits ..^
|
| 138 | 137 | intnand 933 |
. . . 4
bits ..^
|
| 139 | simpll 527 |
. . . . 5
bits ..^
| |
| 140 | elznn0nn 9393 |
. . . . 5
 | |
| 141 | 139, 140 | sylib 122 |
. . . 4
bits ..^
|
| 142 | 138, 141 | ecased 1362 |
. . 3
bits ..^
|
| 143 | simplr 528 |
. . 3
bits ..^
| |
| 144 | simpr 110 |
. . 3
bits ..^
bits
..^ | |
| 145 | eqid 2206 |
. . 3
inf 
inf
| |
| 146 | 142, 143, 144, 145 | bitsfzolem 12309 |
. 2
bits ..^
..^ |
| 147 | 67, 146 | impbida 596 |
1
..^
bits
..^ |
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 104
wb 105 wo 710 DECID wdc 836
w3a 981
wceq 1373
wcel 2177
crab 2489
wss 3167
cpr 3635
class class class wbr 4047 cfv 5276 (class class class)co 5951
csup 7091
infcinf 7092 cr 7931 cc0 7932 c1 7933 caddc 7935 cmul 7937 clt 8114 cle 8115 cneg 8251 cdiv 8752 cn 9043 c2 9094 cn0 9302 cz 9379 cuz 9655 cq 9747 crp 9782 ..^cfzo 10271
cfl 10418
cexp 10690
cdvds 12142 bitscbits 12295 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4163 ax-sep 4166 ax-nul 4174 ax-pow 4222 ax-pr 4257 ax-un 4484 ax-setind 4589 ax-iinf 4640 ax-cnex 8023 ax-resscn 8024 ax-1cn 8025 ax-1re 8026 ax-icn 8027 ax-addcl 8028 ax-addrcl 8029 ax-mulcl 8030 ax-mulrcl 8031 ax-addcom 8032 ax-mulcom 8033 ax-addass 8034 ax-mulass 8035 ax-distr 8036 ax-i2m1 8037 ax-0lt1 8038 ax-1rid 8039 ax-0id 8040 ax-rnegex 8041 ax-precex 8042 ax-cnre 8043 ax-pre-ltirr 8044 ax-pre-ltwlin 8045 ax-pre-lttrn 8046 ax-pre-apti 8047 ax-pre-ltadd 8048 ax-pre-mulgt0 8049 ax-pre-mulext 8050 ax-arch 8051 ax-caucvg 8052 |
| This theorem depends on definitions: df-bi 117 df-dc 837 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-xor 1396 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rmo 2493 df-rab 2494 df-v 2775 df-sbc 3000 df-csb 3095 df-dif 3169 df-un 3171 df-in 3173 df-ss 3180 df-nul 3462 df-if 3573 df-pw 3619 df-sn 3640 df-pr 3641 df-op 3643 df-uni 3853 df-int 3888 df-iun 3931 df-br 4048 df-opab 4110 df-mpt 4111 df-tr 4147 df-id 4344 df-po 4347 df-iso 4348 df-iord 4417 df-on 4419 df-ilim 4420 df-suc 4422 df-iom 4643 df-xp 4685 df-rel 4686 df-cnv 4687 df-co 4688 df-dm 4689 df-rn 4690 df-res 4691 df-ima 4692 df-iota 5237 df-fun 5278 df-fn 5279 df-f 5280 df-f1 5281 df-fo 5282 df-f1o 5283 df-fv 5284 df-isom 5285 df-riota 5906 df-ov 5954 df-oprab 5955 df-mpo 5956 df-1st 6233 df-2nd 6234 df-recs 6398 df-frec 6484 df-sup 7093 df-inf 7094 df-pnf 8116 df-mnf 8117 df-xr 8118 df-ltxr 8119 df-le 8120 df-sub 8252 df-neg 8253 df-reap 8655 df-ap 8662 df-div 8753 df-inn 9044 df-2 9102 df-3 9103 df-4 9104 df-n0 9303 df-z 9380 df-uz 9656 df-q 9748 df-rp 9783 df-fz 10138 df-fzo 10272 df-fl 10420 df-seqfrec 10600 df-exp 10691 df-cj 11197 df-re 11198 df-im 11199 df-rsqrt 11353 df-abs 11354 df-dvds 12143 df-bits 12296 |
| This theorem is referenced by: bitsfi 12312 0bits 12314 bitsinv1 12317 |
| Copyright terms: Public domain | W3C validator |