Proof of Theorem xrmaxiflemcom
Step | Hyp | Ref
| Expression |
1 | | simpr 109 |
. . . 4
|
2 | 1 | iftrued 3532 |
. . 3
|
3 | | xrpnfdc 9786 |
. . . . . . 7
DECID
|
4 | 3 | ad2antrr 485 |
. . . . . 6
DECID |
5 | | exmiddc 831 |
. . . . . 6
DECID
|
6 | 4, 5 | syl 14 |
. . . . 5
|
7 | | eqid 2170 |
. . . . . . . 8
|
8 | 7 | biantru 300 |
. . . . . . 7
|
9 | 8 | a1i 9 |
. . . . . 6
|
10 | | xrmnfdc 9787 |
. . . . . . . . . . 11
DECID
|
11 | 10 | ad2antrr 485 |
. . . . . . . . . 10
DECID |
12 | | exmiddc 831 |
. . . . . . . . . 10
DECID
|
13 | 11, 12 | syl 14 |
. . . . . . . . 9
|
14 | | iba 298 |
. . . . . . . . . . . 12
|
15 | 14 | eqcoms 2173 |
. . . . . . . . . . 11
|
16 | 15 | adantl 275 |
. . . . . . . . . 10
|
17 | 1 | iftrued 3532 |
. . . . . . . . . . . 12
|
18 | 17 | eqcomd 2176 |
. . . . . . . . . . 11
|
19 | 18 | biantrud 302 |
. . . . . . . . . 10
|
20 | 16, 19 | orbi12d 788 |
. . . . . . . . 9
|
21 | 13, 20 | mpbid 146 |
. . . . . . . 8
|
22 | | eqifdc 3559 |
. . . . . . . . 9
DECID
|
23 | 11, 22 | syl 14 |
. . . . . . . 8
|
24 | 21, 23 | mpbird 166 |
. . . . . . 7
|
25 | 24 | biantrud 302 |
. . . . . 6
|
26 | 9, 25 | orbi12d 788 |
. . . . 5
|
27 | 6, 26 | mpbid 146 |
. . . 4
|
28 | | eqifdc 3559 |
. . . . 5
DECID
|
29 | 4, 28 | syl 14 |
. . . 4
|
30 | 27, 29 | mpbird 166 |
. . 3
|
31 | 2, 30 | eqtrd 2203 |
. 2
|
32 | 3, 5 | syl 14 |
. . . . . . . 8
|
33 | 32 | ad3antrrr 489 |
. . . . . . 7
|
34 | | pm4.24 393 |
. . . . . . . . 9
|
35 | 34 | a1i 9 |
. . . . . . . 8
|
36 | 10 | ad3antrrr 489 |
. . . . . . . . . . . 12
DECID
|
37 | 36, 12 | syl 14 |
. . . . . . . . . . 11
|
38 | | simpr 109 |
. . . . . . . . . . . . . . 15
|
39 | 38 | eqeq2d 2182 |
. . . . . . . . . . . . . 14
|
40 | 39 | anbi2d 461 |
. . . . . . . . . . . . 13
|
41 | | anidm 394 |
. . . . . . . . . . . . 13
|
42 | 40, 41 | bitr2di 196 |
. . . . . . . . . . . 12
|
43 | | eqid 2170 |
. . . . . . . . . . . . . 14
|
44 | 43 | biantru 300 |
. . . . . . . . . . . . 13
|
45 | 44 | a1i 9 |
. . . . . . . . . . . 12
|
46 | 42, 45 | orbi12d 788 |
. . . . . . . . . . 11
|
47 | 37, 46 | mpbid 146 |
. . . . . . . . . 10
|
48 | | eqifdc 3559 |
. . . . . . . . . . 11
DECID
|
49 | 36, 48 | syl 14 |
. . . . . . . . . 10
|
50 | 47, 49 | mpbird 166 |
. . . . . . . . 9
|
51 | 50 | biantrud 302 |
. . . . . . . 8
|
52 | 35, 51 | orbi12d 788 |
. . . . . . 7
|
53 | 33, 52 | mpbid 146 |
. . . . . 6
|
54 | 3 | ad3antrrr 489 |
. . . . . . 7
DECID
|
55 | | eqifdc 3559 |
. . . . . . 7
DECID
|
56 | 54, 55 | syl 14 |
. . . . . 6
|
57 | 53, 56 | mpbird 166 |
. . . . 5
|
58 | 38 | iftrued 3532 |
. . . . 5
|
59 | 38 | iftrued 3532 |
. . . . . . 7
|
60 | 59 | ifeq2d 3543 |
. . . . . 6
|
61 | 60 | ifeq2d 3543 |
. . . . 5
|
62 | 57, 58, 61 | 3eqtr4d 2213 |
. . . 4
|
63 | | simpr 109 |
. . . . . 6
|
64 | 63 | iffalsed 3535 |
. . . . 5
|
65 | 63 | iffalsed 3535 |
. . . . . . . 8
|
66 | 65 | ifeq2d 3543 |
. . . . . . 7
|
67 | 66 | ifeq2d 3543 |
. . . . . 6
|
68 | | maxcom 11154 |
. . . . . . 7
|
69 | | ifeq2 3529 |
. . . . . . 7
|
70 | | ifeq2 3529 |
. . . . . . 7
|
71 | 68, 69, 70 | mp2b 8 |
. . . . . 6
|
72 | 67, 71 | eqtrdi 2219 |
. . . . 5
|
73 | 64, 72 | eqtr4d 2206 |
. . . 4
|
74 | | xrmnfdc 9787 |
. . . . . 6
DECID
|
75 | | exmiddc 831 |
. . . . . 6
DECID
|
76 | 74, 75 | syl 14 |
. . . . 5
|
77 | 76 | ad2antlr 486 |
. . . 4
|
78 | 62, 73, 77 | mpjaodan 793 |
. . 3
|
79 | | simpr 109 |
. . . 4
|
80 | 79 | iffalsed 3535 |
. . 3
|
81 | 79 | iffalsed 3535 |
. . . . 5
|
82 | 81 | ifeq2d 3543 |
. . . 4
|
83 | 82 | ifeq2d 3543 |
. . 3
|
84 | 78, 80, 83 | 3eqtr4d 2213 |
. 2
|
85 | | xrpnfdc 9786 |
. . . 4
DECID
|
86 | | exmiddc 831 |
. . . 4
DECID
|
87 | 85, 86 | syl 14 |
. . 3
|
88 | 87 | adantl 275 |
. 2
|
89 | 31, 84, 88 | mpjaodan 793 |
1
|