Step | Hyp | Ref
| Expression |
1 | | ltrelsr 7700 |
. . . . . . 7
|
2 | 1 | brel 4663 |
. . . . . 6
|
3 | 2 | simprd 113 |
. . . . 5
|
4 | 3 | anim2i 340 |
. . . 4
|
5 | | simpr 109 |
. . . 4
|
6 | | m1r 7714 |
. . . . . . . 8
|
7 | 6 | a1i 9 |
. . . . . . 7
|
8 | | simpl 108 |
. . . . . . . . 9
|
9 | | mulclsr 7716 |
. . . . . . . . 9
|
10 | 8, 7, 9 | syl2anc 409 |
. . . . . . . 8
|
11 | | simpr 109 |
. . . . . . . 8
|
12 | | addclsr 7715 |
. . . . . . . 8
|
13 | 10, 11, 12 | syl2anc 409 |
. . . . . . 7
|
14 | | ltasrg 7732 |
. . . . . . 7
|
15 | 7, 13, 8, 14 | syl3anc 1233 |
. . . . . 6
|
16 | | pn0sr 7733 |
. . . . . . . . . . 11
|
17 | 16 | oveq1d 5868 |
. . . . . . . . . 10
|
18 | 17 | adantr 274 |
. . . . . . . . 9
|
19 | | addasssrg 7718 |
. . . . . . . . . 10
|
20 | 8, 10, 11, 19 | syl3anc 1233 |
. . . . . . . . 9
|
21 | | 0r 7712 |
. . . . . . . . . . 11
|
22 | 21 | a1i 9 |
. . . . . . . . . 10
|
23 | | addcomsrg 7717 |
. . . . . . . . . 10
|
24 | 22, 11, 23 | syl2anc 409 |
. . . . . . . . 9
|
25 | 18, 20, 24 | 3eqtr3d 2211 |
. . . . . . . 8
|
26 | | 0idsr 7729 |
. . . . . . . . 9
|
27 | 26 | adantl 275 |
. . . . . . . 8
|
28 | 25, 27 | eqtrd 2203 |
. . . . . . 7
|
29 | 28 | breq2d 4001 |
. . . . . 6
|
30 | 15, 29 | bitrd 187 |
. . . . 5
|
31 | 6, 9 | mpan2 423 |
. . . . . . . 8
|
32 | 31, 12 | sylan 281 |
. . . . . . 7
|
33 | | df-nr 7689 |
. . . . . . . 8
|
34 | | breq2 3993 |
. . . . . . . . 9
|
35 | | eqeq2 2180 |
. . . . . . . . . 10
|
36 | 35 | rexbidv 2471 |
. . . . . . . . 9
|
37 | 34, 36 | imbi12d 233 |
. . . . . . . 8
|
38 | | df-m1r 7695 |
. . . . . . . . . . . 12
|
39 | 38 | breq1i 3996 |
. . . . . . . . . . 11
|
40 | | 1pr 7516 |
. . . . . . . . . . . . . . 15
|
41 | | addassprg 7541 |
. . . . . . . . . . . . . . 15
|
42 | 40, 40, 41 | mp3an12 1322 |
. . . . . . . . . . . . . 14
|
43 | 42 | breq2d 4001 |
. . . . . . . . . . . . 13
|
44 | 43 | adantr 274 |
. . . . . . . . . . . 12
|
45 | | addclpr 7499 |
. . . . . . . . . . . . . 14
|
46 | 40, 40, 45 | mp2an 424 |
. . . . . . . . . . . . 13
|
47 | | ltsrprg 7709 |
. . . . . . . . . . . . 13
|
48 | 40, 46, 47 | mpanl12 434 |
. . . . . . . . . . . 12
|
49 | | simpr 109 |
. . . . . . . . . . . . 13
|
50 | 40 | a1i 9 |
. . . . . . . . . . . . . 14
|
51 | | simpl 108 |
. . . . . . . . . . . . . 14
|
52 | | addclpr 7499 |
. . . . . . . . . . . . . 14
|
53 | 50, 51, 52 | syl2anc 409 |
. . . . . . . . . . . . 13
|
54 | | ltaprg 7581 |
. . . . . . . . . . . . 13
|
55 | 49, 53, 50, 54 | syl3anc 1233 |
. . . . . . . . . . . 12
|
56 | 44, 48, 55 | 3bitr4d 219 |
. . . . . . . . . . 11
|
57 | 39, 56 | syl5bb 191 |
. . . . . . . . . 10
|
58 | | ltexpri 7575 |
. . . . . . . . . 10
|
59 | 57, 58 | syl6bi 162 |
. . . . . . . . 9
|
60 | | enreceq 7698 |
. . . . . . . . . . . . 13
|
61 | 40, 60 | mpanl2 433 |
. . . . . . . . . . . 12
|
62 | 49 | adantl 275 |
. . . . . . . . . . . . . 14
|
63 | | simpl 108 |
. . . . . . . . . . . . . 14
|
64 | | addcomprg 7540 |
. . . . . . . . . . . . . 14
|
65 | 62, 63, 64 | syl2anc 409 |
. . . . . . . . . . . . 13
|
66 | 65 | eqeq1d 2179 |
. . . . . . . . . . . 12
|
67 | 61, 66 | bitr4d 190 |
. . . . . . . . . . 11
|
68 | 67 | ancoms 266 |
. . . . . . . . . 10
|
69 | 68 | rexbidva 2467 |
. . . . . . . . 9
|
70 | 59, 69 | sylibrd 168 |
. . . . . . . 8
|
71 | 33, 37, 70 | ecoptocl 6600 |
. . . . . . 7
|
72 | 32, 71 | syl 14 |
. . . . . 6
|
73 | | oveq2 5861 |
. . . . . . . . 9
|
74 | 73, 28 | sylan9eqr 2225 |
. . . . . . . 8
|
75 | 74 | ex 114 |
. . . . . . 7
|
76 | 75 | reximdv 2571 |
. . . . . 6
|
77 | 72, 76 | syld 45 |
. . . . 5
|
78 | 30, 77 | sylbird 169 |
. . . 4
|
79 | 4, 5, 78 | sylc 62 |
. . 3
|
80 | 79 | ex 114 |
. 2
|
81 | | mappsrprg 7766 |
. . . . 5
|
82 | | breq2 3993 |
. . . . 5
|
83 | 81, 82 | syl5ibcom 154 |
. . . 4
|
84 | 83 | ancoms 266 |
. . 3
|
85 | 84 | rexlimdva 2587 |
. 2
|
86 | 80, 85 | impbid 128 |
1
|