Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  osumcllem3N Structured version   Unicode version

Theorem osumcllem3N 30682
 Description: Lemma for osumclN 30691. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
osumcllem.l
osumcllem.j
osumcllem.a
osumcllem.p
osumcllem.o
osumcllem.c
osumcllem.m
osumcllem.u
Assertion
Ref Expression
osumcllem3N

Proof of Theorem osumcllem3N
StepHypRef Expression
1 incom 3525 . 2
2 osumcllem.u . . . . 5
3 simp1 957 . . . . . . . 8
4 simp3 959 . . . . . . . . 9
5 osumcllem.a . . . . . . . . . . . 12
6 osumcllem.c . . . . . . . . . . . 12
75, 6psubclssatN 30665 . . . . . . . . . . 11
873adant3 977 . . . . . . . . . 10
9 osumcllem.o . . . . . . . . . . 11
105, 9polssatN 30632 . . . . . . . . . 10
113, 8, 10syl2anc 643 . . . . . . . . 9
124, 11sstrd 3350 . . . . . . . 8
13 osumcllem.p . . . . . . . . 9
145, 13, 9poldmj1N 30652 . . . . . . . 8
153, 12, 8, 14syl3anc 1184 . . . . . . 7
16 incom 3525 . . . . . . 7
1715, 16syl6eq 2483 . . . . . 6
1817fveq2d 5724 . . . . 5
192, 18syl5eq 2479 . . . 4
2019ineq1d 3533 . . 3
215, 9polcon2N 30643 . . . . 5
228, 21syld3an2 1231 . . . 4
235, 9poml5N 30678 . . . 4
243, 12, 22, 23syl3anc 1184 . . 3
259, 6psubcli2N 30663 . . . 4