sadcadd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > sadcadd		Structured version Visualization version GIF version

Theorem sadcadd 16403

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

**Hypotheses**
Ref	Expression
sadval.a	⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
sadval.b	⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
sadval.c	⊢ 𝐶 = seq0((𝑐 ∈ 2_o, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1_o, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
sadcp1.n	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
sadcadd.k	⊢ 𝐾 = ^◡(bits ↾ ℕ₀)

**Assertion**
Ref	Expression
sadcadd	⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))

Distinct variable groups: 𝑚,𝑐,𝑛 𝐴,𝑐,𝑚 𝐵,𝑐,𝑚 𝑛,𝑁 Allowed substitution hints: 𝜑(𝑚,𝑛,𝑐) 𝐴(𝑛) 𝐵(𝑛) 𝐶(𝑚,𝑛,𝑐) 𝐾(𝑚,𝑛,𝑐) 𝑁(𝑚,𝑐)

Proof of Theorem sadcadd Dummy variables 𝑘 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sadcp1.n	. 2 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
2		fveq2 6890	. . . . . 6 ⊢ (𝑥 = 0 → (𝐶‘𝑥) = (𝐶‘0))
3	2	eleq2d 2817	. . . . 5 ⊢ (𝑥 = 0 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘0)))
4		oveq2 7419	. . . . . . 7 ⊢ (𝑥 = 0 → (2↑𝑥) = (2↑0))
5		2cn 12291	. . . . . . . 8 ⊢ 2 ∈ ℂ
6		exp0 14035	. . . . . . . 8 ⊢ (2 ∈ ℂ → (2↑0) = 1)
7	5, 6	ax-mp 5	. . . . . . 7 ⊢ (2↑0) = 1
8	4, 7	eqtrdi 2786	. . . . . 6 ⊢ (𝑥 = 0 → (2↑𝑥) = 1)
9		oveq2 7419	. . . . . . . . . . . . 13 ⊢ (𝑥 = 0 → (0..^𝑥) = (0..^0))
10		fzo0 13660	. . . . . . . . . . . . 13 ⊢ (0..^0) = ∅
11	9, 10	eqtrdi 2786	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (0..^𝑥) = ∅)
12	11	ineq2d 4211	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ ∅))
13		in0 4390	. . . . . . . . . . 11 ⊢ (𝐴 ∩ ∅) = ∅
14	12, 13	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝐴 ∩ (0..^𝑥)) = ∅)
15	14	fveq2d 6894	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘∅))
16		sadcadd.k	. . . . . . . . . . 11 ⊢ 𝐾 = ^◡(bits ↾ ℕ₀)
17		0nn0 12491	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℕ₀
18		fvres 6909	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℕ₀ → ((bits ↾ ℕ₀)‘0) = (bits‘0))
19	17, 18	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((bits ↾ ℕ₀)‘0) = (bits‘0)
20		0bits 16384	. . . . . . . . . . . 12 ⊢ (bits‘0) = ∅
21	19, 20	eqtr2i 2759	. . . . . . . . . . 11 ⊢ ∅ = ((bits ↾ ℕ₀)‘0)
22	16, 21	fveq12i 6896	. . . . . . . . . 10 ⊢ (𝐾‘∅) = (^◡(bits ↾ ℕ₀)‘((bits ↾ ℕ₀)‘0))
23		bitsf1o 16390	. . . . . . . . . . 11 ⊢ (bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin)
24		f1ocnvfv1 7276	. . . . . . . . . . 11 ⊢ (((bits ↾ ℕ₀):ℕ₀–1-1-onto→(𝒫 ℕ₀ ∩ Fin) ∧ 0 ∈ ℕ₀) → (^◡(bits ↾ ℕ₀)‘((bits ↾ ℕ₀)‘0)) = 0)
25	23, 17, 24	mp2an 688	. . . . . . . . . 10 ⊢ (^◡(bits ↾ ℕ₀)‘((bits ↾ ℕ₀)‘0)) = 0
26	22, 25	eqtri 2758	. . . . . . . . 9 ⊢ (𝐾‘∅) = 0
27	15, 26	eqtrdi 2786	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = 0)
28	11	ineq2d 4211	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ ∅))
29		in0 4390	. . . . . . . . . . 11 ⊢ (𝐵 ∩ ∅) = ∅
30	28, 29	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑥 = 0 → (𝐵 ∩ (0..^𝑥)) = ∅)
31	30	fveq2d 6894	. . . . . . . . 9 ⊢ (𝑥 = 0 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘∅))
32	31, 26	eqtrdi 2786	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = 0)
33	27, 32	oveq12d 7429	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = (0 + 0))
34		00id 11393	. . . . . . 7 ⊢ (0 + 0) = 0
35	33, 34	eqtrdi 2786	. . . . . 6 ⊢ (𝑥 = 0 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = 0)
36	8, 35	breq12d 5160	. . . . 5 ⊢ (𝑥 = 0 → ((2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) ↔ 1 ≤ 0))
37	3, 36	bibi12d 344	. . . 4 ⊢ (𝑥 = 0 → ((∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥))))) ↔ (∅ ∈ (𝐶‘0) ↔ 1 ≤ 0)))
38	37	imbi2d 339	. . 3 ⊢ (𝑥 = 0 → ((𝜑 → (∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))))) ↔ (𝜑 → (∅ ∈ (𝐶‘0) ↔ 1 ≤ 0))))
39		fveq2 6890	. . . . . 6 ⊢ (𝑥 = 𝑘 → (𝐶‘𝑥) = (𝐶‘𝑘))
40	39	eleq2d 2817	. . . . 5 ⊢ (𝑥 = 𝑘 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑘)))
41		oveq2 7419	. . . . . 6 ⊢ (𝑥 = 𝑘 → (2↑𝑥) = (2↑𝑘))
42		oveq2 7419	. . . . . . . . 9 ⊢ (𝑥 = 𝑘 → (0..^𝑥) = (0..^𝑘))
43	42	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = 𝑘 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^𝑘)))
44	43	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^𝑘))))
45	42	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = 𝑘 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^𝑘)))
46	45	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = 𝑘 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^𝑘))))
47	44, 46	oveq12d 7429	. . . . . 6 ⊢ (𝑥 = 𝑘 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))
48	41, 47	breq12d 5160	. . . . 5 ⊢ (𝑥 = 𝑘 → ((2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))))
49	40, 48	bibi12d 344	. . . 4 ⊢ (𝑥 = 𝑘 → ((∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥))))) ↔ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))))
50	49	imbi2d 339	. . 3 ⊢ (𝑥 = 𝑘 → ((𝜑 → (∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))))) ↔ (𝜑 → (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))))))
51		fveq2 6890	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (𝐶‘𝑥) = (𝐶‘(𝑘 + 1)))
52	51	eleq2d 2817	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘(𝑘 + 1))))
53		oveq2 7419	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → (2↑𝑥) = (2↑(𝑘 + 1)))
54		oveq2 7419	. . . . . . . . 9 ⊢ (𝑥 = (𝑘 + 1) → (0..^𝑥) = (0..^(𝑘 + 1)))
55	54	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = (𝑘 + 1) → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^(𝑘 + 1))))
56	55	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))))
57	54	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = (𝑘 + 1) → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^(𝑘 + 1))))
58	57	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = (𝑘 + 1) → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))
59	56, 58	oveq12d 7429	. . . . . 6 ⊢ (𝑥 = (𝑘 + 1) → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1))))))
60	53, 59	breq12d 5160	. . . . 5 ⊢ (𝑥 = (𝑘 + 1) → ((2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))))
61	52, 60	bibi12d 344	. . . 4 ⊢ (𝑥 = (𝑘 + 1) → ((∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥))))) ↔ (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1))))))))
62	61	imbi2d 339	. . 3 ⊢ (𝑥 = (𝑘 + 1) → ((𝜑 → (∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))))) ↔ (𝜑 → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))))))
63		fveq2 6890	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝐶‘𝑥) = (𝐶‘𝑁))
64	63	eleq2d 2817	. . . . 5 ⊢ (𝑥 = 𝑁 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑁)))
65		oveq2 7419	. . . . . 6 ⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁))
66		oveq2 7419	. . . . . . . . 9 ⊢ (𝑥 = 𝑁 → (0..^𝑥) = (0..^𝑁))
67	66	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^𝑁)))
68	67	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^𝑁))))
69	66	ineq2d 4211	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^𝑁)))
70	69	fveq2d 6894	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^𝑁))))
71	68, 70	oveq12d 7429	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
72	65, 71	breq12d 5160	. . . . 5 ⊢ (𝑥 = 𝑁 → ((2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))
73	64, 72	bibi12d 344	. . . 4 ⊢ (𝑥 = 𝑁 → ((∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥))))) ↔ (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))))
74	73	imbi2d 339	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (∅ ∈ (𝐶‘𝑥) ↔ (2↑𝑥) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))))) ↔ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))))
75		sadval.a	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ ℕ₀)
76		sadval.b	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ ℕ₀)
77		sadval.c	. . . . 5 ⊢ 𝐶 = seq0((𝑐 ∈ 2_o, 𝑚 ∈ ℕ₀ ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1_o, ∅)), (𝑛 ∈ ℕ₀ ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
78	75, 76, 77	sadc0 16399	. . . 4 ⊢ (𝜑 → ¬ ∅ ∈ (𝐶‘0))
79		0lt1 11740	. . . . . 6 ⊢ 0 < 1
80		0re 11220	. . . . . . 7 ⊢ 0 ∈ ℝ
81		1re 11218	. . . . . . 7 ⊢ 1 ∈ ℝ
82	80, 81	ltnlei 11339	. . . . . 6 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
83	79, 82	mpbi 229	. . . . 5 ⊢ ¬ 1 ≤ 0
84	83	a1i 11	. . . 4 ⊢ (𝜑 → ¬ 1 ≤ 0)
85	78, 84	2falsed 375	. . 3 ⊢ (𝜑 → (∅ ∈ (𝐶‘0) ↔ 1 ≤ 0))
86	75	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → 𝐴 ⊆ ℕ₀)
87	76	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → 𝐵 ⊆ ℕ₀)
88		simplr 765	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → 𝑘 ∈ ℕ₀)
89		simpr 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))))
90	86, 87, 77, 88, 16, 89	sadcaddlem 16402	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ℕ₀) ∧ (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))))
91	90	ex 411	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ₀) → ((∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1))))))))
92	91	expcom 412	. . . 4 ⊢ (𝑘 ∈ ℕ₀ → (𝜑 → ((∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))) → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))))))
93	92	a2d 29	. . 3 ⊢ (𝑘 ∈ ℕ₀ → ((𝜑 → (∅ ∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → (𝜑 → (∅ ∈ (𝐶‘(𝑘 + 1)) ↔ (2↑(𝑘 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))))))
94	38, 50, 62, 74, 85, 93	nn0ind 12661	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))))
95	1, 94	mpcom 38	1 ⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 caddwcad 1605 ∈ wcel 2104 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 𝒫 cpw 4601 class class class wbr 5147 ↦ cmpt 5230 ^◡ccnv 5674 ↾ cres 5677 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7411 ∈ cmpo 7413 1_oc1o 8461 2_oc2o 8462 Fincfn 8941 ℂcc 11110 0cc0 11112 1c1 11113 + caddc 11115 < clt 11252 ≤ cle 11253 − cmin 11448 2c2 12271 ℕ₀cn0 12476 ..^cfzo 13631 seqcseq 13970 ↑cexp 14031 bitscbits 16364

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-inf2 9638 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-xor 1508 df-tru 1542 df-fal 1552 df-cad 1606 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-disj 5113 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-se 5631 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-1st 7977 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-1o 8468 df-2o 8469 df-oadd 8472 df-er 8705 df-map 8824 df-pm 8825 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-oi 9507 df-dju 9898 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-3 12280 df-n0 12477 df-xnn0 12549 df-z 12563 df-uz 12827 df-rp 12979 df-fz 13489 df-fzo 13632 df-fl 13761 df-mod 13839 df-seq 13971 df-exp 14032 df-hash 14295 df-cj 15050 df-re 15051 df-im 15052 df-sqrt 15186 df-abs 15187 df-clim 15436 df-sum 15637 df-dvds 16202 df-bits 16367

This theorem is referenced by: (None)

W3C validator