Step | Hyp | Ref
| Expression |
1 | | prarloclemarch 6608 |
. . 3
|
2 | 1 | 3adant2 957 |
. 2
|
3 | | pinn 6499 |
. . . . . . . 8
|
4 | | 1pi 6505 |
. . . . . . . . . . . 12
|
5 | 4 | elexi 2611 |
. . . . . . . . . . 11
|
6 | 5 | sucid 4172 |
. . . . . . . . . 10
|
7 | | df-2o 6025 |
. . . . . . . . . 10
|
8 | 6, 7 | eleqtrri 2154 |
. . . . . . . . 9
|
9 | | 2onn 6117 |
. . . . . . . . . . 11
|
10 | | nnaword2 6110 |
. . . . . . . . . . 11
|
11 | 9, 10 | mpan 414 |
. . . . . . . . . 10
|
12 | 11 | sseld 2998 |
. . . . . . . . 9
|
13 | 8, 12 | mpi 15 |
. . . . . . . 8
|
14 | 3, 13 | syl 14 |
. . . . . . 7
|
15 | | o1p1e2 6071 |
. . . . . . . . 9
|
16 | | addpiord 6506 |
. . . . . . . . . . 11
|
17 | 4, 4, 16 | mp2an 416 |
. . . . . . . . . 10
|
18 | | addclpi 6517 |
. . . . . . . . . . 11
|
19 | 4, 4, 18 | mp2an 416 |
. . . . . . . . . 10
|
20 | 17, 19 | eqeltrri 2152 |
. . . . . . . . 9
|
21 | 15, 20 | eqeltrri 2152 |
. . . . . . . 8
|
22 | | addpiord 6506 |
. . . . . . . 8
|
23 | 21, 22 | mpan2 415 |
. . . . . . 7
|
24 | 14, 23 | eleqtrrd 2158 |
. . . . . 6
|
25 | | addclpi 6517 |
. . . . . . . 8
|
26 | 21, 25 | mpan2 415 |
. . . . . . 7
|
27 | | ltpiord 6509 |
. . . . . . . 8
|
28 | 4, 27 | mpan 414 |
. . . . . . 7
|
29 | 26, 28 | syl 14 |
. . . . . 6
|
30 | 24, 29 | mpbird 165 |
. . . . 5
|
31 | 30 | adantl 271 |
. . . 4
|
32 | 31 | adantrr 462 |
. . 3
|
33 | | nna0 6076 |
. . . . . . . . . . . . . . . . 17
|
34 | | 0lt1o 6046 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | | 1on 6031 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | 35 | onsuci 4260 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | | ontr1 4144 |
. . . . . . . . . . . . . . . . . . . . 21
|
38 | 36, 37 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 34, 6, 38 | mp2an 416 |
. . . . . . . . . . . . . . . . . . 19
|
40 | 39, 7 | eleqtrri 2154 |
. . . . . . . . . . . . . . . . . 18
|
41 | | nnaordi 6104 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 9, 41 | mpan 414 |
. . . . . . . . . . . . . . . . . 18
|
43 | 40, 42 | mpi 15 |
. . . . . . . . . . . . . . . . 17
|
44 | 33, 43 | eqeltrrd 2156 |
. . . . . . . . . . . . . . . 16
|
45 | 3, 44 | syl 14 |
. . . . . . . . . . . . . . 15
|
46 | 45, 23 | eleqtrrd 2158 |
. . . . . . . . . . . . . 14
|
47 | | ltpiord 6509 |
. . . . . . . . . . . . . . 15
|
48 | 26, 47 | mpdan 412 |
. . . . . . . . . . . . . 14
|
49 | 46, 48 | mpbird 165 |
. . . . . . . . . . . . 13
|
50 | | mulidpi 6508 |
. . . . . . . . . . . . 13
|
51 | | mulcompig 6521 |
. . . . . . . . . . . . . . . 16
|
52 | 4, 51 | mpan2 415 |
. . . . . . . . . . . . . . 15
|
53 | 26, 52 | syl 14 |
. . . . . . . . . . . . . 14
|
54 | | mulidpi 6508 |
. . . . . . . . . . . . . . 15
|
55 | 26, 54 | syl 14 |
. . . . . . . . . . . . . 14
|
56 | 53, 55 | eqtr3d 2115 |
. . . . . . . . . . . . 13
|
57 | 49, 50, 56 | 3brtr4d 3815 |
. . . . . . . . . . . 12
|
58 | | ordpipqqs 6564 |
. . . . . . . . . . . . . . 15
|
59 | 4, 58 | mpanl2 425 |
. . . . . . . . . . . . . 14
|
60 | 4, 59 | mpanr2 428 |
. . . . . . . . . . . . 13
|
61 | 26, 60 | mpdan 412 |
. . . . . . . . . . . 12
|
62 | 57, 61 | mpbird 165 |
. . . . . . . . . . 11
|
63 | 62 | adantl 271 |
. . . . . . . . . 10
|
64 | | opelxpi 4394 |
. . . . . . . . . . . . . . . 16
|
65 | 4, 64 | mpan2 415 |
. . . . . . . . . . . . . . 15
|
66 | | enqex 6550 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | ecelqsi 6183 |
. . . . . . . . . . . . . . 15
|
68 | 26, 65, 67 | 3syl 17 |
. . . . . . . . . . . . . 14
|
69 | | df-nqqs 6538 |
. . . . . . . . . . . . . 14
|
70 | 68, 69 | syl6eleqr 2172 |
. . . . . . . . . . . . 13
|
71 | | opelxpi 4394 |
. . . . . . . . . . . . . . . . 17
|
72 | 4, 71 | mpan2 415 |
. . . . . . . . . . . . . . . 16
|
73 | 66 | ecelqsi 6183 |
. . . . . . . . . . . . . . . 16
|
74 | 72, 73 | syl 14 |
. . . . . . . . . . . . . . 15
|
75 | 74, 69 | syl6eleqr 2172 |
. . . . . . . . . . . . . 14
|
76 | | ltmnqg 6591 |
. . . . . . . . . . . . . 14
|
77 | 75, 76 | syl3an1 1202 |
. . . . . . . . . . . . 13
|
78 | 70, 77 | syl3an2 1203 |
. . . . . . . . . . . 12
|
79 | 78 | 3anidm12 1226 |
. . . . . . . . . . 11
|
80 | 79 | ancoms 264 |
. . . . . . . . . 10
|
81 | 63, 80 | mpbid 145 |
. . . . . . . . 9
|
82 | | mulcomnqg 6573 |
. . . . . . . . . 10
|
83 | 75, 82 | sylan2 280 |
. . . . . . . . 9
|
84 | | mulcomnqg 6573 |
. . . . . . . . . 10
|
85 | 70, 84 | sylan2 280 |
. . . . . . . . 9
|
86 | 81, 83, 85 | 3brtr3d 3814 |
. . . . . . . 8
|
87 | 86 | 3ad2antl3 1102 |
. . . . . . 7
|
88 | 87 | adantrr 462 |
. . . . . 6
|
89 | | ltsonq 6588 |
. . . . . . . . . 10
|
90 | | ltrelnq 6555 |
. . . . . . . . . 10
|
91 | 89, 90 | sotri 4740 |
. . . . . . . . 9
|
92 | 91 | ex 113 |
. . . . . . . 8
|
93 | 92 | adantl 271 |
. . . . . . 7
|
94 | 93 | adantl 271 |
. . . . . 6
|
95 | 88, 94 | mpd 13 |
. . . . 5
|
96 | | mulclnq 6566 |
. . . . . . . . . 10
|
97 | 70, 96 | sylan 277 |
. . . . . . . . 9
|
98 | 97 | ancoms 264 |
. . . . . . . 8
|
99 | 98 | 3ad2antl3 1102 |
. . . . . . 7
|
100 | | simpl2 942 |
. . . . . . 7
|
101 | | ltaddnq 6597 |
. . . . . . 7
|
102 | 99, 100, 101 | syl2anc 403 |
. . . . . 6
|
103 | 102 | adantrr 462 |
. . . . 5
|
104 | 89, 90 | sotri 4740 |
. . . . 5
|
105 | 95, 103, 104 | syl2anc 403 |
. . . 4
|
106 | | addcomnqg 6571 |
. . . . . . 7
|
107 | 99, 100, 106 | syl2anc 403 |
. . . . . 6
|
108 | 107 | breq2d 3797 |
. . . . 5
|
109 | 108 | adantrr 462 |
. . . 4
|
110 | 105, 109 | mpbid 145 |
. . 3
|
111 | | simpr 108 |
. . . . 5
|
112 | | breq2 3789 |
. . . . . . . 8
|
113 | | opeq1 3570 |
. . . . . . . . . . . 12
|
114 | 113 | eceq1d 6165 |
. . . . . . . . . . 11
|
115 | 114 | oveq1d 5547 |
. . . . . . . . . 10
|
116 | 115 | oveq2d 5548 |
. . . . . . . . 9
|
117 | 116 | breq2d 3797 |
. . . . . . . 8
|
118 | 112, 117 | anbi12d 456 |
. . . . . . 7
|
119 | 118 | rspcev 2701 |
. . . . . 6
|
120 | 119 | ex 113 |
. . . . 5
|
121 | 111, 26, 120 | 3syl 17 |
. . . 4
|
122 | 121 | adantrr 462 |
. . 3
|
123 | 32, 110, 122 | mp2and 423 |
. 2
|
124 | 2, 123 | rexlimddv 2481 |
1
|