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 12497 |
. . . 4
bits
    | |
| 2 | simp32 1058 |
. . . . . . 7
..^
| |
| 3 | nn0uz 9784 |
. . . . . . 7
  | |
| 4 | 2, 3 | eleqtrdi 2322 |
. . . . . 6
..^
|
| 5 | simp1r 1046 |
. . . . . . 7
..^
| |
| 6 | 5 | nn0zd 9593 |
. . . . . 6
..^
|
| 7 | 2re 9206 |
. . . . . . . . . 10
 | |
| 8 | 7 | a1i 9 |
. . . . . . . . 9
..^
|
| 9 | 8, 2 | reexpcld 10945 |
. . . . . . . 8
..^
|
| 10 | simp1l 1045 |
. . . . . . . . 9
..^
| |
| 11 | 10 | zred 9595 |
. . . . . . . 8
..^
|
| 12 | 8, 5 | reexpcld 10945 |
. . . . . . . 8
..^
|
| 13 | 9 | recnd 8201 |
. . . . . . . . . 10
..^
 |
| 14 | 13 | mullidd 8190 |
. . . . . . . . 9
..^
  |
| 15 | 1z 9498 |
. . . . . . . . . . . . . 14
| |
| 16 | zq 9853 |
. . . . . . . . . . . . . 14
 | |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . . 13
|
| 18 | 17 | a1i 9 |
. . . . . . . . . . . 12
..^
|
| 19 | 2nn 9298 |
. . . . . . . . . . . . . . 15
 | |
| 20 | 19 | a1i 9 |
. . . . . . . . . . . . . 14
..^
|
| 21 | 20, 2 | nnexpcld 10950 |
. . . . . . . . . . . . 13
..^
|
| 22 | znq 9851 |
. . . . . . . . . . . . 13
| |
| 23 | 10, 21, 22 | syl2anc 411 |
. . . . . . . . . . . 12
..^
|
| 24 | qdcle 10499 |
. . . . . . . . . . . 12
DECID 
| |
| 25 | 18, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
..^
DECID
|
| 26 | simp33 1059 |
. . . . . . . . . . . 12
..^
| |
| 27 | qltnle 10496 |
. . . . . . . . . . . . . 14
| |
| 28 | 23, 18, 27 | syl2anc 411 |
. . . . . . . . . . . . 13
..^
|
| 29 | 0p1e1 9250 |
. . . . . . . . . . . . . . 15
 | |
| 30 | 29 | breq2i 4094 |
. . . . . . . . . . . . . 14
|
| 31 | 2rp 9886 |
. . . . . . . . . . . . . . . . . 18
 | |
| 32 | 31 | a1i 9 |
. . . . . . . . . . . . . . . . 17
..^
|
| 33 | 2 | nn0zd 9593 |
. . . . . . . . . . . . . . . . 17
..^
|
| 34 | 32, 33 | rpexpcld 10952 |
. . . . . . . . . . . . . . . 16
..^
|
| 35 | elfzole1 10384 |
. . . . . . . . . . . . . . . . 17
..^
| |
| 36 | 35 | 3ad2ant2 1043 |
. . . . . . . . . . . . . . . 16
..^
|
| 37 | 11, 34, 36 | divge0d 9965 |
. . . . . . . . . . . . . . 15
..^
|
| 38 | 0z 9483 |
. . . . . . . . . . . . . . . . 17
| |
| 39 | flqbi 10543 |
. . . . . . . . . . . . . . . . 17
| |
| 40 | 23, 38, 39 | sylancl 413 |
. . . . . . . . . . . . . . . 16
..^
|
| 41 | z0even 12465 |
. . . . . . . . . . . . . . . . 17
| |
| 42 | id 19 |
. . . . . . . . . . . . . . . . 17
| |
| 43 | 41, 42 | breqtrrid 4124 |
. . . . . . . . . . . . . . . 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 8187 |
. . . . . . . . . . 11
..^
| |
| 52 | 51, 11, 34 | lemuldivd 9974 |
. . . . . . . . . 10
..^
|
| 53 | 50, 52 | mpbird 167 |
. . . . . . . . 9
..^
|
| 54 | 14, 53 | eqbrtrrd 4110 |
. . . . . . . 8
..^
|
| 55 | elfzolt2 10385 |
. . . . . . . . 9
..^
| |
| 56 | 55 | 3ad2ant2 1043 |
. . . . . . . 8
..^
|
| 57 | 9, 11, 12, 54, 56 | lelttrd 8297 |
. . . . . . 7
..^
|
| 58 | 1lt2 9306 |
. . . . . . . . 9
| |
| 59 | 58 | a1i 9 |
. . . . . . . 8
..^
|
| 60 | nn0ltexp2 10964 |
. . . . . . . 8
| |
| 61 | 8, 2, 5, 59, 60 | syl31anc 1274 |
. . . . . . 7
..^
|
| 62 | 57, 61 | mpbird 167 |
. . . . . 6
..^
|
| 63 | elfzo2 10378 |
. . . . . 6
..^
| |
| 64 | 4, 6, 62, 63 | syl3anbrc 1205 |
. . . . 5
..^
..^ |
| 65 | 64 | 3expia 1229 |
. . . 4
..^
..^ |
| 66 | 1, 65 | biimtrid 152 |
. . 3
..^ bits ..^ |
| 67 | 66 | ssrdv 3231 |
. 2
..^ bits
..^ |
| 68 | simpr 110 |
. . . . . . . 8
bits ..^  | |
| 69 | 68 | nnred 9149 |
. . . . . . 7
bits ..^ |
| 70 | simpllr 534 |
. . . . . . . 8
bits ..^ | |
| 71 | 70 | nn0red 9449 |
. . . . . . 7
bits ..^ |
| 72 | maxle2 11766 |
. . . . . . 7
    | |
