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 ) )