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 12440 |
. . . 4
bits
    | |
| 2 | simp32 1058 |
. . . . . . 7
..^
| |
| 3 | nn0uz 9745 |
. . . . . . 7
  | |
| 4 | 2, 3 | eleqtrdi 2322 |
. . . . . 6
..^
|
| 5 | simp1r 1046 |
. . . . . . 7
..^
| |
| 6 | 5 | nn0zd 9555 |
. . . . . 6
..^
|
| 7 | 2re 9168 |
. . . . . . . . . 10
 | |
| 8 | 7 | a1i 9 |
. . . . . . . . 9
..^
|
| 9 | 8, 2 | reexpcld 10899 |
. . . . . . . 8
..^
|
| 10 | simp1l 1045 |
. . . . . . . . 9
..^
| |
| 11 | 10 | zred 9557 |
. . . . . . . 8
..^
|
| 12 | 8, 5 | reexpcld 10899 |
. . . . . . . 8
..^
|
| 13 | 9 | recnd 8163 |
. . . . . . . . . 10
..^
 |
| 14 | 13 | mullidd 8152 |
. . . . . . . . 9
..^
  |
| 15 | 1z 9460 |
. . . . . . . . . . . . . 14
| |
| 16 | zq 9809 |
. . . . . . . . . . . . . 14
 | |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
|
| 18 | 17 | a1i 9 |
. . . . . . . . . . . 12
..^
|
| 19 | 2nn 9260 |
. . . . . . . . . . . . . . 15
 | |
| 20 | 19 | a1i 9 |
. . . . . . . . . . . . . 14
..^
|
| 21 | 20, 2 | nnexpcld 10904 |
. . . . . . . . . . . . 13
..^
|
| 22 | znq 9807 |
. . . . . . . . . . . . 13
| |
| 23 | 10, 21, 22 | syl2anc 411 |
. . . . . . . . . . . 12
..^
|
| 24 | qdcle 10453 |
. . . . . . . . . . . 12
DECID 
| |
| 25 | 18, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
..^
DECID
|
| 26 | simp33 1059 |
. . . . . . . . . . . 12
..^
| |
| 27 | qltnle 10450 |
. . . . . . . . . . . . . 14
| |
| 28 | 23, 18, 27 | syl2anc 411 |
. . . . . . . . . . . . 13
..^
|
| 29 | 0p1e1 9212 |
. . . . . . . . . . . . . . 15
 | |
| 30 | 29 | breq2i 4090 |
. . . . . . . . . . . . . 14
|
| 31 | 2rp 9842 |
. . . . . . . . . . . . . . . . . 18
 | |
| 32 | 31 | a1i 9 |
. . . . . . . . . . . . . . . . 17
..^
|
| 33 | 2 | nn0zd 9555 |
. . . . . . . . . . . . . . . . 17
..^
|
| 34 | 32, 33 | rpexpcld 10906 |
. . . . . . . . . . . . . . . 16
..^
|
| 35 | elfzole1 10340 |
. . . . . . . . . . . . . . . . 17
..^
| |
| 36 | 35 | 3ad2ant2 1043 |
. . . . . . . . . . . . . . . 16
..^
|
| 37 | 11, 34, 36 | divge0d 9921 |
. . . . . . . . . . . . . . 15
..^
|
| 38 | 0z 9445 |
. . . . . . . . . . . . . . . . 17
| |
| 39 | flqbi 10497 |
. . . . . . . . . . . . . . . . 17
| |
| 40 | 23, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
..^
|
| 41 | z0even 12408 |
. . . . . . . . . . . . . . . . 17
| |
| 42 | id 19 |
. . . . . . . . . . . . . . . . 17
| |
| 43 | 41, 42 | breqtrrid 4120 |
. . . . . . . . . . . . . . . 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 667 |
. . . . . . . . . . 11
..^
|
| 49 | notnotrdc 848 |
. . . . . . . . . . 11
DECID
| |
| 50 | 25, 48, 49 | sylc 62 |
. . . . . . . . . 10
..^
|
| 51 | 1red 8149 |
. . . . . . . . . . 11
..^
| |
| 52 | 51, 11, 34 | lemuldivd 9930 |
. . . . . . . . . 10
..^
|
| 53 | 50, 52 | mpbird 167 |
. . . . . . . . 9
..^
|
| 54 | 14, 53 | eqbrtrrd 4106 |
. . . . . . . 8
..^
|
| 55 | elfzolt2 10341 |
. . . . . . . . 9
..^
| |
| 56 | 55 | 3ad2ant2 1043 |
. . . . . . . 8
..^
|
| 57 | 9, 11, 12, 54, 56 | lelttrd 8259 |
. . . . . . 7
..^
|
| 58 | 1lt2 9268 |
. . . . . . . . 9
| |
| 59 | 58 | a1i 9 |
. . . . . . . 8
..^
|
| 60 | nn0ltexp2 10918 |
. . . . . . . 8
| |
| 61 | 8, 2, 5, 59, 60 | syl31anc 1274 |
. . . . . . 7
..^
|
| 62 | 57, 61 | mpbird 167 |
. . . . . 6
..^
|
| 63 | elfzo2 10334 |
. . . . . 6
..^
| |
| 64 | 4, 6, 62, 63 | syl3anbrc 1205 |
. . . . 5
..^
..^ |
| 65 | 64 | 3expia 1229 |
. . . 4
..^
..^ |
| 66 | 1, 65 | biimtrid 152 |
. . 3
..^ bits ..^ |
| 67 | 66 | ssrdv 3230 |
. 2
..^ bits
..^ |
| 68 | simpr 110 |
. . . . . . . 8
bits ..^  | |
| 69 | 68 | nnred 9111 |
. . . . . . 7
bits ..^ |
| 70 | simpllr 534 |
. . . . . . . 8
bits ..^ | |
| 71 | 70 | nn0red 9411 |
. . . . . . 7
bits ..^ |
| 72 | maxle2 11709 |
. . . . . . 7
    | |
