Metamath Proof Explorer

Theorem sadcp1

Description: The carry sequence (which is a sequence of wffs, encoded as 1o and (/) ) is defined recursively as the carry operation applied to the previous carry and the two current inputs. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Hypotheses sadval.a ⊢ φ → A ⊆ ℕ 0
sadval.b ⊢ φ → B ⊆ ℕ 0
sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
sadcp1.n ⊢ φ → N ∈ ℕ 0
Assertion sadcp1 ⊢ φ → ∅ ∈ C ⁡ N + 1 ↔ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ φ → A ⊆ ℕ 0
2 sadval.b ⊢ φ → B ⊆ ℕ 0
3 sadval.c ⊢ C = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
4 sadcp1.n ⊢ φ → N ∈ ℕ 0
5 nn0uz ⊢ ℕ 0 = ℤ ≥ 0
6 4 5 eleqtrdi ⊢ φ → N ∈ ℤ ≥ 0
7 seqp1 ⊢ N ∈ ℤ ≥ 0 → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1
8 6 7 syl ⊢ φ → seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1
9 3 fveq1i ⊢ C ⁡ N + 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1
10 3 fveq1i ⊢ C ⁡ N = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N
11 10 oveq1i ⊢ C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = seq 0 c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1
12 8 9 11 3eqtr4g ⊢ φ → C ⁡ N + 1 = C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1
13 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
14 eqeq1 ⊢ n = N + 1 → n = 0 ↔ N + 1 = 0
15 oveq1 ⊢ n = N + 1 → n − 1 = N + 1 - 1
16 14 15 ifbieq2d ⊢ n = N + 1 → if n = 0 ∅ n − 1 = if N + 1 = 0 ∅ N + 1 - 1
17 eqid ⊢ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 = n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1
18 0ex ⊢ ∅ ∈ V
19 ovex ⊢ N + 1 - 1 ∈ V
20 18 19 ifex ⊢ if N + 1 = 0 ∅ N + 1 - 1 ∈ V
21 16 17 20 fvmpt ⊢ N + 1 ∈ ℕ 0 → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = if N + 1 = 0 ∅ N + 1 - 1
22 4 13 21 3syl ⊢ φ → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = if N + 1 = 0 ∅ N + 1 - 1
23 nn0p1nn ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ
24 4 23 syl ⊢ φ → N + 1 ∈ ℕ
25 24 nnne0d ⊢ φ → N + 1 ≠ 0
26 ifnefalse ⊢ N + 1 ≠ 0 → if N + 1 = 0 ∅ N + 1 - 1 = N + 1 - 1
27 25 26 syl ⊢ φ → if N + 1 = 0 ∅ N + 1 - 1 = N + 1 - 1
28 4 nn0cnd ⊢ φ → N ∈ ℂ
29 1cnd ⊢ φ → 1 ∈ ℂ
30 28 29 pncand ⊢ φ → N + 1 - 1 = N
31 22 27 30 3eqtrd ⊢ φ → n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = N
32 31 oveq2d ⊢ φ → C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ n ∈ ℕ 0 ⟼ if n = 0 ∅ n − 1 ⁡ N + 1 = C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ N
33 1 2 3 sadcf ⊢ φ → C : ℕ 0 ⟶ 2 𝑜
34 33 4 ffvelrnd ⊢ φ → C ⁡ N ∈ 2 𝑜
35 simpr ⊢ x = C ⁡ N ∧ y = N → y = N
36 35 eleq1d ⊢ x = C ⁡ N ∧ y = N → y ∈ A ↔ N ∈ A
37 35 eleq1d ⊢ x = C ⁡ N ∧ y = N → y ∈ B ↔ N ∈ B
38 simpl ⊢ x = C ⁡ N ∧ y = N → x = C ⁡ N
39 38 eleq2d ⊢ x = C ⁡ N ∧ y = N → ∅ ∈ x ↔ ∅ ∈ C ⁡ N
40 36 37 39 cadbi123d ⊢ x = C ⁡ N ∧ y = N → cadd y ∈ A y ∈ B ∅ ∈ x ↔ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
41 40 ifbid ⊢ x = C ⁡ N ∧ y = N → if cadd y ∈ A y ∈ B ∅ ∈ x 1 𝑜 ∅ = if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
42 biidd ⊢ c = x → m ∈ A ↔ m ∈ A
43 biidd ⊢ c = x → m ∈ B ↔ m ∈ B
44 eleq2w ⊢ c = x → ∅ ∈ c ↔ ∅ ∈ x
45 42 43 44 cadbi123d ⊢ c = x → cadd m ∈ A m ∈ B ∅ ∈ c ↔ cadd m ∈ A m ∈ B ∅ ∈ x
46 45 ifbid ⊢ c = x → if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = if cadd m ∈ A m ∈ B ∅ ∈ x 1 𝑜 ∅
47 eleq1w ⊢ m = y → m ∈ A ↔ y ∈ A
48 eleq1w ⊢ m = y → m ∈ B ↔ y ∈ B
49 biidd ⊢ m = y → ∅ ∈ x ↔ ∅ ∈ x
50 47 48 49 cadbi123d ⊢ m = y → cadd m ∈ A m ∈ B ∅ ∈ x ↔ cadd y ∈ A y ∈ B ∅ ∈ x
51 50 ifbid ⊢ m = y → if cadd m ∈ A m ∈ B ∅ ∈ x 1 𝑜 ∅ = if cadd y ∈ A y ∈ B ∅ ∈ x 1 𝑜 ∅
52 46 51 cbvmpov ⊢ c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ = x ∈ 2 𝑜 , y ∈ ℕ 0 ⟼ if cadd y ∈ A y ∈ B ∅ ∈ x 1 𝑜 ∅
53 1oex ⊢ 1 𝑜 ∈ V
54 53 18 ifex ⊢ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ ∈ V
55 41 52 54 ovmpoa ⊢ C ⁡ N ∈ 2 𝑜 ∧ N ∈ ℕ 0 → C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ N = if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
56 34 4 55 syl2anc ⊢ φ → C ⁡ N c ∈ 2 𝑜 , m ∈ ℕ 0 ⟼ if cadd m ∈ A m ∈ B ∅ ∈ c 1 𝑜 ∅ N = if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
57 12 32 56 3eqtrd ⊢ φ → C ⁡ N + 1 = if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
58 57 eleq2d ⊢ φ → ∅ ∈ C ⁡ N + 1 ↔ ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
59 noel ⊢ ¬ ∅ ∈ ∅
60 iffalse ⊢ ¬ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N → if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ = ∅
61 60 eleq2d ⊢ ¬ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N → ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ ↔ ∅ ∈ ∅
62 59 61 mtbiri ⊢ ¬ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N → ¬ ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
63 62 con4i ⊢ ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ → cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
64 0lt1o ⊢ ∅ ∈ 1 𝑜
65 iftrue ⊢ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N → if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ = 1 𝑜
66 64 65 eleqtrrid ⊢ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N → ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅
67 63 66 impbii ⊢ ∅ ∈ if cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N 1 𝑜 ∅ ↔ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N
68 58 67 bitrdi ⊢ φ → ∅ ∈ C ⁡ N + 1 ↔ cadd N ∈ A N ∈ B ∅ ∈ C ⁡ N