Proof of Theorem sadcaddlem
| Step | Hyp | Ref
| Expression |
| 1 | | cad1 1617 |
. . . . 5
⊢ (∅
∈ (𝐶‘𝑁) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
| 2 | 1 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵))) |
| 3 | | 2nn 12339 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
| 4 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℕ) |
| 5 | | sadcp1.n |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 6 | 4, 5 | nnexpcld 14284 |
. . . . . . . . 9
⊢ (𝜑 → (2↑𝑁) ∈ ℕ) |
| 7 | 6 | nnred 12281 |
. . . . . . . 8
⊢ (𝜑 → (2↑𝑁) ∈ ℝ) |
| 8 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ∈ ℝ) |
| 9 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 |
| 10 | | sadval.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ⊆
ℕ0) |
| 11 | 9, 10 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) |
| 12 | | fzofi 14015 |
. . . . . . . . . . . . . 14
⊢
(0..^𝑁) ∈
Fin |
| 13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0..^𝑁) ∈ Fin) |
| 14 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
| 15 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
| 16 | 13, 14, 15 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
| 17 | | elfpw 9394 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐴 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin)) |
| 18 | 11, 16, 17 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
| 19 | | bitsf1o 16482 |
. . . . . . . . . . . . . . 15
⊢ (bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩
Fin) |
| 20 | | f1ocnv 6860 |
. . . . . . . . . . . . . . 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 6836 |
. . . . . . . . . . . . . . 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 231 |
. . . . . . . . . . . . 13
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 |
| 26 | | f1of 6848 |
. . . . . . . . . . . . 13
⊢ (𝐾:(𝒫 ℕ0
∩ Fin)–1-1-onto→ℕ0 → 𝐾:(𝒫 ℕ0 ∩
Fin)⟶ℕ0) |
| 27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐾:(𝒫 ℕ0
∩ Fin)⟶ℕ0 |
| 28 | 27 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) |
| 29 | 18, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈
ℕ0) |
| 30 | | inss1 4237 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵 |
| 31 | | sadval.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆
ℕ0) |
| 32 | 30, 31 | sstrid 3995 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆
ℕ0) |
| 33 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
| 34 | | ssfi 9213 |
. . . . . . . . . . . . 13
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin) |
| 35 | 13, 33, 34 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin) |
| 36 | | elfpw 9394 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐵 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin)) |
| 37 | 32, 35, 36 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
| 38 | 27 | ffvelcdmi 7103 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈
ℕ0) |
| 40 | 29, 39 | nn0addcld 12591 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈
ℕ0) |
| 41 | 40 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
| 42 | 41 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
| 43 | | 2nn0 12543 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℕ0 |
| 44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → 2 ∈
ℕ0) |
| 45 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈
ℕ0) |
| 46 | 44, 45 | nn0expcld 14285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈
ℕ0) |
| 47 | | 0nn0 12541 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℕ0 |
| 48 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐴) → 0 ∈
ℕ0) |
| 49 | 46, 48 | ifclda 4561 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
| 50 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → 2 ∈
ℕ0) |
| 51 | 5 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → 𝑁 ∈
ℕ0) |
| 52 | 50, 51 | nn0expcld 14285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ∈
ℕ0) |
| 53 | 47 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐵) → 0 ∈
ℕ0) |
| 54 | 52, 53 | ifclda 4561 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
| 55 | 49, 54 | nn0addcld 12591 |
. . . . . . . . 9
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈
ℕ0) |
| 56 | 55 | nn0red 12588 |
. . . . . . . 8
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
| 57 | 56 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
| 58 | | sadcaddlem.1 |
. . . . . . . . 9
⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))) |
| 59 | 58 | biimpa 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 60 | 59 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 61 | 6 | nnnn0d 12587 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2↑𝑁) ∈
ℕ0) |
| 62 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
| 63 | 61, 47, 62 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈
ℕ0) |
| 64 | 63 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) |
| 65 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ∈ ℝ) |
| 66 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐵) → 0 ∈ ℝ) |
| 67 | 65, 66 | ifclda 4561 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℝ) |
| 68 | 7, 67 | addge01d 11851 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 69 | 64, 68 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 70 | 69 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 71 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝐴 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = (2↑𝑁)) |
| 72 | 71 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = (2↑𝑁)) |
| 73 | 72 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 74 | 70, 73 | breqtrrd 5171 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 75 | | ifcl 4571 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ∈
ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
| 76 | 61, 47, 75 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈
ℕ0) |
| 77 | 76 | nn0ge0d 12590 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) |
| 78 | 7 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℝ) |
| 79 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ¬ 𝑁 ∈ 𝐴) → 0 ∈ ℝ) |
| 80 | 78, 79 | ifclda 4561 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℝ) |
| 81 | 7, 80 | addge02d 11852 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 ≤ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁)))) |
| 82 | 77, 81 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
| 83 | 82 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
| 84 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ 𝐵 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = (2↑𝑁)) |
| 85 | 84 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = (2↑𝑁)) |
| 86 | 85 | oveq2d 7447 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + (2↑𝑁))) |
| 87 | 83, 86 | breqtrrd 5171 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ 𝑁 ∈ 𝐵) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 88 | 74, 87 | jaodan 960 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → (2↑𝑁) ≤ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 89 | 8, 8, 42, 57, 60, 88 | le2addd 11882 |
. . . . . 6
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 90 | 89 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 91 | | ioran 986 |
. . . . . 6
⊢ (¬
(𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) ↔ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) |
| 92 | | iffalse 4534 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑁 ∈ 𝐴 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = 0) |
| 93 | 92 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = 0) |
| 94 | | iffalse 4534 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑁 ∈ 𝐵 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = 0) |
| 95 | 94 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) = 0) |
| 96 | 93, 95 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (0 + 0)) |
| 97 | | 00id 11436 |
. . . . . . . . . . . 12
⊢ (0 + 0) =
0 |
| 98 | 96, 97 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = 0) |
| 99 | 98 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0)) |
| 100 | 29 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
| 101 | 100 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
| 102 | 39 | nn0red 12588 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
| 103 | 102 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
| 104 | 101, 103 | readdcld 11290 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
| 105 | 104 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℂ) |
| 106 | 105 | addridd 11461 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 107 | 99, 106 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 108 | 22 | fveq1i 6907 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘(𝐴 ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐴 ∩ (0..^𝑁))) |
| 109 | 108 | fveq2i 6909 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) |
| 110 | 29 | fvresd 6926 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁))))) |
| 111 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . 16
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐴 ∩ (0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin)) → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
| 112 | 19, 18, 111 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
| 113 | 109, 110,
112 | 3eqtr3a 2801 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁))) |
| 114 | 113, 14 | eqsstrdi 4028 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
| 115 | 29 | nn0zd 12639 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ) |
| 116 | | bitsfzo 16472 |
. . . . . . . . . . . . . 14
⊢ (((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
| 117 | 115, 5, 116 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
| 118 | 114, 117 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
| 119 | | elfzolt2 13708 |
. . . . . . . . . . . 12
⊢ ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁)) |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁)) |
| 121 | 22 | fveq1i 6907 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘(𝐵 ∩ (0..^𝑁))) = (◡(bits ↾
ℕ0)‘(𝐵 ∩ (0..^𝑁))) |
| 122 | 121 | fveq2i 6909 |
. . . . . . . . . . . . . . 15
⊢ ((bits
↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) |
| 123 | 39 | fvresd 6926 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 124 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . 16
⊢ (((bits
↾ ℕ0):ℕ0–1-1-onto→(𝒫 ℕ0 ∩ Fin)
∧ (𝐵 ∩ (0..^𝑁)) ∈ (𝒫
ℕ0 ∩ Fin)) → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
| 125 | 19, 37, 124 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((bits ↾
ℕ0)‘(◡(bits
↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
| 126 | 122, 123,
125 | 3eqtr3a 2801 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁))) |
| 127 | 126, 33 | eqsstrdi 4028 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)) |
| 128 | 39 | nn0zd 12639 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ) |
| 129 | | bitsfzo 16472 |
. . . . . . . . . . . . . 14
⊢ (((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
| 130 | 128, 5, 129 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))) |
| 131 | 127, 130 | mpbird 257 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁))) |
| 132 | | elfzolt2 13708 |
. . . . . . . . . . . 12
⊢ ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁)) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁)) |
| 134 | 100, 102,
7, 7, 120, 133 | lt2addd 11886 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁))) |
| 135 | 134 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁))) |
| 136 | 107, 135 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁))) |
| 137 | 80 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℝ) |
| 138 | 67 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℝ) |
| 139 | 137, 138 | readdcld 11290 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
| 140 | 104, 139 | readdcld 11290 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
| 141 | 7 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → (2↑𝑁) ∈ ℝ) |
| 142 | 141, 141 | readdcld 11290 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
| 143 | 140, 142 | ltnled 11408 |
. . . . . . . 8
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)) ↔ ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 144 | 136, 143 | mpbid 232 |
. . . . . . 7
⊢ (((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) ∧ (¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵)) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 145 | 144 | ex 412 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 146 | 91, 145 | biimtrid 242 |
. . . . 5
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (¬ (𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 147 | 90, 146 | impcon4bid 227 |
. . . 4
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 148 | 2, 147 | bitrd 279 |
. . 3
⊢ ((𝜑 ∧ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 149 | | cad0 1618 |
. . . . 5
⊢ (¬
∅ ∈ (𝐶‘𝑁) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 150 | 149 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 151 | 40 | nn0ge0d 12590 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))) |
| 152 | 7, 7 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
| 153 | 152, 41 | addge02d 11852 |
. . . . . . . . 9
⊢ (𝜑 → (0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))) |
| 154 | 151, 153 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
| 155 | 154 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
| 156 | 71, 84 | oveqan12d 7450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁))) |
| 157 | 156 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁))) |
| 158 | 157 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))) |
| 159 | 155, 158 | breqtrrd 5171 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) ∧ (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 160 | 159 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 161 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ) |
| 162 | 102 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ) |
| 163 | 161, 162 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
| 164 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (2↑𝑁) ∈ ℝ) |
| 165 | 7, 41 | lenltd 11407 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))) |
| 166 | 58, 165 | bitrd 279 |
. . . . . . . . . . 11
⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))) |
| 167 | 166 | con2bid 354 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁) ↔ ¬ ∅ ∈ (𝐶‘𝑁))) |
| 168 | 167 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)) |
| 169 | 163, 164,
164, 168 | ltadd1dd 11874 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁))) |
| 170 | 163, 164 | readdcld 11290 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) ∈ ℝ) |
| 171 | 152 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ) |
| 172 | 41, 56 | readdcld 11290 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
| 173 | 172 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) ∈ ℝ) |
| 174 | | ltletr 11353 |
. . . . . . . . 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))))) |
| 175 | 170, 171,
173, 174 | syl3anc 1373 |
. . . . . . . 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))))) |
| 176 | 169, 175 | mpand 695 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 177 | 56 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ∈ ℝ) |
| 178 | 41 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ) |
| 179 | 164, 177,
178 | ltadd2d 11417 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ↔ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 180 | 176, 179 | sylibrd 259 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 181 | 7, 56 | ltnled 11408 |
. . . . . . . 8
⊢ (𝜑 → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ↔ ¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
| 182 | 63 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ∈ ℂ) |
| 183 | 182 | addlidd 11462 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) |
| 184 | 7 | leidd 11829 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2↑𝑁) ≤ (2↑𝑁)) |
| 185 | 61 | nn0ge0d 12590 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (2↑𝑁)) |
| 186 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑁) =
if(𝑁 ∈ 𝐵, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))) |
| 187 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑁 ∈ 𝐵, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))) |
| 188 | 186, 187 | ifboth 4565 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ≤
(2↑𝑁) ∧ 0 ≤
(2↑𝑁)) → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)) |
| 189 | 184, 185,
188 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)) |
| 190 | 183, 189 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (𝜑 → (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)) |
| 191 | 92 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ 𝐴 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 192 | 191 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ 𝐴 → ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (0 + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
| 193 | 190, 192 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑁 ∈ 𝐴 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
| 194 | 193 | con1d 145 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁 ∈ 𝐴)) |
| 195 | 76 | nn0cnd 12589 |
. . . . . . . . . . . . 13
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ∈ ℂ) |
| 196 | 195 | addridd 11461 |
. . . . . . . . . . . 12
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) = if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) |
| 197 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢
((2↑𝑁) =
if(𝑁 ∈ 𝐴, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))) |
| 198 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (0 =
if(𝑁 ∈ 𝐴, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))) |
| 199 | 197, 198 | ifboth 4565 |
. . . . . . . . . . . . 13
⊢
(((2↑𝑁) ≤
(2↑𝑁) ∧ 0 ≤
(2↑𝑁)) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)) |
| 200 | 184, 185,
199 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)) |
| 201 | 196, 200 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (𝜑 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁)) |
| 202 | 94 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (¬
𝑁 ∈ 𝐵 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) = (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0)) |
| 203 | 202 | breq1d 5153 |
. . . . . . . . . . 11
⊢ (¬
𝑁 ∈ 𝐵 → ((if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁))) |
| 204 | 201, 203 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ (𝜑 → (¬ 𝑁 ∈ 𝐵 → (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))) |
| 205 | 204 | con1d 145 |
. . . . . . . . 9
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁 ∈ 𝐵)) |
| 206 | 194, 205 | jcad 512 |
. . . . . . . 8
⊢ (𝜑 → (¬ (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 207 | 181, 206 | sylbid 240 |
. . . . . . 7
⊢ (𝜑 → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 208 | 207 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((2↑𝑁) < (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 209 | 180, 208 | syld 47 |
. . . . 5
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) → (𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵))) |
| 210 | 160, 209 | impbid 212 |
. . . 4
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → ((𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 211 | 150, 210 | bitrd 279 |
. . 3
⊢ ((𝜑 ∧ ¬ ∅ ∈ (𝐶‘𝑁)) → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 212 | 148, 211 | pm2.61dan 813 |
. 2
⊢ (𝜑 → (cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 213 | | sadval.c |
. . 3
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦
if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, ∅,
(𝑛 −
1)))) |
| 214 | 10, 31, 213, 5 | sadcp1 16492 |
. 2
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁)))) |
| 215 | | 2cnd 12344 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
| 216 | 215, 5 | expp1d 14187 |
. . . 4
⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2)) |
| 217 | 6 | nncnd 12282 |
. . . . 5
⊢ (𝜑 → (2↑𝑁) ∈ ℂ) |
| 218 | 217 | times2d 12510 |
. . . 4
⊢ (𝜑 → ((2↑𝑁) · 2) = ((2↑𝑁) + (2↑𝑁))) |
| 219 | 216, 218 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) + (2↑𝑁))) |
| 220 | 22 | bitsinvp1 16486 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |
| 221 | 10, 5, 220 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |
| 222 | 22 | bitsinvp1 16486 |
. . . . . 6
⊢ ((𝐵 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 223 | 31, 5, 222 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) |
| 224 | 221, 223 | oveq12d 7449 |
. . . 4
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 225 | 29 | nn0cnd 12589 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ) |
| 226 | 39 | nn0cnd 12589 |
. . . . 5
⊢ (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ) |
| 227 | 225, 195,
226, 182 | add4d 11490 |
. . . 4
⊢ (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 228 | 224, 227 | eqtrd 2777 |
. . 3
⊢ (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0)))) |
| 229 | 219, 228 | breq12d 5156 |
. 2
⊢ (𝜑 → ((2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁 ∈ 𝐴, (2↑𝑁), 0) + if(𝑁 ∈ 𝐵, (2↑𝑁), 0))))) |
| 230 | 212, 214,
229 | 3bitr4d 311 |
1
⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))))) |