Step | Hyp | Ref
| Expression |
1 | | itg2mono.1 |
. . . . . . . . . 10
|
2 | | itg2mono.2 |
. . . . . . . . . 10
MblFn |
3 | | itg2mono.3 |
. . . . . . . . . 10
|
4 | | itg2mono.4 |
. . . . . . . . . 10
|
5 | | itg2mono.5 |
. . . . . . . . . 10
|
6 | | itg2mono.6 |
. . . . . . . . . 10
|
7 | | itg2monolem2.7 |
. . . . . . . . . 10
|
8 | | itg2monolem2.8 |
. . . . . . . . . 10
|
9 | | itg2monolem2.9 |
. . . . . . . . . 10
|
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | itg2monolem2 23518 |
. . . . . . . . 9
|
11 | 10 | adantr 481 |
. . . . . . . 8
|
12 | 11 | recnd 10068 |
. . . . . . 7
|
13 | 7 | adantr 481 |
. . . . . . . . 9
|
14 | | itg1cl 23452 |
. . . . . . . . 9
|
15 | 13, 14 | syl 17 |
. . . . . . . 8
|
16 | 15 | recnd 10068 |
. . . . . . 7
|
17 | | simpr 477 |
. . . . . . . . . 10
|
18 | 17 | rpred 11872 |
. . . . . . . . 9
|
19 | 11, 18 | readdcld 10069 |
. . . . . . . 8
|
20 | 19 | recnd 10068 |
. . . . . . 7
|
21 | | 0red 10041 |
. . . . . . . . 9
|
22 | | 0xr 10086 |
. . . . . . . . . . . 12
|
23 | 22 | a1i 11 |
. . . . . . . . . . 11
|
24 | | 1nn 11031 |
. . . . . . . . . . . . 13
|
25 | | icossicc 12260 |
. . . . . . . . . . . . . . 15
|
26 | | fss 6056 |
. . . . . . . . . . . . . . 15
|
27 | 3, 25, 26 | sylancl 694 |
. . . . . . . . . . . . . 14
|
28 | 27 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
29 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
30 | 29 | feq1d 6030 |
. . . . . . . . . . . . . 14
|
31 | 30 | rspcv 3305 |
. . . . . . . . . . . . 13
|
32 | 24, 28, 31 | mpsyl 68 |
. . . . . . . . . . . 12
|
33 | | itg2cl 23499 |
. . . . . . . . . . . 12
|
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
|
35 | | itg2cl 23499 |
. . . . . . . . . . . . . . . 16
|
36 | 27, 35 | syl 17 |
. . . . . . . . . . . . . . 15
|
37 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
38 | 36, 37 | fmptd 6385 |
. . . . . . . . . . . . . 14
|
39 | | frn 6053 |
. . . . . . . . . . . . . 14
|
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . 13
|
41 | | supxrcl 12145 |
. . . . . . . . . . . . 13
|
42 | 40, 41 | syl 17 |
. . . . . . . . . . . 12
|
43 | 6, 42 | syl5eqel 2705 |
. . . . . . . . . . 11
|
44 | | itg2ge0 23502 |
. . . . . . . . . . . 12
|
45 | 32, 44 | syl 17 |
. . . . . . . . . . 11
|
46 | 29 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
|
47 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
|
48 | 46, 37, 47 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
|
49 | 24, 48 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
50 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
|
51 | 38, 50 | syl 17 |
. . . . . . . . . . . . . . 15
|
52 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . 15
|
53 | 51, 24, 52 | sylancl 694 |
. . . . . . . . . . . . . 14
|
54 | 49, 53 | syl5eqelr 2706 |
. . . . . . . . . . . . 13
|
55 | | supxrub 12154 |
. . . . . . . . . . . . 13
|
56 | 40, 54, 55 | syl2anc 693 |
. . . . . . . . . . . 12
|
57 | 56, 6 | syl6breqr 4695 |
. . . . . . . . . . 11
|
58 | 23, 34, 43, 45, 57 | xrletrd 11993 |
. . . . . . . . . 10
|
59 | 58 | adantr 481 |
. . . . . . . . 9
|
60 | 11, 17 | ltaddrpd 11905 |
. . . . . . . . 9
|
61 | 21, 11, 19, 59, 60 | lelttrd 10195 |
. . . . . . . 8
|
62 | 61 | gt0ne0d 10592 |
. . . . . . 7
|
63 | 12, 16, 20, 62 | div23d 10838 |
. . . . . 6
|
64 | 11, 19, 62 | redivcld 10853 |
. . . . . . . 8
|
65 | 64, 15 | remulcld 10070 |
. . . . . . 7
|
66 | | halfre 11246 |
. . . . . . . . 9
|
67 | | ifcl 4130 |
. . . . . . . . 9
|
68 | 64, 66, 67 | sylancl 694 |
. . . . . . . 8
|
69 | 68, 15 | remulcld 10070 |
. . . . . . 7
|
70 | | max2 12018 |
. . . . . . . . 9
|
71 | 66, 64, 70 | sylancr 695 |
. . . . . . . 8
|
72 | 7, 14 | syl 17 |
. . . . . . . . . . . . . 14
|
73 | 72 | rexrd 10089 |
. . . . . . . . . . . . 13
|
74 | | xrltnle 10105 |
. . . . . . . . . . . . 13
|
75 | 43, 73, 74 | syl2anc 693 |
. . . . . . . . . . . 12
|
76 | 9, 75 | mpbird 247 |
. . . . . . . . . . 11
|
77 | 76 | adantr 481 |
. . . . . . . . . 10
|
78 | 21, 11, 15, 59, 77 | lelttrd 10195 |
. . . . . . . . 9
|
79 | | lemul1 10875 |
. . . . . . . . 9
|
80 | 64, 68, 15, 78, 79 | syl112anc 1330 |
. . . . . . . 8
|
81 | 71, 80 | mpbid 222 |
. . . . . . 7
|
82 | 2 | adantlr 751 |
. . . . . . . 8
MblFn |
83 | 3 | adantlr 751 |
. . . . . . . 8
|
84 | 4 | adantlr 751 |
. . . . . . . 8
|
85 | 5 | adantlr 751 |
. . . . . . . 8
|
86 | 66 | a1i 11 |
. . . . . . . . . 10
|
87 | | halfgt0 11248 |
. . . . . . . . . . 11
|
88 | 87 | a1i 11 |
. . . . . . . . . 10
|
89 | | max1 12016 |
. . . . . . . . . . 11
|
90 | 66, 64, 89 | sylancr 695 |
. . . . . . . . . 10
|
91 | 21, 86, 68, 88, 90 | ltletrd 10197 |
. . . . . . . . 9
|
92 | 20 | mulid1d 10057 |
. . . . . . . . . . . 12
|
93 | 60, 92 | breqtrrd 4681 |
. . . . . . . . . . 11
|
94 | | 1red 10055 |
. . . . . . . . . . . 12
|
95 | | ltdivmul 10898 |
. . . . . . . . . . . 12
|
96 | 11, 94, 19, 61, 95 | syl112anc 1330 |
. . . . . . . . . . 11
|
97 | 93, 96 | mpbird 247 |
. . . . . . . . . 10
|
98 | | halflt1 11250 |
. . . . . . . . . 10
|
99 | | breq1 4656 |
. . . . . . . . . . 11
|
100 | | breq1 4656 |
. . . . . . . . . . 11
|
101 | 99, 100 | ifboth 4124 |
. . . . . . . . . 10
|
102 | 97, 98, 101 | sylancl 694 |
. . . . . . . . 9
|
103 | | 1re 10039 |
. . . . . . . . . . 11
|
104 | 103 | rexri 10097 |
. . . . . . . . . 10
|
105 | | elioo2 12216 |
. . . . . . . . . 10
|
106 | 22, 104, 105 | mp2an 708 |
. . . . . . . . 9
|
107 | 68, 91, 102, 106 | syl3anbrc 1246 |
. . . . . . . 8
|
108 | 8 | adantr 481 |
. . . . . . . 8
|
109 | | fveq2 6191 |
. . . . . . . . . . . 12
|
110 | 109 | oveq2d 6666 |
. . . . . . . . . . 11
|
111 | | fveq2 6191 |
. . . . . . . . . . 11
|
112 | 110, 111 | breq12d 4666 |
. . . . . . . . . 10
|
113 | 112 | cbvrabv 3199 |
. . . . . . . . 9
|
114 | 113 | mpteq2i 4741 |
. . . . . . . 8
|
115 | 1, 82, 83, 84, 85, 6, 107, 13, 108, 11, 114 | itg2monolem1 23517 |
. . . . . . 7
|
116 | 65, 69, 11, 81, 115 | letrd 10194 |
. . . . . 6
|
117 | 63, 116 | eqbrtrd 4675 |
. . . . 5
|
118 | 11, 15 | remulcld 10070 |
. . . . . 6
|
119 | | ledivmul2 10902 |
. . . . . 6
|
120 | 118, 11, 19, 61, 119 | syl112anc 1330 |
. . . . 5
|
121 | 117, 120 | mpbid 222 |
. . . 4
|
122 | 68, 15, 91, 78 | mulgt0d 10192 |
. . . . . 6
|
123 | 21, 69, 11, 122, 115 | ltletrd 10197 |
. . . . 5
|
124 | | lemul2 10876 |
. . . . 5
|
125 | 15, 19, 11, 123, 124 | syl112anc 1330 |
. . . 4
|
126 | 121, 125 | mpbird 247 |
. . 3
|
127 | 126 | ralrimiva 2966 |
. 2
|
128 | | alrple 12037 |
. . 3
|
129 | 72, 10, 128 | syl2anc 693 |
. 2
|
130 | 127, 129 | mpbird 247 |
1
|