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