Step | Hyp | Ref
| Expression |
1 | | vex 2863 |
. . . . . . . 8
⊢ a ∈
V |
2 | 1 | elcompl 3226 |
. . . . . . 7
⊢ (a ∈ ∼ (ran
(ran (( AddC ∘
◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ↔ ¬ a
∈ (ran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn )) |
3 | | elima 4755 |
. . . . . . . . 9
⊢ (a ∈ (ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ↔ ∃n ∈ Nn nran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))a) |
4 | | df-br 4641 |
. . . . . . . . . . 11
⊢ (nran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))a ↔ 〈n, a〉 ∈ ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
5 | | elrn 4897 |
. . . . . . . . . . . 12
⊢ (〈n, a〉 ∈ ran (ran (( AddC
∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ ∃p p(ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))〈n, a〉) |
6 | | df-br 4641 |
. . . . . . . . . . . . . . 15
⊢ (p(ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))〈n, a〉 ↔ 〈p, 〈n, a〉〉 ∈ (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
7 | | oteltxp 5783 |
. . . . . . . . . . . . . . 15
⊢ (〈p, 〈n, a〉〉 ∈ (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ (〈p, n〉 ∈ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∧ 〈p, a〉 ∈ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
8 | 6, 7 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (p(ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))〈n, a〉 ↔ (〈p, n〉 ∈ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∧ 〈p, a〉 ∈ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
9 | | elrn2 4898 |
. . . . . . . . . . . . . . . 16
⊢ (〈p, n〉 ∈ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ ∃q〈q, 〈p, n〉〉 ∈ (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
10 | | oteltxp 5783 |
. . . . . . . . . . . . . . . . . 18
⊢ (〈q, 〈p, n〉〉 ∈ (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ (〈q, p〉 ∈ ( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ∧ 〈q, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))) |
11 | | opelco 4885 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈q, p〉 ∈ ( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ↔ ∃x(q◡(1st ↾ (◡2nd “
{1c}))x ∧ x AddC p)) |
12 | | brcnv 4893 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (q◡(1st ↾ (◡2nd “
{1c}))x ↔ x(1st ↾ (◡2nd “
{1c}))q) |
13 | | brres 4950 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (x(1st ↾ (◡2nd “
{1c}))q ↔ (x1st q ∧ x ∈ (◡2nd “
{1c}))) |
14 | 12, 13 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (q◡(1st ↾ (◡2nd “
{1c}))x ↔ (x1st q ∧ x ∈ (◡2nd “
{1c}))) |
15 | | eliniseg 5021 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (x ∈ (◡2nd “
{1c}) ↔ x2nd
1c) |
16 | 15 | anbi2i 675 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((x1st q ∧ x ∈ (◡2nd “
{1c})) ↔ (x1st q ∧ x2nd
1c)) |
17 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ q ∈
V |
18 | | 1cex 4143 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
1c ∈
V |
19 | 17, 18 | op1st2nd 5791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((x1st q ∧ x2nd 1c) ↔
x = 〈q,
1c〉) |
20 | 14, 16, 19 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (q◡(1st ↾ (◡2nd “
{1c}))x ↔ x = 〈q, 1c〉) |
21 | 20 | anbi1i 676 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((q◡(1st ↾ (◡2nd “
{1c}))x ∧ x AddC p) ↔
(x = 〈q,
1c〉 ∧ x AddC p)) |
22 | 21 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃x(q◡(1st ↾ (◡2nd “
{1c}))x ∧ x AddC p) ↔ ∃x(x = 〈q, 1c〉 ∧ x AddC p)) |
23 | 17, 18 | opex 4589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 〈q,
1c〉 ∈ V |
24 | | breq1 4643 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (x = 〈q, 1c〉 → (x
AddC p ↔
〈q,
1c〉 AddC p)) |
25 | 23, 24 | ceqsexv 2895 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (∃x(x = 〈q, 1c〉 ∧ x AddC p) ↔ 〈q,
1c〉 AddC p) |
26 | 22, 25 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃x(q◡(1st ↾ (◡2nd “
{1c}))x ∧ x AddC p) ↔ 〈q,
1c〉 AddC p) |
27 | 17, 18 | braddcfn 5827 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈q,
1c〉 AddC p ↔
(q +c
1c) = p) |
28 | | eqcom 2355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((q +c 1c) =
p ↔ p = (q
+c 1c)) |
29 | 27, 28 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈q,
1c〉 AddC p ↔
p = (q
+c 1c)) |
30 | 11, 26, 29 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈q, p〉 ∈ ( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ↔ p =
(q +c
1c)) |
31 | | opelcnv 4894 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈q, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ 〈n, q〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) |
32 | | nncdiv3lem1 6276 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈n, q〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ q = ((n
+c n)
+c n)) |
33 | 31, 32 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈q, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ q = ((n
+c n)
+c n)) |
34 | 30, 33 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((〈q, p〉 ∈ ( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ∧ 〈q, n〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ (p = (q
+c 1c) ∧
q = ((n
+c n)
+c n))) |
35 | | ancom 437 |
. . . . . . . . . . . . . . . . . 18
⊢ ((p = (q
+c 1c) ∧
q = ((n
+c n)
+c n)) ↔ (q = ((n
+c n)
+c n) ∧ p = (q +c
1c))) |
36 | 10, 34, 35 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
⊢ (〈q, 〈p, n〉〉 ∈ (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ (q = ((n
+c n)
+c n) ∧ p = (q +c
1c))) |
37 | 36 | exbii 1582 |
. . . . . . . . . . . . . . . 16
⊢ (∃q〈q, 〈p, n〉〉 ∈ (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ ∃q(q = ((n
+c n)
+c n) ∧ p = (q +c
1c))) |
38 | | vex 2863 |
. . . . . . . . . . . . . . . . . . 19
⊢ n ∈
V |
39 | 38, 38 | addcex 4395 |
. . . . . . . . . . . . . . . . . 18
⊢ (n +c n) ∈
V |
40 | 39, 38 | addcex 4395 |
. . . . . . . . . . . . . . . . 17
⊢ ((n +c n) +c n) ∈
V |
41 | | addceq1 4384 |
. . . . . . . . . . . . . . . . . 18
⊢ (q = ((n
+c n)
+c n) → (q +c 1c) =
(((n +c n) +c n) +c
1c)) |
42 | 41 | eqeq2d 2364 |
. . . . . . . . . . . . . . . . 17
⊢ (q = ((n
+c n)
+c n) → (p = (q
+c 1c) ↔ p = (((n
+c n)
+c n)
+c 1c))) |
43 | 40, 42 | ceqsexv 2895 |
. . . . . . . . . . . . . . . 16
⊢ (∃q(q = ((n
+c n)
+c n) ∧ p = (q +c 1c)) ↔
p = (((n +c n) +c n) +c
1c)) |
44 | 9, 37, 43 | 3bitri 262 |
. . . . . . . . . . . . . . 15
⊢ (〈p, n〉 ∈ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ p = (((n
+c n)
+c n)
+c 1c)) |
45 | | opelcnv 4894 |
. . . . . . . . . . . . . . . 16
⊢ (〈p, a〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ 〈a, p〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) |
46 | | nncdiv3lem1 6276 |
. . . . . . . . . . . . . . . 16
⊢ (〈a, p〉 ∈ ran ( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ p = ((a
+c a)
+c a)) |
47 | 45, 46 | bitri 240 |
. . . . . . . . . . . . . . 15
⊢ (〈p, a〉 ∈ ◡ran (
Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ↔ p = ((a
+c a)
+c a)) |
48 | 44, 47 | anbi12i 678 |
. . . . . . . . . . . . . 14
⊢ ((〈p, n〉 ∈ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∧ 〈p, a〉 ∈ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ (p = (((n
+c n)
+c n)
+c 1c) ∧
p = ((a
+c a)
+c a))) |
49 | | ancom 437 |
. . . . . . . . . . . . . 14
⊢ ((p = (((n
+c n)
+c n)
+c 1c) ∧
p = ((a
+c a)
+c a)) ↔ (p = ((a
+c a)
+c a) ∧ p =
(((n +c n) +c n) +c
1c))) |
50 | 8, 48, 49 | 3bitri 262 |
. . . . . . . . . . . . 13
⊢ (p(ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))〈n, a〉 ↔
(p = ((a +c a) +c a) ∧ p = (((n
+c n)
+c n)
+c 1c))) |
51 | 50 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃p p(ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))〈n, a〉 ↔ ∃p(p = ((a
+c a)
+c a) ∧ p =
(((n +c n) +c n) +c
1c))) |
52 | 1, 1 | addcex 4395 |
. . . . . . . . . . . . . 14
⊢ (a +c a) ∈
V |
53 | 52, 1 | addcex 4395 |
. . . . . . . . . . . . 13
⊢ ((a +c a) +c a) ∈
V |
54 | | eqeq1 2359 |
. . . . . . . . . . . . 13
⊢ (p = ((a
+c a)
+c a) → (p = (((n
+c n)
+c n)
+c 1c) ↔ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c))) |
55 | 53, 54 | ceqsexv 2895 |
. . . . . . . . . . . 12
⊢ (∃p(p = ((a
+c a)
+c a) ∧ p =
(((n +c n) +c n) +c 1c))
↔ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
56 | 5, 51, 55 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (〈n, a〉 ∈ ran (ran (( AddC
∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ↔ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
57 | 4, 56 | bitri 240 |
. . . . . . . . . 10
⊢ (nran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))a ↔ ((a
+c a)
+c a) = (((n +c n) +c n) +c
1c)) |
58 | 57 | rexbii 2640 |
. . . . . . . . 9
⊢ (∃n ∈ Nn nran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )))a ↔ ∃n ∈ Nn ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
59 | | dfrex2 2628 |
. . . . . . . . 9
⊢ (∃n ∈ Nn ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ ∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
60 | 3, 58, 59 | 3bitrri 263 |
. . . . . . . 8
⊢ (¬ ∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ a ∈ (ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn )) |
61 | 60 | con1bii 321 |
. . . . . . 7
⊢ (¬ a ∈ (ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ↔ ∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
62 | 2, 61 | bitri 240 |
. . . . . 6
⊢ (a ∈ ∼ (ran
(ran (( AddC ∘
◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ↔ ∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)) |
63 | 62 | abbi2i 2465 |
. . . . 5
⊢ ∼ (ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) = {a ∣ ∀n ∈ Nn ¬ ((a
+c a)
+c a) = (((n +c n) +c n) +c
1c)} |
64 | | addcfnex 5825 |
. . . . . . . . . . . 12
⊢ AddC ∈
V |
65 | | 1stex 4740 |
. . . . . . . . . . . . . 14
⊢ 1st
∈ V |
66 | | 2ndex 5113 |
. . . . . . . . . . . . . . . 16
⊢ 2nd
∈ V |
67 | 66 | cnvex 5103 |
. . . . . . . . . . . . . . 15
⊢ ◡2nd ∈ V |
68 | | snex 4112 |
. . . . . . . . . . . . . . 15
⊢
{1c} ∈
V |
69 | 67, 68 | imaex 4748 |
. . . . . . . . . . . . . 14
⊢ (◡2nd “
{1c}) ∈ V |
70 | 65, 69 | resex 5118 |
. . . . . . . . . . . . 13
⊢ (1st
↾ (◡2nd “
{1c})) ∈ V |
71 | 70 | cnvex 5103 |
. . . . . . . . . . . 12
⊢ ◡(1st ↾ (◡2nd “
{1c})) ∈ V |
72 | 64, 71 | coex 4751 |
. . . . . . . . . . 11
⊢ ( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ∈
V |
73 | 65 | cnvex 5103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ◡1st ∈ V |
74 | 65, 66 | inex 4106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1st
∩ 2nd ) ∈ V |
75 | 73, 74 | txpex 5786 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡1st ⊗ (1st
∩ 2nd )) ∈ V |
76 | 75 | rnex 5108 |
. . . . . . . . . . . . . . . . . 18
⊢ ran (◡1st ⊗ (1st
∩ 2nd )) ∈ V |
77 | 76, 66 | txpex 5786 |
. . . . . . . . . . . . . . . . 17
⊢ (ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) ∈ V |
78 | 77, 64 | imaex 4748 |
. . . . . . . . . . . . . . . 16
⊢ ((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
79 | 78 | cnvex 5103 |
. . . . . . . . . . . . . . 15
⊢ ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
80 | 79 | ins3ex 5799 |
. . . . . . . . . . . . . 14
⊢ Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∈
V |
81 | 65, 65 | coex 4751 |
. . . . . . . . . . . . . . . 16
⊢ (1st
∘ 1st ) ∈ V |
82 | 66, 65 | coex 4751 |
. . . . . . . . . . . . . . . . 17
⊢ (2nd
∘ 1st ) ∈ V |
83 | 82, 66 | txpex 5786 |
. . . . . . . . . . . . . . . 16
⊢ ((2nd
∘ 1st ) ⊗ 2nd )
∈ V |
84 | 81, 83 | txpex 5786 |
. . . . . . . . . . . . . . 15
⊢ ((1st
∘ 1st ) ⊗ ((2nd
∘ 1st ) ⊗ 2nd
)) ∈ V |
85 | 84, 64 | imaex 4748 |
. . . . . . . . . . . . . 14
⊢ (((1st
∘ 1st ) ⊗ ((2nd
∘ 1st ) ⊗ 2nd
)) “ AddC ) ∈ V |
86 | 80, 85 | inex 4106 |
. . . . . . . . . . . . 13
⊢ ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
87 | 86 | rnex 5108 |
. . . . . . . . . . . 12
⊢ ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
88 | 87 | cnvex 5103 |
. . . . . . . . . . 11
⊢ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC )) ∈ V |
89 | 72, 88 | txpex 5786 |
. . . . . . . . . 10
⊢ (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∈ V |
90 | 89 | rnex 5108 |
. . . . . . . . 9
⊢ ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∈ V |
91 | 90, 88 | txpex 5786 |
. . . . . . . 8
⊢ (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∈ V |
92 | 91 | rnex 5108 |
. . . . . . 7
⊢ ran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ∈ V |
93 | | nncex 4397 |
. . . . . . 7
⊢ Nn ∈
V |
94 | 92, 93 | imaex 4748 |
. . . . . 6
⊢ (ran (ran (( AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ∈
V |
95 | 94 | complex 4105 |
. . . . 5
⊢ ∼ (ran (ran ((
AddC ∘ ◡(1st ↾ (◡2nd “
{1c}))) ⊗ ◡ran
( Ins3 ◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) ⊗ ◡ran ( Ins3
◡((ran (◡1st ⊗ (1st
∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd ∘ 1st ) ⊗ 2nd ))
“ AddC ))) “ Nn ) ∈
V |
96 | 63, 95 | eqeltrri 2424 |
. . . 4
⊢ {a ∣ ∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c)} ∈
V |
97 | | addceq12 4386 |
. . . . . . . . . 10
⊢ ((a = 0c ∧ a =
0c) → (a
+c a) =
(0c +c
0c)) |
98 | 97 | anidms 626 |
. . . . . . . . 9
⊢ (a = 0c → (a +c a) = (0c +c
0c)) |
99 | | id 19 |
. . . . . . . . 9
⊢ (a = 0c → a = 0c) |
100 | 98, 99 | addceq12d 4392 |
. . . . . . . 8
⊢ (a = 0c → ((a +c a) +c a) = ((0c +c
0c) +c
0c)) |
101 | | addcid1 4406 |
. . . . . . . . 9
⊢
((0c +c 0c)
+c 0c) = (0c
+c 0c) |
102 | | addcid2 4408 |
. . . . . . . . 9
⊢
(0c +c 0c) =
0c |
103 | 101, 102 | eqtri 2373 |
. . . . . . . 8
⊢
((0c +c 0c)
+c 0c) =
0c |
104 | 100, 103 | syl6eq 2401 |
. . . . . . 7
⊢ (a = 0c → ((a +c a) +c a) = 0c) |
105 | 104 | eqeq1d 2361 |
. . . . . 6
⊢ (a = 0c → (((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ 0c =
(((n +c n) +c n) +c
1c))) |
106 | 105 | notbid 285 |
. . . . 5
⊢ (a = 0c → (¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ 0c =
(((n +c n) +c n) +c
1c))) |
107 | 106 | ralbidv 2635 |
. . . 4
⊢ (a = 0c → (∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ∀n ∈ Nn ¬
0c = (((n
+c n)
+c n)
+c 1c))) |
108 | | addceq12 4386 |
. . . . . . . . 9
⊢ ((a = m ∧ a = m) → (a
+c a) = (m +c m)) |
109 | 108 | anidms 626 |
. . . . . . . 8
⊢ (a = m →
(a +c a) = (m
+c m)) |
110 | | id 19 |
. . . . . . . 8
⊢ (a = m →
a = m) |
111 | 109, 110 | addceq12d 4392 |
. . . . . . 7
⊢ (a = m →
((a +c a) +c a) = ((m
+c m)
+c m)) |
112 | 111 | eqeq1d 2361 |
. . . . . 6
⊢ (a = m →
(((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c))) |
113 | 112 | notbid 285 |
. . . . 5
⊢ (a = m →
(¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c))) |
114 | 113 | ralbidv 2635 |
. . . 4
⊢ (a = m →
(∀n
∈ Nn ¬
((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c))) |
115 | | addceq12 4386 |
. . . . . . . . . 10
⊢ ((a = (m
+c 1c) ∧
a = (m
+c 1c)) → (a +c a) = ((m
+c 1c) +c (m +c
1c))) |
116 | 115 | anidms 626 |
. . . . . . . . 9
⊢ (a = (m
+c 1c) → (a +c a) = ((m
+c 1c) +c (m +c
1c))) |
117 | | id 19 |
. . . . . . . . 9
⊢ (a = (m
+c 1c) → a = (m
+c 1c)) |
118 | 116, 117 | addceq12d 4392 |
. . . . . . . 8
⊢ (a = (m
+c 1c) → ((a +c a) +c a) = (((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c))) |
119 | 118 | eqeq1d 2361 |
. . . . . . 7
⊢ (a = (m
+c 1c) → (((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((n +c n) +c n) +c
1c))) |
120 | 119 | notbid 285 |
. . . . . 6
⊢ (a = (m
+c 1c) → (¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((n +c n) +c n) +c
1c))) |
121 | 120 | ralbidv 2635 |
. . . . 5
⊢ (a = (m
+c 1c) → (∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ∀n ∈ Nn ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((n +c n) +c n) +c
1c))) |
122 | | addceq12 4386 |
. . . . . . . . . . 11
⊢ ((n = p ∧ n = p) → (n
+c n) = (p +c p)) |
123 | 122 | anidms 626 |
. . . . . . . . . 10
⊢ (n = p →
(n +c n) = (p
+c p)) |
124 | | id 19 |
. . . . . . . . . 10
⊢ (n = p →
n = p) |
125 | 123, 124 | addceq12d 4392 |
. . . . . . . . 9
⊢ (n = p →
((n +c n) +c n) = ((p
+c p)
+c p)) |
126 | 125 | addceq1d 4390 |
. . . . . . . 8
⊢ (n = p →
(((n +c n) +c n) +c 1c) =
(((p +c p) +c p) +c
1c)) |
127 | 126 | eqeq2d 2364 |
. . . . . . 7
⊢ (n = p →
((((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((n +c n) +c n) +c 1c) ↔
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
128 | 127 | notbid 285 |
. . . . . 6
⊢ (n = p →
(¬ (((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((n +c n) +c n) +c 1c) ↔
¬ (((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
129 | 128 | cbvralv 2836 |
. . . . 5
⊢ (∀n ∈ Nn ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((n +c n) +c n) +c 1c) ↔
∀p
∈ Nn ¬
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c)) |
130 | 121, 129 | syl6bb 252 |
. . . 4
⊢ (a = (m
+c 1c) → (∀n ∈ Nn ¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ∀p ∈ Nn ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c
1c))) |
131 | | addceq12 4386 |
. . . . . . . . 9
⊢ ((a = A ∧ a = A) → (a
+c a) = (A +c A)) |
132 | 131 | anidms 626 |
. . . . . . . 8
⊢ (a = A →
(a +c a) = (A
+c A)) |
133 | | id 19 |
. . . . . . . 8
⊢ (a = A →
a = A) |
134 | 132, 133 | addceq12d 4392 |
. . . . . . 7
⊢ (a = A →
((a +c a) +c a) = ((A
+c A)
+c A)) |
135 | 134 | eqeq1d 2361 |
. . . . . 6
⊢ (a = A →
(((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c))) |
136 | 135 | notbid 285 |
. . . . 5
⊢ (a = A →
(¬ ((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ ((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c))) |
137 | 136 | ralbidv 2635 |
. . . 4
⊢ (a = A →
(∀n
∈ Nn ¬
((a +c a) +c a) = (((n
+c n)
+c n)
+c 1c) ↔ ∀n ∈ Nn ¬ ((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c))) |
138 | | 1ne0c 6242 |
. . . . . . . 8
⊢
1c ≠ 0c |
139 | | df-ne 2519 |
. . . . . . . 8
⊢
(1c ≠ 0c ↔ ¬
1c = 0c) |
140 | 138, 139 | mpbi 199 |
. . . . . . 7
⊢ ¬
1c = 0c |
141 | 140 | intnan 880 |
. . . . . 6
⊢ ¬ (((n +c n) +c n) = 0c ∧ 1c =
0c) |
142 | | eqcom 2355 |
. . . . . . 7
⊢
(0c = (((n
+c n)
+c n)
+c 1c) ↔ (((n +c n) +c n) +c 1c) =
0c) |
143 | | nncaddccl 4420 |
. . . . . . . . . . 11
⊢ ((n ∈ Nn ∧ n ∈ Nn ) → (n
+c n) ∈ Nn
) |
144 | 143 | anidms 626 |
. . . . . . . . . 10
⊢ (n ∈ Nn → (n
+c n) ∈ Nn
) |
145 | | nncaddccl 4420 |
. . . . . . . . . 10
⊢ (((n +c n) ∈ Nn ∧ n ∈ Nn ) → ((n
+c n)
+c n) ∈ Nn
) |
146 | 144, 145 | mpancom 650 |
. . . . . . . . 9
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ Nn
) |
147 | | nnnc 6147 |
. . . . . . . . 9
⊢ (((n +c n) +c n) ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
148 | 146, 147 | syl 15 |
. . . . . . . 8
⊢ (n ∈ Nn → ((n
+c n)
+c n) ∈ NC
) |
149 | | 1cnc 6140 |
. . . . . . . 8
⊢
1c ∈ NC |
150 | | addceq0 6220 |
. . . . . . . 8
⊢ ((((n +c n) +c n) ∈ NC ∧
1c ∈ NC ) → ((((n
+c n)
+c n)
+c 1c) = 0c ↔
(((n +c n) +c n) = 0c ∧ 1c =
0c))) |
151 | 148, 149,
150 | sylancl 643 |
. . . . . . 7
⊢ (n ∈ Nn → ((((n
+c n)
+c n)
+c 1c) = 0c ↔
(((n +c n) +c n) = 0c ∧ 1c =
0c))) |
152 | 142, 151 | syl5bb 248 |
. . . . . 6
⊢ (n ∈ Nn → (0c = (((n +c n) +c n) +c 1c) ↔
(((n +c n) +c n) = 0c ∧ 1c =
0c))) |
153 | 141, 152 | mtbiri 294 |
. . . . 5
⊢ (n ∈ Nn → ¬ 0c = (((n +c n) +c n) +c
1c)) |
154 | 153 | rgen 2680 |
. . . 4
⊢ ∀n ∈ Nn ¬
0c = (((n
+c n)
+c n)
+c 1c) |
155 | | nnc0suc 4413 |
. . . . . . 7
⊢ (p ∈ Nn ↔ (p =
0c ∨ ∃q ∈ Nn p = (q
+c 1c))) |
156 | | 0cnsuc 4402 |
. . . . . . . . . . . . . . 15
⊢ ((((m +c 1c)
+c m)
+c m)
+c 1c) ≠
0c |
157 | | df-ne 2519 |
. . . . . . . . . . . . . . 15
⊢ (((((m +c 1c)
+c m)
+c m)
+c 1c) ≠ 0c ↔
¬ ((((m +c
1c) +c m) +c m) +c 1c) =
0c) |
158 | 156, 157 | mpbi 199 |
. . . . . . . . . . . . . 14
⊢ ¬ ((((m +c 1c)
+c m)
+c m)
+c 1c) =
0c |
159 | 158 | a1i 10 |
. . . . . . . . . . . . 13
⊢ (m ∈ Nn → ¬ ((((m +c 1c)
+c m)
+c m)
+c 1c) =
0c) |
160 | | addcass 4416 |
. . . . . . . . . . . . . . . 16
⊢ (((m +c 1c)
+c m)
+c 1c) = ((m +c 1c)
+c (m
+c 1c)) |
161 | 160 | addceq1i 4387 |
. . . . . . . . . . . . . . 15
⊢ ((((m +c 1c)
+c m)
+c 1c) +c m) = (((m
+c 1c) +c (m +c 1c))
+c m) |
162 | | addc32 4417 |
. . . . . . . . . . . . . . 15
⊢ ((((m +c 1c)
+c m)
+c 1c) +c m) = ((((m
+c 1c) +c m) +c m) +c
1c) |
163 | 161, 162 | eqtr3i 2375 |
. . . . . . . . . . . . . 14
⊢ (((m +c 1c)
+c (m
+c 1c)) +c m) = ((((m
+c 1c) +c m) +c m) +c
1c) |
164 | 163 | eqeq1i 2360 |
. . . . . . . . . . . . 13
⊢ ((((m +c 1c)
+c (m
+c 1c)) +c m) = 0c ↔ ((((m +c 1c)
+c m)
+c m)
+c 1c) =
0c) |
165 | 159, 164 | sylnibr 296 |
. . . . . . . . . . . 12
⊢ (m ∈ Nn → ¬ (((m
+c 1c) +c (m +c 1c))
+c m) =
0c) |
166 | | peano2 4404 |
. . . . . . . . . . . . . . 15
⊢ (m ∈ Nn → (m
+c 1c) ∈
Nn ) |
167 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . 16
⊢ (((m +c 1c) ∈ Nn ∧ (m
+c 1c) ∈
Nn ) → ((m +c 1c)
+c (m
+c 1c)) ∈
Nn ) |
168 | 167 | anidms 626 |
. . . . . . . . . . . . . . 15
⊢ ((m +c 1c) ∈ Nn → ((m +c 1c)
+c (m
+c 1c)) ∈
Nn ) |
169 | 166, 168 | syl 15 |
. . . . . . . . . . . . . 14
⊢ (m ∈ Nn → ((m
+c 1c) +c (m +c 1c)) ∈ Nn
) |
170 | | nncaddccl 4420 |
. . . . . . . . . . . . . 14
⊢ ((((m +c 1c)
+c (m
+c 1c)) ∈
Nn ∧ m ∈ Nn ) → (((m
+c 1c) +c (m +c 1c))
+c m) ∈ Nn
) |
171 | 169, 170 | mpancom 650 |
. . . . . . . . . . . . 13
⊢ (m ∈ Nn → (((m
+c 1c) +c (m +c 1c))
+c m) ∈ Nn
) |
172 | | peano1 4403 |
. . . . . . . . . . . . 13
⊢
0c ∈ Nn |
173 | | suc11nnc 4559 |
. . . . . . . . . . . . 13
⊢ (((((m +c 1c)
+c (m
+c 1c)) +c m) ∈ Nn ∧
0c ∈ Nn ) → (((((m
+c 1c) +c (m +c 1c))
+c m)
+c 1c) = (0c
+c 1c) ↔ (((m +c 1c)
+c (m
+c 1c)) +c m) = 0c)) |
174 | 171, 172,
173 | sylancl 643 |
. . . . . . . . . . . 12
⊢ (m ∈ Nn → (((((m
+c 1c) +c (m +c 1c))
+c m)
+c 1c) = (0c
+c 1c) ↔ (((m +c 1c)
+c (m
+c 1c)) +c m) = 0c)) |
175 | 165, 174 | mtbird 292 |
. . . . . . . . . . 11
⊢ (m ∈ Nn → ¬ ((((m +c 1c)
+c (m
+c 1c)) +c m) +c 1c) =
(0c +c
1c)) |
176 | | addcass 4416 |
. . . . . . . . . . . 12
⊢ ((((m +c 1c)
+c (m
+c 1c)) +c m) +c 1c) =
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) |
177 | 176 | eqeq1i 2360 |
. . . . . . . . . . 11
⊢ (((((m +c 1c)
+c (m
+c 1c)) +c m) +c 1c) =
(0c +c 1c) ↔
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (0c
+c 1c)) |
178 | 175, 177 | sylnib 295 |
. . . . . . . . . 10
⊢ (m ∈ Nn → ¬ (((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = (0c
+c 1c)) |
179 | | addceq12 4386 |
. . . . . . . . . . . . . . . 16
⊢ ((p = 0c ∧ p =
0c) → (p
+c p) =
(0c +c
0c)) |
180 | 179 | anidms 626 |
. . . . . . . . . . . . . . 15
⊢ (p = 0c → (p +c p) = (0c +c
0c)) |
181 | | id 19 |
. . . . . . . . . . . . . . 15
⊢ (p = 0c → p = 0c) |
182 | 180, 181 | addceq12d 4392 |
. . . . . . . . . . . . . 14
⊢ (p = 0c → ((p +c p) +c p) = ((0c +c
0c) +c
0c)) |
183 | 182, 103 | syl6eq 2401 |
. . . . . . . . . . . . 13
⊢ (p = 0c → ((p +c p) +c p) = 0c) |
184 | 183 | addceq1d 4390 |
. . . . . . . . . . . 12
⊢ (p = 0c → (((p +c p) +c p) +c 1c) =
(0c +c
1c)) |
185 | 184 | eqeq2d 2364 |
. . . . . . . . . . 11
⊢ (p = 0c → ((((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c 1c) ↔
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (0c
+c 1c))) |
186 | 185 | notbid 285 |
. . . . . . . . . 10
⊢ (p = 0c → (¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c 1c) ↔
¬ (((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (0c
+c 1c))) |
187 | 178, 186 | syl5ibrcom 213 |
. . . . . . . . 9
⊢ (m ∈ Nn → (p =
0c → ¬ (((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
188 | 187 | adantr 451 |
. . . . . . . 8
⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → (p = 0c → ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c
1c))) |
189 | | addceq12 4386 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((n = q ∧ n = q) → (n
+c n) = (q +c q)) |
190 | 189 | anidms 626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (n = q →
(n +c n) = (q
+c q)) |
191 | | id 19 |
. . . . . . . . . . . . . . . . . . 19
⊢ (n = q →
n = q) |
192 | 190, 191 | addceq12d 4392 |
. . . . . . . . . . . . . . . . . 18
⊢ (n = q →
((n +c n) +c n) = ((q
+c q)
+c q)) |
193 | 192 | addceq1d 4390 |
. . . . . . . . . . . . . . . . 17
⊢ (n = q →
(((n +c n) +c n) +c 1c) =
(((q +c q) +c q) +c
1c)) |
194 | 193 | eqeq2d 2364 |
. . . . . . . . . . . . . . . 16
⊢ (n = q →
(((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c) ↔ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
195 | 194 | notbid 285 |
. . . . . . . . . . . . . . 15
⊢ (n = q →
(¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
196 | 195 | rspcv 2952 |
. . . . . . . . . . . . . 14
⊢ (q ∈ Nn → (∀n ∈ Nn ¬ ((m
+c m)
+c m) = (((n +c n) +c n) +c 1c) →
¬ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
197 | 196 | adantl 452 |
. . . . . . . . . . . . 13
⊢ ((m ∈ Nn ∧ q ∈ Nn ) → (∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c) → ¬ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
198 | | addc6 4419 |
. . . . . . . . . . . . . . . 16
⊢ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((m +c m) +c m) +c ((1c
+c 1c) +c
1c)) |
199 | | addc6 4419 |
. . . . . . . . . . . . . . . . . 18
⊢ (((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c)) =
(((q +c q) +c q) +c ((1c
+c 1c) +c
1c)) |
200 | 199 | addceq1i 4387 |
. . . . . . . . . . . . . . . . 17
⊢ ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c) = ((((q +c q) +c q) +c ((1c
+c 1c) +c
1c)) +c
1c) |
201 | | addc32 4417 |
. . . . . . . . . . . . . . . . 17
⊢ ((((q +c q) +c q) +c ((1c
+c 1c) +c
1c)) +c 1c) =
((((q +c q) +c q) +c 1c)
+c ((1c +c
1c) +c
1c)) |
202 | 200, 201 | eqtri 2373 |
. . . . . . . . . . . . . . . 16
⊢ ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c) = ((((q +c q) +c q) +c 1c)
+c ((1c +c
1c) +c
1c)) |
203 | 198, 202 | eqeq12i 2366 |
. . . . . . . . . . . . . . 15
⊢ ((((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
((((q +c
1c) +c (q +c 1c))
+c (q
+c 1c)) +c
1c) ↔ (((m
+c m)
+c m)
+c ((1c +c
1c) +c 1c)) =
((((q +c q) +c q) +c 1c)
+c ((1c +c
1c) +c
1c))) |
204 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((m ∈ Nn ∧ m ∈ Nn ) → (m
+c m) ∈ Nn
) |
205 | 204 | anidms 626 |
. . . . . . . . . . . . . . . . 17
⊢ (m ∈ Nn → (m
+c m) ∈ Nn
) |
206 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . 17
⊢ (((m +c m) ∈ Nn ∧ m ∈ Nn ) → ((m
+c m)
+c m) ∈ Nn
) |
207 | 205, 206 | mpancom 650 |
. . . . . . . . . . . . . . . 16
⊢ (m ∈ Nn → ((m
+c m)
+c m) ∈ Nn
) |
208 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((q ∈ Nn ∧ q ∈ Nn ) → (q
+c q) ∈ Nn
) |
209 | 208 | anidms 626 |
. . . . . . . . . . . . . . . . . 18
⊢ (q ∈ Nn → (q
+c q) ∈ Nn
) |
210 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . . 18
⊢ (((q +c q) ∈ Nn ∧ q ∈ Nn ) → ((q
+c q)
+c q) ∈ Nn
) |
211 | 209, 210 | mpancom 650 |
. . . . . . . . . . . . . . . . 17
⊢ (q ∈ Nn → ((q
+c q)
+c q) ∈ Nn
) |
212 | | peano2 4404 |
. . . . . . . . . . . . . . . . 17
⊢ (((q +c q) +c q) ∈ Nn → (((q
+c q)
+c q)
+c 1c) ∈
Nn ) |
213 | 211, 212 | syl 15 |
. . . . . . . . . . . . . . . 16
⊢ (q ∈ Nn → (((q
+c q)
+c q)
+c 1c) ∈
Nn ) |
214 | | 1cnnc 4409 |
. . . . . . . . . . . . . . . . . . 19
⊢
1c ∈ Nn |
215 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1c ∈ Nn ∧
1c ∈ Nn ) → (1c +c
1c) ∈ Nn ) |
216 | 214, 214,
215 | mp2an 653 |
. . . . . . . . . . . . . . . . . 18
⊢
(1c +c 1c) ∈ Nn |
217 | | nncaddccl 4420 |
. . . . . . . . . . . . . . . . . 18
⊢
(((1c +c 1c) ∈ Nn ∧ 1c ∈ Nn ) →
((1c +c 1c)
+c 1c) ∈
Nn ) |
218 | 216, 214,
217 | mp2an 653 |
. . . . . . . . . . . . . . . . 17
⊢
((1c +c 1c)
+c 1c) ∈
Nn |
219 | | addccan1 4561 |
. . . . . . . . . . . . . . . . 17
⊢ ((((m +c m) +c m) ∈ Nn ∧ (((q +c q) +c q) +c 1c) ∈ Nn ∧ ((1c +c
1c) +c 1c) ∈ Nn ) →
((((m +c m) +c m) +c ((1c
+c 1c) +c
1c)) = ((((q
+c q)
+c q)
+c 1c) +c
((1c +c 1c)
+c 1c)) ↔ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
220 | 218, 219 | mp3an3 1266 |
. . . . . . . . . . . . . . . 16
⊢ ((((m +c m) +c m) ∈ Nn ∧ (((q +c q) +c q) +c 1c) ∈ Nn ) →
((((m +c m) +c m) +c ((1c
+c 1c) +c
1c)) = ((((q
+c q)
+c q)
+c 1c) +c
((1c +c 1c)
+c 1c)) ↔ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
221 | 207, 213,
220 | syl2an 463 |
. . . . . . . . . . . . . . 15
⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m
+c m)
+c m)
+c ((1c +c
1c) +c 1c)) =
((((q +c q) +c q) +c 1c)
+c ((1c +c
1c) +c 1c)) ↔
((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
222 | 203, 221 | syl5bb 248 |
. . . . . . . . . . . . . 14
⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c) ↔ ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
223 | 222 | biimpd 198 |
. . . . . . . . . . . . 13
⊢ ((m ∈ Nn ∧ q ∈ Nn ) → ((((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c) → ((m +c m) +c m) = (((q
+c q)
+c q)
+c 1c))) |
224 | 197, 223 | nsyld 132 |
. . . . . . . . . . . 12
⊢ ((m ∈ Nn ∧ q ∈ Nn ) → (∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c) → ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
((((q +c
1c) +c (q +c 1c))
+c (q
+c 1c)) +c
1c))) |
225 | 224 | imp 418 |
. . . . . . . . . . 11
⊢ (((m ∈ Nn ∧ q ∈ Nn ) ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
((((q +c
1c) +c (q +c 1c))
+c (q
+c 1c)) +c
1c)) |
226 | 225 | an32s 779 |
. . . . . . . . . 10
⊢ (((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) ∧
q ∈ Nn ) → ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
((((q +c
1c) +c (q +c 1c))
+c (q
+c 1c)) +c
1c)) |
227 | | addceq12 4386 |
. . . . . . . . . . . . . . 15
⊢ ((p = (q
+c 1c) ∧
p = (q
+c 1c)) → (p +c p) = ((q
+c 1c) +c (q +c
1c))) |
228 | 227 | anidms 626 |
. . . . . . . . . . . . . 14
⊢ (p = (q
+c 1c) → (p +c p) = ((q
+c 1c) +c (q +c
1c))) |
229 | | id 19 |
. . . . . . . . . . . . . 14
⊢ (p = (q
+c 1c) → p = (q
+c 1c)) |
230 | 228, 229 | addceq12d 4392 |
. . . . . . . . . . . . 13
⊢ (p = (q
+c 1c) → ((p +c p) +c p) = (((q
+c 1c) +c (q +c 1c))
+c (q
+c 1c))) |
231 | 230 | addceq1d 4390 |
. . . . . . . . . . . 12
⊢ (p = (q
+c 1c) → (((p +c p) +c p) +c 1c) =
((((q +c
1c) +c (q +c 1c))
+c (q
+c 1c)) +c
1c)) |
232 | 231 | eqeq2d 2364 |
. . . . . . . . . . 11
⊢ (p = (q
+c 1c) → ((((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c 1c) ↔
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c))) |
233 | 232 | notbid 285 |
. . . . . . . . . 10
⊢ (p = (q
+c 1c) → (¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c 1c) ↔
¬ (((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = ((((q +c 1c)
+c (q
+c 1c)) +c (q +c 1c))
+c 1c))) |
234 | 226, 233 | syl5ibrcom 213 |
. . . . . . . . 9
⊢ (((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) ∧
q ∈ Nn ) → (p =
(q +c
1c) → ¬ (((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
235 | 234 | rexlimdva 2739 |
. . . . . . . 8
⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → (∃q ∈ Nn p = (q
+c 1c) → ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c
1c))) |
236 | 188, 235 | jaod 369 |
. . . . . . 7
⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → ((p = 0c
∨ ∃q ∈ Nn p = (q +c 1c)) →
¬ (((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
237 | 155, 236 | syl5bi 208 |
. . . . . 6
⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → (p ∈ Nn → ¬ (((m
+c 1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
238 | 237 | ralrimiv 2697 |
. . . . 5
⊢ ((m ∈ Nn ∧ ∀n ∈ Nn ¬ ((m +c m) +c m) = (((n
+c n)
+c n)
+c 1c)) → ∀p ∈ Nn ¬ (((m +c 1c)
+c (m
+c 1c)) +c (m +c 1c)) =
(((p +c p) +c p) +c
1c)) |
239 | 238 | ex 423 |
. . . 4
⊢ (m ∈ Nn → (∀n ∈ Nn ¬ ((m
+c m)
+c m) = (((n +c n) +c n) +c 1c) →
∀p
∈ Nn ¬
(((m +c
1c) +c (m +c 1c))
+c (m
+c 1c)) = (((p +c p) +c p) +c
1c))) |
240 | 96, 107, 114, 130, 137, 154, 239 | finds 4412 |
. . 3
⊢ (A ∈ Nn → ∀n ∈ Nn ¬ ((A
+c A)
+c A) = (((n +c n) +c n) +c
1c)) |
241 | | addceq12 4386 |
. . . . . . . . 9
⊢ ((n = B ∧ n = B) → (n
+c n) = (B +c B)) |
242 | 241 | anidms 626 |
. . . . . . . 8
⊢ (n = B →
(n +c n) = (B
+c B)) |
243 | | id 19 |
. . . . . . . 8
⊢ (n = B →
n = B) |
244 | 242, 243 | addceq12d 4392 |
. . . . . . 7
⊢ (n = B →
((n +c n) +c n) = ((B
+c B)
+c B)) |
245 | 244 | addceq1d 4390 |
. . . . . 6
⊢ (n = B →
(((n +c n) +c n) +c 1c) =
(((B +c B) +c B) +c
1c)) |
246 | 245 | eqeq2d 2364 |
. . . . 5
⊢ (n = B →
(((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c) ↔ ((A +c A) +c A) = (((B
+c B)
+c B)
+c 1c))) |
247 | 246 | notbid 285 |
. . . 4
⊢ (n = B →
(¬ ((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c) ↔ ¬ ((A +c A) +c A) = (((B
+c B)
+c B)
+c 1c))) |
248 | 247 | rspccv 2953 |
. . 3
⊢ (∀n ∈ Nn ¬ ((A +c A) +c A) = (((n
+c n)
+c n)
+c 1c) → (B ∈ Nn → ¬ ((A
+c A)
+c A) = (((B +c B) +c B) +c
1c))) |
249 | 240, 248 | syl 15 |
. 2
⊢ (A ∈ Nn → (B ∈ Nn → ¬
((A +c A) +c A) = (((B
+c B)
+c B)
+c 1c))) |
250 | 249 | imp 418 |
1
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬ ((A +c A) +c A) = (((B
+c B)
+c B)
+c 1c)) |