Step | Hyp | Ref
| Expression |
1 | | binomcxplem.d |
. . . . 5
|
2 | | nfcv 2764 |
. . . . . 6
|
3 | | nfcv 2764 |
. . . . . . 7
|
4 | | nfcv 2764 |
. . . . . . 7
|
5 | | binomcxplem.r |
. . . . . . . 8
|
6 | | nfcv 2764 |
. . . . . . . . . . . 12
|
7 | | binomcxplem.s |
. . . . . . . . . . . . . 14
|
8 | | nfmpt1 4747 |
. . . . . . . . . . . . . 14
|
9 | 7, 8 | nfcxfr 2762 |
. . . . . . . . . . . . 13
|
10 | | nfcv 2764 |
. . . . . . . . . . . . 13
|
11 | 9, 10 | nffv 6198 |
. . . . . . . . . . . 12
|
12 | 3, 6, 11 | nfseq 12811 |
. . . . . . . . . . 11
|
13 | 12 | nfel1 2779 |
. . . . . . . . . 10
|
14 | | nfcv 2764 |
. . . . . . . . . 10
|
15 | 13, 14 | nfrab 3123 |
. . . . . . . . 9
|
16 | | nfcv 2764 |
. . . . . . . . 9
|
17 | | nfcv 2764 |
. . . . . . . . 9
|
18 | 15, 16, 17 | nfsup 8357 |
. . . . . . . 8
|
19 | 5, 18 | nfcxfr 2762 |
. . . . . . 7
|
20 | 3, 4, 19 | nfov 6676 |
. . . . . 6
|
21 | 2, 20 | nfima 5474 |
. . . . 5
|
22 | 1, 21 | nfcxfr 2762 |
. . . 4
|
23 | | nfcv 2764 |
. . . 4
|
24 | | nfcv 2764 |
. . . 4
|
25 | | nfcv 2764 |
. . . 4
|
26 | | oveq2 6658 |
. . . . 5
|
27 | 26 | oveq1d 6665 |
. . . 4
|
28 | 22, 23, 24, 25, 27 | cbvmptf 4748 |
. . 3
|
29 | 28 | oveq2i 6661 |
. 2
|
30 | | cnelprrecn 10029 |
. . . . 5
|
31 | 30 | a1i 11 |
. . . 4
|
32 | | 1cnd 10056 |
. . . . . 6
|
33 | | cnvimass 5485 |
. . . . . . . . . 10
|
34 | 1, 33 | eqsstri 3635 |
. . . . . . . . 9
|
35 | | absf 14077 |
. . . . . . . . . 10
|
36 | 35 | fdmi 6052 |
. . . . . . . . 9
|
37 | 34, 36 | sseqtri 3637 |
. . . . . . . 8
|
38 | 37 | a1i 11 |
. . . . . . 7
|
39 | 38 | sselda 3603 |
. . . . . 6
|
40 | 32, 39 | addcld 10059 |
. . . . 5
|
41 | | simpr 477 |
. . . . . . 7
|
42 | | 1cnd 10056 |
. . . . . . . . . 10
|
43 | 39 | adantr 481 |
. . . . . . . . . 10
|
44 | 42, 43 | pncan2d 10394 |
. . . . . . . . 9
|
45 | | 1red 10055 |
. . . . . . . . . 10
|
46 | 41, 45 | resubcld 10458 |
. . . . . . . . 9
|
47 | 44, 46 | eqeltrrd 2702 |
. . . . . . . 8
|
48 | | 1pneg1e0 11129 |
. . . . . . . . 9
|
49 | | 1red 10055 |
. . . . . . . . . . 11
|
50 | 49 | renegcld 10457 |
. . . . . . . . . 10
|
51 | | simpr 477 |
. . . . . . . . . 10
|
52 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | 35, 52, 53 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | simprbi 480 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55, 1 | eleq2s 2719 |
. . . . . . . . . . . . . . . . 17
|
57 | | 0re 10040 |
. . . . . . . . . . . . . . . . . 18
|
58 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | 58, 59 | sstri 3612 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | | supxrcl 12145 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 5, 62 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . 18
|
64 | | elico2 12237 |
. . . . . . . . . . . . . . . . . 18
|
65 | 57, 63, 64 | mp2an 708 |
. . . . . . . . . . . . . . . . 17
|
66 | 56, 65 | sylib 208 |
. . . . . . . . . . . . . . . 16
|
67 | 66 | simp3d 1075 |
. . . . . . . . . . . . . . 15
|
68 | 67 | adantl 482 |
. . . . . . . . . . . . . 14
|
69 | | binomcxp.a |
. . . . . . . . . . . . . . . 16
|
70 | | binomcxp.b |
. . . . . . . . . . . . . . . 16
|
71 | | binomcxp.lt |
. . . . . . . . . . . . . . . 16
|
72 | | binomcxp.c |
. . . . . . . . . . . . . . . 16
|
73 | | binomcxplem.f |
. . . . . . . . . . . . . . . 16
C𝑐 |
74 | 69, 70, 71, 72, 73, 7, 5 | binomcxplemradcnv 38551 |
. . . . . . . . . . . . . . 15
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . . 14
|
76 | 68, 75 | breqtrd 4679 |
. . . . . . . . . . . . 13
|
77 | 76 | adantr 481 |
. . . . . . . . . . . 12
|
78 | 51, 49 | absltd 14168 |
. . . . . . . . . . . 12
|
79 | 77, 78 | mpbid 222 |
. . . . . . . . . . 11
|
80 | 79 | simpld 475 |
. . . . . . . . . 10
|
81 | 50, 51, 49, 80 | ltadd2dd 10196 |
. . . . . . . . 9
|
82 | 48, 81 | syl5eqbrr 4689 |
. . . . . . . 8
|
83 | 47, 82 | syldan 487 |
. . . . . . 7
|
84 | 41, 83 | elrpd 11869 |
. . . . . 6
|
85 | 84 | ex 450 |
. . . . 5
|
86 | | eqid 2622 |
. . . . . 6
|
87 | 86 | ellogdm 24385 |
. . . . 5
|
88 | 40, 85, 87 | sylanbrc 698 |
. . . 4
|
89 | | eldifi 3732 |
. . . . . 6
|
90 | 89 | adantl 482 |
. . . . 5
|
91 | 72 | adantr 481 |
. . . . . . 7
|
92 | 91 | negcld 10379 |
. . . . . 6
|
93 | 92 | adantr 481 |
. . . . 5
|
94 | 90, 93 | cxpcld 24454 |
. . . 4
|
95 | | ovexd 6680 |
. . . 4
|
96 | | 1cnd 10056 |
. . . . . . 7
|
97 | | simpr 477 |
. . . . . . 7
|
98 | 96, 97 | addcld 10059 |
. . . . . 6
|
99 | | c0ex 10034 |
. . . . . . . . 9
|
100 | 99 | a1i 11 |
. . . . . . . 8
|
101 | | 1cnd 10056 |
. . . . . . . . 9
|
102 | 31, 101 | dvmptc 23721 |
. . . . . . . 8
|
103 | 31 | dvmptid 23720 |
. . . . . . . 8
|
104 | 31, 96, 100, 102, 97, 96, 103 | dvmptadd 23723 |
. . . . . . 7
|
105 | | 0p1e1 11132 |
. . . . . . . 8
|
106 | 105 | mpteq2i 4741 |
. . . . . . 7
|
107 | 104, 106 | syl6eq 2672 |
. . . . . 6
|
108 | | fvex 6201 |
. . . . . . . 8
ℂfld |
109 | | cnfldtps 22581 |
. . . . . . . . . 10
ℂfld |
110 | | cnfldbas 19750 |
. . . . . . . . . . 11
ℂfld |
111 | | eqid 2622 |
. . . . . . . . . . 11
ℂfld ℂfld |
112 | 110, 111 | tpsuni 20740 |
. . . . . . . . . 10
ℂfld
ℂfld |
113 | 109, 112 | ax-mp 5 |
. . . . . . . . 9
ℂfld |
114 | 113 | restid 16094 |
. . . . . . . 8
ℂfld ℂfld
↾t ℂfld |
115 | 108, 114 | ax-mp 5 |
. . . . . . 7
ℂfld ↾t ℂfld |
116 | 115 | eqcomi 2631 |
. . . . . 6
ℂfld ℂfld ↾t |
117 | 111 | cnfldtop 22587 |
. . . . . . . 8
ℂfld |
118 | | eqid 2622 |
. . . . . . . . . . . 12
|
119 | 118 | cnbl0 22577 |
. . . . . . . . . . 11
|
120 | 63, 119 | ax-mp 5 |
. . . . . . . . . 10
|
121 | 1, 120 | eqtri 2644 |
. . . . . . . . 9
|
122 | | cnxmet 22576 |
. . . . . . . . . 10
|
123 | | 0cn 10032 |
. . . . . . . . . 10
|
124 | 111 | cnfldtopn 22585 |
. . . . . . . . . . 11
ℂfld |
125 | 124 | blopn 22305 |
. . . . . . . . . 10
ℂfld |
126 | 122, 123,
63, 125 | mp3an 1424 |
. . . . . . . . 9
ℂfld |
127 | 121, 126 | eqeltri 2697 |
. . . . . . . 8
ℂfld |
128 | | isopn3i 20886 |
. . . . . . . 8
ℂfld
ℂfld
ℂfld |
129 | 117, 127,
128 | mp2an 708 |
. . . . . . 7
ℂfld |
130 | 129 | a1i 11 |
. . . . . 6
ℂfld |
131 | 31, 98, 96, 107, 38, 116, 111, 130 | dvmptres2 23725 |
. . . . 5
|
132 | | oveq2 6658 |
. . . . . . 7
|
133 | 132 | cbvmptv 4750 |
. . . . . 6
|
134 | 133 | oveq2i 6661 |
. . . . 5
|
135 | | eqidd 2623 |
. . . . . 6
|
136 | 135 | cbvmptv 4750 |
. . . . 5
|
137 | 131, 134,
136 | 3eqtr3g 2679 |
. . . 4
|
138 | 86 | dvcncxp1 24484 |
. . . . 5
|
139 | 92, 138 | syl 17 |
. . . 4
|
140 | | oveq1 6657 |
. . . 4
|
141 | | oveq1 6657 |
. . . . 5
|
142 | 141 | oveq2d 6666 |
. . . 4
|
143 | 31, 31, 88, 32, 94, 95, 137, 139, 140, 142 | dvmptco 23735 |
. . 3
|
144 | 91 | adantr 481 |
. . . . . . 7
|
145 | 144 | negcld 10379 |
. . . . . 6
|
146 | 145, 32 | subcld 10392 |
. . . . . . 7
|
147 | 40, 146 | cxpcld 24454 |
. . . . . 6
|
148 | 145, 147 | mulcld 10060 |
. . . . 5
|
149 | 148 | mulid1d 10057 |
. . . 4
|
150 | 149 | mpteq2dva 4744 |
. . 3
|
151 | | nfcv 2764 |
. . . . 5
|
152 | | nfcv 2764 |
. . . . 5
|
153 | | oveq2 6658 |
. . . . . . 7
|
154 | 153 | oveq1d 6665 |
. . . . . 6
|
155 | 154 | oveq2d 6666 |
. . . . 5
|
156 | 23, 22, 151, 152, 155 | cbvmptf 4748 |
. . . 4
|
157 | 156 | a1i 11 |
. . 3
|
158 | 143, 150,
157 | 3eqtrd 2660 |
. 2
|
159 | 29, 158 | syl5eq 2668 |
1
|