Step | Hyp | Ref
| Expression |
1 | | dvfcn 23672 |
. . . . . . 7
|
2 | | dvbsss 23666 |
. . . . . . . . 9
|
3 | | efcl 14813 |
. . . . . . . . . . . . . . . 16
|
4 | | fconstg 6092 |
. . . . . . . . . . . . . . . 16
|
5 | 3, 4 | syl 17 |
. . . . . . . . . . . . . . 15
|
6 | 3 | snssd 4340 |
. . . . . . . . . . . . . . 15
|
7 | 5, 6 | fssd 6057 |
. . . . . . . . . . . . . 14
|
8 | | ssid 3624 |
. . . . . . . . . . . . . . 15
|
9 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
|
10 | | subcl 10280 |
. . . . . . . . . . . . . . . . 17
|
11 | 10 | ancoms 469 |
. . . . . . . . . . . . . . . 16
|
12 | | efcl 14813 |
. . . . . . . . . . . . . . . 16
|
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . 15
|
14 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
15 | 13, 14 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
16 | | 0cn 10032 |
. . . . . . . . . . . . . . 15
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
|
18 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . . 14
|
20 | 16 | elexi 3213 |
. . . . . . . . . . . . . . . . . 18
|
21 | 20 | snid 4208 |
. . . . . . . . . . . . . . . . 17
|
22 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . 17
|
23 | 21, 22 | mpan2 707 |
. . . . . . . . . . . . . . . 16
|
24 | | dvconst 23680 |
. . . . . . . . . . . . . . . . 17
|
25 | 3, 24 | syl 17 |
. . . . . . . . . . . . . . . 16
|
26 | 23, 25 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
|
27 | | df-br 4654 |
. . . . . . . . . . . . . . 15
|
28 | 26, 27 | sylibr 224 |
. . . . . . . . . . . . . 14
|
29 | | eff 14812 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
32 | 11, 31 | fmptd 6385 |
. . . . . . . . . . . . . . . . 17
|
33 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . 20
|
34 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 33, 31, 34 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . . 19
|
36 | | subid 10300 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 35, 36 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
38 | | dveflem 23742 |
. . . . . . . . . . . . . . . . . 18
|
39 | 37, 38 | syl6eqbr 4692 |
. . . . . . . . . . . . . . . . 17
|
40 | 18 | elexi 3213 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40 | snid 4208 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | | opelxpi 5148 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 41, 42 | mpan2 707 |
. . . . . . . . . . . . . . . . . . 19
|
44 | | cnelprrecn 10029 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
|
47 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
48 | 45 | dvmptid 23720 |
. . . . . . . . . . . . . . . . . . . . 21
|
49 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | 16 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
|
52 | 45, 51 | dvmptc 23721 |
. . . . . . . . . . . . . . . . . . . . 21
|
53 | 45, 46, 47, 48, 49, 50, 52 | dvmptsub 23730 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | | 1m0e1 11131 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | 54 | mpteq2i 4741 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 55, 56 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 53, 57 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 43, 58 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . 18
|
60 | | df-br 4654 |
. . . . . . . . . . . . . . . . . 18
|
61 | 59, 60 | sylibr 224 |
. . . . . . . . . . . . . . . . 17
|
62 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
ℂfld ℂfld |
63 | 30, 9, 32, 9, 9, 9,
19, 19, 39, 61, 62 | dvcobr 23709 |
. . . . . . . . . . . . . . . 16
|
64 | | 1t1e1 11175 |
. . . . . . . . . . . . . . . 16
|
65 | 63, 64 | syl6breq 4694 |
. . . . . . . . . . . . . . 15
|
66 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . 18
|
67 | 30 | feqmptd 6249 |
. . . . . . . . . . . . . . . . . 18
|
68 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
69 | 11, 66, 67, 68 | fmptco 6396 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | breqd 4664 |
. . . . . . . . . . . . . . 15
|
72 | 65, 71 | mpbid 222 |
. . . . . . . . . . . . . 14
|
73 | 7, 9, 15, 9, 9, 17, 19, 28, 72, 62 | dvmulbr 23702 |
. . . . . . . . . . . . 13
|
74 | 15, 51 | ffvelrnd 6360 |
. . . . . . . . . . . . . . . 16
|
75 | 74 | mul02d 10234 |
. . . . . . . . . . . . . . 15
|
76 | | fvex 6201 |
. . . . . . . . . . . . . . . . . 18
|
77 | 76 | fvconst2 6469 |
. . . . . . . . . . . . . . . . 17
|
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
79 | 3 | mulid2d 10058 |
. . . . . . . . . . . . . . . 16
|
80 | 78, 79 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
81 | 75, 80 | oveq12d 6668 |
. . . . . . . . . . . . . 14
|
82 | 3 | addid2d 10237 |
. . . . . . . . . . . . . 14
|
83 | 81, 82 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
84 | 73, 83 | breqtrd 4679 |
. . . . . . . . . . . 12
|
85 | | cnex 10017 |
. . . . . . . . . . . . . . . . 17
|
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
87 | 76 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
88 | | fvex 6201 |
. . . . . . . . . . . . . . . . 17
|
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
90 | | fconstmpt 5163 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
92 | | eqidd 2623 |
. . . . . . . . . . . . . . . 16
|
93 | 86, 87, 89, 91, 92 | offval2 6914 |
. . . . . . . . . . . . . . 15
|
94 | 30 | feqmptd 6249 |
. . . . . . . . . . . . . . . 16
|
95 | | efadd 14824 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 11, 95 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
|
97 | | pncan3 10289 |
. . . . . . . . . . . . . . . . . . 19
|
98 | 97 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
|
99 | 96, 98 | eqtr3d 2658 |
. . . . . . . . . . . . . . . . 17
|
100 | 99 | mpteq2dva 4744 |
. . . . . . . . . . . . . . . 16
|
101 | 94, 100 | eqtr4d 2659 |
. . . . . . . . . . . . . . 15
|
102 | 93, 101 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
|
103 | 102 | oveq2d 6666 |
. . . . . . . . . . . . 13
|
104 | 103 | breqd 4664 |
. . . . . . . . . . . 12
|
105 | 84, 104 | mpbid 222 |
. . . . . . . . . . 11
|
106 | | vex 3203 |
. . . . . . . . . . . 12
|
107 | 106, 76 | breldm 5329 |
. . . . . . . . . . 11
|
108 | 105, 107 | syl 17 |
. . . . . . . . . 10
|
109 | 108 | ssriv 3607 |
. . . . . . . . 9
|
110 | 2, 109 | eqssi 3619 |
. . . . . . . 8
|
111 | 110 | feq2i 6037 |
. . . . . . 7
|
112 | 1, 111 | mpbi 220 |
. . . . . 6
|
113 | 112 | a1i 11 |
. . . . 5
|
114 | 113 | feqmptd 6249 |
. . . 4
|
115 | | ffun 6048 |
. . . . . . 7
|
116 | 1, 115 | ax-mp 5 |
. . . . . 6
|
117 | | funbrfv 6234 |
. . . . . 6
|
118 | 116, 105,
117 | mpsyl 68 |
. . . . 5
|
119 | 118 | mpteq2ia 4740 |
. . . 4
|
120 | 114, 119 | syl6eq 2672 |
. . 3
|
121 | 29 | a1i 11 |
. . . 4
|
122 | 121 | feqmptd 6249 |
. . 3
|
123 | 120, 122 | eqtr4d 2659 |
. 2
|
124 | 123 | trud 1493 |
1
|