Step Hyp Ref
Expression 1 elreal2 9530 . . . . . . 7
2 1 simplbi 460 . . . . . 6
3 2 adantl 466 . . . . 5
4 fo1st 6820 . . . . . . . . . . . 12
5 fof 5800 . . . . . . . . . . . 12
6 ffn 5736 . . . . . . . . . . . 12
7 4 , 5 , 6 mp2b 10 . . . . . . . . . . 11
8 ssv 3523 . . . . . . . . . . 11
9 fvelimab 5929 . . . . . . . . . . 11
10 7 , 8 , 9 mp2an 672 . . . . . . . . . 10
11 r19.29 2992 . . . . . . . . . . . 12
12 ssel2 3498 . . . . . . . . . . . . . . . . 17
13 ltresr2 9539 . . . . . . . . . . . . . . . . . . . 20
14 breq1 4455 . . . . . . . . . . . . . . . . . . . 20
15 13 , 14 sylan9bb 699 . . . . . . . . . . . . . . . . . . 19
16 15 biimpd 207 . . . . . . . . . . . . . . . . . 18
17 16 exp31 604 . . . . . . . . . . . . . . . . 17
18 12 , 17 syl 16 . . . . . . . . . . . . . . . 16
19 18 imp4b 590 . . . . . . . . . . . . . . 15
20 19 ancomsd 454 . . . . . . . . . . . . . 14
21 20 an32s 804 . . . . . . . . . . . . 13
22 21 rexlimdva 2949 . . . . . . . . . . . 12
23 11 , 22 syl5 32 . . . . . . . . . . 11
24 23 expd 436 . . . . . . . . . 10
25 10 , 24 syl7bi 230 . . . . . . . . 9
26 25 impr 619 . . . . . . . 8
27 26 adantlr 714 . . . . . . 7
28 27 ralrimiv 2869 . . . . . 6
29 28 expr 615 . . . . 5
30 breq2 4456 . . . . . . 7
31 30 ralbidv 2896 . . . . . 6
32 31 rspcev 3210 . . . . 5
33 3 , 29 , 32 syl6an 545 . . . 4
34 33 rexlimdva 2949 . . 3
35 n0 3794 . . . . . 6
36 fnfvima 6150 . . . . . . . . 9
37 7 , 8 , 36 mp3an12 1314 . . . . . . . 8
38 ne0i 3790 . . . . . . . 8
39 37 , 38 syl 16 . . . . . . 7
40 39 exlimiv 1722 . . . . . 6
41 35 , 40 sylbi 195 . . . . 5
42 supsr 9510 . . . . . 6
43 42 ex 434 . . . . 5
44 41 , 43 syl 16 . . . 4
45 44 adantl 466 . . 3
46 breq2 4456 . . . . . . . . . . . 12
47 46 notbid 294 . . . . . . . . . . 11
48 47 rspccv 3207 . . . . . . . . . 10
49 37 , 48 syl5com 30 . . . . . . . . 9
50 49 adantl 466 . . . . . . . 8
51 elreal2 9530 . . . . . . . . . . . . 13
52 51 simprbi 464 . . . . . . . . . . . 12
53 52 breq2d 4464 . . . . . . . . . . 11
54 ltresr 9538 . . . . . . . . . . 11
55 53 , 54 syl6bb 261 . . . . . . . . . 10
56 12 , 55 syl 16 . . . . . . . . 9
57 56 notbid 294 . . . . . . . 8
58 50 , 57 sylibrd 234 . . . . . . 7
59 58 ralrimdva 2875 . . . . . 6
60 59 ad2antrr 725 . . . . 5
61 52 breq1d 4462 . . . . . . . . . . . . . 14
62 ltresr 9538 . . . . . . . . . . . . . 14
63 61 , 62 syl6bb 261 . . . . . . . . . . . . 13
64 51 simplbi 460 . . . . . . . . . . . . . . 15
65 breq1 4455 . . . . . . . . . . . . . . . . 17
66 breq1 4455 . . . . . . . . . . . . . . . . . 18
67 66 rexbidv 2968 . . . . . . . . . . . . . . . . 17
68 65 , 67 imbi12d 320 . . . . . . . . . . . . . . . 16
69 68 rspccv 3207 . . . . . . . . . . . . . . 15
70 64 , 69 syl5 32 . . . . . . . . . . . . . 14
71 70 com3l 81 . . . . . . . . . . . . 13
72 63 , 71 sylbid 215 . . . . . . . . . . . 12
73 72 adantr 465 . . . . . . . . . . 11
74 fvelimab 5929 . . . . . . . . . . . . . . . 16
75 7 , 8 , 74 mp2an 672 . . . . . . . . . . . . . . 15
76 ssel2 3498 . . . . . . . . . . . . . . . . . . . . . 22
77 ltresr2 9539 . . . . . . . . . . . . . . . . . . . . . 22
78 76 , 77 sylan2 474 . . . . . . . . . . . . . . . . . . . . 21
79 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
80 78 , 79 sylan9bb 699 . . . . . . . . . . . . . . . . . . . 20
81 80 exbiri 622 . . . . . . . . . . . . . . . . . . 19
82 81 expr 615 . . . . . . . . . . . . . . . . . 18
83 82 com4r 86 . . . . . . . . . . . . . . . . 17
84 83 imp 429 . . . . . . . . . . . . . . . 16
85 84 reximdvai 2929 . . . . . . . . . . . . . . 15
86 75 , 85 syl5bi 217 . . . . . . . . . . . . . 14
87 86 expcom 435 . . . . . . . . . . . . 13
88 87 com23 78 . . . . . . . . . . . 12
89 88 rexlimdv 2947 . . . . . . . . . . 11
90 73 , 89 syl6d 69 . . . . . . . . . 10
91 90 com23 78 . . . . . . . . 9
92 91 ex 434 . . . . . . . 8
93 92 com3l 81 . . . . . . 7
94 93 ad2antrr 725 . . . . . 6
95 94 ralrimdv 2873 . . . . 5
96 opelreal 9528 . . . . . . . 8
97 96 biimpri 206 . . . . . . 7
98 97 adantl 466 . . . . . 6
99 breq1 4455 . . . . . . . . . . 11
100 99 notbid 294 . . . . . . . . . 10
101 100 ralbidv 2896 . . . . . . . . 9
102 breq2 4456 . . . . . . . . . . 11
103 102 imbi1d 317 . . . . . . . . . 10
104 103 ralbidv 2896 . . . . . . . . 9
105 101 , 104 anbi12d 710 . . . . . . . 8
106 105 rspcev 3210 . . . . . . 7
107 106 ex 434 . . . . . 6
108 98 , 107 syl 16 . . . . 5
109 60 , 95 , 108 syl2and 483 . . . 4
110 109 rexlimdva 2949 . . 3
111 34 , 45 , 110 3syld 55 . 2
112 111 3impia 1193 1
