Step | Hyp | Ref
| Expression |
1 | | infleinf.a |
. . . . . 6
|
2 | | infxrcl 12163 |
. . . . . 6
inf |
3 | 1, 2 | syl 17 |
. . . . 5
inf |
4 | | pnfge 11964 |
. . . . 5
inf
inf |
5 | 3, 4 | syl 17 |
. . . 4
inf |
6 | 5 | adantr 481 |
. . 3
inf |
7 | | infeq1 8382 |
. . . . . 6
inf inf |
8 | | xrinf0 12168 |
. . . . . . 7
inf
|
9 | 8 | a1i 11 |
. . . . . 6
inf
|
10 | 7, 9 | eqtrd 2656 |
. . . . 5
inf |
11 | 10 | eqcomd 2628 |
. . . 4
inf |
12 | 11 | adantl 482 |
. . 3
inf
|
13 | 6, 12 | breqtrd 4679 |
. 2
inf inf |
14 | | neqne 2802 |
. . . 4
|
15 | 14 | adantl 482 |
. . 3
|
16 | 3 | adantr 481 |
. . . . . 6
inf inf |
17 | | id 22 |
. . . . . . . . . . . . 13
|
18 | | 2re 11090 |
. . . . . . . . . . . . . 14
|
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
|
20 | 17, 19 | resubcld 10458 |
. . . . . . . . . . . 12
|
21 | 20 | adantl 482 |
. . . . . . . . . . 11
inf
|
22 | | simpr 477 |
. . . . . . . . . . . . 13
inf inf |
23 | | infleinf.b |
. . . . . . . . . . . . . . 15
|
24 | | infxrunb2 39584 |
. . . . . . . . . . . . . . 15
inf |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . . . 14
inf |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
inf
inf |
27 | 22, 26 | mpbird 247 |
. . . . . . . . . . . 12
inf |
28 | 27 | adantr 481 |
. . . . . . . . . . 11
inf
|
29 | | breq2 4657 |
. . . . . . . . . . . . 13
|
30 | 29 | rexbidv 3052 |
. . . . . . . . . . . 12
|
31 | 30 | rspcva 3307 |
. . . . . . . . . . 11
|
32 | 21, 28, 31 | syl2anc 693 |
. . . . . . . . . 10
inf
|
33 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
|
34 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
35 | | 1rp 11836 |
. . . . . . . . . . . . . . . . . 18
|
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
37 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . 18
|
38 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
|
39 | 38 | 3anbi3d 1405 |
. . . . . . . . . . . . . . . . . . 19
|
40 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
|
41 | 40 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . 20
|
42 | 41 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . 19
|
43 | 39, 42 | imbi12d 334 |
. . . . . . . . . . . . . . . . . 18
|
44 | | infleinf.c |
. . . . . . . . . . . . . . . . . 18
|
45 | 37, 43, 44 | vtocl 3259 |
. . . . . . . . . . . . . . . . 17
|
46 | 33, 34, 36, 45 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
47 | 46 | adantlr 751 |
. . . . . . . . . . . . . . 15
|
48 | 47 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
49 | | simp1l 1085 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50, 1 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
52 | 50, 23 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
53 | | simp1r 1086 |
. . . . . . . . . . . . . . . . . 18
|
54 | 53 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
55 | | simp2 1062 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
57 | | simpll3 1102 |
. . . . . . . . . . . . . . . . 17
|
58 | | simplr 792 |
. . . . . . . . . . . . . . . . 17
|
59 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
60 | 51, 52, 54, 56, 57, 58, 59 | infleinflem2 39587 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | ex 450 |
. . . . . . . . . . . . . . 15
|
62 | 61 | reximdva 3017 |
. . . . . . . . . . . . . 14
|
63 | 48, 62 | mpd 15 |
. . . . . . . . . . . . 13
|
64 | 63 | 3exp 1264 |
. . . . . . . . . . . 12
|
65 | 64 | adantlr 751 |
. . . . . . . . . . 11
inf
|
66 | 65 | rexlimdv 3030 |
. . . . . . . . . 10
inf
|
67 | 32, 66 | mpd 15 |
. . . . . . . . 9
inf
|
68 | 67 | ralrimiva 2966 |
. . . . . . . 8
inf |
69 | | infxrunb2 39584 |
. . . . . . . . . 10
inf |
70 | 1, 69 | syl 17 |
. . . . . . . . 9
inf |
71 | 70 | adantr 481 |
. . . . . . . 8
inf
inf |
72 | 68, 71 | mpbid 222 |
. . . . . . 7
inf inf |
73 | 72, 22 | eqtr4d 2659 |
. . . . . 6
inf inf inf |
74 | 16, 73 | xreqled 39546 |
. . . . 5
inf inf inf |
75 | 74 | adantlr 751 |
. . . 4
inf
inf inf |
76 | | mnfxr 10096 |
. . . . . . . 8
|
77 | 76 | a1i 11 |
. . . . . . 7
|
78 | 77 | ad2antrr 762 |
. . . . . 6
inf |
79 | | infxrcl 12163 |
. . . . . . . 8
inf |
80 | 23, 79 | syl 17 |
. . . . . . 7
inf |
81 | 80 | ad2antrr 762 |
. . . . . 6
inf inf |
82 | | mnfle 11969 |
. . . . . . 7
inf
inf |
83 | 81, 82 | syl 17 |
. . . . . 6
inf inf |
84 | | neqne 2802 |
. . . . . . . 8
inf inf |
85 | 84 | necomd 2849 |
. . . . . . 7
inf
inf |
86 | 85 | adantl 482 |
. . . . . 6
inf inf |
87 | 78, 81, 83, 86 | xrleneltd 39539 |
. . . . 5
inf inf |
88 | 3 | ad2antrr 762 |
. . . . . 6
inf inf |
89 | 80 | ad2antrr 762 |
. . . . . 6
inf inf |
90 | | nfv 1843 |
. . . . . . . 8
inf
|
91 | 23 | ad3antrrr 766 |
. . . . . . . 8
inf
|
92 | | simpllr 799 |
. . . . . . . 8
inf
|
93 | | simpr 477 |
. . . . . . . . . 10
inf
inf
|
94 | | infxrbnd2 39585 |
. . . . . . . . . . . 12
inf |
95 | 23, 94 | syl 17 |
. . . . . . . . . . 11
inf |
96 | 95 | adantr 481 |
. . . . . . . . . 10
inf
inf |
97 | 93, 96 | mpbird 247 |
. . . . . . . . 9
inf
|
98 | 97 | ad4ant13 1292 |
. . . . . . . 8
inf
|
99 | | simpr 477 |
. . . . . . . . 9
inf
|
100 | 99 | rphalfcld 11884 |
. . . . . . . 8
inf
|
101 | 90, 91, 92, 98, 100 | infrpge 39567 |
. . . . . . 7
inf
inf |
102 | | simpll 790 |
. . . . . . . . . . . . 13
|
103 | | simpr 477 |
. . . . . . . . . . . . 13
|
104 | | rphalfcl 11858 |
. . . . . . . . . . . . . 14
|
105 | 104 | ad2antlr 763 |
. . . . . . . . . . . . 13
|
106 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
107 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
|
108 | 107 | 3anbi3d 1405 |
. . . . . . . . . . . . . . 15
|
109 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
110 | 109 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
|
111 | 110 | rexbidv 3052 |
. . . . . . . . . . . . . . 15
|
112 | 108, 111 | imbi12d 334 |
. . . . . . . . . . . . . 14
|
113 | 106, 112,
44 | vtocl 3259 |
. . . . . . . . . . . . 13
|
114 | 102, 103,
105, 113 | syl3anc 1326 |
. . . . . . . . . . . 12
|
115 | 114 | 3adant3 1081 |
. . . . . . . . . . 11
inf |
116 | | simp11l 1172 |
. . . . . . . . . . . . . . 15
inf |
117 | 116, 1 | syl 17 |
. . . . . . . . . . . . . 14
inf |
118 | 116, 23 | syl 17 |
. . . . . . . . . . . . . 14
inf |
119 | | simp11 1091 |
. . . . . . . . . . . . . . 15
inf
|
120 | 119 | simprd 479 |
. . . . . . . . . . . . . 14
inf
|
121 | | simp12 1092 |
. . . . . . . . . . . . . 14
inf
|
122 | | simp3 1063 |
. . . . . . . . . . . . . . 15
inf inf |
123 | 122 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
inf inf |
124 | | simp2 1062 |
. . . . . . . . . . . . . 14
inf |
125 | | simp3 1063 |
. . . . . . . . . . . . . 14
inf
|
126 | 117, 118,
120, 121, 123, 124, 125 | infleinflem1 39586 |
. . . . . . . . . . . . 13
inf inf inf |
127 | 126 | 3exp 1264 |
. . . . . . . . . . . 12
inf
inf inf |
128 | 127 | rexlimdv 3030 |
. . . . . . . . . . 11
inf
inf inf |
129 | 115, 128 | mpd 15 |
. . . . . . . . . 10
inf inf inf |
130 | 129 | 3exp 1264 |
. . . . . . . . 9
inf inf inf |
131 | 130 | rexlimdv 3030 |
. . . . . . . 8
inf inf inf |
132 | 131 | ad4ant14 1293 |
. . . . . . 7
inf
inf inf inf |
133 | 101, 132 | mpd 15 |
. . . . . 6
inf
inf inf |
134 | 88, 89, 133 | xrlexaddrp 39568 |
. . . . 5
inf inf inf |
135 | 87, 134 | syldan 487 |
. . . 4
inf inf inf |
136 | 75, 135 | pm2.61dan 832 |
. . 3
inf inf |
137 | 15, 136 | syldan 487 |
. 2
inf inf |
138 | 13, 137 | pm2.61dan 832 |
1
inf inf |