Proof of Theorem sadcaddlem
Step | Hyp | Ref
| Expression |
1 | | cad1 1555 |
. . . . 5
⊢ (∅
∈ (𝐶‘𝑁) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
3 | | 2nn 11185 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
4 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℕ) |
5 | | sadcp1.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | 4, 5 | nnexpcld 13030 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
7 | 6 | nnred 11035 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝑁) ∈ ℝ) |
8 | 7 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ∈ ℝ) |
9 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 |
10 | | sadval.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
11 | 9, 10 | syl5ss 3614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) |
12 | | fzofi 12773 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑁) ∈
Fin |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
14 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
15 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
16 | 13, 14, 15 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
17 | | elfpw 8268 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐴 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin)) |
18 | 11, 16, 17 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
19 | | bitsf1o 15167 |
. . . . . . . . . . . . . . 15
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
20 | | f1ocnv 6149 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
→ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0 |
22 | | sadcadd.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
23 | | f1oeq1 6127 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 = ◡(bits ↾ ℕ0) →
(𝐾:(𝒫
ℕ0 ∩ Fin)–1-1-onto→ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 ↔ ◡(bits ↾
ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0) |
25 | 21, 24 | mpbir 221 |
. . . . . . . . . . . . 13
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 |
26 | | f1of 6137 |
. . . . . . . . . . . . 13
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 → 𝐾:(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 |
28 | 27 | ffvelrni 6358 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) |
29 | 18, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) |
30 | | inss1 3833 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵 |
31 | | sadval.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
32 | 30, 31 | syl5ss 3614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆
ℕ0) |
33 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
34 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin) |
35 | 13, 33, 34 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin) |
36 | | elfpw 8268 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐵 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin)) |
37 | 32, 35, 36 | sylanbrc 698 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
38 | 27 | ffvelrni 6358 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) |
40 | 29, 39 | nn0addcld 11355 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈
ℕ0) |
41 | 40 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
42 | 41 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
43 | | 2nn0 11309 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → 2 ∈
ℕ0) |
45 | 5 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈
ℕ0) |
46 | 44, 45 | nn0expcld 13031 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈
ℕ0) |
47 | | 0nn0 11307 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐴) → 0 ∈
ℕ0) |
49 | 46, 48 | ifclda 4120 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
50 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → 2 ∈
ℕ0) |
51 | 5 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
52 | 50, 51 | nn0expcld 13031 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ∈
ℕ0) |
53 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐵) → 0 ∈
ℕ0) |
54 | 52, 53 | ifclda 4120 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
55 | 49, 54 | nn0addcld 11355 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈
ℕ0) |
56 | 55 | nn0red 11352 |
. . . . . . . 8
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
57 | 56 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
58 | | sadcaddlem.1 |
. . . . . . . . 9
⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))) |
59 | 58 | biimpa 501 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
60 | 59 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
61 | 6 | nnnn0d 11351 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2↑𝑁) ∈
ℕ0) |
62 | | ifcl 4130 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
63 | 61, 47, 62 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
64 | 63 | nn0ge0d 11354 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) |
65 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ∈ ℝ) |
66 | | 0red 10041 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐵) → 0 ∈ ℝ) |
67 | 65, 66 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℝ) |
68 | 7, 67 | addge01d 10615 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
69 | 64, 68 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
70 | 69 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
71 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝐴 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = (2↑𝑁)) |
72 | 71 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = (2↑𝑁)) |
73 | 72 | oveq1d 6665 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
74 | 70, 73 | breqtrrd 4681 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
75 | | ifcl 4130 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
76 | 61, 47, 75 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
77 | 76 | nn0ge0d 11354 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) |
78 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℝ) |
79 | | 0red 10041 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐴) → 0 ∈ ℝ) |
80 | 78, 79 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℝ) |
81 | 7, 80 | addge02d 10616 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁)))) |
82 | 77, 81 | mpbid 222 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
83 | 82 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
84 | | iftrue 4092 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝐵 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = (2↑𝑁)) |
85 | 84 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = (2↑𝑁)) |
86 | 85 | oveq2d 6666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
87 | 83, 86 | breqtrrd 4681 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
88 | 74, 87 | jaodan 826 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
89 | 8, 8, 42, 57, 60, 88 | le2addd 10646 |
. . . . . 6
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
90 | 89 | ex 450 |
. . . . 5
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
91 | | ioran 511 |
. . . . . 6
⊢ (¬
(𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) ↔ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) |
92 | | iffalse 4095 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑁 ∈ 𝐴 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = 0) |
93 | 92 | ad2antrl 764 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = 0) |
94 | | iffalse 4095 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑁 ∈ 𝐵 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = 0) |
95 | 94 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = 0) |
96 | 93, 95 | oveq12d 6668 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (0 + 0)) |
97 | | 00id 10211 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
0 |
98 | 96, 97 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = 0) |
99 | 98 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0)) |
100 | 29 | nn0red 11352 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
101 | 100 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
102 | 39 | nn0red 11352 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
103 | 102 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
104 | 101, 103 | readdcld 10069 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
105 | 104 | recnd 10068 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℂ) |
106 | 105 | addid1d 10236 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
107 | 99, 106 | eqtrd 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
108 | 22 | fveq1i 6192 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘(𝐴 ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) |
109 | 108 | fveq2i 6194 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) |
110 | | fvres 6207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits
↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁))))) |
111 | 29, 110 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁))))) |
112 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . . . . 16
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐴 ∩ (0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin)) → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
113 | 19, 18, 112 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
114 | 109, 111,
113 | 3eqtr3a 2680 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
115 | 114, 14 | syl6eqss 3655 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
116 | 29 | nn0zd 11480 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ) |
117 | | bitsfzo 15157 |
. . . . . . . . . . . . . 14
⊢ (((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
118 | 116, 5, 117 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
119 | 115, 118 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
120 | | elfzolt2 12479 |
. . . . . . . . . . . 12
⊢ ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁)) |
121 | 119, 120 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁)) |
122 | 22 | fveq1i 6192 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘(𝐵 ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁))) |
123 | 122 | fveq2i 6194 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) |
124 | | fvres 6207 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits
↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁))))) |
125 | 39, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁))))) |
126 | | f1ocnvfv2 6533 |
. . . . . . . . . . . . . . . 16
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐵 ∩ (0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin)) → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
127 | 19, 37, 126 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
128 | 123, 125,
127 | 3eqtr3a 2680 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
129 | 128, 33 | syl6eqss 3655 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
130 | 39 | nn0zd 11480 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ) |
131 | | bitsfzo 15157 |
. . . . . . . . . . . . . 14
⊢ (((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
132 | 130, 5, 131 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
133 | 129, 132 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
134 | | elfzolt2 12479 |
. . . . . . . . . . . 12
⊢ ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁)) |
135 | 133, 134 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁)) |
136 | 100, 102,
7, 7, 121, 135 | lt2addd 10650 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁))) |
137 | 136 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁))) |
138 | 107, 137 | eqbrtrd 4675 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁))) |
139 | 80 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℝ) |
140 | 67 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℝ) |
141 | 139, 140 | readdcld 10069 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
142 | 104, 141 | readdcld 10069 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
143 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (2↑𝑁) ∈ ℝ) |
144 | 143, 143 | readdcld 10069 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
145 | 142, 144 | ltnled 10184 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)) ↔ ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
146 | 138, 145 | mpbid 222 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
147 | 146 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
148 | 91, 147 | syl5bi 232 |
. . . . 5
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (¬ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
149 | 90, 148 | impcon4bid 217 |
. . . 4
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
150 | 2, 149 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
151 | | cad0 1556 |
. . . . 5
⊢ (¬
∅ ∈ (𝐶‘𝑁) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
152 | 151 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
153 | 40 | nn0ge0d 11354 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
154 | 7, 7 | readdcld 10069 |
. . . . . . . . . 10
⊢ (𝜑 → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
155 | 154, 41 | addge02d 10616 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))) |
156 | 153, 155 | mpbid 222 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
157 | 156 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
158 | 71, 84 | oveqan12d 6669 |
. . . . . . . . 9
⊢ ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁))) |
159 | 158 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁))) |
160 | 159 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
161 | 157, 160 | breqtrrd 4681 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
162 | 161 | ex 450 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
163 | 100 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
164 | 102 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
165 | 163, 164 | readdcld 10069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
166 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ∈ ℝ) |
167 | 7, 41 | lenltd 10183 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))) |
168 | 58, 167 | bitrd 268 |
. . . . . . . . . . 11
⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))) |
169 | 168 | con2bid 344 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁) ↔ ¬ ∅ ∈ (𝐶‘𝑁))) |
170 | 169 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)) |
171 | 165, 166,
166, 170 | ltadd1dd 10638 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁))) |
172 | 165, 166 | readdcld 10069 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) ∈ ℝ) |
173 | 154 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
174 | 41, 56 | readdcld 10069 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
175 | 174 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
176 | | ltletr 10129 |
. . . . . . . . 9
⊢
(((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) ∈ ℝ ∧ ((2↑𝑁) + (2↑𝑁)) ∈ ℝ ∧ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) → (((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁)) ∧ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
177 | 172, 173,
175, 176 | syl3anc 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁)) ∧ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
178 | 171, 177 | mpand 711 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
179 | 56 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
180 | 41 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
181 | 166, 179,
180 | ltadd2d 10193 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ↔ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
182 | 178, 181 | sylibrd 249 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
183 | 7, 56 | ltnled 10184 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ↔ ¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
184 | 63 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℂ) |
185 | 184 | addid2d 10237 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) |
186 | 7 | leidd 10594 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2↑𝑁) ≤ (2↑𝑁)) |
187 | 61 | nn0ge0d 11354 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (2↑𝑁)) |
188 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑁) =
if(𝑁 ∈ 𝐵, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))) |
189 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑁 ∈ 𝐵, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))) |
190 | 188, 189 | ifboth 4124 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ≤
(2↑𝑁) ∧ 0 ≤
(2↑𝑁)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)) |
191 | 186, 187,
190 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)) |
192 | 185, 191 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)) |
193 | 92 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ 𝐴 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
194 | 193 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ 𝐴 → ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
195 | 192, 194 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑁 ∈ 𝐴 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
196 | 195 | con1d 139 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁 ∈ 𝐴)) |
197 | 76 | nn0cnd 11353 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℂ) |
198 | 197 | addid1d 10236 |
. . . . . . . . . . . 12
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) = if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) |
199 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑁) =
if(𝑁 ∈ 𝐴, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))) |
200 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑁 ∈ 𝐴, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))) |
201 | 199, 200 | ifboth 4124 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ≤
(2↑𝑁) ∧ 0 ≤
(2↑𝑁)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)) |
202 | 186, 187,
201 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)) |
203 | 198, 202 | eqbrtrd 4675 |
. . . . . . . . . . 11
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁)) |
204 | 94 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ 𝐵 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0)) |
205 | 204 | breq1d 4663 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ 𝐵 → ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁))) |
206 | 203, 205 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑁 ∈ 𝐵 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
207 | 206 | con1d 139 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁 ∈ 𝐵)) |
208 | 196, 207 | jcad 555 |
. . . . . . . 8
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
209 | 183, 208 | sylbid 230 |
. . . . . . 7
⊢ (𝜑 → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
210 | 209 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
211 | 182, 210 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
212 | 162, 211 | impbid 202 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
213 | 152, 212 | bitrd 268 |
. . 3
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
214 | 150, 213 | pm2.61dan 832 |
. 2
⊢ (𝜑 → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
215 | | sadval.c |
. . 3
⊢ 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0
↦ if(cadd(𝑚 ∈
𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
216 | 10, 31, 215, 5 | sadcp1 15177 |
. 2
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) |
217 | | 2cnd 11093 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
218 | 217, 5 | expp1d 13009 |
. . . 4
⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) |
219 | 6 | nncnd 11036 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) |
220 | 219 | times2d 11276 |
. . . 4
⊢ (𝜑 → ((2↑𝑁) · 2) = ((2↑𝑁) + (2↑𝑁))) |
221 | 218, 220 | eqtrd 2656 |
. . 3
⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) + (2↑𝑁))) |
222 | 22 | bitsinvp1 15171 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |
223 | 10, 5, 222 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |
224 | 22 | bitsinvp1 15171 |
. . . . . 6
⊢ ((𝐵 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
225 | 31, 5, 224 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
226 | 223, 225 | oveq12d 6668 |
. . . 4
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
227 | 29 | nn0cnd 11353 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ) |
228 | 39 | nn0cnd 11353 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ) |
229 | 227, 197,
228, 184 | add4d 10264 |
. . . 4
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
230 | 226, 229 | eqtrd 2656 |
. . 3
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
231 | 221, 230 | breq12d 4666 |
. 2
⊢ (𝜑 → ((2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
232 | 214, 216,
231 | 3bitr4d 300 |
1
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))))) |