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

Theorem lsppratlem5 16215
 Description: Lemma for lspprat 16217. Combine the two cases and show a contradiction to under the assumptions on and . (Contributed by NM, 29-Aug-2014.)
Hypotheses
Ref Expression
lspprat.v
lspprat.s
lspprat.n
lspprat.w
lspprat.u
lspprat.x
lspprat.y
lspprat.p
lsppratlem1.o
lsppratlem1.x2
lsppratlem1.y2
Assertion
Ref Expression
lsppratlem5

Proof of Theorem lsppratlem5
StepHypRef Expression
1 lspprat.v . . . 4
2 lspprat.s . . . 4
3 lspprat.n . . . 4
4 lspprat.w . . . . 5
54adantr 452 . . . 4
6 lspprat.u . . . . 5
76adantr 452 . . . 4
8 lspprat.x . . . . 5
98adantr 452 . . . 4
10 lspprat.y . . . . 5
1110adantr 452 . . . 4
12 lspprat.p . . . . 5
1312adantr 452 . . . 4
14 lsppratlem1.o . . . 4
15 lsppratlem1.x2 . . . . 5
1615adantr 452 . . . 4
17 lsppratlem1.y2 . . . . 5
1817adantr 452 . . . 4
19 simpr 448 . . . 4
201, 2, 3, 5, 7, 9, 11, 13, 14, 16, 18, 19lsppratlem3 16213 . . 3
214adantr 452 . . . 4
226adantr 452 . . . 4
238adantr 452 . . . 4
2410adantr 452 . . . 4
2512adantr 452 . . . 4
2615adantr 452 . . . 4
2717adantr 452 . . . 4
28 simpr 448 . . . 4
291, 2, 3, 21, 22, 23, 24, 25, 14, 26, 27, 28lsppratlem4 16214 . . 3
301, 2, 3, 4, 6, 8, 10, 12, 14, 15, 17lsppratlem1 16211 . . 3
3120, 29, 30mpjaodan 762 . 2