Step | Hyp | Ref
| Expression |
1 | | sxbrsiga.0 |
. . . 4
|
2 | | dya2ioc.1 |
. . . 4
|
3 | | dya2ioc.2 |
. . . 4
|
4 | 1, 2, 3 | dya2iocucvr 30346 |
. . 3
|
5 | | sxbrsigalem0 30333 |
. . 3
|
6 | 4, 5 | eqtr4i 2647 |
. 2
|
7 | | vex 3203 |
. . . . . 6
|
8 | | vex 3203 |
. . . . . 6
|
9 | 7, 8 | xpex 6962 |
. . . . 5
|
10 | 3, 9 | elrnmpt2 6773 |
. . . 4
|
11 | | simpr 477 |
. . . . . . 7
|
12 | 1, 2 | dya2icobrsiga 30338 |
. . . . . . . . . . . . 13
𝔅ℝ |
13 | | brsigasspwrn 30248 |
. . . . . . . . . . . . 13
𝔅ℝ |
14 | 12, 13 | sstri 3612 |
. . . . . . . . . . . 12
|
15 | 14 | sseli 3599 |
. . . . . . . . . . 11
|
16 | 15 | elpwid 4170 |
. . . . . . . . . 10
|
17 | 14 | sseli 3599 |
. . . . . . . . . . 11
|
18 | 17 | elpwid 4170 |
. . . . . . . . . 10
|
19 | | xpinpreima2 29953 |
. . . . . . . . . 10
|
20 | 16, 18, 19 | syl2an 494 |
. . . . . . . . 9
|
21 | | reex 10027 |
. . . . . . . . . . . . . . . . 17
|
22 | 21 | mptex 6486 |
. . . . . . . . . . . . . . . 16
|
23 | 22 | rnex 7100 |
. . . . . . . . . . . . . . 15
|
24 | 21 | mptex 6486 |
. . . . . . . . . . . . . . . 16
|
25 | 24 | rnex 7100 |
. . . . . . . . . . . . . . 15
|
26 | 23, 25 | unex 6956 |
. . . . . . . . . . . . . 14
|
27 | 26 | a1i 11 |
. . . . . . . . . . . . 13
|
28 | 27 | sgsiga 30205 |
. . . . . . . . . . . 12
sigaGen
sigAlgebra |
29 | 28 | trud 1493 |
. . . . . . . . . . 11
sigaGen
sigAlgebra |
30 | 29 | a1i 11 |
. . . . . . . . . 10
sigaGen sigAlgebra |
31 | | 1stpreima 29484 |
. . . . . . . . . . . . 13
|
32 | 16, 31 | syl 17 |
. . . . . . . . . . . 12
|
33 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
34 | 2, 33 | elrnmpt2 6773 |
. . . . . . . . . . . . 13
|
35 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
36 | 35 | xpeq1d 5138 |
. . . . . . . . . . . . . . . 16
|
37 | | difxp1 5559 |
. . . . . . . . . . . . . . . . . . 19
|
38 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | 38 | zred 11482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | | 2rp 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
42 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
43 | 41, 42 | rpexpcld 13032 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 39, 43 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 44 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . 21
|
46 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
47 | 39, 46 | readdcld 10069 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
48 | 47, 43 | rerpdivcld 11903 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | 48 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . 21
|
50 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . . . 22
|
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
|
52 | 39 | lep1d 10955 |
. . . . . . . . . . . . . . . . . . . . . 22
|
53 | 39, 47, 43, 52 | lediv1dd 11930 |
. . . . . . . . . . . . . . . . . . . . 21
|
54 | | pnfge 11964 |
. . . . . . . . . . . . . . . . . . . . . 22
|
55 | 49, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
|
56 | | difico 29545 |
. . . . . . . . . . . . . . . . . . . . 21
|
57 | 45, 49, 51, 53, 55, 56 | syl32anc 1334 |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 57 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 37, 58 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . . 18
|
60 | 29 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
sigAlgebra |
61 | | ssun1 3776 |
. . . . . . . . . . . . . . . . . . . . 21
|
62 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
63 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
64 | 63 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
65 | 64 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
66 | 65 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 44, 62, 66 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
68 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
69 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
70 | 69, 21 | xpex 6962 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
71 | 68, 70 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . . 22
|
72 | 67, 71 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
|
73 | 61, 72 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | | elsigagen 30210 |
. . . . . . . . . . . . . . . . . . . 20
sigaGen |
75 | 26, 73, 74 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
|
76 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
77 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
78 | 77 | xpeq1d 5138 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
79 | 78 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
80 | 79 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
81 | 48, 76, 80 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
82 | 68, 70 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . . 22
|
83 | 81, 82 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
|
84 | 61, 83 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | | elsigagen 30210 |
. . . . . . . . . . . . . . . . . . . 20
sigaGen |
86 | 26, 84, 85 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
|
87 | | difelsiga 30196 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
sigAlgebra sigaGen
sigaGen
sigaGen
|
88 | 60, 75, 86, 87 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
sigaGen
|
89 | 59, 88 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
sigaGen
|
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . . 16
sigaGen
|
91 | 36, 90 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
sigaGen |
92 | 91 | ex 450 |
. . . . . . . . . . . . . 14
sigaGen |
93 | 92 | rexlimivv 3036 |
. . . . . . . . . . . . 13
sigaGen
|
94 | 34, 93 | sylbi 207 |
. . . . . . . . . . . 12
sigaGen
|
95 | 32, 94 | eqeltrd 2701 |
. . . . . . . . . . 11
sigaGen
|
96 | 95 | adantr 481 |
. . . . . . . . . 10
sigaGen
|
97 | | 2ndpreima 29485 |
. . . . . . . . . . . . 13
|
98 | 18, 97 | syl 17 |
. . . . . . . . . . . 12
|
99 | 2, 33 | elrnmpt2 6773 |
. . . . . . . . . . . . 13
|
100 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | xpeq2d 5139 |
. . . . . . . . . . . . . . . 16
|
102 | | difxp2 5560 |
. . . . . . . . . . . . . . . . . . 19
|
103 | 57 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . 19
|
104 | 102, 103 | syl5reqr 2671 |
. . . . . . . . . . . . . . . . . 18
|
105 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
107 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
108 | 107 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
109 | 108 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
110 | 109 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
111 | 44, 106, 110 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
112 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
113 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
114 | 21, 113 | xpex 6962 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
115 | 112, 114 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . . 22
|
116 | 111, 115 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
|
117 | 105, 116 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
118 | | elsigagen 30210 |
. . . . . . . . . . . . . . . . . . . 20
sigaGen |
119 | 26, 117, 118 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
|
120 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
121 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
122 | 121 | xpeq2d 5139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
123 | 122 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
124 | 123 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
125 | 48, 120, 124 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . 22
|
126 | 112, 114 | elrnmpti 5376 |
. . . . . . . . . . . . . . . . . . . . . 22
|
127 | 125, 126 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
|
128 | 105, 127 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
|
129 | | elsigagen 30210 |
. . . . . . . . . . . . . . . . . . . 20
sigaGen |
130 | 26, 128, 129 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
|
131 | | difelsiga 30196 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
sigAlgebra sigaGen sigaGen
sigaGen
|
132 | 60, 119, 130, 131 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . 18
sigaGen
|
133 | 104, 132 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . 17
sigaGen
|
134 | 133 | adantr 481 |
. . . . . . . . . . . . . . . 16
sigaGen |
135 | 101, 134 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
sigaGen |
136 | 135 | ex 450 |
. . . . . . . . . . . . . 14
sigaGen |
137 | 136 | rexlimivv 3036 |
. . . . . . . . . . . . 13
sigaGen
|
138 | 99, 137 | sylbi 207 |
. . . . . . . . . . . 12
sigaGen
|
139 | 98, 138 | eqeltrd 2701 |
. . . . . . . . . . 11
sigaGen
|
140 | 139 | adantl 482 |
. . . . . . . . . 10
sigaGen
|
141 | | inelsiga 30198 |
. . . . . . . . . 10
sigaGen
sigAlgebra sigaGen
sigaGen
sigaGen
|
142 | 30, 96, 140, 141 | syl3anc 1326 |
. . . . . . . . 9
sigaGen
|
143 | 20, 142 | eqeltrd 2701 |
. . . . . . . 8
sigaGen
|
144 | 143 | adantr 481 |
. . . . . . 7
sigaGen
|
145 | 11, 144 | eqeltrd 2701 |
. . . . . 6
sigaGen
|
146 | 145 | ex 450 |
. . . . 5
sigaGen
|
147 | 146 | rexlimivv 3036 |
. . . 4
sigaGen |
148 | 10, 147 | sylbi 207 |
. . 3
sigaGen
|
149 | 148 | ssriv 3607 |
. 2
sigaGen
|
150 | | sigagenss2 30213 |
. 2
sigaGen
sigaGen sigaGen |
151 | 6, 149, 26, 150 | mp3an 1424 |
1
sigaGen
sigaGen
|