Proof of Theorem reccn2ap
Step | Hyp | Ref
| Expression |
1 | | reccn2ap.t |
. . 3
inf |
2 | | 1red 7922 |
. . . . . 6
#
|
3 | | simp1 992 |
. . . . . . . . 9
#
|
4 | | simp2 993 |
. . . . . . . . 9
#
# |
5 | 3, 4 | absrpclapd 11139 |
. . . . . . . 8
#
|
6 | | simp3 994 |
. . . . . . . 8
#
|
7 | 5, 6 | rpmulcld 9657 |
. . . . . . 7
#
|
8 | 7 | rpred 9640 |
. . . . . 6
#
|
9 | | mincl 11181 |
. . . . . 6
inf |
10 | 2, 8, 9 | syl2anc 409 |
. . . . 5
#
inf |
11 | 7 | rpgt0d 9643 |
. . . . . . 7
#
|
12 | | 0lt1 8033 |
. . . . . . 7
|
13 | 11, 12 | jctil 310 |
. . . . . 6
#
|
14 | | 0red 7908 |
. . . . . . 7
#
|
15 | | ltmininf 11185 |
. . . . . . 7
inf |
16 | 14, 2, 8, 15 | syl3anc 1233 |
. . . . . 6
#
inf
|
17 | 13, 16 | mpbird 166 |
. . . . 5
#
inf |
18 | 10, 17 | elrpd 9637 |
. . . 4
#
inf |
19 | 5 | rphalfcld 9653 |
. . . 4
#
|
20 | 18, 19 | rpmulcld 9657 |
. . 3
#
inf |
21 | 1, 20 | eqeltrid 2257 |
. 2
#
|
22 | 3 | adantr 274 |
. . . . . . . . 9
# # |
23 | | simprl 526 |
. . . . . . . . . . 11
# # #
|
24 | | breq1 3990 |
. . . . . . . . . . . 12
#
# |
25 | 24 | elrab 2886 |
. . . . . . . . . . 11
# # |
26 | 23, 25 | sylib 121 |
. . . . . . . . . 10
# # # |
27 | 26 | simpld 111 |
. . . . . . . . 9
# # |
28 | 22, 27 | mulcld 7927 |
. . . . . . . . 9
# #
|
29 | 4 | adantr 274 |
. . . . . . . . . 10
# # # |
30 | 26 | simprd 113 |
. . . . . . . . . 10
# # # |
31 | 22, 27, 29, 30 | mulap0d 8563 |
. . . . . . . . 9
# #
# |
32 | 22, 27, 28, 31 | divsubdirapd 8734 |
. . . . . . . 8
# #
|
33 | 22 | mulid1d 7924 |
. . . . . . . . . . 11
# #
|
34 | 33 | oveq1d 5865 |
. . . . . . . . . 10
# # |
35 | | 1cnd 7923 |
. . . . . . . . . . 11
# # |
36 | 35, 27, 22, 30, 29 | divcanap5d 8721 |
. . . . . . . . . 10
# # |
37 | 34, 36 | eqtr3d 2205 |
. . . . . . . . 9
# # |
38 | 27 | mulid1d 7924 |
. . . . . . . . . . 11
# # |
39 | 27, 22 | mulcomd 7928 |
. . . . . . . . . . 11
# # |
40 | 38, 39 | oveq12d 5868 |
. . . . . . . . . 10
# # |
41 | 35, 22, 27, 29, 30 | divcanap5d 8721 |
. . . . . . . . . 10
# # |
42 | 40, 41 | eqtr3d 2205 |
. . . . . . . . 9
# # |
43 | 37, 42 | oveq12d 5868 |
. . . . . . . 8
# #
|
44 | 32, 43 | eqtrd 2203 |
. . . . . . 7
# # |
45 | 44 | fveq2d 5498 |
. . . . . 6
# # |
46 | 22, 27 | subcld 8217 |
. . . . . . 7
# #
|
47 | 46, 28, 31 | absdivapd 11146 |
. . . . . 6
# #
|
48 | 45, 47 | eqtr3d 2205 |
. . . . 5
# #
|
49 | 46 | abscld 11132 |
. . . . . . 7
# # |
50 | 21 | adantr 274 |
. . . . . . . 8
# # |
51 | 50 | rpred 9640 |
. . . . . . 7
# # |
52 | 28 | abscld 11132 |
. . . . . . . 8
# # |
53 | 6 | rpred 9640 |
. . . . . . . . 9
#
|
54 | 53 | adantr 274 |
. . . . . . . 8
# # |
55 | 52, 54 | remulcld 7937 |
. . . . . . 7
# #
|
56 | 22, 27 | abssubd 11144 |
. . . . . . . 8
# # |
57 | | simprr 527 |
. . . . . . . 8
# # |
58 | 56, 57 | eqbrtrd 4009 |
. . . . . . 7
# # |
59 | 7 | adantr 274 |
. . . . . . . . . 10
# # |
60 | 59 | rpred 9640 |
. . . . . . . . 9
# # |
61 | 19 | adantr 274 |
. . . . . . . . . 10
# # |
62 | 61 | rpred 9640 |
. . . . . . . . 9
# # |
63 | 60, 62 | remulcld 7937 |
. . . . . . . 8
# # |
64 | | 1re 7906 |
. . . . . . . . . . 11
|
65 | | min2inf 11183 |
. . . . . . . . . . 11
inf
|
66 | 64, 60, 65 | sylancr 412 |
. . . . . . . . . 10
# # inf |
67 | 10 | adantr 274 |
. . . . . . . . . . 11
# # inf |
68 | 67, 60, 61 | lemul1d 9684 |
. . . . . . . . . 10
# # inf
inf |
69 | 66, 68 | mpbid 146 |
. . . . . . . . 9
# # inf |
70 | 1, 69 | eqbrtrid 4022 |
. . . . . . . 8
# # |
71 | 27 | abscld 11132 |
. . . . . . . . . 10
# # |
72 | 22 | abscld 11132 |
. . . . . . . . . . . . . 14
# # |
73 | 72 | recnd 7935 |
. . . . . . . . . . . . 13
# # |
74 | 73 | 2halvesd 9110 |
. . . . . . . . . . . 12
# # |
75 | 72, 71 | resubcld 8287 |
. . . . . . . . . . . . . 14
# # |
76 | 27, 22 | subcld 8217 |
. . . . . . . . . . . . . . . 16
# # |
77 | 76 | abscld 11132 |
. . . . . . . . . . . . . . 15
# # |
78 | 56, 77 | eqeltrd 2247 |
. . . . . . . . . . . . . 14
# # |
79 | 22, 27 | abs2difd 11148 |
. . . . . . . . . . . . . 14
# #
|
80 | | min1inf 11182 |
. . . . . . . . . . . . . . . . . . 19
inf
|
81 | 64, 60, 80 | sylancr 412 |
. . . . . . . . . . . . . . . . . 18
# # inf |
82 | | 1red 7922 |
. . . . . . . . . . . . . . . . . . 19
# # |
83 | 67, 82, 61 | lemul1d 9684 |
. . . . . . . . . . . . . . . . . 18
# # inf
inf |
84 | 81, 83 | mpbid 146 |
. . . . . . . . . . . . . . . . 17
# # inf |
85 | 1, 84 | eqbrtrid 4022 |
. . . . . . . . . . . . . . . 16
# # |
86 | 62 | recnd 7935 |
. . . . . . . . . . . . . . . . 17
# # |
87 | 86 | mulid2d 7925 |
. . . . . . . . . . . . . . . 16
# # |
88 | 85, 87 | breqtrd 4013 |
. . . . . . . . . . . . . . 15
# # |
89 | 78, 51, 62, 58, 88 | ltletrd 8329 |
. . . . . . . . . . . . . 14
# # |
90 | 75, 78, 62, 79, 89 | lelttrd 8031 |
. . . . . . . . . . . . 13
# # |
91 | 72, 71, 62 | ltsubadd2d 8449 |
. . . . . . . . . . . . 13
# #
|
92 | 90, 91 | mpbid 146 |
. . . . . . . . . . . 12
# # |
93 | 74, 92 | eqbrtrd 4009 |
. . . . . . . . . . 11
# # |
94 | 62, 71, 62 | ltadd1d 8444 |
. . . . . . . . . . 11
# # |
95 | 93, 94 | mpbird 166 |
. . . . . . . . . 10
# # |
96 | 62, 71, 59, 95 | ltmul2dd 9697 |
. . . . . . . . 9
# # |
97 | 22, 27 | absmuld 11145 |
. . . . . . . . . . 11
# # |
98 | 97 | oveq1d 5865 |
. . . . . . . . . 10
# #
|
99 | 71 | recnd 7935 |
. . . . . . . . . . 11
# # |
100 | 54 | recnd 7935 |
. . . . . . . . . . 11
# # |
101 | 73, 99, 100 | mul32d 8059 |
. . . . . . . . . 10
# # |
102 | 98, 101 | eqtrd 2203 |
. . . . . . . . 9
# #
|
103 | 96, 102 | breqtrrd 4015 |
. . . . . . . 8
# #
|
104 | 51, 63, 55, 70, 103 | lelttrd 8031 |
. . . . . . 7
# #
|
105 | 49, 51, 55, 58, 104 | lttrd 8032 |
. . . . . 6
# #
|
106 | 28, 31 | absrpclapd 11139 |
. . . . . . 7
# # |
107 | 49, 54, 106 | ltdivmuld 9692 |
. . . . . 6
# #
|
108 | 105, 107 | mpbird 166 |
. . . . 5
# #
|
109 | 48, 108 | eqbrtrd 4009 |
. . . 4
# # |
110 | 109 | expr 373 |
. . 3
# #
|
111 | 110 | ralrimiva 2543 |
. 2
#
#
|
112 | | breq2 3991 |
. . 3
|
113 | 112 | rspceaimv 2842 |
. 2
#
#
|
114 | 21, 111, 113 | syl2anc 409 |
1
#
#
|