Step | Hyp | Ref
| Expression |
1 | | dvntaylp.m |
. . . . 5
|
2 | | nn0uz 11722 |
. . . . 5
|
3 | 1, 2 | syl6eleq 2711 |
. . . 4
|
4 | | eluzfz2b 12350 |
. . . 4
|
5 | 3, 4 | sylib 208 |
. . 3
|
6 | | fveq2 6191 |
. . . . . 6
Tayl Tayl |
7 | | fveq2 6191 |
. . . . . . . 8
|
8 | 7 | oveq2d 6666 |
. . . . . . 7
Tayl Tayl |
9 | | oveq2 6658 |
. . . . . . . 8
|
10 | 9 | oveq2d 6666 |
. . . . . . 7
|
11 | | eqidd 2623 |
. . . . . . 7
|
12 | 8, 10, 11 | oveq123d 6671 |
. . . . . 6
Tayl Tayl |
13 | 6, 12 | eqeq12d 2637 |
. . . . 5
Tayl Tayl
Tayl Tayl |
14 | 13 | imbi2d 330 |
. . . 4
Tayl
Tayl
Tayl Tayl |
15 | | fveq2 6191 |
. . . . . 6
Tayl Tayl |
16 | | fveq2 6191 |
. . . . . . . 8
|
17 | 16 | oveq2d 6666 |
. . . . . . 7
Tayl Tayl |
18 | | oveq2 6658 |
. . . . . . . 8
|
19 | 18 | oveq2d 6666 |
. . . . . . 7
|
20 | | eqidd 2623 |
. . . . . . 7
|
21 | 17, 19, 20 | oveq123d 6671 |
. . . . . 6
Tayl Tayl |
22 | 15, 21 | eqeq12d 2637 |
. . . . 5
Tayl Tayl
Tayl Tayl |
23 | 22 | imbi2d 330 |
. . . 4
Tayl
Tayl
Tayl Tayl |
24 | | fveq2 6191 |
. . . . . 6
Tayl Tayl
|
25 | | fveq2 6191 |
. . . . . . . 8
|
26 | 25 | oveq2d 6666 |
. . . . . . 7
Tayl Tayl |
27 | | oveq2 6658 |
. . . . . . . 8
|
28 | 27 | oveq2d 6666 |
. . . . . . 7
|
29 | | eqidd 2623 |
. . . . . . 7
|
30 | 26, 28, 29 | oveq123d 6671 |
. . . . . 6
Tayl
Tayl |
31 | 24, 30 | eqeq12d 2637 |
. . . . 5
Tayl Tayl
Tayl
Tayl |
32 | 31 | imbi2d 330 |
. . . 4
Tayl
Tayl
Tayl Tayl |
33 | | fveq2 6191 |
. . . . . 6
Tayl Tayl |
34 | | fveq2 6191 |
. . . . . . . 8
|
35 | 34 | oveq2d 6666 |
. . . . . . 7
Tayl Tayl |
36 | | oveq2 6658 |
. . . . . . . 8
|
37 | 36 | oveq2d 6666 |
. . . . . . 7
|
38 | | eqidd 2623 |
. . . . . . 7
|
39 | 35, 37, 38 | oveq123d 6671 |
. . . . . 6
Tayl Tayl |
40 | 33, 39 | eqeq12d 2637 |
. . . . 5
Tayl Tayl
Tayl Tayl |
41 | 40 | imbi2d 330 |
. . . 4
Tayl
Tayl
Tayl Tayl |
42 | | ssid 3624 |
. . . . . . . 8
|
43 | 42 | a1i 11 |
. . . . . . 7
|
44 | | mapsspm 7891 |
. . . . . . . 8
|
45 | | dvntaylp.s |
. . . . . . . . . 10
|
46 | | dvntaylp.f |
. . . . . . . . . 10
|
47 | | dvntaylp.a |
. . . . . . . . . 10
|
48 | | dvntaylp.n |
. . . . . . . . . . 11
|
49 | 48, 1 | nn0addcld 11355 |
. . . . . . . . . 10
|
50 | | dvntaylp.b |
. . . . . . . . . 10
|
51 | | eqid 2622 |
. . . . . . . . . 10
Tayl Tayl |
52 | 45, 46, 47, 49, 50, 51 | taylpf 24120 |
. . . . . . . . 9
Tayl |
53 | | cnex 10017 |
. . . . . . . . . 10
|
54 | 53, 53 | elmap 7886 |
. . . . . . . . 9
Tayl Tayl |
55 | 52, 54 | sylibr 224 |
. . . . . . . 8
Tayl |
56 | 44, 55 | sseldi 3601 |
. . . . . . 7
Tayl |
57 | | dvn0 23687 |
. . . . . . 7
Tayl Tayl Tayl |
58 | 43, 56, 57 | syl2anc 693 |
. . . . . 6
Tayl Tayl |
59 | | recnprss 23668 |
. . . . . . . . . 10
|
60 | 45, 59 | syl 17 |
. . . . . . . . 9
|
61 | 53 | a1i 11 |
. . . . . . . . . 10
|
62 | | elpm2r 7875 |
. . . . . . . . . 10
|
63 | 61, 45, 46, 47, 62 | syl22anc 1327 |
. . . . . . . . 9
|
64 | | dvn0 23687 |
. . . . . . . . 9
|
65 | 60, 63, 64 | syl2anc 693 |
. . . . . . . 8
|
66 | 65 | oveq2d 6666 |
. . . . . . 7
Tayl Tayl |
67 | 1 | nn0cnd 11353 |
. . . . . . . . 9
|
68 | 67 | subid1d 10381 |
. . . . . . . 8
|
69 | 68 | oveq2d 6666 |
. . . . . . 7
|
70 | | eqidd 2623 |
. . . . . . 7
|
71 | 66, 69, 70 | oveq123d 6671 |
. . . . . 6
Tayl Tayl |
72 | 58, 71 | eqtr4d 2659 |
. . . . 5
Tayl Tayl |
73 | 72 | a1i 11 |
. . . 4
Tayl Tayl |
74 | | oveq2 6658 |
. . . . . . 7
Tayl Tayl Tayl Tayl |
75 | 42 | a1i 11 |
. . . . . . . . 9
..^ |
76 | 56 | adantr 481 |
. . . . . . . . 9
..^ Tayl |
77 | | elfzouz 12474 |
. . . . . . . . . . 11
..^
|
78 | 77 | adantl 482 |
. . . . . . . . . 10
..^ |
79 | 78, 2 | syl6eleqr 2712 |
. . . . . . . . 9
..^ |
80 | | dvnp1 23688 |
. . . . . . . . 9
Tayl Tayl
Tayl |
81 | 75, 76, 79, 80 | syl3anc 1326 |
. . . . . . . 8
..^ Tayl
Tayl |
82 | 45 | adantr 481 |
. . . . . . . . . 10
..^
|
83 | 63 | adantr 481 |
. . . . . . . . . . 11
..^
|
84 | | dvnf 23690 |
. . . . . . . . . . 11
|
85 | 82, 83, 79, 84 | syl3anc 1326 |
. . . . . . . . . 10
..^ |
86 | | dvnbss 23691 |
. . . . . . . . . . . . 13
|
87 | 82, 83, 79, 86 | syl3anc 1326 |
. . . . . . . . . . . 12
..^
|
88 | | fdm 6051 |
. . . . . . . . . . . . . 14
|
89 | 46, 88 | syl 17 |
. . . . . . . . . . . . 13
|
90 | 89 | adantr 481 |
. . . . . . . . . . . 12
..^
|
91 | 87, 90 | sseqtrd 3641 |
. . . . . . . . . . 11
..^
|
92 | 47 | adantr 481 |
. . . . . . . . . . 11
..^ |
93 | 91, 92 | sstrd 3613 |
. . . . . . . . . 10
..^
|
94 | 48 | adantr 481 |
. . . . . . . . . . 11
..^ |
95 | | fzofzp1 12565 |
. . . . . . . . . . . . 13
..^
|
96 | 95 | adantl 482 |
. . . . . . . . . . . 12
..^ |
97 | | fznn0sub 12373 |
. . . . . . . . . . . 12
|
98 | 96, 97 | syl 17 |
. . . . . . . . . . 11
..^
|
99 | 94, 98 | nn0addcld 11355 |
. . . . . . . . . 10
..^
|
100 | 50 | adantr 481 |
. . . . . . . . . . 11
..^
|
101 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . 17
..^
|
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . . 16
..^ |
103 | | fznn0sub 12373 |
. . . . . . . . . . . . . . . 16
|
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . 15
..^ |
105 | 94, 104 | nn0addcld 11355 |
. . . . . . . . . . . . . 14
..^
|
106 | | dvnadd 23692 |
. . . . . . . . . . . . . 14
|
107 | 82, 83, 79, 105, 106 | syl22anc 1327 |
. . . . . . . . . . . . 13
..^
|
108 | 48 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . 16
..^ |
110 | 98 | nn0cnd 11353 |
. . . . . . . . . . . . . . . 16
..^
|
111 | | 1cnd 10056 |
. . . . . . . . . . . . . . . 16
..^ |
112 | 109, 110,
111 | addassd 10062 |
. . . . . . . . . . . . . . 15
..^
|
113 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . 17
..^ |
114 | 79 | nn0cnd 11353 |
. . . . . . . . . . . . . . . . 17
..^ |
115 | 113, 114,
111 | nppcan2d 10418 |
. . . . . . . . . . . . . . . 16
..^ |
116 | 115 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
..^
|
117 | 112, 116 | eqtrd 2656 |
. . . . . . . . . . . . . 14
..^
|
118 | 117 | fveq2d 6195 |
. . . . . . . . . . . . 13
..^ |
119 | 114, 113 | pncan3d 10395 |
. . . . . . . . . . . . . . . 16
..^
|
120 | 119 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
..^
|
121 | 113, 114 | subcld 10392 |
. . . . . . . . . . . . . . . 16
..^ |
122 | 109, 114,
121 | add12d 10262 |
. . . . . . . . . . . . . . 15
..^
|
123 | 120, 122 | eqtr3d 2658 |
. . . . . . . . . . . . . 14
..^ |
124 | 123 | fveq2d 6195 |
. . . . . . . . . . . . 13
..^
|
125 | 107, 118,
124 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
..^ |
126 | 125 | dmeqd 5326 |
. . . . . . . . . . 11
..^
|
127 | 100, 126 | eleqtrrd 2704 |
. . . . . . . . . 10
..^
|
128 | 82, 85, 93, 99, 127 | dvtaylp 24124 |
. . . . . . . . 9
..^
Tayl Tayl |
129 | 117 | oveq1d 6665 |
. . . . . . . . . 10
..^ Tayl Tayl |
130 | 129 | oveq2d 6666 |
. . . . . . . . 9
..^
Tayl Tayl |
131 | 60 | adantr 481 |
. . . . . . . . . . . . 13
..^ |
132 | | dvnp1 23688 |
. . . . . . . . . . . . 13
|
133 | 131, 83, 79, 132 | syl3anc 1326 |
. . . . . . . . . . . 12
..^ |
134 | 133 | oveq2d 6666 |
. . . . . . . . . . 11
..^ Tayl Tayl |
135 | 134 | eqcomd 2628 |
. . . . . . . . . 10
..^ Tayl Tayl
|
136 | 135 | oveqd 6667 |
. . . . . . . . 9
..^
Tayl Tayl |
137 | 128, 130,
136 | 3eqtr3rd 2665 |
. . . . . . . 8
..^
Tayl Tayl |
138 | 81, 137 | eqeq12d 2637 |
. . . . . . 7
..^ Tayl
Tayl
Tayl Tayl |
139 | 74, 138 | syl5ibr 236 |
. . . . . 6
..^ Tayl
Tayl
Tayl
Tayl |
140 | 139 | expcom 451 |
. . . . 5
..^
Tayl Tayl Tayl
Tayl |
141 | 140 | a2d 29 |
. . . 4
..^
Tayl Tayl
Tayl Tayl |
142 | 14, 23, 32, 41, 73, 141 | fzind2 12586 |
. . 3
Tayl Tayl |
143 | 5, 142 | mpcom 38 |
. 2
Tayl Tayl |
144 | 67 | subidd 10380 |
. . . . 5
|
145 | 144 | oveq2d 6666 |
. . . 4
|
146 | 108 | addid1d 10236 |
. . . 4
|
147 | 145, 146 | eqtrd 2656 |
. . 3
|
148 | 147 | oveq1d 6665 |
. 2
Tayl Tayl |
149 | 143, 148 | eqtrd 2656 |
1
Tayl Tayl |