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

Theorem pmltpclem2 18809
 Description: Lemma for pmltpc 18810. (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 706 . . . 4
3 pmltpc.3 . . . . 5
43ad2antrr 706 . . . 4
5 pmltpc.4 . . . . 5
65ad2antrr 706 . . . 4
7 simpr 447 . . . 4
8 pmltpc.1 . . . . . . . . . . 11
9 reex 8828 . . . . . . . . . . . 12
109, 9elpm2 6799 . . . . . . . . . . 11
118, 10sylib 188 . . . . . . . . . 10
1211simpld 445 . . . . . . . . 9
13 pmltpc.2 . . . . . . . . . 10
1413, 5sseldd 3181 . . . . . . . . 9
15 ffvelrn 5663 . . . . . . . . 9
1612, 14, 15syl2anc 642 . . . . . . . 8
17 pmltpc.9 . . . . . . . . 9
1813, 3sseldd 3181 . . . . . . . . . . 11
19 ffvelrn 5663 . . . . . . . . . . 11
2012, 18, 19syl2anc 642 . . . . . . . . . 10
2116, 20ltnled 8966 . . . . . . . . 9
2217, 21mpbird 223 . . . . . . . 8
2316, 22gtned 8954 . . . . . . 7
24 fveq2 5525 . . . . . . . . 9
2524eqcomd 2288 . . . . . . . 8
2625necon3i 2485 . . . . . . 7
2723, 26syl 15 . . . . . 6
2811simprd 449 . . . . . . . 8
2928, 18sseldd 3181 . . . . . . 7
3028, 14sseldd 3181 . . . . . . 7
31 pmltpc.7 . . . . . . 7
3229, 30, 31leltned 8970 . . . . . 6
3327, 32mpbird 223 . . . . 5
3433ad2antrr 706 . . . 4
35 simplr 731 . . . . . 6
3622ad2antrr 706 . . . . . 6
3735, 36jca 518 . . . . 5
3837orcd 381 . . . 4
392, 4, 6, 7, 34, 38pmltpclem1 18808 . . 3
403ad2antrr 706 . . . 4
411ad2antrr 706 . . . 4
42 pmltpc.6 . . . . 5
4342ad2antrr 706 . . . 4
4413, 1sseldd 3181 . . . . . . . . 9
45 ffvelrn 5663 . . . . . . . . 9
4612, 44, 45syl2anc 642 . . . . . . . 8
4746ad2antrr 706 . . . . . . 7
48 simplr 731 . . . . . . 7
4947, 48gtned 8954 . . . . . 6
50 fveq2 5525 . . . . . . . 8
5150eqcomd 2288 . . . . . . 7
5251necon3i 2485 . . . . . 6
5349, 52syl 15 . . . . 5
5429ad2antrr 706 . . . . . 6
5528, 44sseldd 3181 . . . . . . 7
5655ad2antrr 706 . . . . . 6
57 simpr 447 . . . . . 6
5854, 56, 57leltned 8970 . . . . 5
5953, 58mpbird 223 . . . 4
60 pmltpc.10 . . . . . . . . 9
6113, 42sseldd 3181 . . . . . . . . . . 11
62 ffvelrn 5663 . . . . . . . . . . 11
6312, 61, 62syl2anc 642 . . . . . . . . . 10
6446, 63ltnled 8966 . . . . . . . . 9
6560, 64mpbird 223 . . . . . . . 8
6646, 65gtned 8954 . . . . . . 7
67 fveq2 5525 . . . . . . . 8
6867necon3i 2485 . . . . . . 7
6966, 68syl 15 . . . . . 6
7028, 61sseldd 3181 . . . . . . 7
71 pmltpc.8 . . . . . . 7
7255, 70, 71leltned 8970 . . . . . 6
7369, 72mpbird 223 . . . . 5
7473ad2antrr 706 . . . 4
7565ad2antrr 706 . . . . . 6
7648, 75jca 518 . . . . 5
7776olcd 382 . . . 4
7840, 41, 43, 59, 74, 77pmltpclem1 18808 . . 3
8139, 78, 79, 80ltlecasei 8928 . 2
823ad2antrr 706 . . . 4
835ad2antrr 706 . . . 4
8442ad2antrr 706 . . . 4
8533ad2antrr 706 . . . 4
86 simpr 447 . . . 4
8722ad2antrr 706 . . . . . 6
8816adantr 451 . . . . . . . 8
8920adantr 451 . . . . . . . 8
9063adantr 451 . . . . . . . 8
9122adantr 451 . . . . . . . 8
9246adantr 451 . . . . . . . . 9
93 simpr 447 . . . . . . . . 9
9465adantr 451 . . . . . . . . 9
9589, 92, 90, 93, 94lelttrd 8974 . . . . . . . 8
9688, 89, 90, 91, 95lttrd 8977 . . . . . . 7
9796adantr 451 . . . . . 6
9887, 97jca 518 . . . . 5
9998olcd 382 . . . 4
10082, 83, 84, 85, 86, 99pmltpclem1 18808 . . 3
1011ad2antrr 706 . . . 4
10242ad2antrr 706 . . . 4
1035ad2antrr 706 . . . 4
10473ad2antrr 706 . . . 4
10516ad2antrr 706 . . . . . . 7
10696adantr 451 . . . . . . 7
107105, 106gtned 8954 . . . . . 6
108 fveq2 5525 . . . . . . . 8
109108eqcomd 2288 . . . . . . 7
110109necon3i 2485 . . . . . 6
111107, 110syl 15 . . . . 5
11270ad2antrr 706 . . . . . 6
11330ad2antrr 706 . . . . . 6
114 simpr 447 . . . . . 6
115112, 113, 114leltned 8970 . . . . 5
116111, 115mpbird 223 . . . 4
11765ad2antrr 706 . . . . . 6
118117, 106jca 518 . . . . 5
119118orcd 381 . . . 4
120101, 102, 103, 104, 116, 119pmltpclem1 18808 . . 3