Metamath Proof Explorer

Theorem sadcadd

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

Ref Expression
Hypotheses sadval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
sadval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
sadval.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
sadcp1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sadcadd.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
Assertion sadcadd ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) ↔ ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )

Proof

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