Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dig2nn1st Structured version   Visualization version   GIF version

Theorem dig2nn1st 47869
Description: The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020.)
Assertion
Ref Expression
dig2nn1st (𝑁 ∈ ℕ → (((#b𝑁) − 1)(digit‘2)𝑁) = 1)

Proof of Theorem dig2nn1st
StepHypRef Expression
1 2nn 12323 . . . 4 2 ∈ ℕ
21a1i 11 . . 3 (𝑁 ∈ ℕ → 2 ∈ ℕ)
3 blennnelnn 47840 . . . 4 (𝑁 ∈ ℕ → (#b𝑁) ∈ ℕ)
4 nnm1nn0 12551 . . . 4 ((#b𝑁) ∈ ℕ → ((#b𝑁) − 1) ∈ ℕ0)
53, 4syl 17 . . 3 (𝑁 ∈ ℕ → ((#b𝑁) − 1) ∈ ℕ0)
6 nnre 12257 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
7 nnnn0 12517 . . . . 5 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
87nn0ge0d 12573 . . . 4 (𝑁 ∈ ℕ → 0 ≤ 𝑁)
9 elrege0 13471 . . . 4 (𝑁 ∈ (0[,)+∞) ↔ (𝑁 ∈ ℝ ∧ 0 ≤ 𝑁))
106, 8, 9sylanbrc 581 . . 3 (𝑁 ∈ ℕ → 𝑁 ∈ (0[,)+∞))
11 nn0digval 47864 . . 3 ((2 ∈ ℕ ∧ ((#b𝑁) − 1) ∈ ℕ0𝑁 ∈ (0[,)+∞)) → (((#b𝑁) − 1)(digit‘2)𝑁) = ((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) mod 2))
122, 5, 10, 11syl3anc 1368 . 2 (𝑁 ∈ ℕ → (((#b𝑁) − 1)(digit‘2)𝑁) = ((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) mod 2))
13 n2dvds1 16356 . . . 4 ¬ 2 ∥ 1
14 blennn 47839 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (#b𝑁) = ((⌊‘(2 logb 𝑁)) + 1))
1514oveq1d 7434 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((#b𝑁) − 1) = (((⌊‘(2 logb 𝑁)) + 1) − 1))
16 2z 12632 . . . . . . . . . . . . . . 15 2 ∈ ℤ
17 uzid 12875 . . . . . . . . . . . . . . 15 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
1816, 17ax-mp 5 . . . . . . . . . . . . . 14 2 ∈ (ℤ‘2)
19 nnrp 13025 . . . . . . . . . . . . . 14 (𝑁 ∈ ℕ → 𝑁 ∈ ℝ+)
20 relogbzcl 26771 . . . . . . . . . . . . . 14 ((2 ∈ (ℤ‘2) ∧ 𝑁 ∈ ℝ+) → (2 logb 𝑁) ∈ ℝ)
2118, 19, 20sylancr 585 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (2 logb 𝑁) ∈ ℝ)
2221flcld 13804 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → (⌊‘(2 logb 𝑁)) ∈ ℤ)
2322zcnd 12705 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (⌊‘(2 logb 𝑁)) ∈ ℂ)
24 pncan1 11675 . . . . . . . . . . 11 ((⌊‘(2 logb 𝑁)) ∈ ℂ → (((⌊‘(2 logb 𝑁)) + 1) − 1) = (⌊‘(2 logb 𝑁)))
2523, 24syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (((⌊‘(2 logb 𝑁)) + 1) − 1) = (⌊‘(2 logb 𝑁)))
2615, 25eqtrd 2765 . . . . . . . . 9 (𝑁 ∈ ℕ → ((#b𝑁) − 1) = (⌊‘(2 logb 𝑁)))
2726oveq2d 7435 . . . . . . . 8 (𝑁 ∈ ℕ → (2↑((#b𝑁) − 1)) = (2↑(⌊‘(2 logb 𝑁))))
2827oveq2d 7435 . . . . . . 7 (𝑁 ∈ ℕ → (𝑁 / (2↑((#b𝑁) − 1))) = (𝑁 / (2↑(⌊‘(2 logb 𝑁)))))
2928fveq2d 6900 . . . . . 6 (𝑁 ∈ ℕ → (⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) = (⌊‘(𝑁 / (2↑(⌊‘(2 logb 𝑁))))))
30 fldivexpfllog2 47829 . . . . . . 7 (𝑁 ∈ ℝ+ → (⌊‘(𝑁 / (2↑(⌊‘(2 logb 𝑁))))) = 1)
3119, 30syl 17 . . . . . 6 (𝑁 ∈ ℕ → (⌊‘(𝑁 / (2↑(⌊‘(2 logb 𝑁))))) = 1)
3229, 31eqtrd 2765 . . . . 5 (𝑁 ∈ ℕ → (⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) = 1)
3332breq2d 5161 . . . 4 (𝑁 ∈ ℕ → (2 ∥ (⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) ↔ 2 ∥ 1))
3413, 33mtbiri 326 . . 3 (𝑁 ∈ ℕ → ¬ 2 ∥ (⌊‘(𝑁 / (2↑((#b𝑁) − 1)))))
35 2re 12324 . . . . . . . 8 2 ∈ ℝ
3635a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 2 ∈ ℝ)
3736, 5reexpcld 14168 . . . . . 6 (𝑁 ∈ ℕ → (2↑((#b𝑁) − 1)) ∈ ℝ)
38 2cnd 12328 . . . . . . 7 (𝑁 ∈ ℕ → 2 ∈ ℂ)
39 2ne0 12354 . . . . . . . 8 2 ≠ 0
4039a1i 11 . . . . . . 7 (𝑁 ∈ ℕ → 2 ≠ 0)
415nn0zd 12622 . . . . . . 7 (𝑁 ∈ ℕ → ((#b𝑁) − 1) ∈ ℤ)
4238, 40, 41expne0d 14157 . . . . . 6 (𝑁 ∈ ℕ → (2↑((#b𝑁) − 1)) ≠ 0)
436, 37, 42redivcld 12080 . . . . 5 (𝑁 ∈ ℕ → (𝑁 / (2↑((#b𝑁) − 1))) ∈ ℝ)
4443flcld 13804 . . . 4 (𝑁 ∈ ℕ → (⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) ∈ ℤ)
45 mod2eq1n2dvds 16335 . . . 4 ((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) ∈ ℤ → (((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) mod 2) = 1 ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑((#b𝑁) − 1))))))
4644, 45syl 17 . . 3 (𝑁 ∈ ℕ → (((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) mod 2) = 1 ↔ ¬ 2 ∥ (⌊‘(𝑁 / (2↑((#b𝑁) − 1))))))
4734, 46mpbird 256 . 2 (𝑁 ∈ ℕ → ((⌊‘(𝑁 / (2↑((#b𝑁) − 1)))) mod 2) = 1)
4812, 47eqtrd 2765 1 (𝑁 ∈ ℕ → (((#b𝑁) − 1)(digit‘2)𝑁) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205   = wceq 1533  wcel 2098  wne 2929   class class class wbr 5149  cfv 6549  (class class class)co 7419  cc 11143  cr 11144  0cc0 11145  1c1 11146   + caddc 11148  +∞cpnf 11282  cle 11286  cmin 11481   / cdiv 11908  cn 12250  2c2 12305  0cn0 12510  cz 12596  cuz 12860  +crp 13014  [,)cico 13366  cfl 13796   mod cmo 13875  cexp 14067  cdvds 16242   logb clogb 26761  #bcblen 47833  digitcdig 47859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-inf2 9671  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223  ax-addf 11224
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-of 7685  df-om 7872  df-1st 7994  df-2nd 7995  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9393  df-fi 9441  df-sup 9472  df-inf 9473  df-oi 9540  df-card 9969  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-4 12315  df-5 12316  df-6 12317  df-7 12318  df-8 12319  df-9 12320  df-n0 12511  df-z 12597  df-dec 12716  df-uz 12861  df-q 12971  df-rp 13015  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13368  df-ioc 13369  df-ico 13370  df-icc 13371  df-fz 13525  df-fzo 13668  df-fl 13798  df-mod 13876  df-seq 14008  df-exp 14068  df-fac 14277  df-bc 14306  df-hash 14334  df-shft 15058  df-cj 15090  df-re 15091  df-im 15092  df-sqrt 15226  df-abs 15227  df-limsup 15459  df-clim 15476  df-rlim 15477  df-sum 15677  df-ef 16055  df-sin 16057  df-cos 16058  df-pi 16060  df-dvds 16243  df-struct 17135  df-sets 17152  df-slot 17170  df-ndx 17182  df-base 17200  df-ress 17229  df-plusg 17265  df-mulr 17266  df-starv 17267  df-sca 17268  df-vsca 17269  df-ip 17270  df-tset 17271  df-ple 17272  df-ds 17274  df-unif 17275  df-hom 17276  df-cco 17277  df-rest 17423  df-topn 17424  df-0g 17442  df-gsum 17443  df-topgen 17444  df-pt 17445  df-prds 17448  df-xrs 17503  df-qtop 17508  df-imas 17509  df-xps 17511  df-mre 17585  df-mrc 17586  df-acs 17588  df-mgm 18619  df-sgrp 18698  df-mnd 18714  df-submnd 18760  df-mulg 19048  df-cntz 19297  df-cmn 19766  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-fbas 21310  df-fg 21311  df-cnfld 21314  df-top 22857  df-topon 22874  df-topsp 22896  df-bases 22910  df-cld 22984  df-ntr 22985  df-cls 22986  df-nei 23063  df-lp 23101  df-perf 23102  df-cn 23192  df-cnp 23193  df-haus 23280  df-tx 23527  df-hmeo 23720  df-fil 23811  df-fm 23903  df-flim 23904  df-flf 23905  df-xms 24287  df-ms 24288  df-tms 24289  df-cncf 24859  df-limc 25856  df-dv 25857  df-log 26552  df-cxp 26553  df-logb 26762  df-blen 47834  df-dig 47860
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator