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 12625 |
. . . 4
bits
    | |
| 2 | simp32 1061 |
. . . . . . 7
..^
| |
| 3 | nn0uz 9888 |
. . . . . . 7
  | |
| 4 | 2, 3 | eleqtrdi 2325 |
. . . . . 6
..^
|
| 5 | simp1r 1049 |
. . . . . . 7
..^
| |
| 6 | 5 | nn0zd 9697 |
. . . . . 6
..^
|
| 7 | 2re 9306 |
. . . . . . . . . 10
 | |
| 8 | 7 | a1i 9 |
. . . . . . . . 9
..^
|
| 9 | 8, 2 | reexpcld 11051 |
. . . . . . . 8
..^
|
| 10 | simp1l 1048 |
. . . . . . . . 9
..^
| |
| 11 | 10 | zred 9699 |
. . . . . . . 8
..^
|
| 12 | 8, 5 | reexpcld 11051 |
. . . . . . . 8
..^
|
| 13 | 9 | recnd 8301 |
. . . . . . . . . 10
..^
 |
| 14 | 13 | mullidd 8291 |
. . . . . . . . 9
..^
  |
| 15 | 1z 9602 |
. . . . . . . . . . . . . 14
| |
| 16 | zq 9957 |
. . . . . . . . . . . . . 14
 | |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
|
| 18 | 17 | a1i 9 |
. . . . . . . . . . . 12
..^
|
| 19 | 2nn 9398 |
. . . . . . . . . . . . . . 15
 | |
| 20 | 19 | a1i 9 |
. . . . . . . . . . . . . 14
..^
|
| 21 | 20, 2 | nnexpcld 11056 |
. . . . . . . . . . . . 13
..^
|
| 22 | znq 9955 |
. . . . . . . . . . . . 13
| |
| 23 | 10, 21, 22 | syl2anc 411 |
. . . . . . . . . . . 12
..^
|
| 24 | qdcle 10605 |
. . . . . . . . . . . 12
DECID 
| |
| 25 | 18, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
..^
DECID
|
| 26 | simp33 1062 |
. . . . . . . . . . . 12
..^
| |
| 27 | qltnle 10602 |
. . . . . . . . . . . . . 14
| |
| 28 | 23, 18, 27 | syl2anc 411 |
. . . . . . . . . . . . 13
..^
|
| 29 | 0p1e1 9350 |
. . . . . . . . . . . . . . 15
 | |
| 30 | 29 | breq2i 4116 |
. . . . . . . . . . . . . 14
|
| 31 | 2rp 9990 |
. . . . . . . . . . . . . . . . . 18
 | |
