Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efexple Structured version   Unicode version

Theorem efexple 24072
 Description: Convert a bound on a power to a bound on the exponent. (Contributed by Mario Carneiro, 11-Mar-2014.)
Assertion
Ref Expression
efexple

Proof of Theorem efexple
StepHypRef Expression
1 simpl 458 . . . . . 6
2 0lt1 10135 . . . . . . . 8
3 0re 9642 . . . . . . . . 9
4 1re 9641 . . . . . . . . 9
5 lttr 9709 . . . . . . . . 9
63, 4, 5mp3an12 1350 . . . . . . . 8
72, 6mpani 680 . . . . . . 7
87imp 430 . . . . . 6
91, 8elrpd 11338 . . . . 5
1093ad2ant1 1026 . . . 4
11 simp2 1006 . . . 4
12 reexplog 23409 . . . 4
1310, 11, 12syl2anc 665 . . 3
14 reeflog 23395 . . . . 5
15143ad2ant3 1028 . . . 4
1615eqcomd 2437 . . 3
1713, 16breq12d 4439 . 2
18 zre 10941 . . . . 5
19183ad2ant2 1027 . . . 4
20 rplogcl 23418 . . . . . 6
21203ad2ant1 1026 . . . . 5
2221rpred 11341 . . . 4
2319, 22remulcld 9670 . . 3
24 relogcl 23390 . . . 4