Metamath Proof Explorer


Theorem saddisjlem

Description: Lemma for sadadd . (Contributed by Mario Carneiro, 9-Sep-2016)

Ref Expression
Hypotheses saddisj.1 φ A 0
saddisj.2 φ B 0
saddisj.3 φ A B =
saddisjlem.c C = seq 0 c 2 𝑜 , m 0 if cadd m A m B c 1 𝑜 n 0 if n = 0 n 1
saddisjlem.3 φ N 0
Assertion saddisjlem φ N A sadd B N A B

Proof

Step Hyp Ref Expression
1 saddisj.1 φ A 0
2 saddisj.2 φ B 0
3 saddisj.3 φ A B =
4 saddisjlem.c C = seq 0 c 2 𝑜 , m 0 if cadd m A m B c 1 𝑜 n 0 if n = 0 n 1
5 saddisjlem.3 φ N 0
6 1 2 4 5 sadval φ N A sadd B hadd N A N B C N
7 fveq2 x = 0 C x = C 0
8 7 eleq2d x = 0 C x C 0
9 8 notbid x = 0 ¬ C x ¬ C 0
10 9 imbi2d x = 0 φ ¬ C x φ ¬ C 0
11 fveq2 x = k C x = C k
12 11 eleq2d x = k C x C k
13 12 notbid x = k ¬ C x ¬ C k
14 13 imbi2d x = k φ ¬ C x φ ¬ C k
15 fveq2 x = k + 1 C x = C k + 1
16 15 eleq2d x = k + 1 C x C k + 1
17 16 notbid x = k + 1 ¬ C x ¬ C k + 1
18 17 imbi2d x = k + 1 φ ¬ C x φ ¬ C k + 1
19 fveq2 x = N C x = C N
20 19 eleq2d x = N C x C N
21 20 notbid x = N ¬ C x ¬ C N
22 21 imbi2d x = N φ ¬ C x φ ¬ C N
23 1 2 4 sadc0 φ ¬ C 0
24 noel ¬ k
25 1 ad2antrr φ k 0 ¬ C k A 0
26 2 ad2antrr φ k 0 ¬ C k B 0
27 simplr φ k 0 ¬ C k k 0
28 25 26 4 27 sadcp1 φ k 0 ¬ C k C k + 1 cadd k A k B C k
29 cad0 ¬ C k cadd k A k B C k k A k B
30 29 adantl φ k 0 ¬ C k cadd k A k B C k k A k B
31 elin k A B k A k B
32 3 ad2antrr φ k 0 ¬ C k A B =
33 32 eleq2d φ k 0 ¬ C k k A B k
34 31 33 bitr3id φ k 0 ¬ C k k A k B k
35 28 30 34 3bitrd φ k 0 ¬ C k C k + 1 k
36 24 35 mtbiri φ k 0 ¬ C k ¬ C k + 1
37 36 ex φ k 0 ¬ C k ¬ C k + 1
38 37 expcom k 0 φ ¬ C k ¬ C k + 1
39 38 a2d k 0 φ ¬ C k φ ¬ C k + 1
40 10 14 18 22 23 39 nn0ind N 0 φ ¬ C N
41 5 40 mpcom φ ¬ C N
42 hadrot hadd C N N A N B hadd N A N B C N
43 had0 ¬ C N hadd C N N A N B N A N B
44 42 43 bitr3id ¬ C N hadd N A N B C N N A N B
45 41 44 syl φ hadd N A N B C N N A N B
46 noel ¬ N
47 elin N A B N A N B
48 3 eleq2d φ N A B N
49 47 48 bitr3id φ N A N B N
50 46 49 mtbiri φ ¬ N A N B
51 xor2 N A N B N A N B ¬ N A N B
52 51 rbaib ¬ N A N B N A N B N A N B
53 50 52 syl φ N A N B N A N B
54 elun N A B N A N B
55 53 54 bitr4di φ N A N B N A B
56 6 45 55 3bitrd φ N A sadd B N A B