MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sadcaddlem Structured version   Visualization version   GIF version

Theorem sadcaddlem 15401
Description: Lemma for sadcadd 15402. (Contributed by Mario Carneiro, 8-Sep-2016.)
Hypotheses
Ref Expression
sadval.a (𝜑𝐴 ⊆ ℕ0)
sadval.b (𝜑𝐵 ⊆ ℕ0)
sadval.c 𝐶 = seq0((𝑐 ∈ 2𝑜, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚𝐴, 𝑚𝐵, ∅ ∈ 𝑐), 1𝑜, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))
sadcp1.n (𝜑𝑁 ∈ ℕ0)
sadcadd.k 𝐾 = (bits ↾ ℕ0)
sadcaddlem.1 (𝜑 → (∅ ∈ (𝐶𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))
Assertion
Ref Expression
sadcaddlem (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))))))
Distinct variable groups:   𝑚,𝑐,𝑛   𝐴,𝑐,𝑚   𝐵,𝑐,𝑚   𝑛,𝑁
Allowed substitution hints:   𝜑(𝑚,𝑛,𝑐)   𝐴(𝑛)   𝐵(𝑛)   𝐶(𝑚,𝑛,𝑐)   𝐾(𝑚,𝑛,𝑐)   𝑁(𝑚,𝑐)

