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

Theorem lcfrlem42 32444
 Description: Lemma for lcfr 32445. Eliminate nonzero condition. (Contributed by NM, 11-Mar-2015.)
Hypotheses
Ref Expression
lcfrlem38.h
lcfrlem38.o
lcfrlem38.u
lcfrlem38.p
lcfrlem38.f LFnl
lcfrlem38.l LKer
lcfrlem38.d LDual
lcfrlem38.q
lcfrlem38.c LFnl
lcfrlem38.e
lcfrlem38.k
lcfrlem38.g
lcfrlem38.gs
lcfrlem38.xe
lcfrlem38.ye
Assertion
Ref Expression
lcfrlem42
Distinct variable groups:   ,   ,   ,,   ,,   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   ()   (,)   ()   (,)   (,)   (,)   ()   (,)   (,)   (,)

Proof of Theorem lcfrlem42
StepHypRef Expression
1 lcfrlem38.h . . . . . 6
2 lcfrlem38.u . . . . . 6
3 lcfrlem38.k . . . . . 6
41, 2, 3dvhlmod 31970 . . . . 5
5 lcfrlem38.o . . . . . 6
6 eqid 2438 . . . . . 6
7 lcfrlem38.l . . . . . 6 LKer
8 lcfrlem38.d . . . . . 6 LDual
9 lcfrlem38.q . . . . . 6
10 lcfrlem38.e . . . . . 6
11 lcfrlem38.g . . . . . 6
12 lcfrlem38.xe . . . . . 6
131, 5, 2, 6, 7, 8, 9, 10, 3, 11, 12lcfrlem4 32405 . . . . 5
14 lcfrlem38.ye . . . . . 6
151, 5, 2, 6, 7, 8, 9, 10, 3, 11, 14lcfrlem4 32405 . . . . 5
16 lcfrlem38.p . . . . . 6
176, 16lmodcom 15992 . . . . 5
184, 13, 15, 17syl3anc 1185 . . . 4
203adantr 453 . . . 4
2111adantr 453 . . . 4
2214adantr 453 . . . 4
23 eqid 2438 . . . 4
24 simpr 449 . . . 4
251, 5, 2, 16, 7, 8, 9, 20, 21, 10, 22, 23, 24lcfrlem7 32408 . . 3
2619, 25eqeltrd 2512 . 2
30 simpr 449 . . 3
311, 5, 2, 16, 7, 8, 9, 27, 28, 10, 29, 23, 30lcfrlem7 32408 . 2
32 lcfrlem38.f . . 3 LFnl
33 lcfrlem38.c . . 3 LFnl