Proof of Theorem addcexg
Step | Hyp | Ref
| Expression |
1 | | dfaddc2 4381 |
. 2
![(](lp.gif) ![B](_cb.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![)](rp.gif) |
2 | | pw1exg 4302 |
. . . . 5
![(](lp.gif) 1 ![_V](rmcv.gif) ![)](rp.gif) |
3 | | pw1exg 4302 |
. . . . 5
![(](lp.gif) 1 1 1 ![_V](rmcv.gif) ![)](rp.gif) |
4 | | addcexlem 4382 |
. . . . . 6
Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
![_V](rmcv.gif) |
5 | | imakexg 4299 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif)
1 1
![_V](rmcv.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![_V](rmcv.gif) ![)](rp.gif) |
6 | 4, 5 | mpan 651 |
. . . . 5
![(](lp.gif) 1 1 ![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![_V](rmcv.gif) ![)](rp.gif) |
7 | 2, 3, 6 | 3syl 18 |
. . . 4
![(](lp.gif) ![(](lp.gif) Ins3k ∼
![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![_V](rmcv.gif) ![)](rp.gif) |
8 | | imakexg 4299 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![V](_cv.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
9 | 7, 8 | sylan 457 |
. . 3
![(](lp.gif) ![(](lp.gif)
![V](_cv.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
10 | 9 | ancoms 439 |
. 2
![(](lp.gif) ![(](lp.gif)
![W](_cw.gif) ![(](lp.gif) ![(](lp.gif) Ins3k ∼ ![(](lp.gif) Ins3k Sk Ins2k Sk ![)](rp.gif) k 1 1 1c ![(](lp.gif) Ins2k Ins2k Sk Ins2k Ins3k Sk Ins3k SIk SIk Sk ![)](rp.gif) ![)](rp.gif) k 1 1 1 1 1c![)](rp.gif) ![)](rp.gif) k 1 1 ![B](_cb.gif) ![)](rp.gif) k![A](_ca.gif) ![_V](rmcv.gif) ![)](rp.gif) |
11 | 1, 10 | syl5eqel 2437 |
1
![(](lp.gif) ![(](lp.gif)
![W](_cw.gif) ![(](lp.gif) ![B](_cb.gif)
![_V](rmcv.gif) ![)](rp.gif) |