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