Step | Hyp | Ref
| Expression |
1 | | abscl 14018 |
. . . 4
|
2 | 1 | ralimi 2952 |
. . 3
|
3 | | cau3.1 |
. . . . . . 7
|
4 | 3 | r19.29uz 14090 |
. . . . . 6
|
5 | 4 | ex 450 |
. . . . 5
|
6 | 5 | ralimdv 2963 |
. . . 4
|
7 | 3 | caubnd2 14097 |
. . . 4
|
8 | 6, 7 | syl6 35 |
. . 3
|
9 | | fzssuz 12382 |
. . . . . . . 8
|
10 | 9, 3 | sseqtr4i 3638 |
. . . . . . 7
|
11 | | ssralv 3666 |
. . . . . . 7
|
12 | 10, 11 | ax-mp 5 |
. . . . . 6
|
13 | | fzfi 12771 |
. . . . . . . 8
|
14 | | fimaxre3 10970 |
. . . . . . . 8
|
15 | 13, 14 | mpan 706 |
. . . . . . 7
|
16 | | peano2re 10209 |
. . . . . . . . . 10
|
17 | 16 | adantl 482 |
. . . . . . . . 9
|
18 | | ltp1 10861 |
. . . . . . . . . . . . . . 15
|
19 | 18 | adantl 482 |
. . . . . . . . . . . . . 14
|
20 | 16 | adantl 482 |
. . . . . . . . . . . . . . 15
|
21 | | lelttr 10128 |
. . . . . . . . . . . . . . 15
|
22 | 20, 21 | mpd3an3 1425 |
. . . . . . . . . . . . . 14
|
23 | 19, 22 | mpan2d 710 |
. . . . . . . . . . . . 13
|
24 | 23 | expcom 451 |
. . . . . . . . . . . 12
|
25 | 24 | ralimdv 2963 |
. . . . . . . . . . 11
|
26 | 25 | impcom 446 |
. . . . . . . . . 10
|
27 | | ralim 2948 |
. . . . . . . . . 10
|
28 | 26, 27 | syl 17 |
. . . . . . . . 9
|
29 | | breq2 4657 |
. . . . . . . . . . 11
|
30 | 29 | ralbidv 2986 |
. . . . . . . . . 10
|
31 | 30 | rspcev 3309 |
. . . . . . . . 9
|
32 | 17, 28, 31 | syl6an 568 |
. . . . . . . 8
|
33 | 32 | rexlimdva 3031 |
. . . . . . 7
|
34 | 15, 33 | mpd 15 |
. . . . . 6
|
35 | 12, 34 | syl 17 |
. . . . 5
|
36 | | max1 12016 |
. . . . . . . . . . . . . . . . . 18
|
37 | 36 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
38 | | simp3 1063 |
. . . . . . . . . . . . . . . . . 18
|
39 | | simp1 1061 |
. . . . . . . . . . . . . . . . . 18
|
40 | | ifcl 4130 |
. . . . . . . . . . . . . . . . . . . 20
|
41 | 40 | ancoms 469 |
. . . . . . . . . . . . . . . . . . 19
|
42 | 41 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . 18
|
43 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . 18
|
44 | 38, 39, 42, 43 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
45 | 37, 44 | mpan2d 710 |
. . . . . . . . . . . . . . . 16
|
46 | | max2 12018 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
48 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
|
49 | | ltletr 10129 |
. . . . . . . . . . . . . . . . . 18
|
50 | 38, 48, 42, 49 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
51 | 47, 50 | mpan2d 710 |
. . . . . . . . . . . . . . . 16
|
52 | 45, 51 | jaod 395 |
. . . . . . . . . . . . . . 15
|
53 | 52 | 3expia 1267 |
. . . . . . . . . . . . . 14
|
54 | 53 | ralimdv 2963 |
. . . . . . . . . . . . 13
|
55 | | ralim 2948 |
. . . . . . . . . . . . 13
|
56 | 54, 55 | syl6 35 |
. . . . . . . . . . . 12
|
57 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | ralbidv 2986 |
. . . . . . . . . . . . . . 15
|
59 | 58 | rspcev 3309 |
. . . . . . . . . . . . . 14
|
60 | 59 | ex 450 |
. . . . . . . . . . . . 13
|
61 | 41, 60 | syl 17 |
. . . . . . . . . . . 12
|
62 | 56, 61 | syl6d 75 |
. . . . . . . . . . 11
|
63 | | uzssz 11707 |
. . . . . . . . . . . . . . . . . . . . . 22
|
64 | 3, 63 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | 64 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 64 | sseli 3599 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | | uztric 11709 |
. . . . . . . . . . . . . . . . . . . 20
|
68 | 65, 66, 67 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
|
69 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . 22
|
70 | 69, 3 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | | elfzuzb 12336 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 71 | baib 944 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 70, 72 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 73 | orbi1d 739 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 68, 74 | mpbird 247 |
. . . . . . . . . . . . . . . . . 18
|
76 | 75 | ex 450 |
. . . . . . . . . . . . . . . . 17
|
77 | | pm3.48 878 |
. . . . . . . . . . . . . . . . 17
|
78 | 76, 77 | syl9 77 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | alimdv 1845 |
. . . . . . . . . . . . . . 15
|
80 | | df-ral 2917 |
. . . . . . . . . . . . . . . . 17
|
81 | | df-ral 2917 |
. . . . . . . . . . . . . . . . 17
|
82 | 80, 81 | anbi12i 733 |
. . . . . . . . . . . . . . . 16
|
83 | | 19.26 1798 |
. . . . . . . . . . . . . . . 16
|
84 | 82, 83 | bitr4i 267 |
. . . . . . . . . . . . . . 15
|
85 | | df-ral 2917 |
. . . . . . . . . . . . . . 15
|
86 | 79, 84, 85 | 3imtr4g 285 |
. . . . . . . . . . . . . 14
|
87 | 86 | 3impib 1262 |
. . . . . . . . . . . . 13
|
88 | 87 | imim1i 63 |
. . . . . . . . . . . 12
|
89 | 88 | 3expd 1284 |
. . . . . . . . . . 11
|
90 | 62, 89 | syl6 35 |
. . . . . . . . . 10
|
91 | 90 | com23 86 |
. . . . . . . . 9
|
92 | 91 | expimpd 629 |
. . . . . . . 8
|
93 | 92 | com3r 87 |
. . . . . . 7
|
94 | 93 | com34 91 |
. . . . . 6
|
95 | 94 | rexlimdv 3030 |
. . . . 5
|
96 | 35, 95 | mpd 15 |
. . . 4
|
97 | 96 | rexlimdvv 3037 |
. . 3
|
98 | 2, 8, 97 | sylsyld 61 |
. 2
|
99 | 98 | imp 445 |
1
|