Step | Hyp | Ref
| Expression |
1 | | peano2nc 6145 |
. . . 4
![(](lp.gif) NC ![(](lp.gif)
1c
NC ![)](rp.gif) |
2 | | dflec2 6210 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) 1c NC ![(](lp.gif) c ![(](lp.gif) 1c ![E.](exists.gif) NC ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
3 | 1, 2 | sylan2 460 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif)
1c
![E.](exists.gif) NC ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
4 | | nc0suc 6217 |
. . . . 5
![(](lp.gif) NC ![(](lp.gif) 0c ![E.](exists.gif)
NC ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
5 | | addceq2 4384 |
. . . . . . . . . 10
![(](lp.gif) 0c ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) 0c![)](rp.gif) ![)](rp.gif) |
6 | | addcid1 4405 |
. . . . . . . . . 10
![(](lp.gif) 0c
![M](_cm.gif) |
7 | 5, 6 | syl6eq 2401 |
. . . . . . . . 9
![(](lp.gif) 0c ![(](lp.gif) ![p](_p.gif)
![M](_cm.gif) ![)](rp.gif) |
8 | 7 | eqeq2d 2364 |
. . . . . . . 8
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif)
1c
![M](_cm.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | olc 373 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 9 | eqcoms 2356 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 8, 10 | syl6bi 219 |
. . . . . . 7
![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | a1i 10 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 0c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | addceq2 4384 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
14 | | addcass 4415 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c
![(](lp.gif) ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
15 | 13, 14 | syl6eqr 2403 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif)
![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) |
16 | 15 | eqeq2d 2364 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | biimpa 470 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![q](_q.gif) 1c![)](rp.gif) ![)](rp.gif) |
18 | | simplr 731 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC
NC ![)](rp.gif) |
19 | | ncaddccl 6144 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![q](_q.gif) NC ![)](rp.gif) |
20 | 19 | adantlr 695 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![q](_q.gif)
NC ![)](rp.gif) |
21 | | peano4nc 6150 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC ![(](lp.gif) ![q](_q.gif)
NC ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 18, 20, 21 | syl2anc 642 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | | addlecncs 6209 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC NC c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | adantlr 695 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | breq2 4643 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![q](_q.gif)
![(](lp.gif) c c ![(](lp.gif) ![q](_q.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 24, 25 | syl5ibrcom 213 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![(](lp.gif) ![q](_q.gif) c ![N](_cn.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | orc 374 |
. . . . . . . . . . 11
![(](lp.gif) c ![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 26, 27 | syl6 29 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![(](lp.gif) ![q](_q.gif) ![(](lp.gif)
c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
29 | 22, 28 | sylbid 206 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![(](lp.gif)
![q](_q.gif) 1c ![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
30 | 17, 29 | syl5 28 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![)](rp.gif) ![(](lp.gif)
c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 30 | exp3a 425 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif)
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) ![(](lp.gif)
c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 31 | rexlimdva 2738 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
NC ![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) 1c
![(](lp.gif) ![p](_p.gif) ![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 12, 32 | jaod 369 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif)
0c ![E.](exists.gif) NC ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) ![(](lp.gif)
c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 4, 33 | syl5 28 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) ![p](_p.gif) ![(](lp.gif) c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | rexlimdv 2737 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![E.](exists.gif)
NC ![(](lp.gif)
1c
![(](lp.gif) ![p](_p.gif) ![(](lp.gif)
c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 3, 35 | sylbid 206 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | | 1cnc 6139 |
. . . . . 6
1c
NC |
38 | | addlecncs 6209 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC 1c NC c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
39 | 37, 38 | mpan2 652 |
. . . . 5
![(](lp.gif) NC c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
40 | 39 | adantl 452 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
41 | 1 | adantl 452 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c
NC ![)](rp.gif) |
42 | | lectr 6211 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c NC ![(](lp.gif) ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 41, 42 | mpd3an3 1278 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 40, 43 | mpan2d 655 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | | nclecid 6197 |
. . . . . 6
![(](lp.gif) ![(](lp.gif)
1c
NC ![(](lp.gif) 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
46 | 1, 45 | syl 15 |
. . . . 5
![(](lp.gif) NC ![(](lp.gif)
1c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | 46 | adantl 452 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
48 | | breq1 4642 |
. . . 4
![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif) c ![(](lp.gif) 1c ![(](lp.gif)
1c
c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 47, 48 | syl5ibrcom 213 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) 1c c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 44, 49 | jaod 369 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 36, 50 | impbid 183 |
1
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) c ![(](lp.gif)
1c
![(](lp.gif) c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |