Step | Hyp | Ref
| Expression |
1 | | simpr 477 |
. . 3
|
2 | | simpl1 1064 |
. . . . 5
|
3 | | simpl3 1066 |
. . . . 5
|
4 | | llncvrlpln2.n |
. . . . . 6
|
5 | | llncvrlpln2.p |
. . . . . 6
|
6 | 4, 5 | lplnnelln 34832 |
. . . . 5
|
7 | 2, 3, 6 | syl2anc 693 |
. . . 4
|
8 | | simpl2 1065 |
. . . . . 6
|
9 | | eleq1 2689 |
. . . . . 6
|
10 | 8, 9 | syl5ibcom 235 |
. . . . 5
|
11 | 10 | necon3bd 2808 |
. . . 4
|
12 | 7, 11 | mpd 15 |
. . 3
|
13 | | llncvrlpln2.l |
. . . . 5
|
14 | | eqid 2622 |
. . . . 5
|
15 | 13, 14 | pltval 16960 |
. . . 4
|
16 | 15 | adantr 481 |
. . 3
|
17 | 1, 12, 16 | mpbir2and 957 |
. 2
|
18 | | simpl1 1064 |
. . . 4
|
19 | | simpl2 1065 |
. . . . 5
|
20 | | eqid 2622 |
. . . . . 6
|
21 | 20, 4 | llnbase 34795 |
. . . . 5
|
22 | 19, 21 | syl 17 |
. . . 4
|
23 | | simpl3 1066 |
. . . . 5
|
24 | 20, 5 | lplnbase 34820 |
. . . . 5
|
25 | 23, 24 | syl 17 |
. . . 4
|
26 | | simpr 477 |
. . . 4
|
27 | | eqid 2622 |
. . . . 5
|
28 | | llncvrlpln2.c |
. . . . 5
|
29 | | eqid 2622 |
. . . . 5
|
30 | 20, 13, 14, 27, 28, 29 | hlrelat3 34698 |
. . . 4
|
31 | 18, 22, 25, 26, 30 | syl31anc 1329 |
. . 3
|
32 | 20, 13, 27, 29, 5 | islpln2 34822 |
. . . . . . . 8
|
33 | 32 | adantr 481 |
. . . . . . 7
|
34 | | simp3 1063 |
. . . . . . . . . . 11
|
35 | 20, 27, 29, 4 | islln2 34797 |
. . . . . . . . . . . . 13
|
36 | | simp3l 1089 |
. . . . . . . . . . . . . . . . . . . 20
|
37 | | simp3r 1090 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
38 | | simp12r 1175 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | 38 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | | simp22 1095 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | 37, 39, 40 | 3brtr3d 4684 |
. . . . . . . . . . . . . . . . . . . . . 22
|
42 | | simp111 1190 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
43 | | simp112 1191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | | simp113 1192 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
45 | | simp23 1096 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
46 | 43, 44, 45 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
47 | | simp13l 1176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
48 | | simp13r 1177 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
49 | | simp21 1094 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
50 | 47, 48, 49 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | 36, 38, 39 | 3brtr3d 4684 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
52 | 20, 27, 29 | hlatjcl 34653 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
53 | 42, 43, 44, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
54 | 20, 13, 27, 28, 29 | cvr1 34696 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
55 | 42, 53, 45, 54 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
56 | 51, 55 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
57 | | simp12l 1174 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
58 | 13, 27, 29 | 3at 34776 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
59 | 42, 46, 50, 56, 57, 58 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . . . 22
|
60 | 41, 59 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
|
61 | 60, 39, 40 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 36, 61 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | 3exp 1264 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | 3expd 1284 |
. . . . . . . . . . . . . . . . 17
|
65 | 64 | 3exp 1264 |
. . . . . . . . . . . . . . . 16
|
66 | 65 | 3expib 1268 |
. . . . . . . . . . . . . . 15
|
67 | 66 | rexlimdvv 3037 |
. . . . . . . . . . . . . 14
|
68 | 67 | adantld 483 |
. . . . . . . . . . . . 13
|
69 | 35, 68 | sylbid 230 |
. . . . . . . . . . . 12
|
70 | 69 | imp31 448 |
. . . . . . . . . . 11
|
71 | 34, 70 | syl7 74 |
. . . . . . . . . 10
|
72 | 71 | rexlimdv 3030 |
. . . . . . . . 9
|
73 | 72 | rexlimdvva 3038 |
. . . . . . . 8
|
74 | 73 | adantld 483 |
. . . . . . 7
|
75 | 33, 74 | sylbid 230 |
. . . . . 6
|
76 | 75 | 3impia 1261 |
. . . . 5
|
77 | 76 | rexlimdv 3030 |
. . . 4
|
78 | 77 | imp 445 |
. . 3
|
79 | 31, 78 | syldan 487 |
. 2
|
80 | 17, 79 | syldan 487 |
1
|