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

Theorem eflt 12720
 Description: The exponential function on the reals is strictly monotonic. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Mario Carneiro, 17-Jul-2014.)
Assertion
Ref Expression
eflt

Proof of Theorem eflt
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1331 . 2
2 fveq2 5730 . . 3
3 fveq2 5730 . . 3
4 fveq2 5730 . . 3
5 ssid 3369 . . 3
6 reefcl 12691 . . . 4
8 simp2 959 . . . . . . . . . 10
9 simp1 958 . . . . . . . . . 10
108, 9resubcld 9467 . . . . . . . . 9
11 posdif 9523 . . . . . . . . . 10
1211biimp3a 1284 . . . . . . . . 9
1310, 12elrpd 10648 . . . . . . . 8
14 efgt1 12719 . . . . . . . 8
1513, 14syl 16 . . . . . . 7
169reefcld 12692 . . . . . . . 8
1710reefcld 12692 . . . . . . . 8
18 efgt0 12706 . . . . . . . . 9
199, 18syl 16 . . . . . . . 8
20 ltmulgt11 9872 . . . . . . . 8
2116, 17, 19, 20syl3anc 1185 . . . . . . 7
2215, 21mpbid 203 . . . . . 6
239recnd 9116 . . . . . . . 8
2410recnd 9116 . . . . . . . 8
25 efadd 12698 . . . . . . . 8
2623, 24, 25syl2anc 644 . . . . . . 7
278recnd 9116 . . . . . . . . 9
2823, 27pncan3d 9416 . . . . . . . 8
2928fveq2d 5734 . . . . . . 7
3026, 29eqtr3d 2472 . . . . . 6
3122, 30breqtrd 4238 . . . . 5
32313expia 1156 . . . 4