| 73 | 69, 71, 72 | syl2anc 411 |
. . . . . 6
bits ..^ |
| 74 | simplr 528 |
. . . . . . . . 9
bits ..^ bits
..^ | |
| 75 | n2dvdsm1 12467 |
. . . . . . . . . . 11
| |
| 76 | simplll 533 |
. . . . . . . . . . . . . . . 16
bits ..^ | |
| 77 | 76 | zred 9595 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 78 | 19 | a1i 9 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 79 | 68 | nnnn0d 9448 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 80 | nn0maxcl 11779 |
. . . . . . . . . . . . . . . . 17
| |
| 81 | 79, 70, 80 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 82 | 78, 81 | nnexpcld 10950 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 83 | 77, 82 | nndivred 9186 |
. . . . . . . . . . . . . 14
bits ..^ |
| 84 | 1red 8187 |
. . . . . . . . . . . . . 14
bits ..^ | |
| 85 | 76 | zcnd 9596 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 86 | 82 | nncnd 9150 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 87 | 82 | nnap0d 9182 |
. . . . . . . . . . . . . . . 16
bits ..^
# |
| 88 | 85, 86, 87 | divnegapd 8976 |
. . . . . . . . . . . . . . 15
bits ..^ |
| 89 | 81 | nn0red 9449 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 90 | 82 | nnred 9149 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 91 | maxle1 11765 |
. . . . . . . . . . . . . . . . . . 19
| |
| 92 | 69, 71, 91 | syl2anc 411 |
. . . . . . . . . . . . . . . . . 18
bits ..^ |
| 93 | 2z 9500 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 94 | uzid 9763 |
. . . . . . . . . . . . . . . . . . . . 21
| |
| 95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
|
| 96 | bernneq3 10917 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 97 | 95, 81, 96 | sylancr 414 |
. . . . . . . . . . . . . . . . . . 19
bits ..^
|
| 98 | 89, 90, 97 | ltled 8291 |
. . . . . . . . . . . . . . . . . 18
bits ..^
|
| 99 | 69, 89, 90, 92, 98 | letrd 8296 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 100 | 86 | mulridd 8189 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 101 | 99, 100 | breqtrrd 4114 |
. . . . . . . . . . . . . . . 16
bits ..^ |
| 102 | 82 | nnrpd 9922 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 103 | 69, 84, 102 | ledivmuld 9978 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 104 | 101, 103 | mpbird 167 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 105 | 88, 104 | eqbrtrd 4108 |
. . . . . . . . . . . . . 14
bits ..^ |
| 106 | 83, 84, 105 | lenegcon1d 8700 |
. . . . . . . . . . . . 13
bits ..^
|
| 107 | 68 | nngt0d 9180 |
. . . . . . . . . . . . . . . . 17
bits ..^ |
| 108 | 82 | nngt0d 9180 |
. . . . . . . . . . . . . . . . 17
bits ..^
|
| 109 | 69, 90, 107, 108 | divgt0d 9108 |
. . . . . . . . . . . . . . . 16
bits ..^
|
| 110 | 109, 88 | breqtrrd 4114 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 111 | 83 | lt0neg1d 8688 |
. . . . . . . . . . . . . . 15
bits ..^
|
| 112 | 110, 111 | mpbird 167 |
. . . . . . . . . . . . . 14
bits ..^ |
| 113 | ax-1cn 8118 |
. . . . . . . . . . . . . . 15
| |
| 114 | neg1cn 9241 |
. . . . . . . . . . . . . . 15
| |
| 115 | 1pneg1e0 9247 |
. . . . . . . . . . . . . . 15
| |
| 116 | 113, 114, 115 | addcomli 8317 |
. . . . . . . . . . . . . 14
|
| 117 | 112, 116 | breqtrrdi 4128 |
. . . . . . . . . . . . 13
bits ..^ |
| 118 | znq 9851 |
. . . . . . . . . . . . . . 15
| |
| 119 | 76, 82, 118 | syl2anc 411 |
. . . . . . . . . . . . . 14
bits ..^ |
| 120 | neg1z 9504 |
. . . . . . . . . . . . . 14
| |
| 121 | flqbi 10543 |
. . . . . . . . . . . . . 14
| |
| 122 | 119, 120, 121 | sylancl 413 |
. . . . . . . . . . . . 13
bits ..^
|
| 123 | 106, 117, 122 | mpbir2and 950 |
. . . . . . . . . . . 12
bits ..^
|
| 124 | 123 | breq2d 4098 |
. . . . . . . . . . 11
bits ..^
|
| 125 | 75, 124 | mtbiri 679 |
. . . . . . . . . 10
bits ..^
|
| 126 | bitsval2 12498 |
. . . . . . . . . . 11
bits
| |
| 127 | 76, 81, 126 | syl2anc 411 |
. . . . . . . . . 10
bits ..^
bits
|
| 128 | 125, 127 | mpbird 167 |
. . . . . . . . 9
bits ..^
bits |
| 129 | 74, 128 | sseldd 3226 |
. . . . . . . 8
bits ..^
..^ |
| 130 | elfzolt2 10385 |
. . . . . . . 8
..^ | |
| 131 | 129, 130 | syl 14 |
. . . . . . 7
bits ..^
|
| 132 | 81 | nn0zd 9593 |
. . . . . . . 8
bits ..^
|
| 133 | 70 | nn0zd 9593 |
. . . . . . . 8
bits ..^ |
| 134 | zltnle 9518 |
. . . . . . . 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 9486 |
. . . . 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 12508 |
. 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 3198
cpr 3668
class class class wbr 4086 cfv 5324 (class class class)co 6013
csup 7175
infcinf 7176 cr 8024 cc0 8025 c1 8026 caddc 8028 cmul 8030 clt 8207 cle 8208 cneg 8344 cdiv 8845 cn 9136 c2 9187 cn0 9395 cz 9472 cuz 9748 cq 9846 crp 9881 ..^cfzo 10370
cfl 10521
cexp 10793
cdvds 12341 bitscbits 12494 |
| 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 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684 ax-cnex 8116 ax-resscn 8117 ax-1cn 8118 ax-1re 8119 ax-icn 8120 ax-addcl 8121 ax-addrcl 8122 ax-mulcl 8123 ax-mulrcl 8124 ax-addcom 8125 ax-mulcom 8126 ax-addass 8127 ax-mulass 8128 ax-distr 8129 ax-i2m1 8130 ax-0lt1 8131 ax-1rid 8132 ax-0id 8133 ax-rnegex 8134 ax-precex 8135 ax-cnre 8136 ax-pre-ltirr 8137 ax-pre-ltwlin 8138 ax-pre-lttrn 8139 ax-pre-apti 8140 ax-pre-ltadd 8141 ax-pre-mulgt0 8142 ax-pre-mulext 8143 ax-arch 8144 ax-caucvg 8145 |
| 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 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-ilim 4464 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-isom 5333 df-riota 5966 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-frec 6552 df-sup 7177 df-inf 7178 df-pnf 8209 df-mnf 8210 df-xr 8211 df-ltxr 8212 df-le 8213 df-sub 8345 df-neg 8346 df-reap 8748 df-ap 8755 df-div 8846 df-inn 9137 df-2 9195 df-3 9196 df-4 9197 df-n0 9396 df-z 9473 df-uz 9749 df-q 9847 df-rp 9882 df-fz 10237 df-fzo 10371 df-fl 10523 df-seqfrec 10703 df-exp 10794 df-cj 11396 df-re 11397 df-im 11398 df-rsqrt 11552 df-abs 11553 df-dvds 12342 df-bits 12495 |
| This theorem is referenced by: bitsfi 12511 0bits 12513 bitsinv1 12516 |
| Copyright terms: Public domain | W3C validator |