Step | Hyp | Ref
| Expression |
1 | | elin 3796 |
. . . . . . . 8
|
2 | | mayete3.a |
. . . . . . . . . . . . 13
|
3 | | mayete3.c |
. . . . . . . . . . . . 13
|
4 | 2, 3 | chjcli 28316 |
. . . . . . . . . . . 12
|
5 | | mayete3.f |
. . . . . . . . . . . 12
|
6 | 4, 5 | chjcli 28316 |
. . . . . . . . . . 11
|
7 | 6 | cheli 28089 |
. . . . . . . . . 10
|
8 | | mayete3.x |
. . . . . . . . . 10
|
9 | 7, 8 | eleq2s 2719 |
. . . . . . . . 9
|
10 | 9 | adantr 481 |
. . . . . . . 8
|
11 | 1, 10 | sylbi 207 |
. . . . . . 7
|
12 | | ax-hvmulid 27863 |
. . . . . . . 8
|
13 | | 2cn 11091 |
. . . . . . . . . . 11
|
14 | | 2ne0 11113 |
. . . . . . . . . . 11
|
15 | | recid2 10700 |
. . . . . . . . . . 11
|
16 | 13, 14, 15 | mp2an 708 |
. . . . . . . . . 10
|
17 | 16 | oveq1i 6660 |
. . . . . . . . 9
|
18 | | halfcn 11247 |
. . . . . . . . . 10
|
19 | | ax-hvmulass 27864 |
. . . . . . . . . 10
|
20 | 18, 13, 19 | mp3an12 1414 |
. . . . . . . . 9
|
21 | 17, 20 | syl5eqr 2670 |
. . . . . . . 8
|
22 | 12, 21 | eqtr3d 2658 |
. . . . . . 7
|
23 | 11, 22 | syl 17 |
. . . . . 6
|
24 | | hv2times 27918 |
. . . . . . . . . . . . . 14
|
25 | 24 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
26 | 11, 25 | syl 17 |
. . . . . . . . . . . 12
|
27 | | inss2 3834 |
. . . . . . . . . . . . . 14
|
28 | 27 | sseli 3599 |
. . . . . . . . . . . . 13
|
29 | | mayete3.y |
. . . . . . . . . . . . . . 15
|
30 | 29 | elin2 3801 |
. . . . . . . . . . . . . 14
|
31 | | elin 3796 |
. . . . . . . . . . . . . . . . 17
|
32 | | mayete3.ab |
. . . . . . . . . . . . . . . . . . 19
|
33 | | mayete3.b |
. . . . . . . . . . . . . . . . . . . 20
|
34 | 2, 33 | pjdsi 28571 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 32, 34 | mpan2 707 |
. . . . . . . . . . . . . . . . . 18
|
36 | | mayete3.cd |
. . . . . . . . . . . . . . . . . . 19
|
37 | | mayete3.d |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 3, 37 | pjdsi 28571 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 36, 38 | mpan2 707 |
. . . . . . . . . . . . . . . . . 18
|
40 | 35, 39 | oveqan12d 6669 |
. . . . . . . . . . . . . . . . 17
|
41 | 31, 40 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
42 | | inss1 3833 |
. . . . . . . . . . . . . . . . . 18
|
43 | 42 | sseli 3599 |
. . . . . . . . . . . . . . . . 17
|
44 | 2, 33 | chjcli 28316 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | cheli 28089 |
. . . . . . . . . . . . . . . . 17
|
46 | 2 | pjhcli 28277 |
. . . . . . . . . . . . . . . . . 18
|
47 | 33 | pjhcli 28277 |
. . . . . . . . . . . . . . . . . 18
|
48 | 3 | pjhcli 28277 |
. . . . . . . . . . . . . . . . . 18
|
49 | 37 | pjhcli 28277 |
. . . . . . . . . . . . . . . . . 18
|
50 | | hvadd4 27893 |
. . . . . . . . . . . . . . . . . 18
|
51 | 46, 47, 48, 49, 50 | syl22anc 1327 |
. . . . . . . . . . . . . . . . 17
|
52 | 43, 45, 51 | 3syl 18 |
. . . . . . . . . . . . . . . 16
|
53 | 41, 52 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
54 | | mayete3.fg |
. . . . . . . . . . . . . . . 16
|
55 | | mayete3.g |
. . . . . . . . . . . . . . . . 17
|
56 | 5, 55 | pjdsi 28571 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 56 | mpan2 707 |
. . . . . . . . . . . . . . 15
|
58 | 53, 57 | oveqan12d 6669 |
. . . . . . . . . . . . . 14
|
59 | 30, 58 | sylbi 207 |
. . . . . . . . . . . . 13
|
60 | 28, 59 | syl 17 |
. . . . . . . . . . . 12
|
61 | | hvaddcl 27869 |
. . . . . . . . . . . . . . 15
|
62 | 46, 48, 61 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
63 | | hvaddcl 27869 |
. . . . . . . . . . . . . . 15
|
64 | 47, 49, 63 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
65 | 5 | pjhcli 28277 |
. . . . . . . . . . . . . 14
|
66 | 55 | pjhcli 28277 |
. . . . . . . . . . . . . 14
|
67 | | hvadd4 27893 |
. . . . . . . . . . . . . 14
|
68 | 62, 64, 65, 66, 67 | syl22anc 1327 |
. . . . . . . . . . . . 13
|
69 | 11, 68 | syl 17 |
. . . . . . . . . . . 12
|
70 | 26, 60, 69 | 3eqtrd 2660 |
. . . . . . . . . . 11
|
71 | | inss1 3833 |
. . . . . . . . . . . . . 14
|
72 | 71 | sseli 3599 |
. . . . . . . . . . . . 13
|
73 | 72, 8 | syl6eleq 2711 |
. . . . . . . . . . . 12
|
74 | | mayete3.ac |
. . . . . . . . . . . 12
|
75 | | mayete3.af |
. . . . . . . . . . . . 13
|
76 | | mayete3.cf |
. . . . . . . . . . . . 13
|
77 | 2, 3, 5 | pjds3i 28572 |
. . . . . . . . . . . . 13
|
78 | 75, 76, 77 | mpanr12 721 |
. . . . . . . . . . . 12
|
79 | 73, 74, 78 | sylancl 694 |
. . . . . . . . . . 11
|
80 | 70, 79 | oveq12d 6668 |
. . . . . . . . . 10
|
81 | | hvmulcl 27870 |
. . . . . . . . . . . . 13
|
82 | 13, 81 | mpan 706 |
. . . . . . . . . . . 12
|
83 | | hvpncan 27896 |
. . . . . . . . . . . 12
|
84 | 82, 83 | mpancom 703 |
. . . . . . . . . . 11
|
85 | 11, 84 | syl 17 |
. . . . . . . . . 10
|
86 | 80, 85 | eqtr3d 2658 |
. . . . . . . . 9
|
87 | | hvaddcl 27869 |
. . . . . . . . . . . 12
|
88 | 62, 65, 87 | syl2anc 693 |
. . . . . . . . . . 11
|
89 | | hvaddcl 27869 |
. . . . . . . . . . . 12
|
90 | 64, 66, 89 | syl2anc 693 |
. . . . . . . . . . 11
|
91 | | hvpncan2 27897 |
. . . . . . . . . . 11
|
92 | 88, 90, 91 | syl2anc 693 |
. . . . . . . . . 10
|
93 | 11, 92 | syl 17 |
. . . . . . . . 9
|
94 | 86, 93 | eqtr3d 2658 |
. . . . . . . 8
|
95 | 33 | pjcli 28276 |
. . . . . . . . . . 11
|
96 | 37 | pjcli 28276 |
. . . . . . . . . . 11
|
97 | 33 | chshii 28084 |
. . . . . . . . . . . 12
|
98 | 37 | chshii 28084 |
. . . . . . . . . . . 12
|
99 | 97, 98 | shsvai 28223 |
. . . . . . . . . . 11
|
100 | 95, 96, 99 | syl2anc 693 |
. . . . . . . . . 10
|
101 | 55 | pjcli 28276 |
. . . . . . . . . 10
|
102 | 97, 98 | shscli 28176 |
. . . . . . . . . . 11
|
103 | 55 | chshii 28084 |
. . . . . . . . . . 11
|
104 | 102, 103 | shsvai 28223 |
. . . . . . . . . 10
|
105 | 100, 101,
104 | syl2anc 693 |
. . . . . . . . 9
|
106 | 11, 105 | syl 17 |
. . . . . . . 8
|
107 | 94, 106 | eqeltrd 2701 |
. . . . . . 7
|
108 | 102, 103 | shscli 28176 |
. . . . . . . 8
|
109 | | shmulcl 28075 |
. . . . . . . 8
|
110 | 108, 18, 109 | mp3an12 1414 |
. . . . . . 7
|
111 | 107, 110 | syl 17 |
. . . . . 6
|
112 | 23, 111 | eqeltrd 2701 |
. . . . 5
|
113 | 112 | ssriv 3607 |
. . . 4
|
114 | 33, 37 | chsleji 28317 |
. . . . 5
|
115 | 33, 37 | chjcli 28316 |
. . . . . . 7
|
116 | 115 | chshii 28084 |
. . . . . 6
|
117 | 102, 116,
103 | shlessi 28236 |
. . . . 5
|
118 | 114, 117 | ax-mp 5 |
. . . 4
|
119 | 113, 118 | sstri 3612 |
. . 3
|
120 | 115, 55 | chsleji 28317 |
. . 3
|
121 | 119, 120 | sstri 3612 |
. 2
|
122 | | mayete3.z |
. 2
|
123 | 121, 122 | sseqtr4i 3638 |
1
|