| 73 | 69, 71, 72 | syl2anc 411 |
. . . . . 6
bits ..^ |
| 74 | simplr 528 |
. . . . . . . . 9
bits ..^ bits
..^ | |
| 75 | n2dvdsm1 12410 |
. . . . . . . . . . 11
| |
| 76 | simplll 533 |
. . . . . . . . . . . . . . . 16
bits ..^ | |
| 77 | 76 | zred 9557 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 78 | 19 | a1i 9 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 79 | 68 | nnnn0d 9410 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 80 | nn0maxcl 11722 |
. . . . . . . . . . . . . . . . 17
| |
| 81 | 79, 70, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 82 | 78, 81 | nnexpcld 10904 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 83 | 77, 82 | nndivred 9148 |
. . . . . . . . . . . . . 14
bits ..^ |
| 84 | 1red 8149 |
. . . . . . . . . . . . . 14
bits ..^ | |
| 85 | 76 | zcnd 9558 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 86 | 82 | nncnd 9112 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 87 | 82 | nnap0d 9144 |
. . . . . . . . . . . . . . . 16
bits ..^
# |
| 88 | 85, 86, 87 | divnegapd 8938 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 89 | 81 | nn0red 9411 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 90 | 82 | nnred 9111 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 91 | maxle1 11708 |
. . . . . . . . . . . . . . . . . . 19
| |
| 92 | 69, 71, 91 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
| 93 | 2z 9462 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 94 | uzid 9724 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 96 | bernneq3 10871 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 97 | 95, 81, 96 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
bits ..^
|
| 98 | 89, 90, 97 | ltled 8253 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 99 | 69, 89, 90, 92, 98 | letrd 8258 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 100 | 86 | mulridd 8151 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 101 | 99, 100 | breqtrrd 4110 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 102 | 82 | nnrpd 9878 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 103 | 69, 84, 102 | ledivmuld 9934 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 104 | 101, 103 | mpbird 167 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 105 | 88, 104 | eqbrtrd 4104 |
. . . . . . . . . . . . . 14
bits ..^ |
| 106 | 83, 84, 105 | lenegcon1d 8662 |
. . . . . . . . . . . . 13
bits ..^
|
| 107 | 68 | nngt0d 9142 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 108 | 82 | nngt0d 9142 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 109 | 69, 90, 107, 108 | divgt0d 9070 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 110 | 109, 88 | breqtrrd 4110 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 111 | 83 | lt0neg1d 8650 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 112 | 110, 111 | mpbird 167 |
. . . . . . . . . . . . . 14
bits ..^ |
| 113 | ax-1cn 8080 |
. . . . . . . . . . . . . . 15
| |
| 114 | neg1cn 9203 |
. . . . . . . . . . . . . . 15
| |
| 115 | 1pneg1e0 9209 |
. . . . . . . . . . . . . . 15
| |
| 116 | 113, 114, 115 | addcomli 8279 |
. . . . . . . . . . . . . 14
|
| 117 | 112, 116 | breqtrrdi 4124 |
. . . . . . . . . . . . 13
bits ..^ |
| 118 | znq 9807 |
. . . . . . . . . . . . . . 15
| |
| 119 | 76, 82, 118 | syl2anc 411 |
. . . . . . . . . . . . . 14
bits ..^ |
| 120 | neg1z 9466 |
. . . . . . . . . . . . . 14
| |
| 121 | flqbi 10497 |
. . . . . . . . . . . . . 14
| |
| 122 | 119, 120, 121 | sylancl 413 |
. . . . . . . . . . . . 13
bits ..^
|
| 123 | 106, 117, 122 | mpbir2and 950 |
. . . . . . . . . . . 12
bits ..^
|
| 124 | 123 | breq2d 4094 |
. . . . . . . . . . 11
bits ..^
|
| 125 | 75, 124 | mtbiri 679 |
. . . . . . . . . 10
bits ..^
|
| 126 | bitsval2 12441 |
. . . . . . . . . . 11
bits
| |
| 127 | 76, 81, 126 | syl2anc 411 |
. . . . . . . . . 10
bits ..^
bits
|
| 128 | 125, 127 | mpbird 167 |
. . . . . . . . 9
bits ..^
bits |
| 129 | 74, 128 | sseldd 3225 |
. . . . . . . 8
bits ..^
..^ |
| 130 | elfzolt2 10341 |
. . . . . . . 8
..^ | |
| 131 | 129, 130 | syl 14 |
. . . . . . 7
bits ..^
|
| 132 | 81 | nn0zd 9555 |
. . . . . . . 8
bits ..^
|
| 133 | 70 | nn0zd 9555 |
. . . . . . . 8
bits ..^ |
| 134 | zltnle 9480 |
. . . . . . . 8
| |
| 135 | 132, 133, 134 | syl2anc 411 |
. . . . . . 7
bits ..^
|
| 136 | 131, 135 | mpbid 147 |
. . . . . 6
bits ..^
|
| 137 | 73, 136 | pm2.65da 665 |
. . . . 5
bits ..^
|
| 138 | 137 | intnand 936 |
. . . 4
bits ..^
|
| 139 | simpll 527 |
. . . . 5
bits ..^
| |
| 140 | elznn0nn 9448 |
. . . . 5
 | |
