Step | Hyp | Ref
| Expression |
1 | | ltexnqi 6507 |
. . . . . 6
|
2 | 1 | adantl 262 |
. . . . 5
|
3 | | ltrelpr 6603 |
. . . . . . . . . 10
|
4 | 3 | brel 4392 |
. . . . . . . . 9
|
5 | 4 | simpld 105 |
. . . . . . . 8
|
6 | | prop 6573 |
. . . . . . . . 9
|
7 | | prarloc 6601 |
. . . . . . . . 9
|
8 | 6, 7 | sylan 267 |
. . . . . . . 8
|
9 | 5, 8 | sylan 267 |
. . . . . . 7
|
10 | 9 | ad2ant2r 478 |
. . . . . 6
|
11 | 4 | simprd 107 |
. . . . . . . . . . . . . 14
|
12 | 11 | ad2antrr 457 |
. . . . . . . . . . . . 13
|
13 | 12 | ad2antrr 457 |
. . . . . . . . . . . 12
|
14 | | ltanqg 6498 |
. . . . . . . . . . . . . . . 16
|
15 | 14 | adantl 262 |
. . . . . . . . . . . . . . 15
|
16 | | elprnqu 6580 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 6, 16 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
|
18 | 5, 17 | sylan 267 |
. . . . . . . . . . . . . . . . 17
|
19 | 18 | adantlr 446 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | ad2ant2rl 480 |
. . . . . . . . . . . . . . 15
|
21 | | elprnql 6579 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 6, 21 | sylan 267 |
. . . . . . . . . . . . . . . . . . 19
|
23 | 5, 22 | sylan 267 |
. . . . . . . . . . . . . . . . . 18
|
24 | 23 | adantlr 446 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | ad2ant2r 478 |
. . . . . . . . . . . . . . . 16
|
26 | | simplrl 487 |
. . . . . . . . . . . . . . . 16
|
27 | | addclnq 6473 |
. . . . . . . . . . . . . . . 16
|
28 | 25, 26, 27 | syl2anc 391 |
. . . . . . . . . . . . . . 15
|
29 | | ltrelnq 6463 |
. . . . . . . . . . . . . . . . . . 19
|
30 | 29 | brel 4392 |
. . . . . . . . . . . . . . . . . 18
|
31 | 30 | simpld 105 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | adantl 262 |
. . . . . . . . . . . . . . . 16
|
33 | 32 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
|
34 | | addcomnqg 6479 |
. . . . . . . . . . . . . . . 16
|
35 | 34 | adantl 262 |
. . . . . . . . . . . . . . 15
|
36 | 15, 20, 28, 33, 35 | caovord2d 5670 |
. . . . . . . . . . . . . 14
|
37 | | addassnqg 6480 |
. . . . . . . . . . . . . . . . 17
|
38 | 25, 26, 33, 37 | syl3anc 1135 |
. . . . . . . . . . . . . . . 16
|
39 | | addcomnqg 6479 |
. . . . . . . . . . . . . . . . . 18
|
40 | 26, 33, 39 | syl2anc 391 |
. . . . . . . . . . . . . . . . 17
|
41 | 40 | oveq2d 5528 |
. . . . . . . . . . . . . . . 16
|
42 | | simplrr 488 |
. . . . . . . . . . . . . . . . 17
|
43 | 42 | oveq2d 5528 |
. . . . . . . . . . . . . . . 16
|
44 | 38, 41, 43 | 3eqtrd 2076 |
. . . . . . . . . . . . . . 15
|
45 | 44 | breq2d 3776 |
. . . . . . . . . . . . . 14
|
46 | 36, 45 | bitrd 177 |
. . . . . . . . . . . . 13
|
47 | 46 | biimpa 280 |
. . . . . . . . . . . 12
|
48 | | prop 6573 |
. . . . . . . . . . . . 13
|
49 | | prloc 6589 |
. . . . . . . . . . . . 13
|
50 | 48, 49 | sylan 267 |
. . . . . . . . . . . 12
|
51 | 13, 47, 50 | syl2anc 391 |
. . . . . . . . . . 11
|
52 | 51 | ex 108 |
. . . . . . . . . 10
|
53 | 52 | anassrs 380 |
. . . . . . . . 9
|
54 | 53 | reximdva 2421 |
. . . . . . . 8
|
55 | 54 | reximdva 2421 |
. . . . . . 7
|
56 | | prml 6575 |
. . . . . . . . . . . 12
|
57 | | rexex 2368 |
. . . . . . . . . . . 12
|
58 | 6, 56, 57 | 3syl 17 |
. . . . . . . . . . 11
|
59 | | r19.45mv 3315 |
. . . . . . . . . . 11
|
60 | 5, 58, 59 | 3syl 17 |
. . . . . . . . . 10
|
61 | 60 | adantr 261 |
. . . . . . . . 9
|
62 | | prmu 6576 |
. . . . . . . . . . . . 13
|
63 | | rexex 2368 |
. . . . . . . . . . . . 13
|
64 | 6, 62, 63 | 3syl 17 |
. . . . . . . . . . . 12
|
65 | | r19.9rmv 3313 |
. . . . . . . . . . . . . 14
|
66 | 65 | orbi2d 704 |
. . . . . . . . . . . . 13
|
67 | | r19.43 2468 |
. . . . . . . . . . . . 13
|
68 | 66, 67 | syl6rbbr 188 |
. . . . . . . . . . . 12
|
69 | 5, 64, 68 | 3syl 17 |
. . . . . . . . . . 11
|
70 | 69 | rexbidv 2327 |
. . . . . . . . . 10
|
71 | 70 | adantr 261 |
. . . . . . . . 9
|
72 | | ibar 285 |
. . . . . . . . . . . . . . 15
|
73 | 72 | adantr 261 |
. . . . . . . . . . . . . 14
|
74 | | ibar 285 |
. . . . . . . . . . . . . . 15
|
75 | 74 | adantl 262 |
. . . . . . . . . . . . . 14
|
76 | 73, 75 | orbi12d 707 |
. . . . . . . . . . . . 13
|
77 | 30, 76 | syl 14 |
. . . . . . . . . . . 12
|
78 | | ltexprlem.1 |
. . . . . . . . . . . . . 14
|
79 | 78 | ltexprlemell 6696 |
. . . . . . . . . . . . 13
|
80 | 78 | ltexprlemelu 6697 |
. . . . . . . . . . . . . 14
|
81 | | eleq1 2100 |
. . . . . . . . . . . . . . . . 17
|
82 | | oveq1 5519 |
. . . . . . . . . . . . . . . . . 18
|
83 | 82 | eleq1d 2106 |
. . . . . . . . . . . . . . . . 17
|
84 | 81, 83 | anbi12d 442 |
. . . . . . . . . . . . . . . 16
|
85 | 84 | cbvexv 1795 |
. . . . . . . . . . . . . . 15
|
86 | 85 | anbi2i 430 |
. . . . . . . . . . . . . 14
|
87 | 80, 86 | bitri 173 |
. . . . . . . . . . . . 13
|
88 | 79, 87 | orbi12i 681 |
. . . . . . . . . . . 12
|
89 | 77, 88 | syl6rbbr 188 |
. . . . . . . . . . 11
|
90 | | df-rex 2312 |
. . . . . . . . . . . 12
|
91 | | df-rex 2312 |
. . . . . . . . . . . 12
|
92 | 90, 91 | orbi12i 681 |
. . . . . . . . . . 11
|
93 | 89, 92 | syl6bbr 187 |
. . . . . . . . . 10
|
94 | 93 | adantl 262 |
. . . . . . . . 9
|
95 | 61, 71, 94 | 3bitr4rd 210 |
. . . . . . . 8
|
96 | 95 | adantr 261 |
. . . . . . 7
|
97 | 55, 96 | sylibrd 158 |
. . . . . 6
|
98 | 10, 97 | mpd 13 |
. . . . 5
|
99 | 2, 98 | rexlimddv 2437 |
. . . 4
|
100 | 99 | ex 108 |
. . 3
|
101 | 100 | ralrimivw 2393 |
. 2
|
102 | 101 | ralrimivw 2393 |
1
|