Theorem sadcadd

Description: Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016)

	Ref	Expression
Hypotheses	sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
	sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
	sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
	sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sadcadd.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
Assertion	sadcadd	$$⊢\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sadval.a	$$⊢\phi \to A\subseteq {\mathbb{N}}_0$$
2		sadval.b	$$⊢\phi \to B\subseteq {\mathbb{N}}_0$$
3		sadval.c	$$⊢C=seq0\left(\left(c\in 2_{𝑜},m\in {\mathbb{N}}_0⟼if\left(cadd\left(m\in A,m\in B,\varnothing \in c\right),1_{𝑜},\varnothing \right)\right),\left(n\in {\mathbb{N}}_0⟼if\left(n=0,\varnothing ,n-1\right)\right)\right)$$
4		sadcp1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
5		sadcadd.k	$$⊢K={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}$$
6		fveq2	$$⊢x=0\to C\left(x\right)=C\left(0\right)$$
7	6	eleq2d	$$⊢x=0\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(0\right)\right)$$
8		oveq2	$$⊢x=0\to 2^x=2^0$$
9		2cn	$$⊢2\in ℂ$$
10		exp0	$$⊢2\in ℂ\to 2^0=1$$
11	9 10	ax-mp	$$⊢2^0=1$$
12	8 11	eqtrdi	$$⊢x=0\to 2^x=1$$
13		oveq2	$$⊢x=0\to \left(0..^x\right)=\left(0..^0\right)$$
14		fzo0	$$⊢\left(0..^0\right)=\varnothing$$
15	13 14	eqtrdi	$$⊢x=0\to \left(0..^x\right)=\varnothing$$
16	15	ineq2d	$$⊢x=0\to A\cap \left(0..^x\right)=A\cap \varnothing$$
17		in0	$$⊢A\cap \varnothing =\varnothing$$
18	16 17	eqtrdi	$$⊢x=0\to A\cap \left(0..^x\right)=\varnothing$$
19	18	fveq2d	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)=K\left(\varnothing \right)$$
20		0nn0	$$⊢0\in {\mathbb{N}}_0$$
21		fvres	$$⊢0\in {\mathbb{N}}_0\to \left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)=\mathrm{bits}\left(0\right)$$
22	20 21	ax-mp	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)=\mathrm{bits}\left(0\right)$$
23		0bits	$$⊢\mathrm{bits}\left(0\right)=\varnothing$$
24	22 23	eqtr2i	$$⊢\varnothing =\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)$$
25	5 24	fveq12i	$$⊢K\left(\varnothing \right)={\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\right)$$
26		bitsf1o	$$⊢\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}$$
27		f1ocnvfv1	$$⊢\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}𝒫{\mathbb{N}}_0\cap \mathrm{Fin}\wedge 0\in {\mathbb{N}}_0\right)\to {\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\right)=0$$
28	26 20 27	mp2an	$$⊢{\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)}^{-1}\left(\left({\mathrm{bits}\upharpoonright }_{{\mathbb{N}}_0}\right)\left(0\right)\right)=0$$
29	25 28	eqtri	$$⊢K\left(\varnothing \right)=0$$
30	19 29	eqtrdi	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)=0$$
31	15	ineq2d	$$⊢x=0\to B\cap \left(0..^x\right)=B\cap \varnothing$$
32		in0	$$⊢B\cap \varnothing =\varnothing$$
33	31 32	eqtrdi	$$⊢x=0\to B\cap \left(0..^x\right)=\varnothing$$
34	33	fveq2d	$$⊢x=0\to K\left(B\cap \left(0..^x\right)\right)=K\left(\varnothing \right)$$
35	34 29	eqtrdi	$$⊢x=0\to K\left(B\cap \left(0..^x\right)\right)=0$$
36	30 35	oveq12d	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=0+0$$
37		00id	$$⊢0+0=0$$
38	36 37	eqtrdi	$$⊢x=0\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=0$$
39	12 38	breq12d	$$⊢x=0\to \left(2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 1\le 0\right)$$
40	7 39	bibi12d	$$⊢x=0\to \left(\left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\varnothing \in C\left(0\right)\leftrightarrow 1\le 0\right)\right)$$
41	40	imbi2d	$$⊢x=0\to \left(\left(\phi \to \left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \in C\left(0\right)\leftrightarrow 1\le 0\right)\right)\right)$$
42		fveq2	$$⊢x=k\to C\left(x\right)=C\left(k\right)$$
43	42	eleq2d	$$⊢x=k\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(k\right)\right)$$
44		oveq2	$$⊢x=k\to 2^x=2^k$$
45		oveq2	$$⊢x=k\to \left(0..^x\right)=\left(0..^k\right)$$
46	45	ineq2d	$$⊢x=k\to A\cap \left(0..^x\right)=A\cap \left(0..^k\right)$$
47	46	fveq2d	$$⊢x=k\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k\right)\right)$$
48	45	ineq2d	$$⊢x=k\to B\cap \left(0..^x\right)=B\cap \left(0..^k\right)$$
49	48	fveq2d	$$⊢x=k\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^k\right)\right)$$
50	47 49	oveq12d	$$⊢x=k\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)$$
51	44 50	breq12d	$$⊢x=k\to \left(2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)$$
52	43 51	bibi12d	$$⊢x=k\to \left(\left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)$$
53	52	imbi2d	$$⊢x=k\to \left(\left(\phi \to \left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\right)$$
54		fveq2	$$⊢x=k+1\to C\left(x\right)=C\left(k+1\right)$$
55	54	eleq2d	$$⊢x=k+1\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(k+1\right)\right)$$
56		oveq2	$$⊢x=k+1\to 2^x=2^{k+1}$$
57		oveq2	$$⊢x=k+1\to \left(0..^x\right)=\left(0..^k+1\right)$$
58	57	ineq2d	$$⊢x=k+1\to A\cap \left(0..^x\right)=A\cap \left(0..^k+1\right)$$
59	58	fveq2d	$$⊢x=k+1\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k+1\right)\right)$$
60	57	ineq2d	$$⊢x=k+1\to B\cap \left(0..^x\right)=B\cap \left(0..^k+1\right)$$
61	60	fveq2d	$$⊢x=k+1\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^k+1\right)\right)$$
62	59 61	oveq12d	$$⊢x=k+1\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)$$
63	56 62	breq12d	$$⊢x=k+1\to \left(2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)$$
64	55 63	bibi12d	$$⊢x=k+1\to \left(\left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)$$
65	64	imbi2d	$$⊢x=k+1\to \left(\left(\phi \to \left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)\right)$$
66		fveq2	$$⊢x=N\to C\left(x\right)=C\left(N\right)$$
67	66	eleq2d	$$⊢x=N\to \left(\varnothing \in C\left(x\right)\leftrightarrow \varnothing \in C\left(N\right)\right)$$
68		oveq2	$$⊢x=N\to 2^x=2^N$$
69		oveq2	$$⊢x=N\to \left(0..^x\right)=\left(0..^N\right)$$
70	69	ineq2d	$$⊢x=N\to A\cap \left(0..^x\right)=A\cap \left(0..^N\right)$$
71	70	fveq2d	$$⊢x=N\to K\left(A\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^N\right)\right)$$
72	69	ineq2d	$$⊢x=N\to B\cap \left(0..^x\right)=B\cap \left(0..^N\right)$$
73	72	fveq2d	$$⊢x=N\to K\left(B\cap \left(0..^x\right)\right)=K\left(B\cap \left(0..^N\right)\right)$$
74	71 73	oveq12d	$$⊢x=N\to K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)=K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)$$
75	68 74	breq12d	$$⊢x=N\to \left(2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)$$
76	67 75	bibi12d	$$⊢x=N\to \left(\left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\leftrightarrow \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)\right)$$
77	76	imbi2d	$$⊢x=N\to \left(\left(\phi \to \left(\varnothing \in C\left(x\right)\leftrightarrow 2^x\le K\left(A\cap \left(0..^x\right)\right)+K\left(B\cap \left(0..^x\right)\right)\right)\right)\leftrightarrow \left(\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)\right)\right)$$
78	1 2 3	sadc0	$$⊢\phi \to \neg \varnothing \in C\left(0\right)$$
79		0lt1	$$⊢0<1$$
80		0re	$$⊢0\in ℝ$$
81		1re	$$⊢1\in ℝ$$
82	80 81	ltnlei	$$⊢0<1\leftrightarrow \neg 1\le 0$$
83	79 82	mpbi	$$⊢\neg 1\le 0$$
84	83	a1i	$$⊢\phi \to \neg 1\le 0$$
85	78 84	2falsed	$$⊢\phi \to \left(\varnothing \in C\left(0\right)\leftrightarrow 1\le 0\right)$$
86	1	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to A\subseteq {\mathbb{N}}_0$$
87	2	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to B\subseteq {\mathbb{N}}_0$$
88		simplr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to k\in {\mathbb{N}}_0$$
89		simpr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)$$
90	86 87 3 88 5 89	sadcaddlem	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)$$
91	90	ex	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(\left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)$$
92	91	expcom	$$⊢k\in {\mathbb{N}}_0\to \left(\phi \to \left(\left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\to \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)\right)$$
93	92	a2d	$$⊢k\in {\mathbb{N}}_0\to \left(\left(\phi \to \left(\varnothing \in C\left(k\right)\leftrightarrow 2^k\le K\left(A\cap \left(0..^k\right)\right)+K\left(B\cap \left(0..^k\right)\right)\right)\right)\to \left(\phi \to \left(\varnothing \in C\left(k+1\right)\leftrightarrow 2^{k+1}\le K\left(A\cap \left(0..^k+1\right)\right)+K\left(B\cap \left(0..^k+1\right)\right)\right)\right)\right)$$
94	41 53 65 77 85 93	nn0ind	$$⊢N\in {\mathbb{N}}_0\to \left(\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)\right)$$
95	4 94	mpcom	$$⊢\phi \to \left(\varnothing \in C\left(N\right)\leftrightarrow 2^N\le K\left(A\cap \left(0..^N\right)\right)+K\left(B\cap \left(0..^N\right)\right)\right)$$