Step | Hyp | Ref
| Expression |
1 | | simpll 524 |
. . . . . . . 8
DECID #
|
2 | | simplr 525 |
. . . . . . . 8
DECID #
DECID |
3 | | simprr 527 |
. . . . . . . 8
DECID #
|
4 | 1, 2, 3 | 3jca 1172 |
. . . . . . 7
DECID #
DECID |
5 | 4 | reximi 2567 |
. . . . . 6
DECID #
DECID |
6 | | simpll 524 |
. . . . . . . 8
DECID #
|
7 | | simplr 525 |
. . . . . . . 8
DECID #
DECID |
8 | | simprr 527 |
. . . . . . . 8
DECID #
|
9 | 6, 7, 8 | 3jca 1172 |
. . . . . . 7
DECID #
DECID |
10 | 9 | reximi 2567 |
. . . . . 6
DECID #
DECID |
11 | | fveq2 5494 |
. . . . . . . . . . . 12
|
12 | 11 | sseq2d 3177 |
. . . . . . . . . . 11
|
13 | 11 | raleqdv 2671 |
. . . . . . . . . . 11
DECID DECID |
14 | | seqeq1 10393 |
. . . . . . . . . . . 12
|
15 | 14 | breq1d 3997 |
. . . . . . . . . . 11
|
16 | 12, 13, 15 | 3anbi123d 1307 |
. . . . . . . . . 10
DECID DECID |
17 | 16 | cbvrexvw 2701 |
. . . . . . . . 9
DECID
DECID |
18 | 17 | anbi2i 454 |
. . . . . . . 8
DECID DECID DECID
DECID
|
19 | | reeanv 2639 |
. . . . . . . 8
DECID DECID DECID
DECID
|
20 | 18, 19 | bitr4i 186 |
. . . . . . 7
DECID DECID
DECID DECID |
21 | | simprl3 1039 |
. . . . . . . . . . . . 13
DECID
DECID |
22 | 21 | adantl 275 |
. . . . . . . . . . . 12
DECID
DECID |
23 | | prodmo.1 |
. . . . . . . . . . . . 13
|
24 | | prodmo.2 |
. . . . . . . . . . . . . 14
|
25 | 24 | adantlr 474 |
. . . . . . . . . . . . 13
DECID
DECID
|
26 | | simprll 532 |
. . . . . . . . . . . . 13
DECID
DECID
|
27 | | simprlr 533 |
. . . . . . . . . . . . 13
DECID
DECID
|
28 | | simprl1 1037 |
. . . . . . . . . . . . . 14
DECID
DECID |
29 | 28 | adantl 275 |
. . . . . . . . . . . . 13
DECID
DECID |
30 | | simprr1 1040 |
. . . . . . . . . . . . . 14
DECID
DECID |
31 | 30 | adantl 275 |
. . . . . . . . . . . . 13
DECID
DECID |
32 | | eleq1w 2231 |
. . . . . . . . . . . . . . 15
|
33 | 32 | dcbid 833 |
. . . . . . . . . . . . . 14
DECID
DECID
|
34 | | simprl2 1038 |
. . . . . . . . . . . . . . 15
DECID
DECID DECID |
35 | 34 | ad2antlr 486 |
. . . . . . . . . . . . . 14
DECID
DECID
DECID |
36 | | simpr 109 |
. . . . . . . . . . . . . 14
DECID
DECID
|
37 | 33, 35, 36 | rspcdva 2839 |
. . . . . . . . . . . . 13
DECID
DECID
DECID |
38 | | simprr2 1041 |
. . . . . . . . . . . . . . 15
DECID
DECID DECID |
39 | 38 | ad2antlr 486 |
. . . . . . . . . . . . . 14
DECID
DECID
DECID |
40 | | simpr 109 |
. . . . . . . . . . . . . 14
DECID
DECID
|
41 | 33, 39, 40 | rspcdva 2839 |
. . . . . . . . . . . . 13
DECID
DECID
DECID |
42 | 23, 25, 26, 27, 29, 31, 37, 41 | prodrbdc 11526 |
. . . . . . . . . . . 12
DECID
DECID
|
43 | 22, 42 | mpbid 146 |
. . . . . . . . . . 11
DECID
DECID |
44 | | simprr3 1042 |
. . . . . . . . . . . 12
DECID
DECID |
45 | 44 | adantl 275 |
. . . . . . . . . . 11
DECID
DECID |
46 | | climuni 11245 |
. . . . . . . . . . 11
|
47 | 43, 45, 46 | syl2anc 409 |
. . . . . . . . . 10
DECID
DECID
|
48 | 47 | expcom 115 |
. . . . . . . . 9
DECID
DECID |
49 | 48 | ex 114 |
. . . . . . . 8
DECID
DECID
|
50 | 49 | rexlimivv 2593 |
. . . . . . 7
DECID DECID |
51 | 20, 50 | sylbi 120 |
. . . . . 6
DECID DECID |
52 | 5, 10, 51 | syl2an 287 |
. . . . 5
DECID
#
DECID
# |
53 | | prodmodc.3 |
. . . . . . . . . 10
♯
|
54 | 23, 24, 53 | prodmodclem2 11529 |
. . . . . . . . 9
DECID
#
|
55 | | equcomi 1697 |
. . . . . . . . 9
|
56 | 54, 55 | syl6 33 |
. . . . . . . 8
DECID
#
|
57 | 56 | expimpd 361 |
. . . . . . 7
DECID
#
|
58 | 57 | com12 30 |
. . . . . 6
DECID
#
|
59 | 58 | ancoms 266 |
. . . . 5
DECID # |
60 | 23, 24, 53 | prodmodclem2 11529 |
. . . . . . 7
DECID
#
|
61 | 60 | expimpd 361 |
. . . . . 6
DECID
#
|
62 | 61 | com12 30 |
. . . . 5
DECID
#
|
63 | | reeanv 2639 |
. . . . . . . 8
♯
♯ |
64 | | exdistrv 1903 |
. . . . . . . . 9
♯
♯ |
65 | 64 | 2rexbii 2479 |
. . . . . . . 8
♯
♯ |
66 | | oveq2 5859 |
. . . . . . . . . . . . . 14
|
67 | 66 | f1oeq2d 5436 |
. . . . . . . . . . . . 13
|
68 | | fveq2 5494 |
. . . . . . . . . . . . . 14
|
69 | 68 | eqeq2d 2182 |
. . . . . . . . . . . . 13
|
70 | 67, 69 | anbi12d 470 |
. . . . . . . . . . . 12
|
71 | 70 | exbidv 1818 |
. . . . . . . . . . 11
|
72 | | f1oeq1 5429 |
. . . . . . . . . . . . 13
|
73 | | fveq1 5493 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 73 | csbeq1d 3056 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 74 | ifeq1d 3542 |
. . . . . . . . . . . . . . . . . 18
♯
♯ |
76 | 75 | mpteq2dv 4078 |
. . . . . . . . . . . . . . . . 17
♯
♯ |
77 | 53, 76 | eqtrid 2215 |
. . . . . . . . . . . . . . . 16
♯ |
78 | 77 | seqeq3d 10398 |
. . . . . . . . . . . . . . 15
♯
|
79 | 78 | fveq1d 5496 |
. . . . . . . . . . . . . 14
♯
|
80 | 79 | eqeq2d 2182 |
. . . . . . . . . . . . 13
♯ |
81 | 72, 80 | anbi12d 470 |
. . . . . . . . . . . 12
♯ |
82 | 81 | cbvexvw 1913 |
. . . . . . . . . . 11
♯ |
83 | 71, 82 | bitrdi 195 |
. . . . . . . . . 10
♯ |
84 | 83 | cbvrexvw 2701 |
. . . . . . . . 9
♯
|
85 | 84 | anbi2i 454 |
. . . . . . . 8
♯ |
86 | 63, 65, 85 | 3bitr4i 211 |
. . . . . . 7
♯
|
87 | | an4 581 |
. . . . . . . . . 10
♯
♯ |
88 | 24 | ad4ant14 511 |
. . . . . . . . . . . . 13
|
89 | | breq1 3990 |
. . . . . . . . . . . . . . . 16
♯ ♯ |
90 | | fveq2 5494 |
. . . . . . . . . . . . . . . . 17
|
91 | 90 | csbeq1d 3056 |
. . . . . . . . . . . . . . . 16
|
92 | 89, 91 | ifbieq1d 3547 |
. . . . . . . . . . . . . . 15
♯
♯ |
93 | 92 | cbvmptv 4083 |
. . . . . . . . . . . . . 14
♯ ♯ |
94 | 53, 93 | eqtri 2191 |
. . . . . . . . . . . . 13
♯
|
95 | | fveq2 5494 |
. . . . . . . . . . . . . . . 16
|
96 | 95 | csbeq1d 3056 |
. . . . . . . . . . . . . . 15
|
97 | 89, 96 | ifbieq1d 3547 |
. . . . . . . . . . . . . 14
♯
♯ |
98 | 97 | cbvmptv 4083 |
. . . . . . . . . . . . 13
♯ ♯ |
99 | | simplr 525 |
. . . . . . . . . . . . 13
|
100 | | simprl 526 |
. . . . . . . . . . . . 13
|
101 | | simprr 527 |
. . . . . . . . . . . . 13
|
102 | 23, 88, 94, 98, 99, 100, 101 | prodmodclem3 11527 |
. . . . . . . . . . . 12
♯ |
103 | | eqeq12 2183 |
. . . . . . . . . . . 12
♯
♯
|
104 | 102, 103 | syl5ibrcom 156 |
. . . . . . . . . . 11
♯
|
105 | 104 | expimpd 361 |
. . . . . . . . . 10
♯
|
106 | 87, 105 | syl5bi 151 |
. . . . . . . . 9
♯
|
107 | 106 | exlimdvv 1890 |
. . . . . . . 8
♯
|
108 | 107 | rexlimdvva 2595 |
. . . . . . 7
♯
|
109 | 86, 108 | syl5bir 152 |
. . . . . 6
|
110 | 109 | com12 30 |
. . . . 5
|
111 | 52, 59, 62, 110 | ccase 959 |
. . . 4
DECID
#
DECID
#
|
112 | 111 | com12 30 |
. . 3
DECID #
DECID
#
|
113 | 112 | alrimivv 1868 |
. 2
DECID #
DECID
#
|
114 | | breq2 3991 |
. . . . . . 7
|
115 | 114 | anbi2d 461 |
. . . . . 6
# # |
116 | 115 | anbi2d 461 |
. . . . 5
DECID
#
DECID
# |
117 | 116 | rexbidv 2471 |
. . . 4
DECID
# DECID
# |
118 | | eqeq1 2177 |
. . . . . . 7
|
119 | 118 | anbi2d 461 |
. . . . . 6
|
120 | 119 | exbidv 1818 |
. . . . 5
|
121 | 120 | rexbidv 2471 |
. . . 4
|
122 | 117, 121 | orbi12d 788 |
. . 3
DECID
#
DECID #
|
123 | 122 | mo4 2080 |
. 2
DECID
#
DECID
#
DECID
#
|
124 | 113, 123 | sylibr 133 |
1
DECID #
|