| 141 | 139, 140 | sylib 122 |
. . . 4
bits ..^
|
| 142 | 138, 141 | ecased 1383 |
. . 3
bits ..^
|
| 143 | simplr 528 |
. . 3
bits ..^
| |
| 144 | simpr 110 |
. . 3
bits ..^
bits
..^ | |
| 145 | eqid 2229 |
. . 3
inf 
inf
| |
| 146 | 142, 143, 144, 145 | bitsfzolem 12451 |
. 2
bits ..^
..^ |
| 147 | 67, 146 | impbida 598 |
1
..^
bits
..^ |
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 104
wb 105 wo 713 DECID wdc 839
w3a 1002
wceq 1395
wcel 2200
crab 2512
wss 3197
cpr 3667
class class class wbr 4082 cfv 5314 (class class class)co 5994
csup 7137
infcinf 7138 cr 7986 cc0 7987 c1 7988 caddc 7990 cmul 7992 clt 8169 cle 8170 cneg 8306 cdiv 8807 cn 9098 c2 9149 cn0 9357 cz 9434 cuz 9710 cq 9802 crp 9837 ..^cfzo 10326
cfl 10475
cexp 10747
cdvds 12284 bitscbits 12437 |
| 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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4521 ax-setind 4626 ax-iinf 4677 ax-cnex 8078 ax-resscn 8079 ax-1cn 8080 ax-1re 8081 ax-icn 8082 ax-addcl 8083 ax-addrcl 8084 ax-mulcl 8085 ax-mulrcl 8086 ax-addcom 8087 ax-mulcom 8088 ax-addass 8089 ax-mulass 8090 ax-distr 8091 ax-i2m1 8092 ax-0lt1 8093 ax-1rid 8094 ax-0id 8095 ax-rnegex 8096 ax-precex 8097 ax-cnre 8098 ax-pre-ltirr 8099 ax-pre-ltwlin 8100 ax-pre-lttrn 8101 ax-pre-apti 8102 ax-pre-ltadd 8103 ax-pre-mulgt0 8104 ax-pre-mulext 8105 ax-arch 8106 ax-caucvg 8107 |
| This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-xor 1418 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4381 df-po 4384 df-iso 4385 df-iord 4454 df-on 4456 df-ilim 4457 df-suc 4459 df-iom 4680 df-xp 4722 df-rel 4723 df-cnv 4724 df-co 4725 df-dm 4726 df-rn 4727 df-res 4728 df-ima 4729 df-iota 5274 df-fun 5316 df-fn 5317 df-f 5318 df-f1 5319 df-fo 5320 df-f1o 5321 df-fv 5322 df-isom 5323 df-riota 5947 df-ov 5997 df-oprab 5998 df-mpo 5999 df-1st 6276 df-2nd 6277 df-recs 6441 df-frec 6527 df-sup 7139 df-inf 7140 df-pnf 8171 df-mnf 8172 df-xr 8173 df-ltxr 8174 df-le 8175 df-sub 8307 df-neg 8308 df-reap 8710 df-ap 8717 df-div 8808 df-inn 9099 df-2 9157 df-3 9158 df-4 9159 df-n0 9358 df-z 9435 df-uz 9711 df-q 9803 df-rp 9838 df-fz 10193 df-fzo 10327 df-fl 10477 df-seqfrec 10657 df-exp 10748 df-cj 11339 df-re 11340 df-im 11341 df-rsqrt 11495 df-abs 11496 df-dvds 12285 df-bits 12438 |
| This theorem is referenced by: bitsfi 12454 0bits 12456 bitsinv1 12459 |
| Copyright terms: Public domain | W3C validator |