Metamath Proof Explorer


Theorem dig1

Description: All but one digits of 1 are 0. (Contributed by AV, 24-May-2020)

Ref Expression
Assertion dig1 ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = if ( 𝐾 = 0 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 eluzelcn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℂ )
2 1 exp0d ( 𝐵 ∈ ( ℤ ‘ 2 ) → ( 𝐵 ↑ 0 ) = 1 )
3 2 eqcomd ( 𝐵 ∈ ( ℤ ‘ 2 ) → 1 = ( 𝐵 ↑ 0 ) )
4 3 ad2antrl ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 1 = ( 𝐵 ↑ 0 ) )
5 4 oveq2d ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = ( 𝐾 ( digit ‘ 𝐵 ) ( 𝐵 ↑ 0 ) ) )
6 simprl ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 𝐵 ∈ ( ℤ ‘ 2 ) )
7 simpr ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
8 7 anim2i ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 0 ≤ 𝐾𝐾 ∈ ℤ ) )
9 8 ancomd ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
10 elnn0z ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℤ ∧ 0 ≤ 𝐾 ) )
11 9 10 sylibr ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℕ0 )
12 0nn0 0 ∈ ℕ0
13 12 a1i ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 0 ∈ ℕ0 )
14 digexp ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 𝐵 ) ( 𝐵 ↑ 0 ) ) = if ( 𝐾 = 0 , 1 , 0 ) )
15 6 11 13 14 syl3anc ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) ( 𝐵 ↑ 0 ) ) = if ( 𝐾 = 0 , 1 , 0 ) )
16 5 15 eqtrd ( ( 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = if ( 𝐾 = 0 , 1 , 0 ) )
17 eluz2nn ( 𝐵 ∈ ( ℤ ‘ 2 ) → 𝐵 ∈ ℕ )
18 17 ad2antrl ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 𝐵 ∈ ℕ )
19 simprr ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
20 nn0ge0 ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 )
21 20 a1i ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ∈ ℕ0 → 0 ≤ 𝐾 ) )
22 21 con3d ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( ¬ 0 ≤ 𝐾 → ¬ 𝐾 ∈ ℕ0 ) )
23 22 impcom ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ¬ 𝐾 ∈ ℕ0 )
24 19 23 eldifd ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ( ℤ ∖ ℕ0 ) )
25 1nn0 1 ∈ ℕ0
26 25 a1i ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → 1 ∈ ℕ0 )
27 dignn0fr ( ( 𝐵 ∈ ℕ ∧ 𝐾 ∈ ( ℤ ∖ ℕ0 ) ∧ 1 ∈ ℕ0 ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = 0 )
28 18 24 26 27 syl3anc ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = 0 )
29 0le0 0 ≤ 0
30 breq2 ( 𝐾 = 0 → ( 0 ≤ 𝐾 ↔ 0 ≤ 0 ) )
31 29 30 mpbiri ( 𝐾 = 0 → 0 ≤ 𝐾 )
32 31 a1i ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 = 0 → 0 ≤ 𝐾 ) )
33 32 con3d ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( ¬ 0 ≤ 𝐾 → ¬ 𝐾 = 0 ) )
34 33 impcom ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ¬ 𝐾 = 0 )
35 34 iffalsed ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → if ( 𝐾 = 0 , 1 , 0 ) = 0 )
36 28 35 eqtr4d ( ( ¬ 0 ≤ 𝐾 ∧ ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = if ( 𝐾 = 0 , 1 , 0 ) )
37 16 36 pm2.61ian ( ( 𝐵 ∈ ( ℤ ‘ 2 ) ∧ 𝐾 ∈ ℤ ) → ( 𝐾 ( digit ‘ 𝐵 ) 1 ) = if ( 𝐾 = 0 , 1 , 0 ) )