Theorem bitsfzo

Description: The bits of a number are all less than M iff the number is nonnegative and less than 2 ^ M . (Contributed by Mario Carneiro, 5-Sep-2016) (Proof shortened by AV, 1-Oct-2020)

	Ref	Expression
Assertion	bitsfzo	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ↔ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bitsval	⊢ ( 𝑚 ∈ ( bits ‘ 𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
2		simp32	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑚 ∈ ℕ0 )
3		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
4	2 3	eleqtrdi	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑚 ∈ ( ℤ≥ ‘ 0 ) )
5		simp1r	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑀 ∈ ℕ0 )
6	5	nn0zd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑀 ∈ ℤ )
7		2re	⊢ 2 ∈ ℝ
8	7	a1i	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 2 ∈ ℝ )
9	8 2	reexpcld	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ )
10		simp1l	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑁 ∈ ℤ )
11	10	zred	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑁 ∈ ℝ )
12	8 5	reexpcld	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑀 ) ∈ ℝ )
13	9	recnd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑚 ) ∈ ℂ )
14	13	mullidd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 1 · ( 2 ↑ 𝑚 ) ) = ( 2 ↑ 𝑚 ) )
15		simp33	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) )
16		2rp	⊢ 2 ∈ ℝ+
17	16	a1i	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 2 ∈ ℝ+ )
18	2	nn0zd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑚 ∈ ℤ )
19	17 18	rpexpcld	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑚 ) ∈ ℝ+ )
20	11 19	rerpdivcld	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 𝑁 / ( 2 ↑ 𝑚 ) ) ∈ ℝ )
21		1red	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 1 ∈ ℝ )
22	20 21	ltnled	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( 𝑁 / ( 2 ↑ 𝑚 ) ) < 1 ↔ ¬ 1 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) )
23		0p1e1	⊢ ( 0 + 1 ) = 1
24	23	breq2i	⊢ ( ( 𝑁 / ( 2 ↑ 𝑚 ) ) < ( 0 + 1 ) ↔ ( 𝑁 / ( 2 ↑ 𝑚 ) ) < 1 )
25		elfzole1	⊢ ( 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) → 0 ≤ 𝑁 )
26	25	3ad2ant2	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 0 ≤ 𝑁 )
27	11 19 26	divge0d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 0 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) )
28		0z	⊢ 0 ∈ ℤ
29		flbi	⊢ ( ( ( 𝑁 / ( 2 ↑ 𝑚 ) ) ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = 0 ↔ ( 0 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ∧ ( 𝑁 / ( 2 ↑ 𝑚 ) ) < ( 0 + 1 ) ) ) )
30	20 28 29	sylancl	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = 0 ↔ ( 0 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ∧ ( 𝑁 / ( 2 ↑ 𝑚 ) ) < ( 0 + 1 ) ) ) )
31		z0even	⊢ 2 ∥ 0
32		id	⊢ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = 0 → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = 0 )
33	31 32	breqtrrid	⊢ ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) = 0 → 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) )
34	30 33	syl6bir	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( 0 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ∧ ( 𝑁 / ( 2 ↑ 𝑚 ) ) < ( 0 + 1 ) ) → 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
35	27 34	mpand	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( 𝑁 / ( 2 ↑ 𝑚 ) ) < ( 0 + 1 ) → 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
36	24 35	biimtrrid	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( 𝑁 / ( 2 ↑ 𝑚 ) ) < 1 → 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
37	22 36	sylbird	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ¬ 1 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) → 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) )
38	15 37	mt3d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 1 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) )
39	21 11 19	lemuldivd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( ( 1 · ( 2 ↑ 𝑚 ) ) ≤ 𝑁 ↔ 1 ≤ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) )
40	38 39	mpbird	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 1 · ( 2 ↑ 𝑚 ) ) ≤ 𝑁 )
41	14 40	eqbrtrrd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑚 ) ≤ 𝑁 )
42		elfzolt2	⊢ ( 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) → 𝑁 < ( 2 ↑ 𝑀 ) )
43	42	3ad2ant2	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑁 < ( 2 ↑ 𝑀 ) )
44	9 11 12 41 43	lelttrd	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 2 ↑ 𝑚 ) < ( 2 ↑ 𝑀 ) )
45		1lt2	⊢ 1 < 2
46	45	a1i	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 1 < 2 )
47	8 18 6 46	ltexp2d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → ( 𝑚 < 𝑀 ↔ ( 2 ↑ 𝑚 ) < ( 2 ↑ 𝑀 ) ) )
48	44 47	mpbird	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑚 < 𝑀 )
49		elfzo2	⊢ ( 𝑚 ∈ ( 0 ..^ 𝑀 ) ↔ ( 𝑚 ∈ ( ℤ≥ ‘ 0 ) ∧ 𝑀 ∈ ℤ ∧ 𝑚 < 𝑀 ) )
50	4 6 48 49	syl3anbrc	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) ) → 𝑚 ∈ ( 0 ..^ 𝑀 ) )
51	50	3expia	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ) → ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℕ0 ∧ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ 𝑚 ) ) ) ) → 𝑚 ∈ ( 0 ..^ 𝑀 ) ) )
52	1 51	biimtrid	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ) → ( 𝑚 ∈ ( bits ‘ 𝑁 ) → 𝑚 ∈ ( 0 ..^ 𝑀 ) ) )
53	52	ssrdv	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ) → ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) )
54		simpr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℕ )
55	54	nnred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℝ )
56		simpllr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑀 ∈ ℕ0 )
57	56	nn0red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑀 ∈ ℝ )
58		max2	⊢ ( ( - 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → 𝑀 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) )
59	55 57 58	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑀 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) )
60		simplr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) )
61		n2dvdsm1	⊢ ¬ 2 ∥ - 1
62		simplll	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℤ )
63	62	zred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℝ )
64		2nn	⊢ 2 ∈ ℕ
65	64	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 2 ∈ ℕ )
66	54	nnnn0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ∈ ℕ0 )
67	56 66	ifcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ℕ0 )
68	65 67	nnexpcld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ∈ ℕ )
69	63 68	nndivred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ∈ ℝ )
70		1red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 1 ∈ ℝ )
71	62	zcnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 𝑁 ∈ ℂ )
72	68	nncnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ∈ ℂ )
73		2cnd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 2 ∈ ℂ )
74		2ne0	⊢ 2 ≠ 0
75	74	a1i	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 2 ≠ 0 )
76	67	nn0zd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ℤ )
77	73 75 76	expne0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ≠ 0 )
78	71 72 77	divnegd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) = ( - 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) )
79	67	nn0red	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ℝ )
80	68	nnred	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ∈ ℝ )
81		max1	⊢ ( ( - 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → - 𝑁 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) )
82	55 57 81	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) )
83		2z	⊢ 2 ∈ ℤ
84		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
85	83 84	ax-mp	⊢ 2 ∈ ( ℤ≥ ‘ 2 )
86		bernneq3	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ℕ0 ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) < ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
87	85 67 86	sylancr	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) < ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
88	79 80 87	ltled	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ≤ ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
89	55 79 80 82 88	letrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ≤ ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
90	72	mulridd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) · 1 ) = ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
91	89 90	breqtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 𝑁 ≤ ( ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) · 1 ) )
92	68	nnrpd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ∈ ℝ+ )
93	55 70 92	ledivmuld	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( ( - 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ≤ 1 ↔ - 𝑁 ≤ ( ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) · 1 ) ) )
94	91 93	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( - 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ≤ 1 )
95	78 94	eqbrtrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ≤ 1 )
96	69 70 95	lenegcon1d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → - 1 ≤ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) )
97	54	nngt0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 0 < - 𝑁 )
98	68	nngt0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 0 < ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
99	55 80 97 98	divgt0d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 0 < ( - 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) )
100	99 78	breqtrrd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → 0 < - ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) )
101	69	lt0neg1d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) < 0 ↔ 0 < - ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) )
102	100 101	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) < 0 )
103		ax-1cn	⊢ 1 ∈ ℂ
104		neg1cn	⊢ - 1 ∈ ℂ
105		1pneg1e0	⊢ ( 1 + - 1 ) = 0
106	103 104 105	addcomli	⊢ ( - 1 + 1 ) = 0
107	102 106	breqtrrdi	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) < ( - 1 + 1 ) )
108		neg1z	⊢ - 1 ∈ ℤ
109		flbi	⊢ ( ( ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ∈ ℝ ∧ - 1 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) = - 1 ↔ ( - 1 ≤ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ∧ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) < ( - 1 + 1 ) ) ) )
110	69 108 109	sylancl	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) = - 1 ↔ ( - 1 ≤ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ∧ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) < ( - 1 + 1 ) ) ) )
111	96 107 110	mpbir2and	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) = - 1 )
112	111	breq2d	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) ↔ 2 ∥ - 1 ) )
113	61 112	mtbiri	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) )
114		bitsval2	⊢ ( ( 𝑁 ∈ ℤ ∧ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ℕ0 ) → ( if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) ) )
115	62 67 114	syl2anc	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ( bits ‘ 𝑁 ) ↔ ¬ 2 ∥ ( ⌊ ‘ ( 𝑁 / ( 2 ↑ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) ) ) ) )
116	113 115	mpbird	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ( bits ‘ 𝑁 ) )
117	60 116	sseldd	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ( 0 ..^ 𝑀 ) )
118		elfzolt2	⊢ ( if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ∈ ( 0 ..^ 𝑀 ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) < 𝑀 )
119	117 118	syl	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) < 𝑀 )
120	79 57	ltnled	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ( if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) < 𝑀 ↔ ¬ 𝑀 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) ) )
121	119 120	mpbid	⊢ ( ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) ∧ - 𝑁 ∈ ℕ ) → ¬ 𝑀 ≤ if ( - 𝑁 ≤ 𝑀 , 𝑀 , - 𝑁 ) )
122	59 121	pm2.65da	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → ¬ - 𝑁 ∈ ℕ )
123	122	intnand	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) )
124		simpll	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ℤ )
125		elznn0nn	⊢ ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
126	124 125	sylib	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
127	126	ord	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → ( ¬ 𝑁 ∈ ℕ0 → ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
128	123 127	mt3d	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ℕ0 )
129		simplr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → 𝑀 ∈ ℕ0 )
130		simpr	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) )
131		eqid	⊢ inf ( { 𝑛 ∈ ℕ0 ∣ 𝑁 < ( 2 ↑ 𝑛 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ0 ∣ 𝑁 < ( 2 ↑ 𝑛 ) } , ℝ , < )
132	128 129 130 131	bitsfzolem	⊢ ( ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) ∧ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) → 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) )
133	53 132	impbida	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ∈ ( 0 ..^ ( 2 ↑ 𝑀 ) ) ↔ ( bits ‘ 𝑁 ) ⊆ ( 0 ..^ 𝑀 ) ) )