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 | | nnc3n3p2 6279 |
. . . . . . 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)
2c![)](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)
2c![)](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) 2c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 2c![)](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) 2c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) 2c![)](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) 2c![)](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 2c Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](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 2c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](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 2c ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](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 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
26 | | nncaddccl 4419 |
. . . . . . . . . 10
![(](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 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn ![)](rp.gif) |
28 | | nntccl 6170 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![)](rp.gif) |
29 | 27, 28 | syl 15 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn ![)](rp.gif) |
30 | | 2nnc 6167 |
. . . . . . . . . 10
2c
Nn |
31 | | nncaddccl 4419 |
. . . . . . . . . 10
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Nn 2c Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Nn ![)](rp.gif) |
32 | 29, 30, 31 | sylancl 643 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Nn ![)](rp.gif) |
33 | | suc11nnc 4558 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
Nn
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 27, 32, 33 | syl2anc 642 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c
![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 19, 34 | mtbird 292 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c![)](rp.gif) ![)](rp.gif) |
36 | | addc32 4416 |
. . . . . . . . 9
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c Tc
1c![)](rp.gif) |
37 | | tc1c 6165 |
. . . . . . . . . 10
Tc 1c 1c |
38 | 37 | addceq2i 4387 |
. . . . . . . . 9
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc 1c ![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c![)](rp.gif) |
39 | 36, 38 | eqtri 2373 |
. . . . . . . 8
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c 1c![)](rp.gif) |
40 | 39 | eqeq2i 2363 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c ![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
1c![)](rp.gif) ![)](rp.gif) |
41 | 35, 40 | sylnibr 296 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c![)](rp.gif) ![)](rp.gif) |
42 | | nnnc 6146 |
. . . . . . . . . 10
![(](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) |
43 | 27, 42 | syl 15 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC ![)](rp.gif) |
44 | | 1cnc 6139 |
. . . . . . . . 9
1c
NC |
45 | | tcdi 6164 |
. . . . . . . . 9
![(](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) |
46 | 43, 44, 45 | sylancl 643 |
. . . . . . . 8
![(](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) |
47 | 46 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
2c
![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c![)](rp.gif) ![)](rp.gif) |
48 | 47 | eqeq2d 2364 |
. . . . . 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
2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 1c ![(](lp.gif) Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 1c 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 41, 48 | 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
2c![)](rp.gif) ![)](rp.gif) |
50 | | 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) |
51 | | 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) |
52 | 51 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
Tc 2c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
2c![)](rp.gif) ![)](rp.gif) |
53 | 50, 52 | eqeq12d 2367 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif)
Tc 2c ![(](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
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 53 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
1c
![(](lp.gif) Tc 2c ![(](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
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 49, 54 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 1c
Tc 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | | peano2 4403 |
. . . . . . . . 9
![(](lp.gif) Nn ![(](lp.gif)
1c
Nn ![)](rp.gif) |
57 | | nntccl 6170 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif)
1c
Nn Tc ![(](lp.gif)
1c
Nn ![)](rp.gif) |
58 | 56, 57 | syl 15 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) 1c
Nn ![)](rp.gif) |
59 | | nnc3p1n3p2 6280 |
. . . . . . . 8
![(](lp.gif) Tc ![(](lp.gif) 1c
Nn
Nn ![(](lp.gif) ![(](lp.gif)
Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
60 | 58, 2, 59 | syl2anc 642 |
. . . . . . 7
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
61 | | eqcom 2355 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) Tc ![(](lp.gif) 1c Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c![)](rp.gif) ![)](rp.gif) |
62 | 60, 61 | sylnibr 296 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) ![(](lp.gif)
Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
63 | | addcass 4415 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
1c 1c![)](rp.gif) ![)](rp.gif) |
64 | | addcass 4415 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
1c
![(](lp.gif) ![(](lp.gif)
Tc 1c Tc 1c![)](rp.gif) Tc 1c![)](rp.gif) ![)](rp.gif) |
65 | 64 | addceq1i 4386 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
1c
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc 1c![)](rp.gif)
1c![)](rp.gif) |
66 | | 1p1e2c 6155 |
. . . . . . . . . . . . . 14
1c
1c
2c |
67 | 66 | addceq2i 4387 |
. . . . . . . . . . . . 13
![(](lp.gif) Tc Tc ![n](_n.gif)
1c 1c![)](rp.gif)
![(](lp.gif) Tc Tc ![n](_n.gif) 2c![)](rp.gif) |
68 | | addc4 4417 |
. . . . . . . . . . . . 13
![(](lp.gif) Tc 1c
Tc 1c![)](rp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) 1c 1c![)](rp.gif) ![)](rp.gif) |
69 | | tc2c 6166 |
. . . . . . . . . . . . . 14
Tc 2c 2c |
70 | 69 | addceq2i 4387 |
. . . . . . . . . . . . 13
![(](lp.gif) Tc Tc ![n](_n.gif)
Tc 2c ![(](lp.gif) Tc Tc ![n](_n.gif) 2c![)](rp.gif) |
71 | 67, 68, 70 | 3eqtr4i 2383 |
. . . . . . . . . . . 12
![(](lp.gif) Tc 1c
Tc 1c![)](rp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc
2c![)](rp.gif) |
72 | 71 | addceq1i 4386 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
![(](lp.gif) ![(](lp.gif)
Tc Tc ![n](_n.gif) Tc 2c Tc ![n](_n.gif) ![)](rp.gif) |
73 | | addc32 4416 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc
2c
Tc ![n](_n.gif)
![(](lp.gif) ![(](lp.gif)
Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c![)](rp.gif) |
74 | 72, 73 | eqtri 2373 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
![(](lp.gif) ![(](lp.gif)
Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c![)](rp.gif) |
75 | 74, 66 | addceq12i 4388 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc ![n](_n.gif)
1c 1c![)](rp.gif)
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c 2c![)](rp.gif) |
76 | 63, 65, 75 | 3eqtr3ri 2382 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c 2c ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c
Tc 1c![)](rp.gif) Tc 1c![)](rp.gif)
1c![)](rp.gif) |
77 | | 2nc 6168 |
. . . . . . . . . . 11
2c
NC |
78 | | tcdi 6164 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif)
NC 2c NC Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 2c![)](rp.gif) ![)](rp.gif) |
79 | 43, 77, 78 | sylancl 643 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c
Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 2c![)](rp.gif) ![)](rp.gif) |
80 | 16 | addceq1d 4389 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) Tc 2c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c![)](rp.gif) ![)](rp.gif) |
81 | 79, 80 | eqtrd 2385 |
. . . . . . . . 9
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c![)](rp.gif) ![)](rp.gif) |
82 | 81 | addceq1d 4389 |
. . . . . . . 8
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc Tc ![n](_n.gif) Tc ![n](_n.gif) Tc 2c 2c![)](rp.gif) ![)](rp.gif) |
83 | | tcdi 6164 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) NC 1c NC Tc ![(](lp.gif)
1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
84 | 10, 44, 83 | sylancl 643 |
. . . . . . . . . . . 12
![(](lp.gif) Nn Tc ![(](lp.gif) 1c
Tc Tc 1c![)](rp.gif) ![)](rp.gif) |
85 | 37 | addceq2i 4387 |
. . . . . . . . . . . 12
Tc Tc 1c Tc 1c![)](rp.gif) |
86 | 84, 85 | syl6eq 2401 |
. . . . . . . . . . 11
![(](lp.gif) Nn Tc ![(](lp.gif) 1c
Tc 1c![)](rp.gif) ![)](rp.gif) |
87 | 86, 86 | addceq12d 4391 |
. . . . . . . . . 10
![(](lp.gif) Nn Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
88 | 87, 86 | addceq12d 4391 |
. . . . . . . . 9
![(](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) Tc 1c Tc 1c![)](rp.gif) Tc 1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
89 | 88 | addceq1d 4389 |
. . . . . . . 8
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) Tc 1c Tc 1c![)](rp.gif) Tc 1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
90 | 76, 82, 89 | 3eqtr4a 2411 |
. . . . . . 7
![(](lp.gif) Nn Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
2c
![(](lp.gif) ![(](lp.gif)
Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) |
91 | 90 | eqeq2d 2364 |
. . . . . 6
![(](lp.gif) Nn ![(](lp.gif) ![(](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
2c
![(](lp.gif) ![(](lp.gif) ![(](lp.gif)
![n](_n.gif) ![n](_n.gif) 2c ![(](lp.gif) ![(](lp.gif) Tc ![(](lp.gif)
1c
Tc ![(](lp.gif)
1c![)](rp.gif) Tc ![(](lp.gif)
1c![)](rp.gif)
1c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
92 | 62, 91 | mtbird 292 |
. . . . 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
2c![)](rp.gif) ![)](rp.gif) |
93 | | 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) |
94 | | 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) |
95 | 94 | addceq1d 4389 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
Tc 2c Tc ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
2c![)](rp.gif) ![)](rp.gif) |
96 | 93, 95 | eqeq12d 2367 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif)
Tc 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
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
97 | 96 | notbid 285 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif) ![n](_n.gif)
2c
![(](lp.gif) Tc 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
2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
98 | 92, 97 | syl5ibrcom 213 |
. . . 4
![(](lp.gif) Nn ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![n](_n.gif)
![n](_n.gif) 2c
Tc 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
99 | 25, 55, 98 | 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 2c![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
100 | 99 | 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 2c![)](rp.gif) ![)](rp.gif) |
101 | 1, 100 | syl 15 |
1
![(](lp.gif) Nn Tc 2c![)](rp.gif) ![)](rp.gif) |