Step | Hyp | Ref
| Expression |
1 | | opelxpi 4641 |
. . . 4
|
2 | | enq0ex 7388 |
. . . . 5
~Q0 |
3 | 2 | ecelqsi 6563 |
. . . 4
~Q0
~Q0 |
4 | 1, 3 | syl 14 |
. . 3
~Q0
~Q0 |
5 | | opelxpi 4641 |
. . . 4
|
6 | 2 | ecelqsi 6563 |
. . . 4
~Q0
~Q0 |
7 | 5, 6 | syl 14 |
. . 3
~Q0
~Q0 |
8 | 4, 7 | anim12i 336 |
. 2
~Q0
~Q0
~Q0
~Q0 |
9 | | eqid 2170 |
. . . 4
~Q0
~Q0 |
10 | | eqid 2170 |
. . . 4
~Q0
~Q0 |
11 | 9, 10 | pm3.2i 270 |
. . 3
~Q0 ~Q0 ~Q0 ~Q0 |
12 | | eqid 2170 |
. . 3
~Q0
~Q0 |
13 | | opeq12 3765 |
. . . . . . . . 9
|
14 | 13 | eceq1d 6545 |
. . . . . . . 8
~Q0 ~Q0 |
15 | 14 | eqeq2d 2182 |
. . . . . . 7
~Q0
~Q0 ~Q0 ~Q0 |
16 | 15 | anbi1d 462 |
. . . . . 6
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
17 | | simpl 108 |
. . . . . . . . . . 11
|
18 | 17 | oveq1d 5865 |
. . . . . . . . . 10
|
19 | | simpr 109 |
. . . . . . . . . . 11
|
20 | 19 | oveq1d 5865 |
. . . . . . . . . 10
|
21 | 18, 20 | oveq12d 5868 |
. . . . . . . . 9
|
22 | 19 | oveq1d 5865 |
. . . . . . . . 9
|
23 | 21, 22 | opeq12d 3771 |
. . . . . . . 8
|
24 | 23 | eceq1d 6545 |
. . . . . . 7
~Q0 ~Q0 |
25 | 24 | eqeq2d 2182 |
. . . . . 6
~Q0
~Q0 ~Q0 ~Q0 |
26 | 16, 25 | anbi12d 470 |
. . . . 5
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
27 | 26 | spc2egv 2820 |
. . . 4
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
28 | | opeq12 3765 |
. . . . . . . . . 10
|
29 | 28 | eceq1d 6545 |
. . . . . . . . 9
~Q0 ~Q0 |
30 | 29 | eqeq2d 2182 |
. . . . . . . 8
~Q0
~Q0 ~Q0 ~Q0 |
31 | 30 | anbi2d 461 |
. . . . . . 7
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
32 | | simpr 109 |
. . . . . . . . . . . 12
|
33 | 32 | oveq2d 5866 |
. . . . . . . . . . 11
|
34 | | simpl 108 |
. . . . . . . . . . . 12
|
35 | 34 | oveq2d 5866 |
. . . . . . . . . . 11
|
36 | 33, 35 | oveq12d 5868 |
. . . . . . . . . 10
|
37 | 32 | oveq2d 5866 |
. . . . . . . . . 10
|
38 | 36, 37 | opeq12d 3771 |
. . . . . . . . 9
|
39 | 38 | eceq1d 6545 |
. . . . . . . 8
~Q0 ~Q0 |
40 | 39 | eqeq2d 2182 |
. . . . . . 7
~Q0
~Q0 ~Q0 ~Q0 |
41 | 31, 40 | anbi12d 470 |
. . . . . 6
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
42 | 41 | spc2egv 2820 |
. . . . 5
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
43 | 42 | 2eximdv 1875 |
. . . 4
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
44 | 27, 43 | sylan9 407 |
. . 3
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
45 | 11, 12, 44 | mp2ani 430 |
. 2
~Q0 ~Q0 ~Q0 ~Q0
~Q0
~Q0 |
46 | | ecexg 6513 |
. . . 4
~Q0
~Q0 |
47 | 2, 46 | ax-mp 5 |
. . 3
~Q0 |
48 | | simp1 992 |
. . . . . . . 8
~Q0 ~Q0
~Q0
~Q0 |
49 | 48 | eqeq1d 2179 |
. . . . . . 7
~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 |
50 | | simp2 993 |
. . . . . . . 8
~Q0 ~Q0
~Q0
~Q0 |
51 | 50 | eqeq1d 2179 |
. . . . . . 7
~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0 |
52 | 49, 51 | anbi12d 470 |
. . . . . 6
~Q0 ~Q0
~Q0
~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0 |
53 | | simp3 994 |
. . . . . . 7
~Q0 ~Q0
~Q0
~Q0 |
54 | 53 | eqeq1d 2179 |
. . . . . 6
~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0 |
55 | 52, 54 | anbi12d 470 |
. . . . 5
~Q0 ~Q0
~Q0
~Q0
~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
56 | 55 | 4exbidv 1863 |
. . . 4
~Q0 ~Q0
~Q0
~Q0 ~Q0 ~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0 |
57 | | addnq0mo 7396 |
. . . 4
~Q0 ~Q0 ~Q0
~Q0 ~Q0 |
58 | | dfplq0qs 7379 |
. . . 4
+Q0
~Q0 ~Q0
~Q0 ~Q0 ~Q0 |
59 | 56, 57, 58 | ovig 5971 |
. . 3
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
+Q0 ~Q0
~Q0 |
60 | 47, 59 | mp3an3 1321 |
. 2
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
~Q0
+Q0 ~Q0
~Q0 |
61 | 8, 45, 60 | sylc 62 |
1
~Q0
+Q0 ~Q0
~Q0 |