Step | Hyp | Ref
| Expression |
1 | | sadcp1.n |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | fveq2 6768 |
. . . . . 6
⊢ (𝑥 = 0 → (𝐶‘𝑥) = (𝐶‘0)) |
3 | 2 | eleq2d 2825 |
. . . . 5
⊢ (𝑥 = 0 → (∅ ∈
(𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘0))) |
4 | | oveq2 7276 |
. . . . . . 7
⊢ (𝑥 = 0 → (2↑𝑥) = (2↑0)) |
5 | | 2cn 12031 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
6 | | exp0 13767 |
. . . . . . . 8
⊢ (2 ∈
ℂ → (2↑0) = 1) |
7 | 5, 6 | ax-mp 5 |
. . . . . . 7
⊢
(2↑0) = 1 |
8 | 4, 7 | eqtrdi 2795 |
. . . . . 6
⊢ (𝑥 = 0 → (2↑𝑥) = 1) |
9 | | oveq2 7276 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → (0..^𝑥) = (0..^0)) |
10 | | fzo0 13392 |
. . . . . . . . . . . . 13
⊢ (0..^0) =
∅ |
11 | 9, 10 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → (0..^𝑥) = ∅) |
12 | 11 | ineq2d 4151 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ ∅)) |
13 | | in0 4330 |
. . . . . . . . . . 11
⊢ (𝐴 ∩ ∅) =
∅ |
14 | 12, 13 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝐴 ∩ (0..^𝑥)) = ∅) |
15 | 14 | fveq2d 6772 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘∅)) |
16 | | sadcadd.k |
. . . . . . . . . . 11
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
17 | | 0nn0 12231 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℕ0 |
18 | | fvres 6787 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℕ0 → ((bits ↾ ℕ0)‘0) =
(bits‘0)) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((bits
↾ ℕ0)‘0) = (bits‘0) |
20 | | 0bits 16127 |
. . . . . . . . . . . 12
⊢
(bits‘0) = ∅ |
21 | 19, 20 | eqtr2i 2768 |
. . . . . . . . . . 11
⊢ ∅ =
((bits ↾ ℕ0)‘0) |
22 | 16, 21 | fveq12i 6774 |
. . . . . . . . . 10
⊢ (𝐾‘∅) = (◡(bits ↾
ℕ0)‘((bits ↾
ℕ0)‘0)) |
23 | | bitsf1o 16133 |
. . . . . . . . . . 11
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
24 | | f1ocnvfv1 7142 |
. . . . . . . . . . 11
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ 0 ∈ ℕ0) → (◡(bits ↾
ℕ0)‘((bits ↾ ℕ0)‘0)) =
0) |
25 | 23, 17, 24 | mp2an 688 |
. . . . . . . . . 10
⊢ (◡(bits ↾
ℕ0)‘((bits ↾ ℕ0)‘0)) =
0 |
26 | 22, 25 | eqtri 2767 |
. . . . . . . . 9
⊢ (𝐾‘∅) =
0 |
27 | 15, 26 | eqtrdi 2795 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = 0) |
28 | 11 | ineq2d 4151 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ ∅)) |
29 | | in0 4330 |
. . . . . . . . . . 11
⊢ (𝐵 ∩ ∅) =
∅ |
30 | 28, 29 | eqtrdi 2795 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (𝐵 ∩ (0..^𝑥)) = ∅) |
31 | 30 | fveq2d 6772 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘∅)) |
32 | 31, 26 | eqtrdi 2795 |
. . . . . . . 8
⊢ (𝑥 = 0 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = 0) |
33 | 27, 32 | oveq12d 7286 |
. . . . . . 7
⊢ (𝑥 = 0 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = (0 + 0)) |
34 | | 00id 11133 |
. . . . . . 7
⊢ (0 + 0) =
0 |
35 | 33, 34 | eqtrdi 2795 |
. . . . . 6
⊢ (𝑥 = 0 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = 0) |
36 | 8, 35 | breq12d 5091 |
. . . . 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 6768 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (𝐶‘𝑥) = (𝐶‘𝑘)) |
40 | 39 | eleq2d 2825 |
. . . . 5
⊢ (𝑥 = 𝑘 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑘))) |
41 | | oveq2 7276 |
. . . . . 6
⊢ (𝑥 = 𝑘 → (2↑𝑥) = (2↑𝑘)) |
42 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑥 = 𝑘 → (0..^𝑥) = (0..^𝑘)) |
43 | 42 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^𝑘))) |
44 | 43 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^𝑘)))) |
45 | 42 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = 𝑘 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^𝑘))) |
46 | 45 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = 𝑘 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^𝑘)))) |
47 | 44, 46 | oveq12d 7286 |
. . . . . 6
⊢ (𝑥 = 𝑘 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘))))) |
48 | 41, 47 | breq12d 5091 |
. . . . 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 6768 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (𝐶‘𝑥) = (𝐶‘(𝑘 + 1))) |
52 | 51 | eleq2d 2825 |
. . . . 5
⊢ (𝑥 = (𝑘 + 1) → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘(𝑘 + 1)))) |
53 | | oveq2 7276 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → (2↑𝑥) = (2↑(𝑘 + 1))) |
54 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑥 = (𝑘 + 1) → (0..^𝑥) = (0..^(𝑘 + 1))) |
55 | 54 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^(𝑘 + 1)))) |
56 | 55 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^(𝑘 + 1))))) |
57 | 54 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = (𝑘 + 1) → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^(𝑘 + 1)))) |
58 | 57 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = (𝑘 + 1) → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1))))) |
59 | 56, 58 | oveq12d 7286 |
. . . . . 6
⊢ (𝑥 = (𝑘 + 1) → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^(𝑘 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑘 + 1)))))) |
60 | 53, 59 | breq12d 5091 |
. . . . 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 6768 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝐶‘𝑥) = (𝐶‘𝑁)) |
64 | 63 | eleq2d 2825 |
. . . . 5
⊢ (𝑥 = 𝑁 → (∅ ∈ (𝐶‘𝑥) ↔ ∅ ∈ (𝐶‘𝑁))) |
65 | | oveq2 7276 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (2↑𝑥) = (2↑𝑁)) |
66 | | oveq2 7276 |
. . . . . . . . 9
⊢ (𝑥 = 𝑁 → (0..^𝑥) = (0..^𝑁)) |
67 | 66 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐴 ∩ (0..^𝑥)) = (𝐴 ∩ (0..^𝑁))) |
68 | 67 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐾‘(𝐴 ∩ (0..^𝑥))) = (𝐾‘(𝐴 ∩ (0..^𝑁)))) |
69 | 66 | ineq2d 4151 |
. . . . . . . 8
⊢ (𝑥 = 𝑁 → (𝐵 ∩ (0..^𝑥)) = (𝐵 ∩ (0..^𝑁))) |
70 | 69 | fveq2d 6772 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝐾‘(𝐵 ∩ (0..^𝑥))) = (𝐾‘(𝐵 ∩ (0..^𝑁)))) |
71 | 68, 70 | oveq12d 7286 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ((𝐾‘(𝐴 ∩ (0..^𝑥))) + (𝐾‘(𝐵 ∩ (0..^𝑥)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
72 | 65, 71 | breq12d 5091 |
. . . . 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 16142 |
. . . 4
⊢ (𝜑 → ¬ ∅ ∈
(𝐶‘0)) |
79 | | 0lt1 11480 |
. . . . . 6
⊢ 0 <
1 |
80 | | 0re 10961 |
. . . . . . 7
⊢ 0 ∈
ℝ |
81 | | 1re 10959 |
. . . . . . 7
⊢ 1 ∈
ℝ |
82 | 80, 81 | ltnlei 11079 |
. . . . . 6
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
83 | 79, 82 | mpbi 229 |
. . . . 5
⊢ ¬ 1
≤ 0 |
84 | 83 | a1i 11 |
. . . 4
⊢ (𝜑 → ¬ 1 ≤
0) |
85 | 78, 84 | 2falsed 376 |
. . 3
⊢ (𝜑 → (∅ ∈ (𝐶‘0) ↔ 1 ≤
0)) |
86 | 75 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ (∅
∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → 𝐴 ⊆
ℕ0) |
87 | 76 | ad2antrr 722 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ ℕ0) ∧ (∅
∈ (𝐶‘𝑘) ↔ (2↑𝑘) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑘))) + (𝐾‘(𝐵 ∩ (0..^𝑘)))))) → 𝐵 ⊆
ℕ0) |
88 | | simplr 765 |
. . . . . . 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 16145 |
. . . . . 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 12398 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (𝜑 → (∅
∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))) |
95 | 1, 94 | mpcom 38 |
1
⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))) |