Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . . . 12
|
2 | | rpssre 11843 |
. . . . . . . . . . . . 13
|
3 | 2 | a1i 11 |
. . . . . . . . . . . 12
|
4 | 1, 3 | fssd 6057 |
. . . . . . . . . . 11
|
5 | 4 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
6 | 5 | adantr 481 |
. . . . . . . . 9
|
7 | 6 | ffvelrnda 6359 |
. . . . . . . 8
|
8 | | simplrr 801 |
. . . . . . . 8
|
9 | | simpl2 1065 |
. . . . . . . . . 10
|
10 | 9 | ffvelrnda 6359 |
. . . . . . . . 9
|
11 | 10 | rpregt0d 11878 |
. . . . . . . 8
|
12 | 7, 8, 11 | 3jca 1242 |
. . . . . . 7
|
13 | | ledivmul2 10902 |
. . . . . . . 8
|
14 | 13 | bicomd 213 |
. . . . . . 7
|
15 | 12, 14 | syl 17 |
. . . . . 6
|
16 | | id 22 |
. . . . . . . . . . . . 13
|
17 | 2 | a1i 11 |
. . . . . . . . . . . . 13
|
18 | 16, 17 | fssd 6057 |
. . . . . . . . . . . 12
|
19 | 18 | 3ad2ant2 1083 |
. . . . . . . . . . 11
|
20 | | reex 10027 |
. . . . . . . . . . . . 13
|
21 | 20 | ssex 4802 |
. . . . . . . . . . . 12
|
22 | 21 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
23 | 5, 19, 22 | 3jca 1242 |
. . . . . . . . . 10
|
24 | 23 | adantr 481 |
. . . . . . . . 9
|
25 | 24 | adantr 481 |
. . . . . . . 8
|
26 | | ffun 6048 |
. . . . . . . . . . . . . . . 16
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . 15
|
28 | 21 | anim1i 592 |
. . . . . . . . . . . . . . . . 17
|
29 | 28 | ancomd 467 |
. . . . . . . . . . . . . . . 16
|
30 | | fex 6490 |
. . . . . . . . . . . . . . . 16
|
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . 15
|
32 | | 0red 10041 |
. . . . . . . . . . . . . . 15
|
33 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
34 | | 0nrp 11865 |
. . . . . . . . . . . . . . . . . . 19
|
35 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
|
36 | 35 | ssneld 3605 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 34, 36 | mpi 20 |
. . . . . . . . . . . . . . . . . 18
|
38 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . 18
|
39 | 37, 38 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
40 | 33, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
|
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . 15
|
42 | | suppdm 42300 |
. . . . . . . . . . . . . . 15
supp
|
43 | 27, 31, 32, 41, 42 | syl31anc 1329 |
. . . . . . . . . . . . . 14
supp |
44 | | fdm 6051 |
. . . . . . . . . . . . . . 15
|
45 | 44 | adantl 482 |
. . . . . . . . . . . . . 14
|
46 | 43, 45 | eqtrd 2656 |
. . . . . . . . . . . . 13
supp |
47 | 46 | 3adant3 1081 |
. . . . . . . . . . . 12
supp |
48 | 47 | eqcomd 2628 |
. . . . . . . . . . 11
supp |
49 | 48 | adantr 481 |
. . . . . . . . . 10
supp |
50 | 49 | eleq2d 2687 |
. . . . . . . . 9
supp |
51 | 50 | biimpa 501 |
. . . . . . . 8
supp |
52 | | refdivmptfv 42340 |
. . . . . . . 8
supp /_f |
53 | 25, 51, 52 | syl2anc 693 |
. . . . . . 7
/_f |
54 | 53 | breq1d 4663 |
. . . . . 6
/_f
|
55 | 15, 54 | bitr4d 271 |
. . . . 5
/_f |
56 | 55 | imbi2d 330 |
. . . 4
/_f
|
57 | 56 | ralbidva 2985 |
. . 3
/_f
|
58 | 57 | 2rexbidva 3056 |
. 2
/_f
|
59 | | simp1 1061 |
. . 3
|
60 | | ssid 3624 |
. . . 4
|
61 | 60 | a1i 11 |
. . 3
|
62 | | elbigo2 42346 |
. . 3
_O
|
63 | 19, 59, 5, 61, 62 | syl22anc 1327 |
. 2
_O
|
64 | | refdivmptf 42336 |
. . . . 5
/_f supp |
65 | 23, 64 | syl 17 |
. . . 4
/_f supp |
66 | 44 | eqcomd 2628 |
. . . . . . 7
|
67 | 66 | 3ad2ant2 1083 |
. . . . . 6
|
68 | | simpr 477 |
. . . . . . . . 9
|
69 | 21 | adantr 481 |
. . . . . . . . 9
|
70 | 68, 69, 30 | syl2anc 693 |
. . . . . . . 8
|
71 | 27, 70, 32, 41, 42 | syl31anc 1329 |
. . . . . . 7
supp |
72 | 71 | 3adant3 1081 |
. . . . . 6
supp |
73 | 67, 72 | eqtr4d 2659 |
. . . . 5
supp |
74 | 73 | feq2d 6031 |
. . . 4
/_f
/_f supp |
75 | 65, 74 | mpbird 247 |
. . 3
/_f |
76 | | ello12 14247 |
. . 3
/_f /_f
/_f
|
77 | 75, 59, 76 | syl2anc 693 |
. 2
/_f
/_f |
78 | 58, 63, 77 | 3bitr4d 300 |
1
_O /_f |