Step | Hyp | Ref
| Expression |
1 | | 2re 11090 |
. . . . 5
|
2 | | simp1 1061 |
. . . . 5
|
3 | | remulcl 10021 |
. . . . 5
|
4 | 1, 2, 3 | sylancr 695 |
. . . 4
|
5 | | simp3 1063 |
. . . . 5
|
6 | | 1re 10039 |
. . . . . 6
|
7 | | simp2 1062 |
. . . . . 6
|
8 | | difrp 11868 |
. . . . . 6
|
9 | 6, 7, 8 | sylancr 695 |
. . . . 5
|
10 | 5, 9 | mpbid 222 |
. . . 4
|
11 | 4, 10 | rerpdivcld 11903 |
. . 3
|
12 | | expnbnd 12993 |
. . 3
|
13 | 11, 7, 5, 12 | syl3anc 1326 |
. 2
|
14 | | 2nn0 11309 |
. . . 4
|
15 | | nnnn0 11299 |
. . . . 5
|
16 | 15 | ad2antrl 764 |
. . . 4
|
17 | | nn0mulcl 11329 |
. . . 4
|
18 | 14, 16, 17 | sylancr 695 |
. . 3
|
19 | 2 | ad2antrr 762 |
. . . . . 6
|
20 | | 2nn 11185 |
. . . . . . . . 9
|
21 | | simprl 794 |
. . . . . . . . 9
|
22 | | nnmulcl 11043 |
. . . . . . . . 9
|
23 | 20, 21, 22 | sylancr 695 |
. . . . . . . 8
|
24 | | eluznn 11758 |
. . . . . . . 8
|
25 | 23, 24 | sylan 488 |
. . . . . . 7
|
26 | 25 | nnred 11035 |
. . . . . 6
|
27 | 19, 26 | remulcld 10070 |
. . . . 5
|
28 | | 0re 10040 |
. . . . . . . 8
|
29 | | ifcl 4130 |
. . . . . . . 8
|
30 | 19, 28, 29 | sylancl 694 |
. . . . . . 7
|
31 | | remulcl 10021 |
. . . . . . 7
|
32 | 1, 30, 31 | sylancr 695 |
. . . . . 6
|
33 | | simplrl 800 |
. . . . . . . 8
|
34 | 33 | nnred 11035 |
. . . . . . 7
|
35 | 26, 34 | resubcld 10458 |
. . . . . 6
|
36 | 32, 35 | remulcld 10070 |
. . . . 5
|
37 | 7 | ad2antrr 762 |
. . . . . 6
|
38 | 25 | nnnn0d 11351 |
. . . . . 6
|
39 | | reexpcl 12877 |
. . . . . 6
|
40 | 37, 38, 39 | syl2anc 693 |
. . . . 5
|
41 | | remulcl 10021 |
. . . . . . . 8
|
42 | 1, 35, 41 | sylancr 695 |
. . . . . . 7
|
43 | 38 | nn0ge0d 11354 |
. . . . . . 7
|
44 | | max1 12016 |
. . . . . . . 8
|
45 | 28, 19, 44 | sylancr 695 |
. . . . . . 7
|
46 | | remulcl 10021 |
. . . . . . . . . . . 12
|
47 | 1, 34, 46 | sylancr 695 |
. . . . . . . . . . 11
|
48 | | eluzle 11700 |
. . . . . . . . . . . 12
|
49 | 48 | adantl 482 |
. . . . . . . . . . 11
|
50 | 47, 26, 26, 49 | leadd2dd 10642 |
. . . . . . . . . 10
|
51 | 26 | recnd 10068 |
. . . . . . . . . . 11
|
52 | 51 | 2timesd 11275 |
. . . . . . . . . 10
|
53 | 50, 52 | breqtrrd 4681 |
. . . . . . . . 9
|
54 | | remulcl 10021 |
. . . . . . . . . . 11
|
55 | 1, 26, 54 | sylancr 695 |
. . . . . . . . . 10
|
56 | | leaddsub 10504 |
. . . . . . . . . 10
|
57 | 26, 47, 55, 56 | syl3anc 1326 |
. . . . . . . . 9
|
58 | 53, 57 | mpbid 222 |
. . . . . . . 8
|
59 | | 2cnd 11093 |
. . . . . . . . 9
|
60 | 34 | recnd 10068 |
. . . . . . . . 9
|
61 | 59, 51, 60 | subdid 10486 |
. . . . . . . 8
|
62 | 58, 61 | breqtrrd 4681 |
. . . . . . 7
|
63 | | max2 12018 |
. . . . . . . 8
|
64 | 28, 19, 63 | sylancr 695 |
. . . . . . 7
|
65 | 26, 42, 19, 30, 43, 45, 62, 64 | lemul12bd 10967 |
. . . . . 6
|
66 | 19 | recnd 10068 |
. . . . . . 7
|
67 | 66, 51 | mulcomd 10061 |
. . . . . 6
|
68 | 30 | recnd 10068 |
. . . . . . 7
|
69 | 35 | recnd 10068 |
. . . . . . 7
|
70 | 59, 68, 69 | mul32d 10246 |
. . . . . 6
|
71 | 65, 67, 70 | 3brtr4d 4685 |
. . . . 5
|
72 | 10 | ad2antrr 762 |
. . . . . . . . 9
|
73 | 72 | rpred 11872 |
. . . . . . . 8
|
74 | 73, 35 | remulcld 10070 |
. . . . . . 7
|
75 | 33 | nnnn0d 11351 |
. . . . . . . 8
|
76 | | reexpcl 12877 |
. . . . . . . 8
|
77 | 37, 75, 76 | syl2anc 693 |
. . . . . . 7
|
78 | 74, 77 | remulcld 10070 |
. . . . . 6
|
79 | | simplrr 801 |
. . . . . . . . . 10
|
80 | 1, 19, 3 | sylancr 695 |
. . . . . . . . . . 11
|
81 | 80, 77, 72 | ltdivmuld 11923 |
. . . . . . . . . 10
|
82 | 79, 81 | mpbid 222 |
. . . . . . . . 9
|
83 | 5 | ad2antrr 762 |
. . . . . . . . . . 11
|
84 | | posdif 10521 |
. . . . . . . . . . . 12
|
85 | 6, 37, 84 | sylancr 695 |
. . . . . . . . . . 11
|
86 | 83, 85 | mpbid 222 |
. . . . . . . . . 10
|
87 | 33 | nnzd 11481 |
. . . . . . . . . . 11
|
88 | 28 | a1i 11 |
. . . . . . . . . . . 12
|
89 | 6 | a1i 11 |
. . . . . . . . . . . 12
|
90 | | 0lt1 10550 |
. . . . . . . . . . . . 13
|
91 | 90 | a1i 11 |
. . . . . . . . . . . 12
|
92 | 88, 89, 37, 91, 83 | lttrd 10198 |
. . . . . . . . . . 11
|
93 | | expgt0 12893 |
. . . . . . . . . . 11
|
94 | 37, 87, 92, 93 | syl3anc 1326 |
. . . . . . . . . 10
|
95 | 73, 77, 86, 94 | mulgt0d 10192 |
. . . . . . . . 9
|
96 | | oveq2 6658 |
. . . . . . . . . . 11
|
97 | 96 | breq1d 4663 |
. . . . . . . . . 10
|
98 | | 2t0e0 11183 |
. . . . . . . . . . . 12
|
99 | | oveq2 6658 |
. . . . . . . . . . . 12
|
100 | 98, 99 | syl5eqr 2670 |
. . . . . . . . . . 11
|
101 | 100 | breq1d 4663 |
. . . . . . . . . 10
|
102 | 97, 101 | ifboth 4124 |
. . . . . . . . 9
|
103 | 82, 95, 102 | syl2anc 693 |
. . . . . . . 8
|
104 | 73, 77 | remulcld 10070 |
. . . . . . . . 9
|
105 | | simpr 477 |
. . . . . . . . . . . . 13
|
106 | 60 | 2timesd 11275 |
. . . . . . . . . . . . . 14
|
107 | 106 | fveq2d 6195 |
. . . . . . . . . . . . 13
|
108 | 105, 107 | eleqtrd 2703 |
. . . . . . . . . . . 12
|
109 | | eluzsub 11717 |
. . . . . . . . . . . 12
|
110 | 87, 87, 108, 109 | syl3anc 1326 |
. . . . . . . . . . 11
|
111 | | eluznn 11758 |
. . . . . . . . . . 11
|
112 | 33, 110, 111 | syl2anc 693 |
. . . . . . . . . 10
|
113 | 112 | nngt0d 11064 |
. . . . . . . . 9
|
114 | | ltmul1 10873 |
. . . . . . . . 9
|
115 | 32, 104, 35, 113, 114 | syl112anc 1330 |
. . . . . . . 8
|
116 | 103, 115 | mpbid 222 |
. . . . . . 7
|
117 | 73 | recnd 10068 |
. . . . . . . 8
|
118 | 77 | recnd 10068 |
. . . . . . . 8
|
119 | 117, 118,
69 | mul32d 10246 |
. . . . . . 7
|
120 | 116, 119 | breqtrd 4679 |
. . . . . 6
|
121 | | peano2re 10209 |
. . . . . . . . . 10
|
122 | 74, 121 | syl 17 |
. . . . . . . . 9
|
123 | 112 | nnnn0d 11351 |
. . . . . . . . . 10
|
124 | | reexpcl 12877 |
. . . . . . . . . 10
|
125 | 37, 123, 124 | syl2anc 693 |
. . . . . . . . 9
|
126 | 74 | ltp1d 10954 |
. . . . . . . . 9
|
127 | 88, 37, 92 | ltled 10185 |
. . . . . . . . . 10
|
128 | | bernneq2 12991 |
. . . . . . . . . 10
|
129 | 37, 123, 127, 128 | syl3anc 1326 |
. . . . . . . . 9
|
130 | 74, 122, 125, 126, 129 | ltletrd 10197 |
. . . . . . . 8
|
131 | 37 | recnd 10068 |
. . . . . . . . 9
|
132 | 92 | gt0ne0d 10592 |
. . . . . . . . 9
|
133 | | eluzelz 11697 |
. . . . . . . . . 10
|
134 | 133 | adantl 482 |
. . . . . . . . 9
|
135 | | expsub 12908 |
. . . . . . . . 9
|
136 | 131, 132,
134, 87, 135 | syl22anc 1327 |
. . . . . . . 8
|
137 | 130, 136 | breqtrd 4679 |
. . . . . . 7
|
138 | | ltmuldiv 10896 |
. . . . . . . 8
|
139 | 74, 40, 77, 94, 138 | syl112anc 1330 |
. . . . . . 7
|
140 | 137, 139 | mpbird 247 |
. . . . . 6
|
141 | 36, 78, 40, 120, 140 | lttrd 10198 |
. . . . 5
|
142 | 27, 36, 40, 71, 141 | lelttrd 10195 |
. . . 4
|
143 | 142 | ralrimiva 2966 |
. . 3
|
144 | | fveq2 6191 |
. . . . 5
|
145 | 144 | raleqdv 3144 |
. . . 4
|
146 | 145 | rspcev 3309 |
. . 3
|
147 | 18, 143, 146 | syl2anc 693 |
. 2
|
148 | 13, 147 | rexlimddv 3035 |
1
|