Step | Hyp | Ref
| Expression |
1 | | r2al 2939 |
. . . . . . 7
|
2 | | simpl 473 |
. . . . . . . . . . 11
|
3 | 2 | anim1i 592 |
. . . . . . . . . 10
|
4 | 3 | imim1i 63 |
. . . . . . . . 9
|
5 | 4 | expd 452 |
. . . . . . . 8
|
6 | 5 | 2alimi 1740 |
. . . . . . 7
|
7 | 1, 6 | sylbi 207 |
. . . . . 6
|
8 | | r2al 2939 |
. . . . . 6
|
9 | 7, 8 | sylibr 224 |
. . . . 5
|
10 | | elequ1 1997 |
. . . . . . . . . . . 12
|
11 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
12 | 11 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
13 | 12 | notbid 308 |
. . . . . . . . . . . 12
|
14 | 10, 13 | imbi12d 334 |
. . . . . . . . . . 11
|
15 | 14 | cbvralv 3171 |
. . . . . . . . . 10
|
16 | 15 | ralbii 2980 |
. . . . . . . . 9
|
17 | | elequ2 2004 |
. . . . . . . . . . . 12
|
18 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
19 | 18 | eqeq1d 2624 |
. . . . . . . . . . . . 13
|
20 | 19 | notbid 308 |
. . . . . . . . . . . 12
|
21 | 17, 20 | imbi12d 334 |
. . . . . . . . . . 11
|
22 | 21 | ralbidv 2986 |
. . . . . . . . . 10
|
23 | 22 | cbvralv 3171 |
. . . . . . . . 9
|
24 | | elequ1 1997 |
. . . . . . . . . . . . 13
|
25 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
26 | 25 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
27 | 26 | notbid 308 |
. . . . . . . . . . . . 13
|
28 | 24, 27 | imbi12d 334 |
. . . . . . . . . . . 12
|
29 | 28 | cbvralv 3171 |
. . . . . . . . . . 11
|
30 | 29 | ralbii 2980 |
. . . . . . . . . 10
|
31 | | elequ2 2004 |
. . . . . . . . . . . . 13
|
32 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
33 | 32 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
34 | 33 | notbid 308 |
. . . . . . . . . . . . 13
|
35 | 31, 34 | imbi12d 334 |
. . . . . . . . . . . 12
|
36 | 35 | ralbidv 2986 |
. . . . . . . . . . 11
|
37 | 36 | cbvralv 3171 |
. . . . . . . . . 10
|
38 | 30, 37 | bitri 264 |
. . . . . . . . 9
|
39 | 16, 23, 38 | 3bitri 286 |
. . . . . . . 8
|
40 | | ralcom2 3104 |
. . . . . . . 8
|
41 | 39, 40 | sylbi 207 |
. . . . . . 7
|
42 | 41 | ancri 575 |
. . . . . 6
|
43 | | r19.26-2 3065 |
. . . . . 6
|
44 | 42, 43 | sylibr 224 |
. . . . 5
|
45 | 9, 44 | syl 17 |
. . . 4
|
46 | | fvres 6207 |
. . . . . . . . . . 11
|
47 | | fvres 6207 |
. . . . . . . . . . 11
|
48 | 46, 47 | eqeqan12d 2638 |
. . . . . . . . . 10
|
49 | 48 | ad2antrl 764 |
. . . . . . . . 9
|
50 | | ssel 3597 |
. . . . . . . . . . . 12
|
51 | | ssel 3597 |
. . . . . . . . . . . 12
|
52 | 50, 51 | anim12d 586 |
. . . . . . . . . . 11
|
53 | | pm3.48 878 |
. . . . . . . . . . . . . 14
|
54 | | oridm 536 |
. . . . . . . . . . . . . . 15
|
55 | | eqcom 2629 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | notbii 310 |
. . . . . . . . . . . . . . . 16
|
57 | 56 | orbi1i 542 |
. . . . . . . . . . . . . . 15
|
58 | 54, 57 | bitr3i 266 |
. . . . . . . . . . . . . 14
|
59 | 53, 58 | syl6ibr 242 |
. . . . . . . . . . . . 13
|
60 | 59 | con2d 129 |
. . . . . . . . . . . 12
|
61 | | eloni 5733 |
. . . . . . . . . . . . 13
|
62 | | eloni 5733 |
. . . . . . . . . . . . 13
|
63 | | ordtri3 5759 |
. . . . . . . . . . . . . 14
|
64 | 63 | biimprd 238 |
. . . . . . . . . . . . 13
|
65 | 61, 62, 64 | syl2an 494 |
. . . . . . . . . . . 12
|
66 | 60, 65 | syl9r 78 |
. . . . . . . . . . 11
|
67 | 52, 66 | syl6 35 |
. . . . . . . . . 10
|
68 | 67 | imp32 449 |
. . . . . . . . 9
|
69 | 49, 68 | sylbid 230 |
. . . . . . . 8
|
70 | 69 | exp32 631 |
. . . . . . 7
|
71 | 70 | a2d 29 |
. . . . . 6
|
72 | 71 | 2alimdv 1847 |
. . . . 5
|
73 | | r2al 2939 |
. . . . 5
|
74 | | r2al 2939 |
. . . . 5
|
75 | 72, 73, 74 | 3imtr4g 285 |
. . . 4
|
76 | 45, 75 | syl5 34 |
. . 3
|
77 | 76 | imdistani 726 |
. 2
|
78 | | tz7.48.1 |
. . . 4
|
79 | | fnssres 6004 |
. . . 4
|
80 | 78, 79 | mpan 706 |
. . 3
|
81 | | dffn2 6047 |
. . . 4
|
82 | | dff13 6512 |
. . . . . 6
|
83 | | df-f1 5893 |
. . . . . 6
|
84 | 82, 83 | bitr3i 266 |
. . . . 5
|
85 | 84 | simprbi 480 |
. . . 4
|
86 | 81, 85 | sylanb 489 |
. . 3
|
87 | 80, 86 | sylan 488 |
. 2
|
88 | 77, 87 | syl 17 |
1
|