Step | Hyp | Ref
| Expression |
1 | | shscl.1 |
. . . 4
|
2 | | shscl.2 |
. . . 4
|
3 | | shsss 28172 |
. . . 4
|
4 | 1, 2, 3 | mp2an 708 |
. . 3
|
5 | | sh0 28073 |
. . . . . 6
|
6 | 1, 5 | ax-mp 5 |
. . . . 5
|
7 | | sh0 28073 |
. . . . . 6
|
8 | 2, 7 | ax-mp 5 |
. . . . 5
|
9 | | ax-hv0cl 27860 |
. . . . . . 7
|
10 | 9 | hvaddid2i 27886 |
. . . . . 6
|
11 | 10 | eqcomi 2631 |
. . . . 5
|
12 | | rspceov 6692 |
. . . . 5
|
13 | 6, 8, 11, 12 | mp3an 1424 |
. . . 4
|
14 | 1, 2 | shseli 28175 |
. . . 4
|
15 | 13, 14 | mpbir 221 |
. . 3
|
16 | 4, 15 | pm3.2i 471 |
. 2
|
17 | 1, 2 | shseli 28175 |
. . . . . 6
|
18 | 1, 2 | shseli 28175 |
. . . . . 6
|
19 | | shaddcl 28074 |
. . . . . . . . . . . . . . . 16
|
20 | 1, 19 | mp3an1 1411 |
. . . . . . . . . . . . . . 15
|
21 | 20 | ad2ant2r 783 |
. . . . . . . . . . . . . 14
|
22 | 21 | ad2ant2r 783 |
. . . . . . . . . . . . 13
|
23 | | shaddcl 28074 |
. . . . . . . . . . . . . . . 16
|
24 | 2, 23 | mp3an1 1411 |
. . . . . . . . . . . . . . 15
|
25 | 24 | ad2ant2l 782 |
. . . . . . . . . . . . . 14
|
26 | 25 | ad2ant2r 783 |
. . . . . . . . . . . . 13
|
27 | | oveq12 6659 |
. . . . . . . . . . . . . . 15
|
28 | 27 | ad2ant2l 782 |
. . . . . . . . . . . . . 14
|
29 | 1 | sheli 28071 |
. . . . . . . . . . . . . . . . . 18
|
30 | 1 | sheli 28071 |
. . . . . . . . . . . . . . . . . 18
|
31 | 29, 30 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
32 | 2 | sheli 28071 |
. . . . . . . . . . . . . . . . . 18
|
33 | 2 | sheli 28071 |
. . . . . . . . . . . . . . . . . 18
|
34 | 32, 33 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
35 | | hvadd4 27893 |
. . . . . . . . . . . . . . . . 17
|
36 | 31, 34, 35 | syl2an 494 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | an4s 869 |
. . . . . . . . . . . . . . 15
|
38 | 37 | ad2ant2r 783 |
. . . . . . . . . . . . . 14
|
39 | 28, 38 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
40 | | rspceov 6692 |
. . . . . . . . . . . . 13
|
41 | 22, 26, 39, 40 | syl3anc 1326 |
. . . . . . . . . . . 12
|
42 | 41 | ancoms 469 |
. . . . . . . . . . 11
|
43 | 42 | exp43 640 |
. . . . . . . . . 10
|
44 | 43 | rexlimivv 3036 |
. . . . . . . . 9
|
45 | 44 | com3l 89 |
. . . . . . . 8
|
46 | 45 | rexlimivv 3036 |
. . . . . . 7
|
47 | 46 | imp 445 |
. . . . . 6
|
48 | 17, 18, 47 | syl2anb 496 |
. . . . 5
|
49 | 1, 2 | shseli 28175 |
. . . . 5
|
50 | 48, 49 | sylibr 224 |
. . . 4
|
51 | 50 | rgen2a 2977 |
. . 3
|
52 | | shmulcl 28075 |
. . . . . . . . . . . . . 14
|
53 | 1, 52 | mp3an1 1411 |
. . . . . . . . . . . . 13
|
54 | 53 | adantrr 753 |
. . . . . . . . . . . 12
|
55 | | shmulcl 28075 |
. . . . . . . . . . . . . . 15
|
56 | 2, 55 | mp3an1 1411 |
. . . . . . . . . . . . . 14
|
57 | 56 | adantrr 753 |
. . . . . . . . . . . . 13
|
58 | 57 | adantrl 752 |
. . . . . . . . . . . 12
|
59 | | oveq2 6658 |
. . . . . . . . . . . . . . 15
|
60 | 59 | adantl 482 |
. . . . . . . . . . . . . 14
|
61 | 60 | ad2antll 765 |
. . . . . . . . . . . . 13
|
62 | | id 22 |
. . . . . . . . . . . . . . . 16
|
63 | | ax-hvdistr1 27865 |
. . . . . . . . . . . . . . . 16
|
64 | 62, 30, 33, 63 | syl3an 1368 |
. . . . . . . . . . . . . . 15
|
65 | 64 | 3expb 1266 |
. . . . . . . . . . . . . 14
|
66 | 65 | adantrrr 761 |
. . . . . . . . . . . . 13
|
67 | 61, 66 | eqtrd 2656 |
. . . . . . . . . . . 12
|
68 | | rspceov 6692 |
. . . . . . . . . . . 12
|
69 | 54, 58, 67, 68 | syl3anc 1326 |
. . . . . . . . . . 11
|
70 | 69 | ancoms 469 |
. . . . . . . . . 10
|
71 | 70 | exp42 639 |
. . . . . . . . 9
|
72 | 71 | imp 445 |
. . . . . . . 8
|
73 | 72 | rexlimivv 3036 |
. . . . . . 7
|
74 | 73 | impcom 446 |
. . . . . 6
|
75 | 18, 74 | sylan2b 492 |
. . . . 5
|
76 | 1, 2 | shseli 28175 |
. . . . 5
|
77 | 75, 76 | sylibr 224 |
. . . 4
|
78 | 77 | rgen2 2975 |
. . 3
|
79 | 51, 78 | pm3.2i 471 |
. 2
|
80 | | issh2 28066 |
. 2
|
81 | 16, 79, 80 | mpbir2an 955 |
1
|