Proof of Theorem prarloclemlt
Step | Hyp | Ref
| Expression |
1 | | 2onn 6117 |
. . . . . . . . . . . 12
|
2 | | nnacl 6082 |
. . . . . . . . . . . 12
|
3 | 1, 2 | mpan2 415 |
. . . . . . . . . . 11
|
4 | | nnaword1 6109 |
. . . . . . . . . . 11
|
5 | 3, 4 | sylan 277 |
. . . . . . . . . 10
|
6 | | 1onn 6116 |
. . . . . . . . . . . . . . 15
|
7 | 6 | elexi 2611 |
. . . . . . . . . . . . . 14
|
8 | 7 | sucid 4172 |
. . . . . . . . . . . . 13
|
9 | | df-2o 6025 |
. . . . . . . . . . . . 13
|
10 | 8, 9 | eleqtrri 2154 |
. . . . . . . . . . . 12
|
11 | | nnaordi 6104 |
. . . . . . . . . . . . 13
|
12 | 1, 11 | mpan 414 |
. . . . . . . . . . . 12
|
13 | 10, 12 | mpi 15 |
. . . . . . . . . . 11
|
14 | 13 | adantr 270 |
. . . . . . . . . 10
|
15 | 5, 14 | sseldd 3000 |
. . . . . . . . 9
|
16 | 15 | ancoms 264 |
. . . . . . . 8
|
17 | | 1pi 6505 |
. . . . . . . . . . 11
|
18 | | nnppipi 6533 |
. . . . . . . . . . 11
|
19 | 17, 18 | mpan2 415 |
. . . . . . . . . 10
|
20 | 19 | adantl 271 |
. . . . . . . . 9
|
21 | | o1p1e2 6071 |
. . . . . . . . . . . . . 14
|
22 | | nnppipi 6533 |
. . . . . . . . . . . . . . 15
|
23 | 6, 17, 22 | mp2an 416 |
. . . . . . . . . . . . . 14
|
24 | 21, 23 | eqeltrri 2152 |
. . . . . . . . . . . . 13
|
25 | | nnppipi 6533 |
. . . . . . . . . . . . 13
|
26 | 24, 25 | mpan2 415 |
. . . . . . . . . . . 12
|
27 | | pinn 6499 |
. . . . . . . . . . . 12
|
28 | 26, 27 | syl 14 |
. . . . . . . . . . 11
|
29 | | nnacom 6086 |
. . . . . . . . . . 11
|
30 | 28, 29 | sylan2 280 |
. . . . . . . . . 10
|
31 | | nnppipi 6533 |
. . . . . . . . . . 11
|
32 | 26, 31 | sylan2 280 |
. . . . . . . . . 10
|
33 | 30, 32 | eqeltrrd 2156 |
. . . . . . . . 9
|
34 | | ltpiord 6509 |
. . . . . . . . 9
|
35 | 20, 33, 34 | syl2anc 403 |
. . . . . . . 8
|
36 | 16, 35 | mpbird 165 |
. . . . . . 7
|
37 | | mulidpi 6508 |
. . . . . . . . 9
|
38 | 20, 37 | syl 14 |
. . . . . . . 8
|
39 | | mulcompig 6521 |
. . . . . . . . . 10
|
40 | 33, 17, 39 | sylancl 404 |
. . . . . . . . 9
|
41 | | mulidpi 6508 |
. . . . . . . . . 10
|
42 | 33, 41 | syl 14 |
. . . . . . . . 9
|
43 | 40, 42 | eqtr3d 2115 |
. . . . . . . 8
|
44 | 38, 43 | breq12d 3798 |
. . . . . . 7
|
45 | 36, 44 | mpbird 165 |
. . . . . 6
|
46 | | simpr 108 |
. . . . . . 7
|
47 | | ordpipqqs 6564 |
. . . . . . . . . 10
|
48 | 17, 47 | mpanl2 425 |
. . . . . . . . 9
|
49 | 17, 48 | mpanr2 428 |
. . . . . . . 8
|
50 | 19, 49 | sylan 277 |
. . . . . . 7
|
51 | 46, 33, 50 | syl2anc 403 |
. . . . . 6
|
52 | 45, 51 | mpbird 165 |
. . . . 5
|
53 | 52 | adantlr 460 |
. . . 4
|
54 | | opelxpi 4394 |
. . . . . . . . 9
|
55 | 20, 17, 54 | sylancl 404 |
. . . . . . . 8
|
56 | | enqex 6550 |
. . . . . . . . 9
|
57 | 56 | ecelqsi 6183 |
. . . . . . . 8
|
58 | 55, 57 | syl 14 |
. . . . . . 7
|
59 | | df-nqqs 6538 |
. . . . . . 7
|
60 | 58, 59 | syl6eleqr 2172 |
. . . . . 6
|
61 | 60 | adantlr 460 |
. . . . 5
|
62 | | opelxpi 4394 |
. . . . . . . . 9
|
63 | 33, 17, 62 | sylancl 404 |
. . . . . . . 8
|
64 | 56 | ecelqsi 6183 |
. . . . . . . 8
|
65 | 63, 64 | syl 14 |
. . . . . . 7
|
66 | 65, 59 | syl6eleqr 2172 |
. . . . . 6
|
67 | 66 | adantlr 460 |
. . . . 5
|
68 | | simplr3 982 |
. . . . 5
|
69 | | ltmnqg 6591 |
. . . . 5
|
70 | 61, 67, 68, 69 | syl3anc 1169 |
. . . 4
|
71 | 53, 70 | mpbid 145 |
. . 3
|
72 | | mulcomnqg 6573 |
. . . . 5
|
73 | 68, 61, 72 | syl2anc 403 |
. . . 4
|
74 | | mulcomnqg 6573 |
. . . . 5
|
75 | 68, 67, 74 | syl2anc 403 |
. . . 4
|
76 | 73, 75 | breq12d 3798 |
. . 3
|
77 | 71, 76 | mpbid 145 |
. 2
|
78 | | mulclnq 6566 |
. . . 4
|
79 | 61, 68, 78 | syl2anc 403 |
. . 3
|
80 | | mulclnq 6566 |
. . . 4
|
81 | 67, 68, 80 | syl2anc 403 |
. . 3
|
82 | | simplr1 980 |
. . . 4
|
83 | | simplr2 981 |
. . . 4
|
84 | | elprnql 6671 |
. . . 4
|
85 | 82, 83, 84 | syl2anc 403 |
. . 3
|
86 | | ltanqg 6590 |
. . 3
|
87 | 79, 81, 85, 86 | syl3anc 1169 |
. 2
|
88 | 77, 87 | mpbid 145 |
1
|