Step | Hyp | Ref
| Expression |
1 | | nncdiv3 6277 |
. 2
![(](lp.gif) Nn ![E.](exists.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
2 | | id 19 |
. . . . . . 7
![(](lp.gif) Nn Nn ![)](rp.gif) |
3 | | nntccl 6170 |
. . . . . . 7
![(](lp.gif) Nn Tc Nn ![)](rp.gif) |
4 | | nnc3n3p1 6278 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Nn Tc Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif)
Tc ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) |
5 | 2, 3, 4 | syl2anc 642 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif)
Tc ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) |
6 | | nncaddccl 4419 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nn Nn ![(](lp.gif) ![n](_n.gif) Nn ![)](rp.gif) |
7 | 6 | anidms 626 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) ![n](_n.gif)
Nn ![)](rp.gif) |
8 | | nnnc 6146 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) Nn ![(](lp.gif) ![n](_n.gif)
NC ![)](rp.gif) |
9 | 7, 8 | syl 15 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) ![n](_n.gif)
NC ![)](rp.gif) |
10 | | nnnc 6146 |
. . . . . . . . . 10
![(](lp.gif) Nn NC ![)](rp.gif) |
11 | | tcdi 6164 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
NC
NC Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc ![(](lp.gif) ![n](_n.gif) Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 9, 10, 11 | syl2anc 642 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc ![(](lp.gif) ![n](_n.gif) Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | tcdi 6164 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) NC NC Tc ![(](lp.gif)
![n](_n.gif)
Tc Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 10, 10, 13 | syl2anc 642 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![n](_n.gif) Tc Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 14 | addceq1d 4389 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![n](_n.gif) Tc ![n](_n.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 12, 15 | eqtrd 2385 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
18 | 17 | eqeq2d 2364 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 5, 18 | mtbird 292 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
20 | | id 19 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
21 | | tceq 6158 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
23 | 20, 22 | eqeq12d 2367 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) Tc 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 23 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif)
Tc 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 19, 24 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | nncaddccl 4419 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
Nn
Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![)](rp.gif) |
27 | 7, 2, 26 | syl2anc 642 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn ![)](rp.gif) |
28 | | nnnc 6146 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) NC ![)](rp.gif) |
29 | 27, 28 | syl 15 |
. . . . . . . . . 10
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC ![)](rp.gif) |
30 | | 1cnc 6139 |
. . . . . . . . . 10
1c
NC |
31 | | tcdi 6164 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC 1c NC Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c![)](rp.gif) ![)](rp.gif) |
32 | 29, 30, 31 | sylancl 643 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c![)](rp.gif) ![)](rp.gif) |
33 | | tc1c 6165 |
. . . . . . . . . . 11
Tc 1c 1c |
34 | 33 | a1i 10 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc
1c
1c![)](rp.gif) |
35 | 16, 34 | addceq12d 4391 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
36 | 32, 35 | eqtrd 2385 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
37 | 36 | eqeq2d 2364 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif)
Tc ![n](_n.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 5, 37 | mtbird 292 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
39 | | peano2 4403 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c Nn ![)](rp.gif) |
40 | 27, 39 | syl 15 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c Nn ![)](rp.gif) |
41 | | nntccl 6170 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c Nn ![)](rp.gif) |
42 | 40, 41 | syl 15 |
. . . . . . 7
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c Nn ![)](rp.gif) |
43 | | suc11nnc 4558 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 27, 42, 43 | syl2anc 642 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 38, 44 | mtbird 292 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
46 | | id 19 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
47 | | tceq 6158 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c![)](rp.gif) ![)](rp.gif) |
48 | 47 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc 1c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
49 | 46, 48 | eqeq12d 2367 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif)
Tc 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 49 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 45, 50 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | | peano2 4403 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
53 | | nntccl 6170 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
Nn Tc ![(](lp.gif)
1c
Nn ![)](rp.gif) |
54 | 52, 53 | syl 15 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) 1c
Nn ![)](rp.gif) |
55 | | nnc3n3p2 6279 |
. . . . . . . 8
![(](lp.gif) Tc ![(](lp.gif) 1c
Nn
Nn ![(](lp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
56 | 54, 2, 55 | syl2anc 642 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
57 | | 2nnc 6167 |
. . . . . . . . . . . . . 14
2c
Nn |
58 | | nncaddccl 4419 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn 2c Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Nn ![)](rp.gif) |
59 | 27, 57, 58 | sylancl 643 |
. . . . . . . . . . . . 13
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Nn ![)](rp.gif) |
60 | | nnnc 6146 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
NC ![)](rp.gif) |
61 | 59, 60 | syl 15 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c NC ![)](rp.gif) |
62 | | tcdi 6164 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c NC 1c NC Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Tc 1c![)](rp.gif) ![)](rp.gif) |
63 | 61, 30, 62 | sylancl 643 |
. . . . . . . . . . 11
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Tc 1c![)](rp.gif) ![)](rp.gif) |
64 | 63 | eqcomd 2358 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Tc 1c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) |
65 | 33 | addceq2i 4387 |
. . . . . . . . . 10
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Tc 1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) |
66 | | addccom 4406 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) 1c 1c ![n](_n.gif) ![(](lp.gif) 1c
1c![)](rp.gif) ![)](rp.gif) |
67 | | 1p1e2c 6155 |
. . . . . . . . . . . . . . . . . 18
1c
1c
2c |
68 | 67 | addceq2i 4387 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) 1c 1c![)](rp.gif)
![(](lp.gif) 2c![)](rp.gif) |
69 | 66, 68 | eqtr2i 2374 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) 2c
![(](lp.gif) 1c 1c ![n](_n.gif) ![)](rp.gif) |
70 | 69 | addceq1i 4386 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
2c
1c
![(](lp.gif) ![(](lp.gif) 1c 1c ![n](_n.gif) 1c![)](rp.gif) |
71 | | addcass 4415 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif)
2c
1c
![(](lp.gif) 2c 1c![)](rp.gif) ![)](rp.gif) |
72 | | addcass 4415 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) 1c 1c ![n](_n.gif) 1c ![(](lp.gif) 1c 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
73 | 70, 71, 72 | 3eqtr3i 2381 |
. . . . . . . . . . . . . 14
![(](lp.gif) 2c 1c![)](rp.gif)
![(](lp.gif) 1c 1c ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
74 | 73 | addceq2i 4387 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) 2c 1c![)](rp.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) 1c
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
75 | | addcass 4415 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![(](lp.gif) 2c 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
76 | | addcass 4415 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 1c![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![(](lp.gif) 1c
1c
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
77 | 74, 75, 76 | 3eqtr4i 2383 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 1c![)](rp.gif)
![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
78 | | addcass 4415 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c![)](rp.gif) ![)](rp.gif) |
79 | | addc4 4417 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) 1c 1c![)](rp.gif) ![)](rp.gif) |
80 | 79 | addceq1i 4386 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
1c 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
81 | 77, 78, 80 | 3eqtr4i 2383 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
82 | | tceq 6158 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . . 10
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) |
84 | 64, 65, 83 | 3eqtr3g 2408 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
85 | | nnnc 6146 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif)
1c
Nn ![(](lp.gif) 1c NC ![)](rp.gif) |
86 | 52, 85 | syl 15 |
. . . . . . . . . . . 12
![(](lp.gif) Nn ![(](lp.gif)
1c
NC ![)](rp.gif) |
87 | | ncaddccl 6144 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
NC ![(](lp.gif) 1c NC ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) NC ![)](rp.gif) |
88 | 86, 86, 87 | syl2anc 642 |
. . . . . . . . . . 11
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) NC ![)](rp.gif) |
89 | | tcdi 6164 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) NC ![(](lp.gif) 1c NC Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
90 | 88, 86, 89 | syl2anc 642 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
91 | | tcdi 6164 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
NC ![(](lp.gif) 1c NC Tc ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | 86, 86, 91 | syl2anc 642 |
. . . . . . . . . . 11
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
93 | 92 | addceq1d 4389 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
94 | 90, 93 | eqtrd 2385 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
1c
![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) 1c![)](rp.gif) ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
95 | 84, 94 | eqtrd 2385 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
96 | 95 | eqeq1d 2361 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif)
Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 56, 96 | mtbird 292 |
. . . . . 6
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
98 | | eqcom 2355 |
. . . . . 6
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) |
99 | 97, 98 | sylnib 295 |
. . . . 5
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) |
100 | | id 19 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
101 | | tceq 6158 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
102 | 101 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc 1c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) |
103 | 100, 102 | eqeq12d 2367 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif)
Tc 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
104 | 103 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) Tc 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
105 | 99, 104 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
106 | 25, 51, 105 | 3jaod 1246 |
. . 3
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
107 | 106 | rexlimiv 2732 |
. 2
![(](lp.gif) ![E.](exists.gif)
Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) Tc 1c![)](rp.gif) ![)](rp.gif) |
108 | 1, 107 | syl 15 |
1
![(](lp.gif) Nn Tc 1c![)](rp.gif) ![)](rp.gif) |