Step | Hyp | Ref
| Expression |
1 | | simpr 103 |
. . . . 5
|
2 | | resqrexlemex.seq |
. . . . . . . . . . 11
|
3 | | resqrexlemex.a |
. . . . . . . . . . 11
|
4 | | resqrexlemex.agt0 |
. . . . . . . . . . 11
|
5 | 2, 3, 4 | resqrexlemf 9605 |
. . . . . . . . . 10
|
6 | 5 | adantr 261 |
. . . . . . . . 9
|
7 | | 1nn 7925 |
. . . . . . . . . 10
|
8 | 7 | a1i 9 |
. . . . . . . . 9
|
9 | 6, 8 | ffvelrnd 5303 |
. . . . . . . 8
|
10 | 9 | rpred 8622 |
. . . . . . 7
|
11 | | resqrexlemgt0.rr |
. . . . . . . 8
|
12 | 11 | adantr 261 |
. . . . . . 7
|
13 | 10, 12 | readdcld 7055 |
. . . . . 6
|
14 | 9 | rpgt0d 8625 |
. . . . . . 7
|
15 | | resqrexlemgt0.lim |
. . . . . . . . 9
|
16 | 2, 3, 4, 11, 15 | resqrexlemgt0 9618 |
. . . . . . . 8
|
17 | 16 | adantr 261 |
. . . . . . 7
|
18 | | addgtge0 7445 |
. . . . . . 7
|
19 | 10, 12, 14, 17, 18 | syl22anc 1136 |
. . . . . 6
|
20 | 13, 19 | elrpd 8620 |
. . . . 5
|
21 | 1, 20 | rpdivcld 8640 |
. . . 4
|
22 | | fveq2 5178 |
. . . . . . . . . . . 12
|
23 | 22 | breq1d 3774 |
. . . . . . . . . . 11
|
24 | 22 | oveq1d 5527 |
. . . . . . . . . . . 12
|
25 | 24 | breq2d 3776 |
. . . . . . . . . . 11
|
26 | 23, 25 | anbi12d 442 |
. . . . . . . . . 10
|
27 | 26 | cbvralv 2533 |
. . . . . . . . 9
|
28 | 27 | rexbii 2331 |
. . . . . . . 8
|
29 | 28 | ralbii 2330 |
. . . . . . 7
|
30 | 15, 29 | sylib 127 |
. . . . . 6
|
31 | | oveq2 5520 |
. . . . . . . . . 10
|
32 | 31 | breq2d 3776 |
. . . . . . . . 9
|
33 | | oveq2 5520 |
. . . . . . . . . 10
|
34 | 33 | breq2d 3776 |
. . . . . . . . 9
|
35 | 32, 34 | anbi12d 442 |
. . . . . . . 8
|
36 | 35 | rexralbidv 2350 |
. . . . . . 7
|
37 | 36 | cbvralv 2533 |
. . . . . 6
|
38 | 30, 37 | sylib 127 |
. . . . 5
|
39 | 38 | adantr 261 |
. . . 4
|
40 | | oveq2 5520 |
. . . . . . . 8
|
41 | 40 | breq2d 3776 |
. . . . . . 7
|
42 | | oveq2 5520 |
. . . . . . . 8
|
43 | 42 | breq2d 3776 |
. . . . . . 7
|
44 | 41, 43 | anbi12d 442 |
. . . . . 6
|
45 | 44 | rexralbidv 2350 |
. . . . 5
|
46 | 45 | rspcv 2652 |
. . . 4
|
47 | 21, 39, 46 | sylc 56 |
. . 3
|
48 | | simpllr 486 |
. . . . . . . . . 10
|
49 | | simplr 482 |
. . . . . . . . . 10
|
50 | | eluznn 8538 |
. . . . . . . . . 10
|
51 | 48, 49, 50 | syl2anc 391 |
. . . . . . . . 9
|
52 | 6 | ad3antrrr 461 |
. . . . . . . . . . 11
|
53 | 52, 51 | ffvelrnd 5303 |
. . . . . . . . . 10
|
54 | | 2z 8273 |
. . . . . . . . . . 11
|
55 | 54 | a1i 9 |
. . . . . . . . . 10
|
56 | 53, 55 | rpexpcld 9404 |
. . . . . . . . 9
|
57 | | fveq2 5178 |
. . . . . . . . . . 11
|
58 | 57 | oveq1d 5527 |
. . . . . . . . . 10
|
59 | | resqrexlemsqa.g |
. . . . . . . . . 10
|
60 | 58, 59 | fvmptg 5248 |
. . . . . . . . 9
|
61 | 51, 56, 60 | syl2anc 391 |
. . . . . . . 8
|
62 | 53 | rpred 8622 |
. . . . . . . . . . . 12
|
63 | 62 | recnd 7054 |
. . . . . . . . . . 11
|
64 | 12 | ad3antrrr 461 |
. . . . . . . . . . . 12
|
65 | 64 | recnd 7054 |
. . . . . . . . . . 11
|
66 | | subsq 9358 |
. . . . . . . . . . 11
|
67 | 63, 65, 66 | syl2anc 391 |
. . . . . . . . . 10
|
68 | 62, 64 | readdcld 7055 |
. . . . . . . . . . . 12
|
69 | 62, 64 | resubcld 7379 |
. . . . . . . . . . . 12
|
70 | 68, 69 | remulcld 7056 |
. . . . . . . . . . 11
|
71 | 13 | ad3antrrr 461 |
. . . . . . . . . . . 12
|
72 | 71, 69 | remulcld 7056 |
. . . . . . . . . . 11
|
73 | 1 | ad3antrrr 461 |
. . . . . . . . . . . 12
|
74 | 73 | rpred 8622 |
. . . . . . . . . . 11
|
75 | 3 | ad4antr 463 |
. . . . . . . . . . . . . 14
|
76 | 4 | ad4antr 463 |
. . . . . . . . . . . . . 14
|
77 | 15 | ad4antr 463 |
. . . . . . . . . . . . . 14
|
78 | 2, 75, 76, 64, 77, 51 | resqrexlemoverl 9619 |
. . . . . . . . . . . . 13
|
79 | 62, 64 | subge0d 7526 |
. . . . . . . . . . . . 13
|
80 | 78, 79 | mpbird 156 |
. . . . . . . . . . . 12
|
81 | | fveq2 5178 |
. . . . . . . . . . . . . . 15
|
82 | 81 | oveq1d 5527 |
. . . . . . . . . . . . . 14
|
83 | | eqle 7109 |
. . . . . . . . . . . . . 14
|
84 | 68, 82, 83 | syl2an 273 |
. . . . . . . . . . . . 13
|
85 | 62 | adantr 261 |
. . . . . . . . . . . . . 14
|
86 | 10 | ad4antr 463 |
. . . . . . . . . . . . . 14
|
87 | 64 | adantr 261 |
. . . . . . . . . . . . . 14
|
88 | 3 | ad5antr 465 |
. . . . . . . . . . . . . . . 16
|
89 | 4 | ad5antr 465 |
. . . . . . . . . . . . . . . 16
|
90 | 7 | a1i 9 |
. . . . . . . . . . . . . . . 16
|
91 | 51 | adantr 261 |
. . . . . . . . . . . . . . . 16
|
92 | | simpr 103 |
. . . . . . . . . . . . . . . 16
|
93 | 2, 88, 89, 90, 91, 92 | resqrexlemdecn 9610 |
. . . . . . . . . . . . . . 15
|
94 | 85, 86, 93 | ltled 7135 |
. . . . . . . . . . . . . 14
|
95 | 85, 86, 87, 94 | leadd1dd 7550 |
. . . . . . . . . . . . 13
|
96 | | nn1gt1 7947 |
. . . . . . . . . . . . . 14
|
97 | 51, 96 | syl 14 |
. . . . . . . . . . . . 13
|
98 | 84, 95, 97 | mpjaodan 711 |
. . . . . . . . . . . 12
|
99 | 68, 71, 69, 80, 98 | lemul1ad 7905 |
. . . . . . . . . . 11
|
100 | | simprl 483 |
. . . . . . . . . . . . 13
|
101 | 21 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
|
102 | 101 | rpred 8622 |
. . . . . . . . . . . . . 14
|
103 | 62, 64, 102 | ltsubadd2d 7534 |
. . . . . . . . . . . . 13
|
104 | 100, 103 | mpbird 156 |
. . . . . . . . . . . 12
|
105 | 20 | ad3antrrr 461 |
. . . . . . . . . . . . 13
|
106 | 69, 74, 105 | ltmuldiv2d 8671 |
. . . . . . . . . . . 12
|
107 | 104, 106 | mpbird 156 |
. . . . . . . . . . 11
|
108 | 70, 72, 74, 99, 107 | lelttrd 7139 |
. . . . . . . . . 10
|
109 | 67, 108 | eqbrtrd 3784 |
. . . . . . . . 9
|
110 | 62 | resqcld 9406 |
. . . . . . . . . 10
|
111 | 64 | resqcld 9406 |
. . . . . . . . . 10
|
112 | 110, 111,
74 | ltsubadd2d 7534 |
. . . . . . . . 9
|
113 | 109, 112 | mpbid 135 |
. . . . . . . 8
|
114 | 61, 113 | eqbrtrd 3784 |
. . . . . . 7
|
115 | 61, 110 | eqeltrd 2114 |
. . . . . . . 8
|
116 | 115, 74 | readdcld 7055 |
. . . . . . . 8
|
117 | 17 | ad3antrrr 461 |
. . . . . . . . . 10
|
118 | | le2sq2 9329 |
. . . . . . . . . 10
|
119 | 64, 117, 62, 78, 118 | syl22anc 1136 |
. . . . . . . . 9
|
120 | 119, 61 | breqtrrd 3790 |
. . . . . . . 8
|
121 | 115, 73 | ltaddrpd 8656 |
. . . . . . . 8
|
122 | 111, 115,
116, 120, 121 | lelttrd 7139 |
. . . . . . 7
|
123 | 114, 122 | jca 290 |
. . . . . 6
|
124 | 123 | ex 108 |
. . . . 5
|
125 | 124 | ralimdva 2387 |
. . . 4
|
126 | 125 | reximdva 2421 |
. . 3
|
127 | 47, 126 | mpd 13 |
. 2
|
128 | 127 | ralrimiva 2392 |
1
|