| 32 | 31 | a1i 9 |
. . . . . . . . . . . . . . . . 17
..^
|
| 33 | 2 | nn0zd 9697 |
. . . . . . . . . . . . . . . . 17
..^
|
| 34 | 32, 33 | rpexpcld 11058 |
. . . . . . . . . . . . . . . 16
..^
|
| 35 | elfzole1 10489 |
. . . . . . . . . . . . . . . . 17
..^
| |
| 36 | 35 | 3ad2ant2 1046 |
. . . . . . . . . . . . . . . 16
..^
|
| 37 | 11, 34, 36 | divge0d 10069 |
. . . . . . . . . . . . . . 15
..^
|
| 38 | 0z 9587 |
. . . . . . . . . . . . . . . . 17
| |
| 39 | flqbi 10649 |
. . . . . . . . . . . . . . . . 17
| |
| 40 | 23, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
..^
|
| 41 | z0even 12593 |
. . . . . . . . . . . . . . . . 17
| |
| 42 | id 19 |
. . . . . . . . . . . . . . . . 17
| |
| 43 | 41, 42 | breqtrrid 4146 |
. . . . . . . . . . . . . . . 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 669 |
. . . . . . . . . . 11
..^
|
| 49 | notnotrdc 851 |
. . . . . . . . . . 11
DECID
| |
| 50 | 25, 48, 49 | sylc 62 |
. . . . . . . . . 10
..^
|
| 51 | 1red 8288 |
. . . . . . . . . . 11
..^
| |
| 52 | 51, 11, 34 | lemuldivd 10078 |
. . . . . . . . . 10
..^
|
| 53 | 50, 52 | mpbird 167 |
. . . . . . . . 9
..^
|
| 54 | 14, 53 | eqbrtrrd 4132 |
. . . . . . . 8
..^
|
| 55 | elfzolt2 10490 |
. . . . . . . . 9
..^
| |
| 56 | 55 | 3ad2ant2 1046 |
. . . . . . . 8
..^
|
| 57 | 9, 11, 12, 54, 56 | lelttrd 8397 |
. . . . . . 7
..^
|
| 58 | 1lt2 9406 |
. . . . . . . . 9
| |
| 59 | 58 | a1i 9 |
. . . . . . . 8
..^
|
| 60 | nn0ltexp2 11070 |
. . . . . . . 8
| |
| 61 | 8, 2, 5, 59, 60 | syl31anc 1277 |
. . . . . . 7
..^
|
| 62 | 57, 61 | mpbird 167 |
. . . . . 6
..^
|
| 63 | elfzo2 10483 |
. . . . . 6
..^
| |
| 64 | 4, 6, 62, 63 | syl3anbrc 1208 |
. . . . 5
..^
..^ |
| 65 | 64 | 3expia 1232 |
. . . 4
..^
..^ |
| 66 | 1, 65 | biimtrid 152 |
. . 3
..^ bits ..^ |
| 67 | 66 | ssrdv 3243 |
. 2
..^ bits
..^ |
| 68 | simpr 110 |
. . . . . . . 8
bits ..^  | |
| 69 | 68 | nnred 9249 |
. . . . . . 7
bits ..^ |
| 70 | simpllr 536 |
. . . . . . . 8
bits ..^ | |
| 71 | 70 | nn0red 9553 |
. . . . . . 7
bits ..^ |
| 72 | maxle2 11893 |
. . . . . . 7
    | |
