Metamath Proof Explorer

Theorem bitsfzolem

Description: Lemma for bitsfzo . (Contributed by Mario Carneiro, 5-Sep-2016) (Revised by AV, 1-Oct-2020)

Ref Expression
Hypotheses bitsfzo.1 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
bitsfzo.2 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
bitsfzo.3 โŠข ( ๐œ‘ โ†’ ( bits โ€˜ ๐‘ ) โŠ† ( 0 ..^ ๐‘€ ) )
bitsfzo.4 โŠข ๐‘† = inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < )
Assertion bitsfzolem ( ๐œ‘ โ†’ ๐‘ โˆˆ ( 0 ..^ ( 2 โ†‘ ๐‘€ ) ) )

Proof

Step Hyp Ref Expression
1 bitsfzo.1 โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
2 bitsfzo.2 โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
3 bitsfzo.3 โŠข ( ๐œ‘ โ†’ ( bits โ€˜ ๐‘ ) โŠ† ( 0 ..^ ๐‘€ ) )
4 bitsfzo.4 โŠข ๐‘† = inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < )
5 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
6 1 5 eleqtrdi โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) )
7 2nn โŠข 2 โˆˆ โ„•
8 7 a1i โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„• )
9 8 2 nnexpcld โŠข ( ๐œ‘ โ†’ ( 2 โ†‘ ๐‘€ ) โˆˆ โ„• )
10 9 nnzd โŠข ( ๐œ‘ โ†’ ( 2 โ†‘ ๐‘€ ) โˆˆ โ„ค )
11 3 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( bits โ€˜ ๐‘ ) โŠ† ( 0 ..^ ๐‘€ ) )
12 n2dvds1 โŠข ยฌ 2 โˆฅ 1
13 7 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 2 โˆˆ โ„• )
14 ssrab2 โŠข { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โŠ† โ„•0
15 14 5 sseqtri โŠข { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โŠ† ( โ„คโ‰ฅ โ€˜ 0 )
16 nnssnn0 โŠข โ„• โŠ† โ„•0
17 1 nn0red โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ )
18 2re โŠข 2 โˆˆ โ„
19 18 a1i โŠข ( ๐œ‘ โ†’ 2 โˆˆ โ„ )
20 1lt2 โŠข 1 < 2
21 20 a1i โŠข ( ๐œ‘ โ†’ 1 < 2 )
22 expnbnd โŠข ( ( ๐‘ โˆˆ โ„ โˆง 2 โˆˆ โ„ โˆง 1 < 2 ) โ†’ โˆƒ ๐‘› โˆˆ โ„• ๐‘ < ( 2 โ†‘ ๐‘› ) )
23 17 19 21 22 syl3anc โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘› โˆˆ โ„• ๐‘ < ( 2 โ†‘ ๐‘› ) )
24 ssrexv โŠข ( โ„• โŠ† โ„•0 โ†’ ( โˆƒ ๐‘› โˆˆ โ„• ๐‘ < ( 2 โ†‘ ๐‘› ) โ†’ โˆƒ ๐‘› โˆˆ โ„•0 ๐‘ < ( 2 โ†‘ ๐‘› ) ) )
25 16 23 24 mpsyl โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘› โˆˆ โ„•0 ๐‘ < ( 2 โ†‘ ๐‘› ) )
26 rabn0 โŠข ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ‰  โˆ… โ†” โˆƒ ๐‘› โˆˆ โ„•0 ๐‘ < ( 2 โ†‘ ๐‘› ) )
27 25 26 sylibr โŠข ( ๐œ‘ โ†’ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ‰  โˆ… )
28 infssuzcl โŠข ( ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โŠ† ( โ„คโ‰ฅ โ€˜ 0 ) โˆง { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ‰  โˆ… ) โ†’ inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } )
29 15 27 28 sylancr โŠข ( ๐œ‘ โ†’ inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } )
30 4 29 eqeltrid โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } )
31 14 30 sselid โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ โ„•0 )
32 31 nn0zd โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ โ„ค )
33 32 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘† โˆˆ โ„ค )
34 0red โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 0 โˆˆ โ„ )
35 2 nn0zd โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค )
36 35 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘€ โˆˆ โ„ค )
37 36 zred โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘€ โˆˆ โ„ )
38 33 zred โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘† โˆˆ โ„ )
39 2 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘€ โˆˆ โ„•0 )
40 39 nn0ge0d โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 0 โ‰ค ๐‘€ )
41 18 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 2 โˆˆ โ„ )
42 41 39 reexpcld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘€ ) โˆˆ โ„ )
43 17 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘ โˆˆ โ„ )
44 8 31 nnexpcld โŠข ( ๐œ‘ โ†’ ( 2 โ†‘ ๐‘† ) โˆˆ โ„• )
45 44 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘† ) โˆˆ โ„• )
46 45 nnred โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘† ) โˆˆ โ„ )
47 simpr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ )
48 30 adantr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘† โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } )
49 oveq2 โŠข ( ๐‘š = ๐‘† โ†’ ( 2 โ†‘ ๐‘š ) = ( 2 โ†‘ ๐‘† ) )
50 49 breq2d โŠข ( ๐‘š = ๐‘† โ†’ ( ๐‘ < ( 2 โ†‘ ๐‘š ) โ†” ๐‘ < ( 2 โ†‘ ๐‘† ) ) )
51 oveq2 โŠข ( ๐‘› = ๐‘š โ†’ ( 2 โ†‘ ๐‘› ) = ( 2 โ†‘ ๐‘š ) )
52 51 breq2d โŠข ( ๐‘› = ๐‘š โ†’ ( ๐‘ < ( 2 โ†‘ ๐‘› ) โ†” ๐‘ < ( 2 โ†‘ ๐‘š ) ) )
53 52 cbvrabv โŠข { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } = { ๐‘š โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘š ) }
54 50 53 elrab2 โŠข ( ๐‘† โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†” ( ๐‘† โˆˆ โ„•0 โˆง ๐‘ < ( 2 โ†‘ ๐‘† ) ) )
55 54 simprbi โŠข ( ๐‘† โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†’ ๐‘ < ( 2 โ†‘ ๐‘† ) )
56 48 55 syl โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘ < ( 2 โ†‘ ๐‘† ) )
57 42 43 46 47 56 lelttrd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘€ ) < ( 2 โ†‘ ๐‘† ) )
58 20 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 1 < 2 )
59 41 36 33 58 ltexp2d โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘€ < ๐‘† โ†” ( 2 โ†‘ ๐‘€ ) < ( 2 โ†‘ ๐‘† ) ) )
60 57 59 mpbird โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘€ < ๐‘† )
61 34 37 38 40 60 lelttrd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 0 < ๐‘† )
62 elnnz โŠข ( ๐‘† โˆˆ โ„• โ†” ( ๐‘† โˆˆ โ„ค โˆง 0 < ๐‘† ) )
63 33 61 62 sylanbrc โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘† โˆˆ โ„• )
64 nnm1nn0 โŠข ( ๐‘† โˆˆ โ„• โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ โ„•0 )
65 63 64 syl โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ โ„•0 )
66 13 65 nnexpcld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โˆˆ โ„• )
67 66 nncnd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โˆˆ โ„‚ )
68 67 mullidd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 1 ยท ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) = ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) )
69 66 nnred โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โˆˆ โ„ )
70 38 ltm1d โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) < ๐‘† )
71 65 nn0red โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ โ„ )
72 71 38 ltnled โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( ๐‘† โˆ’ 1 ) < ๐‘† โ†” ยฌ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) ) )
73 70 72 mpbid โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ยฌ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) )
74 oveq2 โŠข ( ๐‘š = ( ๐‘† โˆ’ 1 ) โ†’ ( 2 โ†‘ ๐‘š ) = ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) )
75 74 breq2d โŠข ( ๐‘š = ( ๐‘† โˆ’ 1 ) โ†’ ( ๐‘ < ( 2 โ†‘ ๐‘š ) โ†” ๐‘ < ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) )
76 75 53 elrab2 โŠข ( ( ๐‘† โˆ’ 1 ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†” ( ( ๐‘† โˆ’ 1 ) โˆˆ โ„•0 โˆง ๐‘ < ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) )
77 infssuzle โŠข ( ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โŠ† ( โ„คโ‰ฅ โ€˜ 0 ) โˆง ( ๐‘† โˆ’ 1 ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } ) โ†’ inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < ) โ‰ค ( ๐‘† โˆ’ 1 ) )
78 15 77 mpan โŠข ( ( ๐‘† โˆ’ 1 ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†’ inf ( { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } , โ„ , < ) โ‰ค ( ๐‘† โˆ’ 1 ) )
79 4 78 eqbrtrid โŠข ( ( ๐‘† โˆ’ 1 ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†’ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) )
80 79 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( ๐‘† โˆ’ 1 ) โˆˆ { ๐‘› โˆˆ โ„•0 โˆฃ ๐‘ < ( 2 โ†‘ ๐‘› ) } โ†’ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) ) )
81 76 80 biimtrrid โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( ( ๐‘† โˆ’ 1 ) โˆˆ โ„•0 โˆง ๐‘ < ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โ†’ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) ) )
82 65 81 mpand โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘ < ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โ†’ ๐‘† โ‰ค ( ๐‘† โˆ’ 1 ) ) )
83 73 82 mtod โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ยฌ ๐‘ < ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) )
84 69 43 83 nltled โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โ‰ค ๐‘ )
85 68 84 eqbrtrd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 1 ยท ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โ‰ค ๐‘ )
86 1red โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 1 โˆˆ โ„ )
87 2rp โŠข 2 โˆˆ โ„+
88 87 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 2 โˆˆ โ„+ )
89 1z โŠข 1 โˆˆ โ„ค
90 89 a1i โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 1 โˆˆ โ„ค )
91 33 90 zsubcld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ โ„ค )
92 88 91 rpexpcld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) โˆˆ โ„+ )
93 86 43 92 lemuldivd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( 1 ยท ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โ‰ค ๐‘ โ†” 1 โ‰ค ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) )
94 85 93 mpbid โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ 1 โ‰ค ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) )
95 2cn โŠข 2 โˆˆ โ„‚
96 expm1t โŠข ( ( 2 โˆˆ โ„‚ โˆง ๐‘† โˆˆ โ„• ) โ†’ ( 2 โ†‘ ๐‘† ) = ( ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ยท 2 ) )
97 95 63 96 sylancr โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โ†‘ ๐‘† ) = ( ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ยท 2 ) )
98 56 97 breqtrd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘ < ( ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ยท 2 ) )
99 43 41 92 ltdivmuld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) < 2 โ†” ๐‘ < ( ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ยท 2 ) ) )
100 98 99 mpbird โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) < 2 )
101 df-2 โŠข 2 = ( 1 + 1 )
102 100 101 breqtrdi โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) < ( 1 + 1 ) )
103 43 92 rerpdivcld โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โˆˆ โ„ )
104 flbi โŠข ( ( ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โˆˆ โ„ โˆง 1 โˆˆ โ„ค ) โ†’ ( ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) = 1 โ†” ( 1 โ‰ค ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โˆง ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) < ( 1 + 1 ) ) ) )
105 103 89 104 sylancl โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) = 1 โ†” ( 1 โ‰ค ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) โˆง ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) < ( 1 + 1 ) ) ) )
106 94 102 105 mpbir2and โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) = 1 )
107 106 breq2d โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( 2 โˆฅ ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) โ†” 2 โˆฅ 1 ) )
108 12 107 mtbiri โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ยฌ 2 โˆฅ ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) )
109 1 nn0zd โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ค )
110 bitsval2 โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ( ๐‘† โˆ’ 1 ) โˆˆ โ„•0 ) โ†’ ( ( ๐‘† โˆ’ 1 ) โˆˆ ( bits โ€˜ ๐‘ ) โ†” ยฌ 2 โˆฅ ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) ) )
111 109 65 110 syl2an2r โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ( ๐‘† โˆ’ 1 ) โˆˆ ( bits โ€˜ ๐‘ ) โ†” ยฌ 2 โˆฅ ( โŒŠ โ€˜ ( ๐‘ / ( 2 โ†‘ ( ๐‘† โˆ’ 1 ) ) ) ) ) )
112 108 111 mpbird โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ ( bits โ€˜ ๐‘ ) )
113 11 112 sseldd โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) โˆˆ ( 0 ..^ ๐‘€ ) )
114 elfzolt2 โŠข ( ( ๐‘† โˆ’ 1 ) โˆˆ ( 0 ..^ ๐‘€ ) โ†’ ( ๐‘† โˆ’ 1 ) < ๐‘€ )
115 113 114 syl โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โˆ’ 1 ) < ๐‘€ )
116 zlem1lt โŠข ( ( ๐‘† โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค ) โ†’ ( ๐‘† โ‰ค ๐‘€ โ†” ( ๐‘† โˆ’ 1 ) < ๐‘€ ) )
117 32 36 116 syl2an2r โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘† โ‰ค ๐‘€ โ†” ( ๐‘† โˆ’ 1 ) < ๐‘€ ) )
118 115 117 mpbird โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ๐‘† โ‰ค ๐‘€ )
119 37 38 ltnled โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ( ๐‘€ < ๐‘† โ†” ยฌ ๐‘† โ‰ค ๐‘€ ) )
120 60 119 mpbid โŠข ( ( ๐œ‘ โˆง ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) โ†’ ยฌ ๐‘† โ‰ค ๐‘€ )
121 118 120 pm2.65da โŠข ( ๐œ‘ โ†’ ยฌ ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ )
122 9 nnred โŠข ( ๐œ‘ โ†’ ( 2 โ†‘ ๐‘€ ) โˆˆ โ„ )
123 17 122 ltnled โŠข ( ๐œ‘ โ†’ ( ๐‘ < ( 2 โ†‘ ๐‘€ ) โ†” ยฌ ( 2 โ†‘ ๐‘€ ) โ‰ค ๐‘ ) )
124 121 123 mpbird โŠข ( ๐œ‘ โ†’ ๐‘ < ( 2 โ†‘ ๐‘€ ) )
125 elfzo2 โŠข ( ๐‘ โˆˆ ( 0 ..^ ( 2 โ†‘ ๐‘€ ) ) โ†” ( ๐‘ โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) โˆง ( 2 โ†‘ ๐‘€ ) โˆˆ โ„ค โˆง ๐‘ < ( 2 โ†‘ ๐‘€ ) ) )
126 6 10 124 125 syl3anbrc โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ ( 0 ..^ ( 2 โ†‘ ๐‘€ ) ) )