NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nncdiv3lem2 GIF version

Theorem nncdiv3lem2 6276
Description: Lemma for nncdiv3 6277. Set up stratification for induction. (Contributed by SF, 2-Mar-2015.)
Assertion
Ref Expression
nncdiv3lem2 {a n Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c))} V
Distinct variable group:   n,a

Proof of Theorem nncdiv3lem2
Dummy variable b is distinct from all other variables.
StepHypRef Expression
1 elima 4754 . . . 4 (a (((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) “ Nn ) ↔ n Nn n((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))a)
2 df-br 4640 . . . . . 6 (n((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))an, a ((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))))
3 elun 3220 . . . . . . . . 9 (n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ↔ (n, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))))
4 nncdiv3lem1 6275 . . . . . . . . . 10 (n, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ a = ((n +c n) +c n))
5 elrn2 4897 . . . . . . . . . . 11 (n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ bb, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )))
6 oteltxp 5782 . . . . . . . . . . . . 13 (b, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ (b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) b, a ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )))
7 opelcnv 4893 . . . . . . . . . . . . . . 15 (b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ n, b ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )))
8 nncdiv3lem1 6275 . . . . . . . . . . . . . . 15 (n, b ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))
97, 8bitri 240 . . . . . . . . . . . . . 14 (b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))
10 elrn2 4897 . . . . . . . . . . . . . . . 16 (b, a ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ nn, b, a ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))
11 oteltxp 5782 . . . . . . . . . . . . . . . . . 18 (n, b, a ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ (n, b (1st ∩ ((2nd “ {1c}) × V)) n, a AddC ))
12 elin 3219 . . . . . . . . . . . . . . . . . . . 20 (n, b (1st ∩ ((2nd “ {1c}) × V)) ↔ (n, b 1st n, b ((2nd “ {1c}) × V)))
13 df-br 4640 . . . . . . . . . . . . . . . . . . . . . 22 (n1st bn, b 1st )
1413bicomi 193 . . . . . . . . . . . . . . . . . . . . 21 (n, b 1stn1st b)
15 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 b V
16 opelxp 4811 . . . . . . . . . . . . . . . . . . . . . . 23 (n, b ((2nd “ {1c}) × V) ↔ (n (2nd “ {1c}) b V))
1715, 16mpbiran2 885 . . . . . . . . . . . . . . . . . . . . . 22 (n, b ((2nd “ {1c}) × V) ↔ n (2nd “ {1c}))
18 eliniseg 5020 . . . . . . . . . . . . . . . . . . . . . 22 (n (2nd “ {1c}) ↔ n2nd 1c)
1917, 18bitri 240 . . . . . . . . . . . . . . . . . . . . 21 (n, b ((2nd “ {1c}) × V) ↔ n2nd 1c)
2014, 19anbi12i 678 . . . . . . . . . . . . . . . . . . . 20 ((n, b 1st n, b ((2nd “ {1c}) × V)) ↔ (n1st b n2nd 1c))
21 1cex 4142 . . . . . . . . . . . . . . . . . . . . 21 1c V
2215, 21op1st2nd 5790 . . . . . . . . . . . . . . . . . . . 20 ((n1st b n2nd 1c) ↔ n = b, 1c)
2312, 20, 223bitri 262 . . . . . . . . . . . . . . . . . . 19 (n, b (1st ∩ ((2nd “ {1c}) × V)) ↔ n = b, 1c)
24 df-br 4640 . . . . . . . . . . . . . . . . . . . 20 (n AddC an, a AddC )
2524bicomi 193 . . . . . . . . . . . . . . . . . . 19 (n, a AddCn AddC a)
2623, 25anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((n, b (1st ∩ ((2nd “ {1c}) × V)) n, a AddC ) ↔ (n = b, 1c n AddC a))
2711, 26bitri 240 . . . . . . . . . . . . . . . . 17 (n, b, a ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ (n = b, 1c n AddC a))
2827exbii 1582 . . . . . . . . . . . . . . . 16 (nn, b, a ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ n(n = b, 1c n AddC a))
2910, 28bitri 240 . . . . . . . . . . . . . . 15 (b, a ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ n(n = b, 1c n AddC a))
3015, 21opex 4588 . . . . . . . . . . . . . . . 16 b, 1c V
31 breq1 4642 . . . . . . . . . . . . . . . 16 (n = b, 1c → (n AddC ab, 1c AddC a))
3230, 31ceqsexv 2894 . . . . . . . . . . . . . . 15 (n(n = b, 1c n AddC a) ↔ b, 1c AddC a)
3315, 21braddcfn 5826 . . . . . . . . . . . . . . . 16 (b, 1c AddC a ↔ (b +c 1c) = a)
34 eqcom 2355 . . . . . . . . . . . . . . . 16 ((b +c 1c) = aa = (b +c 1c))
3533, 34bitri 240 . . . . . . . . . . . . . . 15 (b, 1c AddC aa = (b +c 1c))
3629, 32, 353bitri 262 . . . . . . . . . . . . . 14 (b, a ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) ↔ a = (b +c 1c))
379, 36anbi12i 678 . . . . . . . . . . . . 13 ((b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) b, a ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ (b = ((n +c n) +c n) a = (b +c 1c)))
386, 37bitri 240 . . . . . . . . . . . 12 (b, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ (b = ((n +c n) +c n) a = (b +c 1c)))
3938exbii 1582 . . . . . . . . . . 11 (bb, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ b(b = ((n +c n) +c n) a = (b +c 1c)))
40 vex 2862 . . . . . . . . . . . . . 14 n V
4140, 40addcex 4394 . . . . . . . . . . . . 13 (n +c n) V
4241, 40addcex 4394 . . . . . . . . . . . 12 ((n +c n) +c n) V
43 addceq1 4383 . . . . . . . . . . . . 13 (b = ((n +c n) +c n) → (b +c 1c) = (((n +c n) +c n) +c 1c))
4443eqeq2d 2364 . . . . . . . . . . . 12 (b = ((n +c n) +c n) → (a = (b +c 1c) ↔ a = (((n +c n) +c n) +c 1c)))
4542, 44ceqsexv 2894 . . . . . . . . . . 11 (b(b = ((n +c n) +c n) a = (b +c 1c)) ↔ a = (((n +c n) +c n) +c 1c))
465, 39, 453bitri 262 . . . . . . . . . 10 (n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) ↔ a = (((n +c n) +c n) +c 1c))
474, 46orbi12i 507 . . . . . . . . 9 ((n, a ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ↔ (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c)))
483, 47bitri 240 . . . . . . . 8 (n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ↔ (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c)))
49 elrn2 4897 . . . . . . . . 9 (n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ bb, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))
50 oteltxp 5782 . . . . . . . . . . 11 (b, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ (b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) b, a ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))
51 elrn2 4897 . . . . . . . . . . . . . 14 (b, a ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ nn, b, a ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))
52 oteltxp 5782 . . . . . . . . . . . . . . . 16 (n, b, a ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ (n, b (1st ∩ ((2nd “ {2c}) × V)) n, a AddC ))
53 elin 3219 . . . . . . . . . . . . . . . . . 18 (n, b (1st ∩ ((2nd “ {2c}) × V)) ↔ (n, b 1st n, b ((2nd “ {2c}) × V)))
54 opelxp 4811 . . . . . . . . . . . . . . . . . . . . 21 (n, b ((2nd “ {2c}) × V) ↔ (n (2nd “ {2c}) b V))
5515, 54mpbiran2 885 . . . . . . . . . . . . . . . . . . . 20 (n, b ((2nd “ {2c}) × V) ↔ n (2nd “ {2c}))
56 eliniseg 5020 . . . . . . . . . . . . . . . . . . . 20 (n (2nd “ {2c}) ↔ n2nd 2c)
5755, 56bitri 240 . . . . . . . . . . . . . . . . . . 19 (n, b ((2nd “ {2c}) × V) ↔ n2nd 2c)
5814, 57anbi12i 678 . . . . . . . . . . . . . . . . . 18 ((n, b 1st n, b ((2nd “ {2c}) × V)) ↔ (n1st b n2nd 2c))
59 df-2c 6104 . . . . . . . . . . . . . . . . . . . 20 2c = Nc {, V}
60 ncex 6117 . . . . . . . . . . . . . . . . . . . 20 Nc {, V} V
6159, 60eqeltri 2423 . . . . . . . . . . . . . . . . . . 19 2c V
6215, 61op1st2nd 5790 . . . . . . . . . . . . . . . . . 18 ((n1st b n2nd 2c) ↔ n = b, 2c)
6353, 58, 623bitri 262 . . . . . . . . . . . . . . . . 17 (n, b (1st ∩ ((2nd “ {2c}) × V)) ↔ n = b, 2c)
6463, 25anbi12i 678 . . . . . . . . . . . . . . . 16 ((n, b (1st ∩ ((2nd “ {2c}) × V)) n, a AddC ) ↔ (n = b, 2c n AddC a))
6552, 64bitri 240 . . . . . . . . . . . . . . 15 (n, b, a ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ (n = b, 2c n AddC a))
6665exbii 1582 . . . . . . . . . . . . . 14 (nn, b, a ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ n(n = b, 2c n AddC a))
6715, 61opex 4588 . . . . . . . . . . . . . . 15 b, 2c V
68 breq1 4642 . . . . . . . . . . . . . . 15 (n = b, 2c → (n AddC ab, 2c AddC a))
6967, 68ceqsexv 2894 . . . . . . . . . . . . . 14 (n(n = b, 2c n AddC a) ↔ b, 2c AddC a)
7051, 66, 693bitri 262 . . . . . . . . . . . . 13 (b, a ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ b, 2c AddC a)
7115, 61braddcfn 5826 . . . . . . . . . . . . 13 (b, 2c AddC a ↔ (b +c 2c) = a)
72 eqcom 2355 . . . . . . . . . . . . 13 ((b +c 2c) = aa = (b +c 2c))
7370, 71, 723bitri 262 . . . . . . . . . . . 12 (b, a ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) ↔ a = (b +c 2c))
749, 73anbi12i 678 . . . . . . . . . . 11 ((b, n ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) b, a ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ (b = ((n +c n) +c n) a = (b +c 2c)))
7550, 74bitri 240 . . . . . . . . . 10 (b, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ (b = ((n +c n) +c n) a = (b +c 2c)))
7675exbii 1582 . . . . . . . . 9 (bb, n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ b(b = ((n +c n) +c n) a = (b +c 2c)))
77 addceq1 4383 . . . . . . . . . . 11 (b = ((n +c n) +c n) → (b +c 2c) = (((n +c n) +c n) +c 2c))
7877eqeq2d 2364 . . . . . . . . . 10 (b = ((n +c n) +c n) → (a = (b +c 2c) ↔ a = (((n +c n) +c n) +c 2c)))
7942, 78ceqsexv 2894 . . . . . . . . 9 (b(b = ((n +c n) +c n) a = (b +c 2c)) ↔ a = (((n +c n) +c n) +c 2c))
8049, 76, 793bitri 262 . . . . . . . 8 (n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) ↔ a = (((n +c n) +c n) +c 2c))
8148, 80orbi12i 507 . . . . . . 7 ((n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) ↔ ((a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c)) a = (((n +c n) +c n) +c 2c)))
82 elun 3220 . . . . . . 7 (n, a ((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) ↔ (n, a (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) n, a ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))))
83 df-3or 935 . . . . . . 7 ((a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c)) ↔ ((a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c)) a = (((n +c n) +c n) +c 2c)))
8481, 82, 833bitr4i 268 . . . . . 6 (n, a ((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) ↔ (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c)))
852, 84bitri 240 . . . . 5 (n((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))a ↔ (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c)))
8685rexbii 2639 . . . 4 (n Nn n((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )))an Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c)))
871, 86bitri 240 . . 3 (a (((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) “ Nn ) ↔ n Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c)))
8887abbi2i 2464 . 2 (((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) “ Nn ) = {a n Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c))}
89 1stex 4739 . . . . . . . . . . . . . 14 1st V
9089cnvex 5102 . . . . . . . . . . . . 13 1st V
91 2ndex 5112 . . . . . . . . . . . . . 14 2nd V
9289, 91inex 4105 . . . . . . . . . . . . 13 (1st ∩ 2nd ) V
9390, 92txpex 5785 . . . . . . . . . . . 12 (1st ⊗ (1st ∩ 2nd )) V
9493rnex 5107 . . . . . . . . . . 11 ran (1st ⊗ (1st ∩ 2nd )) V
9594, 91txpex 5785 . . . . . . . . . 10 (ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) V
96 addcfnex 5824 . . . . . . . . . 10 AddC V
9795, 96imaex 4747 . . . . . . . . 9 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
9897cnvex 5102 . . . . . . . 8 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
9998ins3ex 5798 . . . . . . 7 Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) V
10089, 89coex 4750 . . . . . . . . 9 (1st 1st ) V
10191, 89coex 4750 . . . . . . . . . 10 (2nd 1st ) V
102101, 91txpex 5785 . . . . . . . . 9 ((2nd 1st ) ⊗ 2nd ) V
103100, 102txpex 5785 . . . . . . . 8 ((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) V
104103, 96imaex 4747 . . . . . . 7 (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC ) V
10599, 104inex 4105 . . . . . 6 ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
106105rnex 5107 . . . . 5 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
107106cnvex 5102 . . . . . . 7 ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) V
10891cnvex 5102 . . . . . . . . . . . 12 2nd V
109 snex 4111 . . . . . . . . . . . 12 {1c} V
110108, 109imaex 4747 . . . . . . . . . . 11 (2nd “ {1c}) V
111 vvex 4109 . . . . . . . . . . 11 V V
112110, 111xpex 5115 . . . . . . . . . 10 ((2nd “ {1c}) × V) V
11389, 112inex 4105 . . . . . . . . 9 (1st ∩ ((2nd “ {1c}) × V)) V
114113, 96txpex 5785 . . . . . . . 8 ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) V
115114rnex 5107 . . . . . . 7 ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ) V
116107, 115txpex 5785 . . . . . 6 (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) V
117116rnex 5107 . . . . 5 ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC )) V
118106, 117unex 4106 . . . 4 (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) V
119 snex 4111 . . . . . . . . . . 11 {2c} V
120108, 119imaex 4747 . . . . . . . . . 10 (2nd “ {2c}) V
121120, 111xpex 5115 . . . . . . . . 9 ((2nd “ {2c}) × V) V
12289, 121inex 4105 . . . . . . . 8 (1st ∩ ((2nd “ {2c}) × V)) V
123122, 96txpex 5785 . . . . . . 7 ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) V
124123rnex 5107 . . . . . 6 ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ) V
125107, 124txpex 5785 . . . . 5 (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) V
126125rnex 5107 . . . 4 ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC )) V
127118, 126unex 4106 . . 3 ((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) V
128 nncex 4396 . . 3 Nn V
129127, 128imaex 4747 . 2 (((ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {1c}) × V)) ⊗ AddC ))) ∪ ran (ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ⊗ ran ((1st ∩ ((2nd “ {2c}) × V)) ⊗ AddC ))) “ Nn ) V
13088, 129eqeltrri 2424 1 {a n Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c))} V
Colors of variables: wff setvar class
Syntax hints:   wo 357   wa 358   w3o 933  wex 1541   = wceq 1642   wcel 1710  {cab 2339  wrex 2615  Vcvv 2859  cun 3207  cin 3208  c0 3550  {csn 3737  {cpr 3738  1cc1c 4134   Nn cnnc 4373   +c cplc 4375  cop 4561   class class class wbr 4639  1st c1st 4717   ccom 4721  cima 4722   × cxp 4770  ccnv 4771  ran crn 4773  2nd c2nd 4783  ctxp 5735   AddC caddcfn 5745   Ins3 cins3 5751   Nc cnc 6091  2cc2c 6094
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-csb 3137  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-iun 3971  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-xp 4784  df-cnv 4785  df-rn 4786  df-dm 4787  df-res 4788  df-fun 4789  df-fn 4790  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794  df-fv 4795  df-2nd 4797  df-ov 5526  df-oprab 5528  df-mpt 5652  df-mpt2 5654  df-txp 5736  df-cup 5742  df-disj 5744  df-addcfn 5746  df-ins2 5750  df-ins3 5752  df-image 5754  df-ins4 5756  df-si3 5758  df-funs 5760  df-fns 5762  df-ec 5947  df-en 6029  df-nc 6101  df-2c 6104
This theorem is referenced by:  nncdiv3  6277
  Copyright terms: Public domain W3C validator