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

Theorem pmltpclem2 19338
 Description: Lemma for pmltpc 19339. (Contributed by Mario Carneiro, 1-Jul-2014.)
Hypotheses
Ref Expression
pmltpc.1
pmltpc.2
pmltpc.3
pmltpc.4
pmltpc.5
pmltpc.6
pmltpc.7
pmltpc.8
pmltpc.9
pmltpc.10
Assertion
Ref Expression
pmltpclem2
Distinct variable groups:   ,,,   ,,,   ,,   ,,,   ,,,   ,,
Allowed substitution hints:   (,,)   ()   ()

Proof of Theorem pmltpclem2
StepHypRef Expression
1 pmltpc.5 . . . . 5
21ad2antrr 707 . . . 4
3 pmltpc.3 . . . . 5
43ad2antrr 707 . . . 4
5 pmltpc.4 . . . . 5
65ad2antrr 707 . . . 4
7 simpr 448 . . . 4
8 pmltpc.1 . . . . . . . . . . 11
9 reex 9073 . . . . . . . . . . . 12
109, 9elpm2 7037 . . . . . . . . . . 11
118, 10sylib 189 . . . . . . . . . 10
1211simpld 446 . . . . . . . . 9
13 pmltpc.2 . . . . . . . . . 10
1413, 5sseldd 3341 . . . . . . . . 9
1512, 14ffvelrnd 5863 . . . . . . . 8
16 pmltpc.9 . . . . . . . . 9
1713, 3sseldd 3341 . . . . . . . . . . 11
1812, 17ffvelrnd 5863 . . . . . . . . . 10
1915, 18ltnled 9212 . . . . . . . . 9
2016, 19mpbird 224 . . . . . . . 8
2115, 20gtned 9200 . . . . . . 7
22 fveq2 5720 . . . . . . . . 9
2322eqcomd 2440 . . . . . . . 8
2423necon3i 2637 . . . . . . 7
2521, 24syl 16 . . . . . 6
2611simprd 450 . . . . . . . 8
2726, 17sseldd 3341 . . . . . . 7
2826, 14sseldd 3341 . . . . . . 7
29 pmltpc.7 . . . . . . 7
3027, 28, 29leltned 9216 . . . . . 6
3125, 30mpbird 224 . . . . 5
3231ad2antrr 707 . . . 4
33 simplr 732 . . . . . 6
3420ad2antrr 707 . . . . . 6
3533, 34jca 519 . . . . 5
3635orcd 382 . . . 4
372, 4, 6, 7, 32, 36pmltpclem1 19337 . . 3
383ad2antrr 707 . . . 4
391ad2antrr 707 . . . 4
40 pmltpc.6 . . . . 5
4140ad2antrr 707 . . . 4
4213, 1sseldd 3341 . . . . . . . . 9
4312, 42ffvelrnd 5863 . . . . . . . 8
4443ad2antrr 707 . . . . . . 7
45 simplr 732 . . . . . . 7
4644, 45gtned 9200 . . . . . 6
47 fveq2 5720 . . . . . . . 8
4847eqcomd 2440 . . . . . . 7
4948necon3i 2637 . . . . . 6
5046, 49syl 16 . . . . 5
5127ad2antrr 707 . . . . . 6
5226, 42sseldd 3341 . . . . . . 7
5352ad2antrr 707 . . . . . 6
54 simpr 448 . . . . . 6
5551, 53, 54leltned 9216 . . . . 5
5650, 55mpbird 224 . . . 4
57 pmltpc.10 . . . . . . . . 9
5813, 40sseldd 3341 . . . . . . . . . . 11
5912, 58ffvelrnd 5863 . . . . . . . . . 10
6043, 59ltnled 9212 . . . . . . . . 9
6157, 60mpbird 224 . . . . . . . 8
6243, 61gtned 9200 . . . . . . 7
63 fveq2 5720 . . . . . . . 8
6463necon3i 2637 . . . . . . 7
6562, 64syl 16 . . . . . 6
6626, 58sseldd 3341 . . . . . . 7
67 pmltpc.8 . . . . . . 7
6852, 66, 67leltned 9216 . . . . . 6
6965, 68mpbird 224 . . . . 5
7069ad2antrr 707 . . . 4
7161ad2antrr 707 . . . . . 6
7245, 71jca 519 . . . . 5
7372olcd 383 . . . 4
7438, 39, 41, 56, 70, 73pmltpclem1 19337 . . 3
7737, 74, 75, 76ltlecasei 9173 . 2
783ad2antrr 707 . . . 4
795ad2antrr 707 . . . 4
8040ad2antrr 707 . . . 4
8131ad2antrr 707 . . . 4
82 simpr 448 . . . 4
8320ad2antrr 707 . . . . . 6
8415adantr 452 . . . . . . . 8
8518adantr 452 . . . . . . . 8
8659adantr 452 . . . . . . . 8
8720adantr 452 . . . . . . . 8
8843adantr 452 . . . . . . . . 9
89 simpr 448 . . . . . . . . 9
9061adantr 452 . . . . . . . . 9
9185, 88, 86, 89, 90lelttrd 9220 . . . . . . . 8
9284, 85, 86, 87, 91lttrd 9223 . . . . . . 7
9392adantr 452 . . . . . 6
9483, 93jca 519 . . . . 5
9594olcd 383 . . . 4
9678, 79, 80, 81, 82, 95pmltpclem1 19337 . . 3
971ad2antrr 707 . . . 4
9840ad2antrr 707 . . . 4
995ad2antrr 707 . . . 4
10069ad2antrr 707 . . . 4
10115ad2antrr 707 . . . . . . 7
10292adantr 452 . . . . . . 7
103101, 102gtned 9200 . . . . . 6
104 fveq2 5720 . . . . . . . 8
105104eqcomd 2440 . . . . . . 7
106105necon3i 2637 . . . . . 6
107103, 106syl 16 . . . . 5
10866ad2antrr 707 . . . . . 6
10928ad2antrr 707 . . . . . 6
110 simpr 448 . . . . . 6
111108, 109, 110leltned 9216 . . . . 5
112107, 111mpbird 224 . . . 4
11361ad2antrr 707 . . . . . 6
114113, 102jca 519 . . . . 5
115114orcd 382 . . . 4
11697, 98, 99, 100, 112, 115pmltpclem1 19337 . . 3