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

Theorem rpnnen2lem4 12818
 Description: Lemma for rpnnen2 12826. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.)
Hypothesis
Ref Expression
rpnnen2.1
Assertion
Ref Expression
rpnnen2lem4
Distinct variable groups:   ,,,   ,,,   ,
Allowed substitution hints:   (,)

Proof of Theorem rpnnen2lem4
StepHypRef Expression
1 nnnn0 10229 . . . . . 6
2 0re 9092 . . . . . . 7
3 1re 9091 . . . . . . . 8
4 3nn 10135 . . . . . . . 8
5 nndivre 10036 . . . . . . . 8
63, 4, 5mp2an 655 . . . . . . 7
7 3re 10072 . . . . . . . 8
8 3pos 10085 . . . . . . . 8
97, 8recgt0ii 9917 . . . . . . 7
102, 6, 9ltleii 9197 . . . . . 6
11 expge0 11417 . . . . . . 7
126, 11mp3an1 1267 . . . . . 6
131, 10, 12sylancl 645 . . . . 5
14133ad2ant3 981 . . . 4
15 0le0 10082 . . . 4
16 breq2 4217 . . . . 5
17 breq2 4217 . . . . 5
1816, 17ifboth 3771 . . . 4
1914, 15, 18sylancl 645 . . 3
20 sstr 3357 . . . . 5
21 rpnnen2.1 . . . . . 6
2221rpnnen2lem1 12815 . . . . 5
2320, 22sylan 459 . . . 4
24233impa 1149 . . 3
2519, 24breqtrrd 4239 . 2
26 reexpcl 11399 . . . . . 6
276, 1, 26sylancr 646 . . . . 5
28273ad2ant3 981 . . . 4
292a1i 11 . . . 4
30 simp1 958 . . . . 5
3130sseld 3348 . . . 4
32 ifle 10784 . . . 4
3328, 29, 14, 31, 32syl31anc 1188 . . 3
3421rpnnen2lem1 12815 . . . 4