Proof of Theorem infrpge
Step | Hyp | Ref
| Expression |
1 | | infrpge.an0 |
. . . . . 6
|
2 | | n0 3931 |
. . . . . . 7
|
3 | 2 | biimpi 206 |
. . . . . 6
|
4 | 1, 3 | syl 17 |
. . . . 5
|
5 | 4 | adantr 481 |
. . . 4
inf |
6 | | nfv 1843 |
. . . . 5
inf
|
7 | | simpr 477 |
. . . . . . 7
inf
|
8 | | infrpge.a |
. . . . . . . . . . . 12
|
9 | 8 | adantr 481 |
. . . . . . . . . . 11
|
10 | | simpr 477 |
. . . . . . . . . . 11
|
11 | 9, 10 | sseldd 3604 |
. . . . . . . . . 10
|
12 | | pnfge 11964 |
. . . . . . . . . 10
|
13 | 11, 12 | syl 17 |
. . . . . . . . 9
|
14 | 13 | adantlr 751 |
. . . . . . . 8
inf
|
15 | | oveq1 6657 |
. . . . . . . . . . 11
inf inf |
16 | 15 | adantl 482 |
. . . . . . . . . 10
inf inf |
17 | | infrpge.b |
. . . . . . . . . . . . 13
|
18 | 17 | rpxrd 11873 |
. . . . . . . . . . . 12
|
19 | 17 | rpred 11872 |
. . . . . . . . . . . . 13
|
20 | | renemnf 10088 |
. . . . . . . . . . . . 13
|
21 | 19, 20 | syl 17 |
. . . . . . . . . . . 12
|
22 | | xaddpnf2 12058 |
. . . . . . . . . . . 12
|
23 | 18, 21, 22 | syl2anc 693 |
. . . . . . . . . . 11
|
24 | 23 | adantr 481 |
. . . . . . . . . 10
inf |
25 | 16, 24 | eqtr2d 2657 |
. . . . . . . . 9
inf inf |
26 | 25 | adantr 481 |
. . . . . . . 8
inf
inf |
27 | 14, 26 | breqtrd 4679 |
. . . . . . 7
inf
inf
|
28 | 7, 27 | jca 554 |
. . . . . 6
inf
inf |
29 | 28 | ex 450 |
. . . . 5
inf
inf |
30 | 6, 29 | eximd 2085 |
. . . 4
inf
inf |
31 | 5, 30 | mpd 15 |
. . 3
inf
inf |
32 | | df-rex 2918 |
. . 3
inf inf |
33 | 31, 32 | sylibr 224 |
. 2
inf
inf |
34 | | simpl 473 |
. . . 4
inf |
35 | | infrpge.bnd |
. . . . . . . . 9
|
36 | | infrpge.xph |
. . . . . . . . . 10
|
37 | | nfv 1843 |
. . . . . . . . . 10
inf |
38 | | mnfxr 10096 |
. . . . . . . . . . . . 13
|
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
|
40 | | rexr 10085 |
. . . . . . . . . . . . 13
|
41 | 40 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
|
42 | | infxrcl 12163 |
. . . . . . . . . . . . . 14
inf |
43 | 8, 42 | syl 17 |
. . . . . . . . . . . . 13
inf |
44 | 43 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
inf |
45 | | mnflt 11957 |
. . . . . . . . . . . . 13
|
46 | 45 | 3ad2ant2 1083 |
. . . . . . . . . . . 12
|
47 | | simp3 1063 |
. . . . . . . . . . . . 13
|
48 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
|
49 | 40 | adantl 482 |
. . . . . . . . . . . . . . 15
|
50 | | infxrgelb 12165 |
. . . . . . . . . . . . . . 15
inf |
51 | 48, 49, 50 | syl2anc 693 |
. . . . . . . . . . . . . 14
inf
|
52 | 51 | 3adant3 1081 |
. . . . . . . . . . . . 13
inf
|
53 | 47, 52 | mpbird 247 |
. . . . . . . . . . . 12
inf |
54 | 39, 41, 44, 46, 53 | xrltletrd 11992 |
. . . . . . . . . . 11
inf
|
55 | 54 | 3exp 1264 |
. . . . . . . . . 10
inf |
56 | 36, 37, 55 | rexlimd 3026 |
. . . . . . . . 9
inf |
57 | 35, 56 | mpd 15 |
. . . . . . . 8
inf |
58 | 57 | adantr 481 |
. . . . . . 7
inf inf |
59 | | neqne 2802 |
. . . . . . . . 9
inf inf |
60 | 59 | adantl 482 |
. . . . . . . 8
inf inf |
61 | 43 | adantr 481 |
. . . . . . . 8
inf inf |
62 | 60, 61 | nepnfltpnf 39558 |
. . . . . . 7
inf inf |
63 | 58, 62 | jca 554 |
. . . . . 6
inf inf inf |
64 | | xrrebnd 11999 |
. . . . . . . 8
inf
inf
inf inf
|
65 | 43, 64 | syl 17 |
. . . . . . 7
inf inf inf |
66 | 65 | adantr 481 |
. . . . . 6
inf inf
inf inf
|
67 | 63, 66 | mpbird 247 |
. . . . 5
inf inf |
68 | | simpr 477 |
. . . . . . . 8
inf inf |
69 | 17 | adantr 481 |
. . . . . . . 8
inf |
70 | 68, 69 | ltaddrpd 11905 |
. . . . . . 7
inf inf inf |
71 | 19 | adantr 481 |
. . . . . . . . 9
inf |
72 | | rexadd 12063 |
. . . . . . . . 9
inf inf inf |
73 | 68, 71, 72 | syl2anc 693 |
. . . . . . . 8
inf inf inf |
74 | 73 | eqcomd 2628 |
. . . . . . 7
inf inf inf |
75 | 70, 74 | breqtrd 4679 |
. . . . . 6
inf inf inf |
76 | 43 | adantr 481 |
. . . . . . 7
inf inf |
77 | 43, 18 | xaddcld 12131 |
. . . . . . . 8
inf |
78 | 77 | adantr 481 |
. . . . . . 7
inf inf |
79 | | xrltnle 10105 |
. . . . . . 7
inf inf inf inf inf inf |
80 | 76, 78, 79 | syl2anc 693 |
. . . . . 6
inf inf inf inf inf |
81 | 75, 80 | mpbid 222 |
. . . . 5
inf inf inf |
82 | 34, 67, 81 | syl2anc 693 |
. . . 4
inf inf inf |
83 | | simpr 477 |
. . . . . 6
inf inf
inf
inf |
84 | | simpl 473 |
. . . . . . 7
inf inf |
85 | | infxrgelb 12165 |
. . . . . . . 8
inf inf inf
inf |
86 | 8, 77, 85 | syl2anc 693 |
. . . . . . 7
inf inf
inf
|
87 | 84, 86 | syl 17 |
. . . . . 6
inf inf inf inf
inf
|
88 | 83, 87 | mtbid 314 |
. . . . 5
inf inf
inf
|
89 | | rexnal 2995 |
. . . . 5
inf inf |
90 | 88, 89 | sylibr 224 |
. . . 4
inf inf inf |
91 | 34, 82, 90 | syl2anc 693 |
. . 3
inf
inf |
92 | 11 | adantr 481 |
. . . . . . 7
inf
|
93 | 77 | ad2antrr 762 |
. . . . . . 7
inf
inf
|
94 | | simpr 477 |
. . . . . . . 8
inf
inf |
95 | | xrltnle 10105 |
. . . . . . . . 9
inf
inf
inf |
96 | 92, 93, 95 | syl2anc 693 |
. . . . . . . 8
inf
inf
inf |
97 | 94, 96 | mpbird 247 |
. . . . . . 7
inf
inf |
98 | 92, 93, 97 | xrltled 39486 |
. . . . . 6
inf
inf |
99 | 98 | ex 450 |
. . . . 5
inf
inf |
100 | 99 | adantlr 751 |
. . . 4
inf
inf inf |
101 | 100 | reximdva 3017 |
. . 3
inf
inf
inf |
102 | 91, 101 | mpd 15 |
. 2
inf
inf |
103 | 33, 102 | pm2.61dan 832 |
1
inf |