| 73 | 69, 71, 72 | syl2anc 411 |
. . . . . 6
bits ..^ |
| 74 | simplr 529 |
. . . . . . . . 9
bits ..^ bits
..^ | |
| 75 | n2dvdsm1 12595 |
. . . . . . . . . . 11
| |
| 76 | simplll 535 |
. . . . . . . . . . . . . . . 16
bits ..^ | |
| 77 | 76 | zred 9699 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 78 | 19 | a1i 9 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 79 | 68 | nnnn0d 9552 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 80 | nn0maxcl 11906 |
. . . . . . . . . . . . . . . . 17
| |
| 81 | 79, 70, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 82 | 78, 81 | nnexpcld 11056 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 83 | 77, 82 | nndivred 9286 |
. . . . . . . . . . . . . 14
bits ..^ |
| 84 | 1red 8288 |
. . . . . . . . . . . . . 14
bits ..^ | |
| 85 | 76 | zcnd 9700 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 86 | 82 | nncnd 9250 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 87 | 82 | nnap0d 9282 |
. . . . . . . . . . . . . . . 16
bits ..^
# |
| 88 | 85, 86, 87 | divnegapd 9076 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 89 | 81 | nn0red 9553 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 90 | 82 | nnred 9249 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 91 | maxle1 11892 |
. . . . . . . . . . . . . . . . . . 19
| |
| 92 | 69, 71, 91 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
| 93 | 2z 9604 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 94 | uzid 9867 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 96 | bernneq3 11023 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 97 | 95, 81, 96 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
bits ..^
|
| 98 | 89, 90, 97 | ltled 8391 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 99 | 69, 89, 90, 92, 98 | letrd 8396 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 100 | 86 | mulridd 8290 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 101 | 99, 100 | breqtrrd 4136 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 102 | 82 | nnrpd 10026 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 103 | 69, 84, 102 | ledivmuld 10082 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 104 | 101, 103 | mpbird 167 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 105 | 88, 104 | eqbrtrd 4130 |
. . . . . . . . . . . . . 14
bits ..^ |
| 106 | 83, 84, 105 | lenegcon1d 8800 |
. . . . . . . . . . . . 13
bits ..^
|
| 107 | 68 | nngt0d 9280 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 108 | 82 | nngt0d 9280 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 109 | 69, 90, 107, 108 | divgt0d 9208 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 110 | 109, 88 | breqtrrd 4136 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 111 | 83 | lt0neg1d 8788 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 112 | 110, 111 | mpbird 167 |
. . . . . . . . . . . . . 14
bits ..^ |
| 113 | ax-1cn 8219 |
. . . . . . . . . . . . . . 15
| |
| 114 | neg1cn 9341 |
. . . . . . . . . . . . . . 15
| |
| 115 | 1pneg1e0 9347 |
. . . . . . . . . . . . . . 15
| |
| 116 | 113, 114, 115 | addcomli 8417 |
. . . . . . . . . . . . . 14
|
| 117 | 112, 116 | breqtrrdi 4150 |
. . . . . . . . . . . . 13
bits ..^ |
| 118 | znq 9955 |
. . . . . . . . . . . . . . 15
| |
| 119 | 76, 82, 118 | syl2anc 411 |
. . . . . . . . . . . . . 14
bits ..^ |
| 120 | neg1z 9608 |
. . . . . . . . . . . . . 14
| |
| 121 | flqbi 10649 |
. . . . . . . . . . . . . 14
| |
| 122 | 119, 120, 121 | sylancl 413 |
. . . . . . . . . . . . 13
bits ..^
|
| 123 | 106, 117, 122 | mpbir2and 953 |
. . . . . . . . . . . 12
bits ..^
|
| 124 | 123 | breq2d 4120 |
. . . . . . . . . . 11
bits ..^
|
| 125 | 75, 124 | mtbiri 682 |
. . . . . . . . . 10
bits ..^
|
| 126 | bitsval2 12626 |
. . . . . . . . . . 11
bits
| |
| 127 | 76, 81, 126 | syl2anc 411 |
. . . . . . . . . 10
bits ..^
bits
|
| 128 | 125, 127 | mpbird 167 |
. . . . . . . . 9
bits ..^
bits |
| 129 | 74, 128 | sseldd 3238 |
. . . . . . . 8
bits ..^
..^ |
| 130 | elfzolt2 10490 |
. . . . . . . 8
..^ | |
| 131 | 129, 130 | syl 14 |
. . . . . . 7
bits ..^
|
| 132 | 81 | nn0zd 9697 |
. . . . . . . 8
bits ..^
|
| 133 | 70 | nn0zd 9697 |
. . . . . . . 8
bits ..^ |
| 134 | zltnle 9622 |
. . . . . . . 8
| |
| 135 | 132, 133, 134 | syl2anc 411 |
. . . . . . 7
bits ..^
|
| 136 | 131, 135 | mpbid 147 |
. . . . . 6
bits ..^
|
| 137 | 73, 136 | pm2.65da 667 |
. . . . 5
bits ..^
|
| 138 | 137 | intnand 939 |
. . . 4
bits ..^
|
| 139 | simpll 527 |
. . . . 5
bits ..^
| |
| 140 | elznn0nn 9590 |
. . . . 5
 | |
