Step Hyp Ref
Expression 1 brdomi 7547 . 2
2 neq0 3795 . . . . 5
3 simpl3 1001 . . . . . . . . . . 11
4 elmapi 7460 . . . . . . . . . . . . . . 15
5 4 ad2antlr 726 . . . . . . . . . . . . . 14
6 simpll1 1035 . . . . . . . . . . . . . . . . 17
7 f1f1orn 5832 . . . . . . . . . . . . . . . . 17
8 f1ocnv 5833 . . . . . . . . . . . . . . . . 17
9 f1of 5821 . . . . . . . . . . . . . . . . 17
10 6 , 7 , 8 , 9 4syl 21 . . . . . . . . . . . . . . . 16
11 10 ffvelrnda 6031 . . . . . . . . . . . . . . 15
12 simpl2 1000 . . . . . . . . . . . . . . . 16
13 12 ad2antrr 725 . . . . . . . . . . . . . . 15
14 11 , 13 ifclda 3973 . . . . . . . . . . . . . 14
15 5 , 14 ffvelrnd 6032 . . . . . . . . . . . . 13
16 eldifsn 4155 . . . . . . . . . . . . . 14
17 elpwi 4021 . . . . . . . . . . . . . . 15
18 17 anim1i 568 . . . . . . . . . . . . . 14
19 16 , 18 sylbi 195 . . . . . . . . . . . . 13
20 15 , 19 syl 16 . . . . . . . . . . . 12
21 20 ralrimiva 2871 . . . . . . . . . . 11
22 acni2 8448 . . . . . . . . . . 11
23 3 , 21 , 22 syl2anc 661 . . . . . . . . . 10
24 f1dm 5790 . . . . . . . . . . . . . 14
25 vex 3112 . . . . . . . . . . . . . . 15
26 25 dmex 6733 . . . . . . . . . . . . . 14
27 24 , 26 syl6eqelr 2554 . . . . . . . . . . . . 13
28 27 3ad2ant1 1017 . . . . . . . . . . . 12
29 28 ad2antrr 725 . . . . . . . . . . 11
30 simpll1 1035 . . . . . . . . . . . . . . . 16
31 f1f 5786 . . . . . . . . . . . . . . . 16
32 frn 5742 . . . . . . . . . . . . . . . 16
33 ssralv 3563 . . . . . . . . . . . . . . . 16
34 30 , 31 , 32 , 33 4syl 21 . . . . . . . . . . . . . . 15
35 iftrue 3947 . . . . . . . . . . . . . . . . . 18
36 35 fveq2d 5875 . . . . . . . . . . . . . . . . 17
37 36 eleq2d 2527 . . . . . . . . . . . . . . . 16
38 37 ralbiia 2887 . . . . . . . . . . . . . . 15
39 34 , 38 syl6ib 226 . . . . . . . . . . . . . 14
40 f1fn 5787 . . . . . . . . . . . . . . 15
41 fveq2 5871 . . . . . . . . . . . . . . . . 17
42 fveq2 5871 . . . . . . . . . . . . . . . . . 18
43 42 fveq2d 5875 . . . . . . . . . . . . . . . . 17
44 41 , 43 eleq12d 2539 . . . . . . . . . . . . . . . 16
45 44 ralrn 6034 . . . . . . . . . . . . . . 15
46 30 , 40 , 45 3syl 20 . . . . . . . . . . . . . 14
47 39 , 46 sylibd 214 . . . . . . . . . . . . 13
48 30 , 7 syl 16 . . . . . . . . . . . . . . . . 17
49 f1ocnvfv1 6182 . . . . . . . . . . . . . . . . 17
50 48 , 49 sylan 471 . . . . . . . . . . . . . . . 16
51 50 fveq2d 5875 . . . . . . . . . . . . . . 15
52 51 eleq2d 2527 . . . . . . . . . . . . . 14
53 52 ralbidva 2893 . . . . . . . . . . . . 13
54 47 , 53 sylibd 214 . . . . . . . . . . . 12
55 54 impr 619 . . . . . . . . . . 11
56 acnlem 8450 . . . . . . . . . . 11
57 29 , 55 , 56 syl2anc 661 . . . . . . . . . 10
58 23 , 57 exlimddv 1726 . . . . . . . . 9
59 58 ralrimiva 2871 . . . . . . . 8
60 elex 3118 . . . . . . . . . 10
61 isacn 8446 . . . . . . . . . 10
62 60 , 27 , 61 syl2anr 478 . . . . . . . . 9
63 62 3adant2 1015 . . . . . . . 8
64 59 , 63 mpbird 232 . . . . . . 7
65 64 3exp 1195 . . . . . 6
66 65 exlimdv 1724 . . . . 5
67 2 , 66 syl5bi 217 . . . 4
68 acneq 8445 . . . . . . 7
69 0fin 7767 . . . . . . . 8
70 finacn 8452 . . . . . . . 8
71 69 , 70 ax-mp 5 . . . . . . 7
72 68 , 71 syl6eq 2514 . . . . . 6
73 72 eleq2d 2527 . . . . 5
74 60 , 73 syl5ibr 221 . . . 4
75 67 , 74 pm2.61d2 160 . . 3
76 75 exlimiv 1722 . 2
77 1 , 76 syl 16 1
