Proof of Theorem mbfi1fseqlem3
Step | Hyp | Ref
| Expression |
1 | | rge0ssre 12280 |
. . . . . . . . . . . . . . . . . . 19
|
2 | | mbfi1fseq.2 |
. . . . . . . . . . . . . . . . . . . 20
|
3 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
4 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . 20
|
5 | 2, 3, 4 | syl2an 494 |
. . . . . . . . . . . . . . . . . . 19
|
6 | 1, 5 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
|
7 | | 2nn 11185 |
. . . . . . . . . . . . . . . . . . . . 21
|
8 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . 21
|
9 | | nnexpcl 12873 |
. . . . . . . . . . . . . . . . . . . . 21
|
10 | 7, 8, 9 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
|
11 | 10 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . 19
|
12 | 11 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
|
13 | 6, 12 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
14 | | reflcl 12597 |
. . . . . . . . . . . . . . . . 17
|
15 | 13, 14 | syl 17 |
. . . . . . . . . . . . . . . 16
|
16 | 15, 11 | nndivred 11069 |
. . . . . . . . . . . . . . 15
|
17 | 16 | ralrimivva 2971 |
. . . . . . . . . . . . . 14
|
18 | | mbfi1fseq.3 |
. . . . . . . . . . . . . . 15
|
19 | 18 | fmpt2 7237 |
. . . . . . . . . . . . . 14
|
20 | 17, 19 | sylib 208 |
. . . . . . . . . . . . 13
|
21 | | fovrn 6804 |
. . . . . . . . . . . . 13
|
22 | 20, 21 | syl3an1 1359 |
. . . . . . . . . . . 12
|
23 | 22 | 3expa 1265 |
. . . . . . . . . . 11
|
24 | | nnre 11027 |
. . . . . . . . . . . 12
|
25 | 24 | ad2antlr 763 |
. . . . . . . . . . 11
|
26 | | nnnn0 11299 |
. . . . . . . . . . . . . 14
|
27 | | nnexpcl 12873 |
. . . . . . . . . . . . . 14
|
28 | 7, 26, 27 | sylancr 695 |
. . . . . . . . . . . . 13
|
29 | 28 | ad2antlr 763 |
. . . . . . . . . . . 12
|
30 | | nnre 11027 |
. . . . . . . . . . . . 13
|
31 | | nngt0 11049 |
. . . . . . . . . . . . 13
|
32 | 30, 31 | jca 554 |
. . . . . . . . . . . 12
|
33 | 29, 32 | syl 17 |
. . . . . . . . . . 11
|
34 | | lemul1 10875 |
. . . . . . . . . . 11
|
35 | 23, 25, 33, 34 | syl3anc 1326 |
. . . . . . . . . 10
|
36 | 35 | biimpa 501 |
. . . . . . . . 9
|
37 | | simplr 792 |
. . . . . . . . . . . . . . . 16
|
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . 15
|
39 | | simplr 792 |
. . . . . . . . . . . . . . 15
|
40 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
|
42 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 42 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 41, 43 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
|
46 | 45, 43 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
|
47 | | ovex 6678 |
. . . . . . . . . . . . . . . 16
|
48 | 46, 18, 47 | ovmpt2a 6791 |
. . . . . . . . . . . . . . 15
|
49 | 38, 39, 48 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
50 | 49 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
51 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 51 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | | elrege0 12278 |
. . . . . . . . . . . . . . . . . . . 20
|
54 | 52, 53 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
|
55 | 54 | simpld 475 |
. . . . . . . . . . . . . . . . . 18
|
56 | 29 | nnred 11035 |
. . . . . . . . . . . . . . . . . 18
|
57 | 55, 56 | remulcld 10070 |
. . . . . . . . . . . . . . . . 17
|
58 | 29 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | nn0ge0d 11354 |
. . . . . . . . . . . . . . . . . 18
|
60 | | mulge0 10546 |
. . . . . . . . . . . . . . . . . 18
|
61 | 54, 56, 59, 60 | syl12anc 1324 |
. . . . . . . . . . . . . . . . 17
|
62 | | flge0nn0 12621 |
. . . . . . . . . . . . . . . . 17
|
63 | 57, 61, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . 15
|
65 | 64 | nn0cnd 11353 |
. . . . . . . . . . . . . 14
|
66 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
|
67 | 66 | nncnd 11036 |
. . . . . . . . . . . . . 14
|
68 | 66 | nnne0d 11065 |
. . . . . . . . . . . . . 14
|
69 | 65, 67, 68 | divcan1d 10802 |
. . . . . . . . . . . . 13
|
70 | 50, 69 | eqtrd 2656 |
. . . . . . . . . . . 12
|
71 | 70, 64 | eqeltrd 2701 |
. . . . . . . . . . 11
|
72 | | nn0uz 11722 |
. . . . . . . . . . 11
|
73 | 71, 72 | syl6eleq 2711 |
. . . . . . . . . 10
|
74 | | nnmulcl 11043 |
. . . . . . . . . . . . . 14
|
75 | 28, 74 | mpdan 702 |
. . . . . . . . . . . . 13
|
76 | 75 | ad2antlr 763 |
. . . . . . . . . . . 12
|
77 | 76 | adantr 481 |
. . . . . . . . . . 11
|
78 | 77 | nnzd 11481 |
. . . . . . . . . 10
|
79 | | elfz5 12334 |
. . . . . . . . . 10
|
80 | 73, 78, 79 | syl2anc 693 |
. . . . . . . . 9
|
81 | 36, 80 | mpbird 247 |
. . . . . . . 8
|
82 | | oveq1 6657 |
. . . . . . . . 9
|
83 | | eqid 2622 |
. . . . . . . . 9
|
84 | | ovex 6678 |
. . . . . . . . 9
|
85 | 82, 83, 84 | fvmpt 6282 |
. . . . . . . 8
|
86 | 81, 85 | syl 17 |
. . . . . . 7
|
87 | 23 | adantr 481 |
. . . . . . . . 9
|
88 | 87 | recnd 10068 |
. . . . . . . 8
|
89 | 88, 67, 68 | divcan4d 10807 |
. . . . . . 7
|
90 | 86, 89 | eqtrd 2656 |
. . . . . 6
|
91 | | elfznn0 12433 |
. . . . . . . . . . . . 13
|
92 | 91 | nn0red 11352 |
. . . . . . . . . . . 12
|
93 | 28 | adantl 482 |
. . . . . . . . . . . 12
|
94 | | nndivre 11056 |
. . . . . . . . . . . 12
|
95 | 92, 93, 94 | syl2anr 495 |
. . . . . . . . . . 11
|
96 | 95, 83 | fmptd 6385 |
. . . . . . . . . 10
|
97 | | ffn 6045 |
. . . . . . . . . 10
|
98 | 96, 97 | syl 17 |
. . . . . . . . 9
|
99 | 98 | adantr 481 |
. . . . . . . 8
|
100 | 99 | adantr 481 |
. . . . . . 7
|
101 | | fnfvelrn 6356 |
. . . . . . 7
|
102 | 100, 81, 101 | syl2anc 693 |
. . . . . 6
|
103 | 90, 102 | eqeltrrd 2702 |
. . . . 5
|
104 | 76 | nnnn0d 11351 |
. . . . . . . . . . 11
|
105 | 104, 72 | syl6eleq 2711 |
. . . . . . . . . 10
|
106 | | eluzfz2 12349 |
. . . . . . . . . 10
|
107 | 105, 106 | syl 17 |
. . . . . . . . 9
|
108 | | oveq1 6657 |
. . . . . . . . . 10
|
109 | | ovex 6678 |
. . . . . . . . . 10
|
110 | 108, 83, 109 | fvmpt 6282 |
. . . . . . . . 9
|
111 | 107, 110 | syl 17 |
. . . . . . . 8
|
112 | 25 | recnd 10068 |
. . . . . . . . 9
|
113 | 29 | nncnd 11036 |
. . . . . . . . 9
|
114 | 29 | nnne0d 11065 |
. . . . . . . . 9
|
115 | 112, 113,
114 | divcan4d 10807 |
. . . . . . . 8
|
116 | 111, 115 | eqtrd 2656 |
. . . . . . 7
|
117 | | fnfvelrn 6356 |
. . . . . . . 8
|
118 | 99, 107, 117 | syl2anc 693 |
. . . . . . 7
|
119 | 116, 118 | eqeltrrd 2702 |
. . . . . 6
|
120 | 119 | adantr 481 |
. . . . 5
|
121 | 103, 120 | ifclda 4120 |
. . . 4
|
122 | | eluzfz1 12348 |
. . . . . . . 8
|
123 | 105, 122 | syl 17 |
. . . . . . 7
|
124 | | oveq1 6657 |
. . . . . . . 8
|
125 | | ovex 6678 |
. . . . . . . 8
|
126 | 124, 83, 125 | fvmpt 6282 |
. . . . . . 7
|
127 | 123, 126 | syl 17 |
. . . . . 6
|
128 | | nncn 11028 |
. . . . . . . 8
|
129 | | nnne0 11053 |
. . . . . . . 8
|
130 | 128, 129 | div0d 10800 |
. . . . . . 7
|
131 | 29, 130 | syl 17 |
. . . . . 6
|
132 | 127, 131 | eqtrd 2656 |
. . . . 5
|
133 | | fnfvelrn 6356 |
. . . . . 6
|
134 | 99, 123, 133 | syl2anc 693 |
. . . . 5
|
135 | 132, 134 | eqeltrrd 2702 |
. . . 4
|
136 | 121, 135 | ifcld 4131 |
. . 3
|
137 | | eqid 2622 |
. . 3
|
138 | 136, 137 | fmptd 6385 |
. 2
|
139 | | mbfi1fseq.1 |
. . . . 5
MblFn |
140 | | mbfi1fseq.4 |
. . . . 5
|
141 | 139, 2, 18, 140 | mbfi1fseqlem2 23483 |
. . . 4
|
142 | 141 | adantl 482 |
. . 3
|
143 | 142 | feq1d 6030 |
. 2
|
144 | 138, 143 | mpbird 247 |
1
|