Proof of Theorem itgmulc2nclem2
Step | Hyp | Ref
| Expression |
1 | | itgmulc2nc.4 |
. . . . . . 7
|
2 | | max0sub 12027 |
. . . . . . 7
|
3 | 1, 2 | syl 17 |
. . . . . 6
|
4 | 3 | oveq1d 6665 |
. . . . 5
|
5 | 4 | adantr 481 |
. . . 4
|
6 | | 0re 10040 |
. . . . . . . 8
|
7 | | ifcl 4130 |
. . . . . . . 8
|
8 | 1, 6, 7 | sylancl 694 |
. . . . . . 7
|
9 | 8 | recnd 10068 |
. . . . . 6
|
10 | 9 | adantr 481 |
. . . . 5
|
11 | 1 | renegcld 10457 |
. . . . . . . 8
|
12 | | ifcl 4130 |
. . . . . . . 8
|
13 | 11, 6, 12 | sylancl 694 |
. . . . . . 7
|
14 | 13 | recnd 10068 |
. . . . . 6
|
15 | 14 | adantr 481 |
. . . . 5
|
16 | | itgmulc2nc.5 |
. . . . . 6
|
17 | 16 | recnd 10068 |
. . . . 5
|
18 | 10, 15, 17 | subdird 10487 |
. . . 4
|
19 | 5, 18 | eqtr3d 2658 |
. . 3
|
20 | 19 | itgeq2dv 23548 |
. 2
|
21 | | ovexd 6680 |
. . 3
|
22 | | itgmulc2nc.3 |
. . . 4
|
23 | | itgmulc2nc.m |
. . . . . . 7
MblFn |
24 | | ovexd 6680 |
. . . . . . 7
|
25 | 23, 24 | mbfdm2 23405 |
. . . . . 6
|
26 | 8 | adantr 481 |
. . . . . 6
|
27 | | fconstmpt 5163 |
. . . . . . 7
|
28 | 27 | a1i 11 |
. . . . . 6
|
29 | | eqidd 2623 |
. . . . . 6
|
30 | 25, 26, 16, 28, 29 | offval2 6914 |
. . . . 5
|
31 | | iblmbf 23534 |
. . . . . . 7
MblFn |
32 | 22, 31 | syl 17 |
. . . . . 6
MblFn |
33 | | eqid 2622 |
. . . . . . 7
|
34 | 17, 33 | fmptd 6385 |
. . . . . 6
|
35 | 32, 8, 34 | mbfmulc2re 23415 |
. . . . 5
MblFn |
36 | 30, 35 | eqeltrrd 2702 |
. . . 4
MblFn |
37 | 9, 16, 22, 36 | iblmulc2nc 33475 |
. . 3
|
38 | | ovexd 6680 |
. . 3
|
39 | 13 | adantr 481 |
. . . . . 6
|
40 | | fconstmpt 5163 |
. . . . . . 7
|
41 | 40 | a1i 11 |
. . . . . 6
|
42 | 25, 39, 16, 41, 29 | offval2 6914 |
. . . . 5
|
43 | 32, 13, 34 | mbfmulc2re 23415 |
. . . . 5
MblFn |
44 | 42, 43 | eqeltrrd 2702 |
. . . 4
MblFn |
45 | 14, 16, 22, 44 | iblmulc2nc 33475 |
. . 3
|
46 | 19 | mpteq2dva 4744 |
. . . 4
|
47 | 46, 23 | eqeltrrd 2702 |
. . 3
MblFn |
48 | 21, 37, 38, 45, 47 | itgsubnc 33472 |
. 2
|
49 | | ovexd 6680 |
. . . . . 6
|
50 | | ifcl 4130 |
. . . . . . . 8
|
51 | 16, 6, 50 | sylancl 694 |
. . . . . . 7
|
52 | 16 | iblre 23560 |
. . . . . . . . 9
|
53 | 22, 52 | mpbid 222 |
. . . . . . . 8
|
54 | 53 | simpld 475 |
. . . . . . 7
|
55 | | eqidd 2623 |
. . . . . . . . 9
|
56 | 25, 26, 51, 28, 55 | offval2 6914 |
. . . . . . . 8
|
57 | 16, 32 | mbfpos 23418 |
. . . . . . . . 9
MblFn |
58 | 51 | recnd 10068 |
. . . . . . . . . 10
|
59 | | eqid 2622 |
. . . . . . . . . 10
|
60 | 58, 59 | fmptd 6385 |
. . . . . . . . 9
|
61 | 57, 8, 60 | mbfmulc2re 23415 |
. . . . . . . 8
MblFn |
62 | 56, 61 | eqeltrrd 2702 |
. . . . . . 7
MblFn |
63 | 9, 51, 54, 62 | iblmulc2nc 33475 |
. . . . . 6
|
64 | | ovexd 6680 |
. . . . . 6
|
65 | 16 | renegcld 10457 |
. . . . . . . 8
|
66 | | ifcl 4130 |
. . . . . . . 8
|
67 | 65, 6, 66 | sylancl 694 |
. . . . . . 7
|
68 | 53 | simprd 479 |
. . . . . . 7
|
69 | | eqidd 2623 |
. . . . . . . . 9
|
70 | 25, 26, 67, 28, 69 | offval2 6914 |
. . . . . . . 8
|
71 | 16, 32 | mbfneg 23417 |
. . . . . . . . . 10
MblFn |
72 | 65, 71 | mbfpos 23418 |
. . . . . . . . 9
MblFn |
73 | 67 | recnd 10068 |
. . . . . . . . . 10
|
74 | | eqid 2622 |
. . . . . . . . . 10
|
75 | 73, 74 | fmptd 6385 |
. . . . . . . . 9
|
76 | 72, 8, 75 | mbfmulc2re 23415 |
. . . . . . . 8
MblFn |
77 | 70, 76 | eqeltrrd 2702 |
. . . . . . 7
MblFn |
78 | 9, 67, 68, 77 | iblmulc2nc 33475 |
. . . . . 6
|
79 | | max0sub 12027 |
. . . . . . . . . . . 12
|
80 | 16, 79 | syl 17 |
. . . . . . . . . . 11
|
81 | 80 | oveq2d 6666 |
. . . . . . . . . 10
|
82 | 10, 58, 73 | subdid 10486 |
. . . . . . . . . 10
|
83 | 81, 82 | eqtr3d 2658 |
. . . . . . . . 9
|
84 | 83 | mpteq2dva 4744 |
. . . . . . . 8
|
85 | 30, 84 | eqtrd 2656 |
. . . . . . 7
|
86 | 85, 35 | eqeltrrd 2702 |
. . . . . 6
MblFn |
87 | 49, 63, 64, 78, 86 | itgsubnc 33472 |
. . . . 5
|
88 | 83 | itgeq2dv 23548 |
. . . . 5
|
89 | 16, 22 | itgreval 23563 |
. . . . . . 7
|
90 | 89 | oveq2d 6666 |
. . . . . 6
|
91 | 51, 54 | itgcl 23550 |
. . . . . . 7
|
92 | 67, 68 | itgcl 23550 |
. . . . . . 7
|
93 | 9, 91, 92 | subdid 10486 |
. . . . . 6
|
94 | | max1 12016 |
. . . . . . . . 9
|
95 | 6, 1, 94 | sylancr 695 |
. . . . . . . 8
|
96 | | max1 12016 |
. . . . . . . . 9
|
97 | 6, 16, 96 | sylancr 695 |
. . . . . . . 8
|
98 | 9, 51, 54, 62, 8, 51, 95, 97 | itgmulc2nclem1 33476 |
. . . . . . 7
|
99 | | max1 12016 |
. . . . . . . . 9
|
100 | 6, 65, 99 | sylancr 695 |
. . . . . . . 8
|
101 | 9, 67, 68, 77, 8, 67, 95, 100 | itgmulc2nclem1 33476 |
. . . . . . 7
|
102 | 98, 101 | oveq12d 6668 |
. . . . . 6
|
103 | 90, 93, 102 | 3eqtrd 2660 |
. . . . 5
|
104 | 87, 88, 103 | 3eqtr4d 2666 |
. . . 4
|
105 | | ovexd 6680 |
. . . . . 6
|
106 | 25, 39, 51, 41, 55 | offval2 6914 |
. . . . . . . 8
|
107 | 57, 13, 60 | mbfmulc2re 23415 |
. . . . . . . 8
MblFn |
108 | 106, 107 | eqeltrrd 2702 |
. . . . . . 7
MblFn |
109 | 14, 51, 54, 108 | iblmulc2nc 33475 |
. . . . . 6
|
110 | | ovexd 6680 |
. . . . . 6
|
111 | 25, 39, 67, 41, 69 | offval2 6914 |
. . . . . . . 8
|
112 | 72, 13, 75 | mbfmulc2re 23415 |
. . . . . . . 8
MblFn |
113 | 111, 112 | eqeltrrd 2702 |
. . . . . . 7
MblFn |
114 | 14, 67, 68, 113 | iblmulc2nc 33475 |
. . . . . 6
|
115 | 80 | oveq2d 6666 |
. . . . . . . . . 10
|
116 | 15, 58, 73 | subdid 10486 |
. . . . . . . . . 10
|
117 | 115, 116 | eqtr3d 2658 |
. . . . . . . . 9
|
118 | 117 | mpteq2dva 4744 |
. . . . . . . 8
|
119 | 42, 118 | eqtrd 2656 |
. . . . . . 7
|
120 | 119, 43 | eqeltrrd 2702 |
. . . . . 6
MblFn |
121 | 105, 109,
110, 114, 120 | itgsubnc 33472 |
. . . . 5
|
122 | 117 | itgeq2dv 23548 |
. . . . 5
|
123 | 89 | oveq2d 6666 |
. . . . . 6
|
124 | 14, 91, 92 | subdid 10486 |
. . . . . 6
|
125 | | max1 12016 |
. . . . . . . . 9
|
126 | 6, 11, 125 | sylancr 695 |
. . . . . . . 8
|
127 | 14, 51, 54, 108, 13, 51, 126, 97 | itgmulc2nclem1 33476 |
. . . . . . 7
|
128 | 14, 67, 68, 113, 13, 67, 126, 100 | itgmulc2nclem1 33476 |
. . . . . . 7
|
129 | 127, 128 | oveq12d 6668 |
. . . . . 6
|
130 | 123, 124,
129 | 3eqtrd 2660 |
. . . . 5
|
131 | 121, 122,
130 | 3eqtr4d 2666 |
. . . 4
|
132 | 104, 131 | oveq12d 6668 |
. . 3
|
133 | 16, 22 | itgcl 23550 |
. . . 4
|
134 | 9, 14, 133 | subdird 10487 |
. . 3
|
135 | 3 | oveq1d 6665 |
. . 3
|
136 | 132, 134,
135 | 3eqtr2d 2662 |
. 2
|
137 | 20, 48, 136 | 3eqtrrd 2661 |
1
|