Metamath Proof Explorer

Theorem dignn0ldlem

Description: Lemma for dignnld . (Contributed by AV, 25-May-2020)

Ref Expression
Assertion dignn0ldlem ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 < ( 𝐵 ↑ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 nnre ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
2 1 3ad2ant2 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 ∈ ℝ )
3 eluzelre ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℝ )
4 3 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ∈ ℝ )
5 eluz2nn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℕ )
6 nnnn0 ⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 )
7 6 nn0ge0d ⊢ ( 𝐵 ∈ ℕ → 0 ≤ 𝐵 )
8 5 7 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 0 ≤ 𝐵 )
9 8 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 0 ≤ 𝐵 )
10 nnrp ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
11 relogbzcl ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℝ+ ) → ( 𝐵 logb 𝑁 ) ∈ ℝ )
12 10 11 sylan2 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) ∈ ℝ )
13 12 3adant3 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 logb 𝑁 ) ∈ ℝ )
14 4 9 13 recxpcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) ∈ ℝ )
15 eluzelre ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → 𝐾 ∈ ℝ )
16 15 3ad2ant3 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐾 ∈ ℝ )
17 4 9 16 recxpcld ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 𝐾 ) ∈ ℝ )
18 1 leidd ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≤ 𝑁 )
19 18 adantl ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ 𝑁 )
20 eluz2cnn0n1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
21 nncn ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℂ )
22 nnne0 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ≠ 0 )
23 eldifsn ⊢ ( 𝑁 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑁 ∈ ℂ ∧ 𝑁 ≠ 0 ) )
24 21 22 23 sylanbrc ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℂ ∖ { 0 } ) )
25 cxplogb ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝑁 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) = 𝑁 )
26 20 24 25 syl2an ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) = 𝑁 )
27 19 26 breqtrrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → 𝑁 ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) )
28 27 3adant3 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 ≤ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) )
29 eluz2 ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ↔ ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) )
30 12 adantl ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( 𝐵 logb 𝑁 ) ∈ ℝ )
31 flltp1 ⊢ ( ( 𝐵 logb 𝑁 ) ∈ ℝ → ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) )
32 30 31 syl ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) )
33 zre ⊢ ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ )
34 33 adantr ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ )
35 34 adantr ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ )
36 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
37 36 adantl ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℝ )
38 37 adantr ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → 𝐾 ∈ ℝ )
39 ltletr ⊢ ( ( ( 𝐵 logb 𝑁 ) ∈ ℝ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( ( ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
40 30 35 38 39 syl3anc ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ( 𝐵 logb 𝑁 ) < ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
41 32 40 mpand ⊢ ( ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
42 41 ex ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) )
43 42 com23 ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) ) )
44 43 3impia ⊢ ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
45 44 com12 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( ( ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ≤ 𝐾 ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
46 29 45 biimtrid ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → ( 𝐵 logb 𝑁 ) < 𝐾 ) )
47 46 3impia ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 logb 𝑁 ) < 𝐾 )
48 eluz2gt1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝐵 )
49 3 48 jca ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) )
50 49 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) )
51 cxplt ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 1 < 𝐵 ) ∧ ( ( 𝐵 logb 𝑁 ) ∈ ℝ ∧ 𝐾 ∈ ℝ ) ) → ( ( 𝐵 logb 𝑁 ) < 𝐾 ↔ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) ) )
52 50 13 16 51 syl12anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( ( 𝐵 logb 𝑁 ) < 𝐾 ↔ ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) ) )
53 47 52 mpbid ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝐵 ↑𝑐 ( 𝐵 logb 𝑁 ) ) < ( 𝐵 ↑𝑐 𝐾 ) )
54 2 14 17 28 53 lelttrd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) )
55 eluzelcn ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ∈ ℂ )
56 55 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ∈ ℂ )
57 eluz2n0 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → 𝐵 ≠ 0 )
58 57 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐵 ≠ 0 )
59 eluzelz ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) → 𝐾 ∈ ℤ )
60 59 3ad2ant3 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝐾 ∈ ℤ )
61 cxpexpz ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝐵 ↑𝑐 𝐾 ) = ( 𝐵 ↑ 𝐾 ) )
62 61 breq2d ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) ↔ 𝑁 < ( 𝐵 ↑ 𝐾 ) ) )
63 56 58 60 62 syl3anc ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → ( 𝑁 < ( 𝐵 ↑𝑐 𝐾 ) ↔ 𝑁 < ( 𝐵 ↑ 𝐾 ) ) )
64 54 63 mpbid ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ℕ ∧ 𝐾 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 𝐵 logb 𝑁 ) ) + 1 ) ) ) → 𝑁 < ( 𝐵 ↑ 𝐾 ) )