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=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
sadcp1.n ⊢φ→N∈ℕ0
Assertion sadcp1 ⊢φ→∅∈C⁡N+1↔caddN∈AN∈B∅∈C⁡N

Proof

Step Hyp Ref Expression
1 sadval.a ⊢φ→A⊆ℕ0
2 sadval.b ⊢φ→B⊆ℕ0
3 sadval.c ⊢C=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1
4 sadcp1.n ⊢φ→N∈ℕ0
5 nn0uz ⊢ℕ0=ℤ≥0
6 4 5 eleqtrdi ⊢φ→N∈ℤ≥0
7 seqp1 ⊢N∈ℤ≥0→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1
8 6 7 syl ⊢φ→seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1
9 3 fveq1i ⊢C⁡N+1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1
10 3 fveq1i ⊢C⁡N=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N
11 10 oveq1i ⊢C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1=seq0c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1
12 8 9 11 3eqtr4g ⊢φ→C⁡N+1=C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=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→ifn=0∅n−1=ifN+1=0∅N+1-1
17 eqid ⊢n∈ℕ0⟼ifn=0∅n−1=n∈ℕ0⟼ifn=0∅n−1
18 0ex ⊢∅∈V
19 ovex ⊢N+1-1∈V
20 18 19 ifex ⊢ifN+1=0∅N+1-1∈V
21 16 17 20 fvmpt ⊢N+1∈ℕ0→n∈ℕ0⟼ifn=0∅n−1⁡N+1=ifN+1=0∅N+1-1
22 4 13 21 3syl ⊢φ→n∈ℕ0⟼ifn=0∅n−1⁡N+1=ifN+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→ifN+1=0∅N+1-1=N+1-1
27 25 26 syl ⊢φ→ifN+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⟼ifn=0∅n−1⁡N+1=N
32 31 oveq2d ⊢φ→C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅n∈ℕ0⟼ifn=0∅n−1⁡N+1=C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅N
33 1 2 3 sadcf ⊢φ→C:ℕ0⟶2𝑜
34 33 4 ffvelcdmd ⊢φ→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→caddy∈Ay∈B∅∈x↔caddN∈AN∈B∅∈C⁡N
41 40 ifbid ⊢x=C⁡N∧y=N→ifcaddy∈Ay∈B∅∈x1𝑜∅=ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
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→caddm∈Am∈B∅∈c↔caddm∈Am∈B∅∈x
46 45 ifbid ⊢c=x→ifcaddm∈Am∈B∅∈c1𝑜∅=ifcaddm∈Am∈B∅∈x1𝑜∅
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→caddm∈Am∈B∅∈x↔caddy∈Ay∈B∅∈x
51 50 ifbid ⊢m=y→ifcaddm∈Am∈B∅∈x1𝑜∅=ifcaddy∈Ay∈B∅∈x1𝑜∅
52 46 51 cbvmpov ⊢c∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅=x∈2𝑜,y∈ℕ0⟼ifcaddy∈Ay∈B∅∈x1𝑜∅
53 1oex ⊢1𝑜∈V
54 53 18 ifex ⊢ifcaddN∈AN∈B∅∈C⁡N1𝑜∅∈V
55 41 52 54 ovmpoa ⊢C⁡N∈2𝑜∧N∈ℕ0→C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅N=ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
56 34 4 55 syl2anc ⊢φ→C⁡Nc∈2𝑜,m∈ℕ0⟼ifcaddm∈Am∈B∅∈c1𝑜∅N=ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
57 12 32 56 3eqtrd ⊢φ→C⁡N+1=ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
58 57 eleq2d ⊢φ→∅∈C⁡N+1↔∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
59 noel ⊢¬∅∈∅
60 iffalse ⊢¬caddN∈AN∈B∅∈C⁡N→ifcaddN∈AN∈B∅∈C⁡N1𝑜∅=∅
61 60 eleq2d ⊢¬caddN∈AN∈B∅∈C⁡N→∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅↔∅∈∅
62 59 61 mtbiri ⊢¬caddN∈AN∈B∅∈C⁡N→¬∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
63 62 con4i ⊢∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅→caddN∈AN∈B∅∈C⁡N
64 0lt1o ⊢∅∈1𝑜
65 iftrue ⊢caddN∈AN∈B∅∈C⁡N→ifcaddN∈AN∈B∅∈C⁡N1𝑜∅=1𝑜
66 64 65 eleqtrrid ⊢caddN∈AN∈B∅∈C⁡N→∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅
67 63 66 impbii ⊢∅∈ifcaddN∈AN∈B∅∈C⁡N1𝑜∅↔caddN∈AN∈B∅∈C⁡N
68 58 67 bitrdi ⊢φ→∅∈C⁡N+1↔caddN∈AN∈B∅∈C⁡N