Metamath Proof Explorer


Theorem dignn0ldlem

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

Ref Expression
Assertion dignn0ldlem
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N < ( B ^ K ) )

Proof

Step Hyp Ref Expression
1 nnre
 |-  ( N e. NN -> N e. RR )
2 1 3ad2ant2
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N e. RR )
3 eluzelre
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. RR )
4 3 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> B e. RR )
5 eluz2nn
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. NN )
6 nnnn0
 |-  ( B e. NN -> B e. NN0 )
7 6 nn0ge0d
 |-  ( B e. NN -> 0 <_ B )
8 5 7 syl
 |-  ( B e. ( ZZ>= ` 2 ) -> 0 <_ B )
9 8 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> 0 <_ B )
10 nnrp
 |-  ( N e. NN -> N e. RR+ )
11 relogbzcl
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. RR+ ) -> ( B logb N ) e. RR )
12 10 11 sylan2
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( B logb N ) e. RR )
13 12 3adant3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B logb N ) e. RR )
14 4 9 13 recxpcld
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B ^c ( B logb N ) ) e. RR )
15 eluzelre
 |-  ( K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) -> K e. RR )
16 15 3ad2ant3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> K e. RR )
17 4 9 16 recxpcld
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B ^c K ) e. RR )
18 1 leidd
 |-  ( N e. NN -> N <_ N )
19 18 adantl
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N <_ N )
20 eluz2cnn0n1
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. ( CC \ { 0 , 1 } ) )
21 nncn
 |-  ( N e. NN -> N e. CC )
22 nnne0
 |-  ( N e. NN -> N =/= 0 )
23 eldifsn
 |-  ( N e. ( CC \ { 0 } ) <-> ( N e. CC /\ N =/= 0 ) )
24 21 22 23 sylanbrc
 |-  ( N e. NN -> N e. ( CC \ { 0 } ) )
25 cxplogb
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ N e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb N ) ) = N )
26 20 24 25 syl2an
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( B ^c ( B logb N ) ) = N )
27 19 26 breqtrrd
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> N <_ ( B ^c ( B logb N ) ) )
28 27 3adant3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N <_ ( B ^c ( B logb N ) ) )
29 eluz2
 |-  ( K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) <-> ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ /\ ( ( |_ ` ( B logb N ) ) + 1 ) <_ K ) )
30 12 adantl
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> ( B logb N ) e. RR )
31 flltp1
 |-  ( ( B logb N ) e. RR -> ( B logb N ) < ( ( |_ ` ( B logb N ) ) + 1 ) )
32 30 31 syl
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> ( B logb N ) < ( ( |_ ` ( B logb N ) ) + 1 ) )
33 zre
 |-  ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ -> ( ( |_ ` ( B logb N ) ) + 1 ) e. RR )
34 33 adantr
 |-  ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( |_ ` ( B logb N ) ) + 1 ) e. RR )
35 34 adantr
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> ( ( |_ ` ( B logb N ) ) + 1 ) e. RR )
36 zre
 |-  ( K e. ZZ -> K e. RR )
37 36 adantl
 |-  ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) -> K e. RR )
38 37 adantr
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> K e. RR )
39 ltletr
 |-  ( ( ( B logb N ) e. RR /\ ( ( |_ ` ( B logb N ) ) + 1 ) e. RR /\ K e. RR ) -> ( ( ( B logb N ) < ( ( |_ ` ( B logb N ) ) + 1 ) /\ ( ( |_ ` ( B logb N ) ) + 1 ) <_ K ) -> ( B logb N ) < K ) )
40 30 35 38 39 syl3anc
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> ( ( ( B logb N ) < ( ( |_ ` ( B logb N ) ) + 1 ) /\ ( ( |_ ` ( B logb N ) ) + 1 ) <_ K ) -> ( B logb N ) < K ) )
41 32 40 mpand
 |-  ( ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) /\ ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) ) -> ( ( ( |_ ` ( B logb N ) ) + 1 ) <_ K -> ( B logb N ) < K ) )
42 41 ex
 |-  ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( |_ ` ( B logb N ) ) + 1 ) <_ K -> ( B logb N ) < K ) ) )
43 42 com23
 |-  ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ ) -> ( ( ( |_ ` ( B logb N ) ) + 1 ) <_ K -> ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( B logb N ) < K ) ) )
44 43 3impia
 |-  ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ /\ ( ( |_ ` ( B logb N ) ) + 1 ) <_ K ) -> ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( B logb N ) < K ) )
45 44 com12
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( ( ( |_ ` ( B logb N ) ) + 1 ) e. ZZ /\ K e. ZZ /\ ( ( |_ ` ( B logb N ) ) + 1 ) <_ K ) -> ( B logb N ) < K ) )
46 29 45 syl5bi
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) -> ( B logb N ) < K ) )
47 46 3impia
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B logb N ) < K )
48 eluz2gt1
 |-  ( B e. ( ZZ>= ` 2 ) -> 1 < B )
49 3 48 jca
 |-  ( B e. ( ZZ>= ` 2 ) -> ( B e. RR /\ 1 < B ) )
50 49 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B e. RR /\ 1 < B ) )
51 cxplt
 |-  ( ( ( B e. RR /\ 1 < B ) /\ ( ( B logb N ) e. RR /\ K e. RR ) ) -> ( ( B logb N ) < K <-> ( B ^c ( B logb N ) ) < ( B ^c K ) ) )
52 50 13 16 51 syl12anc
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( ( B logb N ) < K <-> ( B ^c ( B logb N ) ) < ( B ^c K ) ) )
53 47 52 mpbid
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( B ^c ( B logb N ) ) < ( B ^c K ) )
54 2 14 17 28 53 lelttrd
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N < ( B ^c K ) )
55 eluzelcn
 |-  ( B e. ( ZZ>= ` 2 ) -> B e. CC )
56 55 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> B e. CC )
57 eluz2n0
 |-  ( B e. ( ZZ>= ` 2 ) -> B =/= 0 )
58 57 3ad2ant1
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> B =/= 0 )
59 eluzelz
 |-  ( K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) -> K e. ZZ )
60 59 3ad2ant3
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> K e. ZZ )
61 cxpexpz
 |-  ( ( B e. CC /\ B =/= 0 /\ K e. ZZ ) -> ( B ^c K ) = ( B ^ K ) )
62 61 breq2d
 |-  ( ( B e. CC /\ B =/= 0 /\ K e. ZZ ) -> ( N < ( B ^c K ) <-> N < ( B ^ K ) ) )
63 56 58 60 62 syl3anc
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> ( N < ( B ^c K ) <-> N < ( B ^ K ) ) )
64 54 63 mpbid
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ N e. NN /\ K e. ( ZZ>= ` ( ( |_ ` ( B logb N ) ) + 1 ) ) ) -> N < ( B ^ K ) )