Step | Hyp | Ref
| Expression |
1 | | climinf.5 |
. . . . . . . . . . . 12
|
2 | | frn 6053 |
. . . . . . . . . . . 12
|
3 | 1, 2 | syl 17 |
. . . . . . . . . . 11
|
4 | | ffn 6045 |
. . . . . . . . . . . . . 14
|
5 | 1, 4 | syl 17 |
. . . . . . . . . . . . 13
|
6 | | climinf.4 |
. . . . . . . . . . . . . . 15
|
7 | | uzid 11702 |
. . . . . . . . . . . . . . 15
|
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . 14
|
9 | | climinf.3 |
. . . . . . . . . . . . . 14
|
10 | 8, 9 | syl6eleqr 2712 |
. . . . . . . . . . . . 13
|
11 | | fnfvelrn 6356 |
. . . . . . . . . . . . 13
|
12 | 5, 10, 11 | syl2anc 693 |
. . . . . . . . . . . 12
|
13 | | ne0i 3921 |
. . . . . . . . . . . 12
|
14 | 12, 13 | syl 17 |
. . . . . . . . . . 11
|
15 | | climinf.7 |
. . . . . . . . . . . 12
|
16 | | breq2 4657 |
. . . . . . . . . . . . . . 15
|
17 | 16 | ralrn 6362 |
. . . . . . . . . . . . . 14
|
18 | 17 | rexbidv 3052 |
. . . . . . . . . . . . 13
|
19 | 5, 18 | syl 17 |
. . . . . . . . . . . 12
|
20 | 15, 19 | mpbird 247 |
. . . . . . . . . . 11
|
21 | 3, 14, 20 | 3jca 1242 |
. . . . . . . . . 10
|
22 | 21 | adantr 481 |
. . . . . . . . 9
|
23 | | infrecl 11005 |
. . . . . . . . 9
inf |
24 | 22, 23 | syl 17 |
. . . . . . . 8
inf |
25 | | simpr 477 |
. . . . . . . 8
|
26 | 24, 25 | ltaddrpd 11905 |
. . . . . . 7
inf inf |
27 | | rpre 11839 |
. . . . . . . . . 10
|
28 | 27 | adantl 482 |
. . . . . . . . 9
|
29 | 24, 28 | readdcld 10069 |
. . . . . . . 8
inf |
30 | | infrglb 39822 |
. . . . . . . 8
inf inf inf inf |
31 | 22, 29, 30 | syl2anc 693 |
. . . . . . 7
inf inf inf |
32 | 26, 31 | mpbid 222 |
. . . . . 6
inf |
33 | 3 | sselda 3603 |
. . . . . . . . . . 11
|
34 | 33 | adantlr 751 |
. . . . . . . . . 10
|
35 | 24 | adantr 481 |
. . . . . . . . . . 11
inf |
36 | 27 | ad2antlr 763 |
. . . . . . . . . . 11
|
37 | 35, 36 | readdcld 10069 |
. . . . . . . . . 10
inf |
38 | 34, 37, 36 | ltsub1d 10636 |
. . . . . . . . 9
inf inf |
39 | 3, 14, 20, 23 | syl3anc 1326 |
. . . . . . . . . . . . 13
inf
|
40 | 39 | recnd 10068 |
. . . . . . . . . . . 12
inf
|
41 | 40 | ad2antrr 762 |
. . . . . . . . . . 11
inf |
42 | 36 | recnd 10068 |
. . . . . . . . . . 11
|
43 | 41, 42 | pncand 10393 |
. . . . . . . . . 10
inf inf
|
44 | 43 | breq2d 4665 |
. . . . . . . . 9
inf
inf |
45 | 38, 44 | bitrd 268 |
. . . . . . . 8
inf inf |
46 | 45 | biimpd 219 |
. . . . . . 7
inf
inf |
47 | 46 | reximdva 3017 |
. . . . . 6
inf
inf |
48 | 32, 47 | mpd 15 |
. . . . 5
inf |
49 | | oveq1 6657 |
. . . . . . . . 9
|
50 | 49 | breq1d 4663 |
. . . . . . . 8
inf
inf |
51 | 50 | rexrn 6361 |
. . . . . . 7
inf
inf |
52 | 5, 51 | syl 17 |
. . . . . 6
inf
inf |
53 | 52 | biimpa 501 |
. . . . 5
inf
inf |
54 | 48, 53 | syldan 487 |
. . . 4
inf |
55 | 1 | adantr 481 |
. . . . . . . . . . 11
|
56 | 9 | uztrn2 11705 |
. . . . . . . . . . 11
|
57 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
58 | 55, 56, 57 | syl2an 494 |
. . . . . . . . . 10
|
59 | | simpl 473 |
. . . . . . . . . . 11
|
60 | | ffvelrn 6357 |
. . . . . . . . . . 11
|
61 | 55, 59, 60 | syl2an 494 |
. . . . . . . . . 10
|
62 | 39 | ad2antrr 762 |
. . . . . . . . . 10
inf |
63 | | simprr 796 |
. . . . . . . . . . 11
|
64 | | fzssuz 12382 |
. . . . . . . . . . . . . 14
|
65 | | uzss 11708 |
. . . . . . . . . . . . . . . . 17
|
66 | 65, 9 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . 16
|
67 | 66, 9 | eleq2s 2719 |
. . . . . . . . . . . . . . 15
|
68 | 67 | ad2antrl 764 |
. . . . . . . . . . . . . 14
|
69 | 64, 68 | syl5ss 3614 |
. . . . . . . . . . . . 13
|
70 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
|
71 | 70 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
|
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . 14
|
73 | 72 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
74 | | ssralv 3666 |
. . . . . . . . . . . . 13
|
75 | 69, 73, 74 | sylc 65 |
. . . . . . . . . . . 12
|
76 | 75 | r19.21bi 2932 |
. . . . . . . . . . 11
|
77 | | fzssuz 12382 |
. . . . . . . . . . . . . 14
|
78 | 77, 68 | syl5ss 3614 |
. . . . . . . . . . . . 13
|
79 | 78 | sselda 3603 |
. . . . . . . . . . . 12
|
80 | | climinf.6 |
. . . . . . . . . . . . . . 15
|
81 | 80 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
|
82 | 81 | ad2antrr 762 |
. . . . . . . . . . . . 13
|
83 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
84 | 83 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
|
85 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
|
86 | 84, 85 | breq12d 4666 |
. . . . . . . . . . . . . 14
|
87 | 86 | rspccva 3308 |
. . . . . . . . . . . . 13
|
88 | 82, 87 | sylan 488 |
. . . . . . . . . . . 12
|
89 | 79, 88 | syldan 487 |
. . . . . . . . . . 11
|
90 | 63, 76, 89 | monoord2 12832 |
. . . . . . . . . 10
|
91 | 58, 61, 62, 90 | lesub1dd 10643 |
. . . . . . . . 9
inf inf |
92 | 58, 62 | resubcld 10458 |
. . . . . . . . . 10
inf |
93 | 61, 62 | resubcld 10458 |
. . . . . . . . . 10
inf |
94 | 27 | ad2antlr 763 |
. . . . . . . . . 10
|
95 | | lelttr 10128 |
. . . . . . . . . 10
inf inf
inf
inf
inf
inf |
96 | 92, 93, 94, 95 | syl3anc 1326 |
. . . . . . . . 9
inf
inf
inf
inf |
97 | 91, 96 | mpand 711 |
. . . . . . . 8
inf
inf |
98 | | ltsub23 10508 |
. . . . . . . . 9
inf inf
inf
|
99 | 61, 94, 62, 98 | syl3anc 1326 |
. . . . . . . 8
inf
inf
|
100 | 3 | ad2antrr 762 |
. . . . . . . . . . 11
|
101 | 5 | adantr 481 |
. . . . . . . . . . . 12
|
102 | | fnfvelrn 6356 |
. . . . . . . . . . . 12
|
103 | 101, 56, 102 | syl2an 494 |
. . . . . . . . . . 11
|
104 | 100, 103 | sseldd 3604 |
. . . . . . . . . 10
|
105 | 20 | ad2antrr 762 |
. . . . . . . . . . 11
|
106 | | infrelb 11008 |
. . . . . . . . . . 11
inf |
107 | 100, 105,
103, 106 | syl3anc 1326 |
. . . . . . . . . 10
inf |
108 | 62, 104, 107 | abssubge0d 14170 |
. . . . . . . . 9
inf
inf |
109 | 108 | breq1d 4663 |
. . . . . . . 8
inf inf |
110 | 97, 99, 109 | 3imtr4d 283 |
. . . . . . 7
inf inf |
111 | 110 | anassrs 680 |
. . . . . 6
inf inf |
112 | 111 | ralrimdva 2969 |
. . . . 5
inf inf |
113 | 112 | reximdva 3017 |
. . . 4
inf
inf |
114 | 54, 113 | mpd 15 |
. . 3
inf |
115 | 114 | ralrimiva 2966 |
. 2
inf |
116 | | fvex 6201 |
. . . . 5
|
117 | 9, 116 | eqeltri 2697 |
. . . 4
|
118 | | fex 6490 |
. . . 4
|
119 | 1, 117, 118 | sylancl 694 |
. . 3
|
120 | | eqidd 2623 |
. . 3
|
121 | 1 | ffvelrnda 6359 |
. . . 4
|
122 | 121 | recnd 10068 |
. . 3
|
123 | 9, 6, 119, 120, 40, 122 | clim2c 14236 |
. 2
inf
inf |
124 | 115, 123 | mpbird 247 |
1
inf |