Proof of Theorem sadcaddlem
StepHypRef Expression
1 cad1 1710 . . . . 5 (∅ ∈ (𝐶𝑁) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
21adantl 469 . . . 4 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
3 2nn 11465 . . . . . . . . . . 11 2 ∈ ℕ
43a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℕ)
5 sadcp1.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
64, 5nnexpcld 13256 . . . . . . . . 9 (𝜑 → (2↑𝑁) ∈ ℕ)
76nnred 11323 . . . . . . . 8 (𝜑 → (2↑𝑁) ∈ ℝ)
87ad2antrr 708 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ∈ ℝ)
9 inss1 4036 . . . . . . . . . . . . 13 (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴
10 sadval.a . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℕ0)
119, 10syl5ss 3816 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆ ℕ0)
12 fzofi 13000 . . . . . . . . . . . . . 14 (0..^𝑁) ∈ Fin
1312a1i 11 . . . . . . . . . . . . 13 (𝜑 → (0..^𝑁) ∈ Fin)
14 inss2 4037 . . . . . . . . . . . . 13 (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
15 ssfi 8422 . . . . . . . . . . . . 13 (((0..^𝑁) ∈ Fin ∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
1613, 14, 15sylancl 576 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
17 elfpw 8510 . . . . . . . . . . . 12 ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((𝐴 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin))
1811, 16, 17sylanbrc 574 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
19 bitsf1o 15389 . . . . . . . . . . . . . . 15 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
20 f1ocnv 6368 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) → (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
2119, 20ax-mp 5 . . . . . . . . . . . . . 14 (bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0
22 sadcadd.k . . . . . . . . . . . . . . 15 𝐾 = (bits ↾ ℕ0)
23 f1oeq1 6346 . . . . . . . . . . . . . . 15 (𝐾 = (bits ↾ ℕ0) → (𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0))
2422, 23ax-mp 5 . . . . . . . . . . . . . 14 (𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0(bits ↾ ℕ0):(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0)
2521, 24mpbir 222 . . . . . . . . . . . . 13 𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0
26 f1of 6356 . . . . . . . . . . . . 13 (𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
2725, 26ax-mp 5 . . . . . . . . . . . 12 𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0
2827ffvelrni 6583 . . . . . . . . . . 11 ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0)
2918, 28syl 17 . . . . . . . . . 10 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0)
30 inss1 4036 . . . . . . . . . . . . 13 (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵
31 sadval.b . . . . . . . . . . . . 13 (𝜑𝐵 ⊆ ℕ0)
3230, 31syl5ss 3816 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆ ℕ0)
33 inss2 4037 . . . . . . . . . . . . 13 (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
34 ssfi 8422 . . . . . . . . . . . . 13 (((0..^𝑁) ∈ Fin ∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
3513, 33, 34sylancl 576 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
36 elfpw 8510 . . . . . . . . . . . 12 ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((𝐵 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin))
3732, 35, 36sylanbrc 574 . . . . . . . . . . 11 (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
3827ffvelrni 6583 . . . . . . . . . . 11 ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0)
3937, 38syl 17 . . . . . . . . . 10 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0)
4029, 39nn0addcld 11624 . . . . . . . . 9 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℕ0)
4140nn0red 11621 . . . . . . . 8 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
4241ad2antrr 708 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
43 2nn0 11579 . . . . . . . . . . . . 13 2 ∈ ℕ0
4443a1i 11 . . . . . . . . . . . 12 ((𝜑𝑁𝐴) → 2 ∈ ℕ0)
455adantr 468 . . . . . . . . . . . 12 ((𝜑𝑁𝐴) → 𝑁 ∈ ℕ0)
4644, 45nn0expcld 13257 . . . . . . . . . . 11 ((𝜑𝑁𝐴) → (2↑𝑁) ∈ ℕ0)
47 0nn0 11577 . . . . . . . . . . . 12 0 ∈ ℕ0
4847a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝑁𝐴) → 0 ∈ ℕ0)
4946, 48ifclda 4320 . . . . . . . . . 10 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
5043a1i 11 . . . . . . . . . . . 12 ((𝜑𝑁𝐵) → 2 ∈ ℕ0)
515adantr 468 . . . . . . . . . . . 12 ((𝜑𝑁𝐵) → 𝑁 ∈ ℕ0)
5250, 51nn0expcld 13257 . . . . . . . . . . 11 ((𝜑𝑁𝐵) → (2↑𝑁) ∈ ℕ0)
5347a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝑁𝐵) → 0 ∈ ℕ0)
5452, 53ifclda 4320 . . . . . . . . . 10 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
5549, 54nn0addcld 11624 . . . . . . . . 9 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℕ0)
5655nn0red 11621 . . . . . . . 8 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
5756ad2antrr 708 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
58 sadcaddlem.1 . . . . . . . . 9 (𝜑 → (∅ ∈ (𝐶𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))
5958biimpa 464 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
6059adantr 468 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
616nnnn0d 11620 . . . . . . . . . . . . 13 (𝜑 → (2↑𝑁) ∈ ℕ0)
62 ifcl 4330 . . . . . . . . . . . . 13 (((2↑𝑁) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
6361, 47, 62sylancl 576 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
6463nn0ge0d 11623 . . . . . . . . . . 11 (𝜑 → 0 ≤ if(𝑁𝐵, (2↑𝑁), 0))
657adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑁𝐵) → (2↑𝑁) ∈ ℝ)
66 0red 10331 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑁𝐵) → 0 ∈ ℝ)
6765, 66ifclda 4320 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℝ)
687, 67addge01d 10903 . . . . . . . . . . 11 (𝜑 → (0 ≤ if(𝑁𝐵, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0))))
6964, 68mpbid 223 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
7069ad2antrr 708 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
71 iftrue 4292 . . . . . . . . . . 11 (𝑁𝐴 → if(𝑁𝐴, (2↑𝑁), 0) = (2↑𝑁))
7271adantl 469 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → if(𝑁𝐴, (2↑𝑁), 0) = (2↑𝑁))
7372oveq1d 6892 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
7470, 73breqtrrd 4879 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
75 ifcl 4330 . . . . . . . . . . . . 13 (((2↑𝑁) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
7661, 47, 75sylancl 576 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
7776nn0ge0d 11623 . . . . . . . . . . 11 (𝜑 → 0 ≤ if(𝑁𝐴, (2↑𝑁), 0))
787adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑁𝐴) → (2↑𝑁) ∈ ℝ)
79 0red 10331 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑁𝐴) → 0 ∈ ℝ)
8078, 79ifclda 4320 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℝ)
817, 80addge02d 10904 . . . . . . . . . . 11 (𝜑 → (0 ≤ if(𝑁𝐴, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁))))
8277, 81mpbid 223 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
8382ad2antrr 708 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
84 iftrue 4292 . . . . . . . . . . 11 (𝑁𝐵 → if(𝑁𝐵, (2↑𝑁), 0) = (2↑𝑁))
8584adantl 469 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → if(𝑁𝐵, (2↑𝑁), 0) = (2↑𝑁))
8685oveq2d 6893 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
8783, 86breqtrrd 4879 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
8874, 87jaodan 971 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
898, 8, 42, 57, 60, 88le2addd 10934 . . . . . 6 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
9089ex 399 . . . . 5 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
91 ioran 997 . . . . . 6 (¬ (𝑁𝐴𝑁𝐵) ↔ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵))
92 iffalse 4295 . . . . . . . . . . . . . 14 𝑁𝐴 → if(𝑁𝐴, (2↑𝑁), 0) = 0)
9392ad2antrl 710 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐴, (2↑𝑁), 0) = 0)
94 iffalse 4295 . . . . . . . . . . . . . 14 𝑁𝐵 → if(𝑁𝐵, (2↑𝑁), 0) = 0)
9594ad2antll 711 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐵, (2↑𝑁), 0) = 0)
9693, 95oveq12d 6895 . . . . . . . . . . . 12 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (0 + 0))
97 00id 10499 . . . . . . . . . . . 12 (0 + 0) = 0
9896, 97syl6eq 2863 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = 0)
9998oveq2d 6893 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0))
10029nn0red 11621 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
101100ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
10239nn0red 11621 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
103102ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
104101, 103readdcld 10357 . . . . . . . . . . . 12 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
105104recnd 10356 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℂ)
106105addid1d 10524 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
10799, 106eqtrd 2847 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
10822fveq1i 6412 . . . . . . . . . . . . . . . 16 (𝐾‘(𝐴 ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))
109108fveq2i 6414 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁))))
110 fvres 6430 . . . . . . . . . . . . . . . 16 ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))))
11129, 110syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))))
112 f1ocnvfv2 6760 . . . . . . . . . . . . . . . 16 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
11319, 18, 112sylancr 577 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
114109, 111, 1133eqtr3a 2871 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
115114, 14syl6eqss 3859 . . . . . . . . . . . . 13 (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
11629nn0zd 11749 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ)
117 bitsfzo 15379 . . . . . . . . . . . . . 14 (((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
118116, 5, 117syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
119115, 118mpbird 248 . . . . . . . . . . . 12 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
120 elfzolt2 12706 . . . . . . . . . . . 12 ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁))
121119, 120syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁))
12222fveq1i 6412 . . . . . . . . . . . . . . . 16 (𝐾‘(𝐵 ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))
123122fveq2i 6414 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁))))
124 fvres 6430 . . . . . . . . . . . . . . . 16 ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))))
12539, 124syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))))
126 f1ocnvfv2 6760 . . . . . . . . . . . . . . . 16 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
12719, 37, 126sylancr 577 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
128123, 125, 1273eqtr3a 2871 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
129128, 33syl6eqss 3859 . . . . . . . . . . . . 13 (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
13039nn0zd 11749 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ)
131 bitsfzo 15379 . . . . . . . . . . . . . 14 (((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
132130, 5, 131syl2anc 575 . . . . . . . . . . . . 13 (𝜑 → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
133129, 132mpbird 248 . . . . . . . . . . . 12 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
134 elfzolt2 12706 . . . . . . . . . . . 12 ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁))
135133, 134syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁))
136100, 102, 7, 7, 121, 135lt2addd 10938 . . . . . . . . . 10 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁)))
137136ad2antrr 708 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁)))
138107, 137eqbrtrd 4873 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)))
13980ad2antrr 708 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℝ)
14067ad2antrr 708 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℝ)
141139, 140readdcld 10357 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
142104, 141readdcld 10357 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
1437ad2antrr 708 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (2↑𝑁) ∈ ℝ)
144143, 143readdcld 10357 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
145142, 144ltnled 10472 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)) ↔ ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
146138, 145mpbid 223 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
147146ex 399 . . . . . 6 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
14891, 147syl5bi 233 . . . . 5 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (¬ (𝑁𝐴𝑁𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
14990, 148impcon4bid 218 . . . 4 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
1502, 149bitrd 270 . . 3 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
151 cad0 1711 . . . . 5 (¬ ∅ ∈ (𝐶𝑁) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
152151adantl 469 . . . 4 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
15340nn0ge0d 11623 . . . . . . . . 9 (𝜑 → 0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
1547, 7readdcld 10357 . . . . . . . . . 10 (𝜑 → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
155154, 41addge02d 10904 . . . . . . . . 9 (𝜑 → (0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))))
156153, 155mpbid 223 . . . . . . . 8 (𝜑 → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
157156ad2antrr 708 . . . . . . 7 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
15871, 84oveqan12d 6896 . . . . . . . . 9 ((𝑁𝐴𝑁𝐵) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁)))
159158adantl 469 . . . . . . . 8 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁)))
160159oveq2d 6893 . . . . . . 7 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
161157, 160breqtrrd 4879 . . . . . 6 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
162161ex 399 . . . . 5 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
163100adantr 468 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
164102adantr 468 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
165163, 164readdcld 10357 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
1667adantr 468 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (2↑𝑁) ∈ ℝ)
1677, 41lenltd 10471 . . . . . . . . . . . 12 (𝜑 → ((2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)))
16858, 167bitrd 270 . . . . . . . . . . 11 (𝜑 → (∅ ∈ (𝐶𝑁) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)))
169168con2bid 345 . . . . . . . . . 10 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁) ↔ ¬ ∅ ∈ (𝐶𝑁)))
170169biimpar 465 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))
171165, 166, 166, 170ltadd1dd 10926 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁)))
172165, 166readdcld 10357 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) ∈ ℝ)
173154adantr 468 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
17441, 56readdcld 10357 . . . . . . . . . 10 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
175174adantr 468 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
176 ltletr 10417 . . . . . . . . 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)))))
177172, 173, 175, 176syl3anc 1483 . . . . . . . 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)))))
178171, 177mpand 678 . . . . . . 7 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
17956adantr 468 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
18041adantr 468 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
181166, 179, 180ltadd2d 10481 . . . . . . 7 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ↔ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
182178, 181sylibrd 250 . . . . . 6 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
1837, 56ltnled 10472 . . . . . . . 8 (𝜑 → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ↔ ¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
18463nn0cnd 11622 . . . . . . . . . . . . 13 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℂ)
185184addid2d 10525 . . . . . . . . . . . 12 (𝜑 → (0 + if(𝑁𝐵, (2↑𝑁), 0)) = if(𝑁𝐵, (2↑𝑁), 0))
1867leidd 10882 . . . . . . . . . . . . 13 (𝜑 → (2↑𝑁) ≤ (2↑𝑁))
18761nn0ge0d 11623 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (2↑𝑁))
188 breq1 4854 . . . . . . . . . . . . . 14 ((2↑𝑁) = if(𝑁𝐵, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)))
189 breq1 4854 . . . . . . . . . . . . . 14 (0 = if(𝑁𝐵, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)))
190188, 189ifboth 4324 . . . . . . . . . . . . 13 (((2↑𝑁) ≤ (2↑𝑁) ∧ 0 ≤ (2↑𝑁)) → if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))
191186, 187, 190syl2anc 575 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))
192185, 191eqbrtrd 4873 . . . . . . . . . . 11 (𝜑 → (0 + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))
19392oveq1d 6892 . . . . . . . . . . . 12 𝑁𝐴 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (0 + if(𝑁𝐵, (2↑𝑁), 0)))
194193breq1d 4861 . . . . . . . . . . 11 𝑁𝐴 → ((if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (0 + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
195192, 194syl5ibrcom 238 . . . . . . . . . 10 (𝜑 → (¬ 𝑁𝐴 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
196195con1d 141 . . . . . . . . 9 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁𝐴))
19776nn0cnd 11622 . . . . . . . . . . . . 13 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℂ)
198197addid1d 10524 . . . . . . . . . . . 12 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + 0) = if(𝑁𝐴, (2↑𝑁), 0))
199 breq1 4854 . . . . . . . . . . . . . 14 ((2↑𝑁) = if(𝑁𝐴, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)))
200 breq1 4854 . . . . . . . . . . . . . 14 (0 = if(𝑁𝐴, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)))
201199, 200ifboth 4324 . . . . . . . . . . . . 13 (((2↑𝑁) ≤ (2↑𝑁) ∧ 0 ≤ (2↑𝑁)) → if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))
202186, 187, 201syl2anc 575 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))
203198, 202eqbrtrd 4873 . . . . . . . . . . 11 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁))
20494oveq2d 6893 . . . . . . . . . . . 12 𝑁𝐵 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (if(𝑁𝐴, (2↑𝑁), 0) + 0))
205204breq1d 4861 . . . . . . . . . . 11 𝑁𝐵 → ((if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (if(𝑁𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁)))
206203, 205syl5ibrcom 238 . . . . . . . . . 10 (𝜑 → (¬ 𝑁𝐵 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
207206con1d 141 . . . . . . . . 9 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁𝐵))
208196, 207jcad 504 . . . . . . . 8 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → (𝑁𝐴𝑁𝐵)))
209183, 208sylbid 231 . . . . . . 7 (𝜑 → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) → (𝑁𝐴𝑁𝐵)))
210209adantr 468 . . . . . 6 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) → (𝑁𝐴𝑁𝐵)))
211182, 210syld 47 . . . . 5 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (𝑁𝐴𝑁𝐵)))
212162, 211impbid 203 . . . 4 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
213152, 212bitrd 270 . . 3 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
214150, 213pm2.61dan 838 . 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))))
21610, 31, 215, 5sadcp1 15399 . 2 (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
217 2cnd 11380 . . . . 5 (𝜑 → 2 ∈ ℂ)
218217, 5expp1d 13235 . . . 4 (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
2196nncnd 11324 . . . . 5 (𝜑 → (2↑𝑁) ∈ ℂ)
220219times2d 11546 . . . 4 (𝜑 → ((2↑𝑁) · 2) = ((2↑𝑁) + (2↑𝑁)))
221218, 220eqtrd 2847 . . 3 (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) + (2↑𝑁)))
22222bitsinvp1 15393 . . . . . 6 ((𝐴 ⊆ ℕ0𝑁 ∈ ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)))
22310, 5, 222syl2anc 575 . . . . 5 (𝜑 → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)))
22422bitsinvp1 15393 . . . . . 6 ((𝐵 ⊆ ℕ0𝑁 ∈ ℕ0) → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0)))
22531, 5, 224syl2anc 575 . . . . 5 (𝜑 → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0)))
226223, 225oveq12d 6895 . . . 4 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0))))
22729nn0cnd 11622 . . . . 5 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ)
22839nn0cnd 11622 . . . . 5 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ)
229227, 197, 228, 184add4d 10552 . . . 4 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
230226, 229eqtrd 2847 . . 3 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
231221, 230breq12d 4864 . 2 (𝜑 → ((2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
232214, 216, 2313bitr4d 302 1 (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  caddwcad 1700  wcel 2157  cin 3775  wss 3776  c0 4123  ifcif 4286  𝒫 cpw 4358   class class class wbr 4851  cmpt 4930  ccnv 5317  cres 5320  wf 6100  1-1-ontowf1o 6103  cfv 6104  (class class class)co 6877  cmpt2 6879  1𝑜c1o 7792  2𝑜c2o 7793  Fincfn 8195  cr 10223  0cc0 10224  1c1 10225   + caddc 10227   · cmul 10229   < clt 10362  cle 10363  cmin 10554  cn 11308  2c2 11359  0cn0 11562  cz 11646  ..^cfzo 12692  seqcseq 13027  cexp 13086  bitscbits 15363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788  ax-cnex 10280  ax-resscn 10281  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-mulcom 10288  ax-addass 10289  ax-mulass 10290  ax-distr 10291  ax-i2m1 10292  ax-1ne0 10293  ax-1rid 10294  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297  ax-pre-lttri 10298  ax-pre-lttrn 10299  ax-pre-ltadd 10300  ax-pre-mulgt0 10301  ax-pre-sup 10302
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-xor 1619  df-tru 1641  df-fal 1651  df-cad 1701  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-disj 4820  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-map 8097  df-pm 8098  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-sup 8590  df-inf 8591  df-oi 8657  df-card 9051  df-cda 9278  df-pnf 10364  df-mnf 10365  df-xr 10366  df-ltxr 10367  df-le 10368  df-sub 10556  df-neg 10557  df-div 10973  df-nn 11309  df-2 11367  df-3 11368  df-n0 11563  df-xnn0 11633  df-z 11647  df-uz 11908  df-rp 12050  df-fz 12553  df-fzo 12693  df-fl 12820  df-mod 12896  df-seq 13028  df-exp 13087  df-hash 13341  df-cj 14065  df-re 14066  df-im 14067  df-sqrt 14201  df-abs 14202  df-clim 14445  df-sum 14643  df-dvds 15207  df-bits 15366
This theorem is referenced by:  sadcadd  15402
  Copyright terms: Public domain W3C validator