| 141 | 139, 140 | sylib 122 |
. . . 4
bits ..^
|
| 142 | 138, 141 | ecased 1386 |
. . 3
bits ..^
|
| 143 | simplr 529 |
. . 3
bits ..^
| |
| 144 | simpr 110 |
. . 3
bits ..^
bits
..^ | |
| 145 | eqid 2232 |
. . 3
inf 
inf
| |
| 146 | 142, 143, 144, 145 | bitsfzolem 12636 |
. 2
bits ..^
..^ |
| 147 | 67, 146 | impbida 600 |
1
..^
bits
..^ |
| Colors of variables: wff set class |
| Syntax hints: wn 3
wi 4
wa 104
wb 105 wo 716 DECID wdc 842
w3a 1005
wceq 1398
wcel 2203
crab 2524
wss 3210
cpr 3689
class class class wbr 4108 cfv 5351 (class class class)co 6049
csup 7272
infcinf 7273 cr 8125 cc0 8126 c1 8127 caddc 8129 cmul 8131 clt 8307 cle 8308 cneg 8444 cdiv 8945 cn 9236 c2 9287 cn0 9495 cz 9576 cuz 9852 cq 9950 crp 9985 ..^cfzo 10475
cfl 10627
cexp 10899
cdvds 12469 bitscbits 12622 |
| 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 619 ax-in2 620 ax-io 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-coll 4224 ax-sep 4227 ax-nul 4235 ax-pow 4286 ax-pr 4321 ax-un 4553 ax-setind 4658 ax-iinf 4709 ax-cnex 8217 ax-resscn 8218 ax-1cn 8219 ax-1re 8220 ax-icn 8221 ax-addcl 8222 ax-addrcl 8223 ax-mulcl 8224 ax-mulrcl 8225 ax-addcom 8226 ax-mulcom 8227 ax-addass 8228 ax-mulass 8229 ax-distr 8230 ax-i2m1 8231 ax-0lt1 8232 ax-1rid 8233 ax-0id 8234 ax-rnegex 8235 ax-precex 8236 ax-cnre 8237 ax-pre-ltirr 8238 ax-pre-ltwlin 8239 ax-pre-lttrn 8240 ax-pre-apti 8241 ax-pre-ltadd 8242 ax-pre-mulgt0 8243 ax-pre-mulext 8244 ax-arch 8245 ax-caucvg 8246 |
| This theorem depends on definitions: df-bi 117 df-dc 843 df-3or 1006 df-3an 1007 df-tru 1401 df-fal 1404 df-xor 1421 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-nel 2508 df-ral 2525 df-rex 2526 df-reu 2527 df-rmo 2528 df-rab 2529 df-v 2814 df-sbc 3042 df-csb 3138 df-dif 3212 df-un 3214 df-in 3216 df-ss 3223 df-nul 3508 df-if 3620 df-pw 3670 df-sn 3694 df-pr 3695 df-op 3697 df-uni 3914 df-int 3949 df-iun 3992 df-br 4109 df-opab 4171 df-mpt 4172 df-tr 4208 df-id 4413 df-po 4416 df-iso 4417 df-iord 4486 df-on 4488 df-ilim 4489 df-suc 4491 df-iom 4712 df-xp 4754 df-rel 4755 df-cnv 4756 df-co 4757 df-dm 4758 df-rn 4759 df-res 4760 df-ima 4761 df-iota 5311 df-fun 5353 df-fn 5354 df-f 5355 df-f1 5356 df-fo 5357 df-f1o 5358 df-fv 5359 df-isom 5360 df-riota 6002 df-ov 6052 df-oprab 6053 df-mpo 6054 df-1st 6333 df-2nd 6334 df-recs 6535 df-frec 6621 df-sup 7274 df-inf 7275 df-pnf 8309 df-mnf 8310 df-xr 8311 df-ltxr 8312 df-le 8313 df-sub 8445 df-neg 8446 df-reap 8848 df-ap 8855 df-div 8946 df-inn 9237 df-2 9295 df-3 9296 df-4 9297 df-n0 9496 df-z 9577 df-uz 9853 df-q 9951 df-rp 9986 df-fz 10342 df-fzo 10476 df-fl 10629 df-seqfrec 10809 df-exp 10900 df-cj 11523 df-re 11524 df-im 11525 df-rsqrt 11679 df-abs 11680 df-dvds 12470 df-bits 12623 |
| This theorem is referenced by: bitsfi 12639 0bits 12641 bitsinv1 12644 |
| Copyright terms: Public domain | W3C validator |