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

Theorem sadcaddlem 15110
Description: Lemma for sadcadd 15111. (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 1552 . . . . 5 (∅ ∈ (𝐶𝑁) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
21adantl 482 . . . 4 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
3 2nn 11136 . . . . . . . . . . 11 2 ∈ ℕ
43a1i 11 . . . . . . . . . 10 (𝜑 → 2 ∈ ℕ)
5 sadcp1.n . . . . . . . . . 10 (𝜑𝑁 ∈ ℕ0)
64, 5nnexpcld 12977 . . . . . . . . 9 (𝜑 → (2↑𝑁) ∈ ℕ)
76nnred 10986 . . . . . . . 8 (𝜑 → (2↑𝑁) ∈ ℝ)
87ad2antrr 761 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ∈ ℝ)
9 inss1 3816 . . . . . . . . . . . . 13 (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴
10 sadval.a . . . . . . . . . . . . 13 (𝜑𝐴 ⊆ ℕ0)
119, 10syl5ss 3598 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∩ (0..^𝑁)) ⊆ ℕ0)
12 fzofi 12720 . . . . . . . . . . . . . 14 (0..^𝑁) ∈ Fin
1312a1i 11 . . . . . . . . . . . . 13 (𝜑 → (0..^𝑁) ∈ Fin)
14 inss2 3817 . . . . . . . . . . . . 13 (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
15 ssfi 8131 . . . . . . . . . . . . 13 (((0..^𝑁) ∈ Fin ∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
1613, 14, 15sylancl 693 . . . . . . . . . . . 12 (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ Fin)
17 elfpw 8219 . . . . . . . . . . . 12 ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((𝐴 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin))
1811, 16, 17sylanbrc 697 . . . . . . . . . . 11 (𝜑 → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
19 bitsf1o 15098 . . . . . . . . . . . . . . 15 (bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin)
20 f1ocnv 6111 . . . . . . . . . . . . . . 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 6089 . . . . . . . . . . . . . . 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 221 . . . . . . . . . . . . 13 𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0
26 f1of 6099 . . . . . . . . . . . . 13 (𝐾:(𝒫 ℕ0 ∩ Fin)–1-1-onto→ℕ0𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0)
2725, 26ax-mp 5 . . . . . . . . . . . 12 𝐾:(𝒫 ℕ0 ∩ Fin)⟶ℕ0
2827ffvelrni 6319 . . . . . . . . . . 11 ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0)
2918, 28syl 17 . . . . . . . . . 10 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0)
30 inss1 3816 . . . . . . . . . . . . 13 (𝐵 ∩ (0..^𝑁)) ⊆ 𝐵
31 sadval.b . . . . . . . . . . . . 13 (𝜑𝐵 ⊆ ℕ0)
3230, 31syl5ss 3598 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∩ (0..^𝑁)) ⊆ ℕ0)
33 inss2 3817 . . . . . . . . . . . . 13 (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)
34 ssfi 8131 . . . . . . . . . . . . 13 (((0..^𝑁) ∈ Fin ∧ (𝐵 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
3513, 33, 34sylancl 693 . . . . . . . . . . . 12 (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ Fin)
36 elfpw 8219 . . . . . . . . . . . 12 ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) ↔ ((𝐵 ∩ (0..^𝑁)) ⊆ ℕ0 ∧ (𝐵 ∩ (0..^𝑁)) ∈ Fin))
3732, 35, 36sylanbrc 697 . . . . . . . . . . 11 (𝜑 → (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin))
3827ffvelrni 6319 . . . . . . . . . . 11 ((𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0)
3937, 38syl 17 . . . . . . . . . 10 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0)
4029, 39nn0addcld 11306 . . . . . . . . 9 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℕ0)
4140nn0red 11303 . . . . . . . 8 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
4241ad2antrr 761 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
43 2nn0 11260 . . . . . . . . . . . . 13 2 ∈ ℕ0
4443a1i 11 . . . . . . . . . . . 12 ((𝜑𝑁𝐴) → 2 ∈ ℕ0)
455adantr 481 . . . . . . . . . . . 12 ((𝜑𝑁𝐴) → 𝑁 ∈ ℕ0)
4644, 45nn0expcld 12978 . . . . . . . . . . 11 ((𝜑𝑁𝐴) → (2↑𝑁) ∈ ℕ0)
47 0nn0 11258 . . . . . . . . . . . 12 0 ∈ ℕ0
4847a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝑁𝐴) → 0 ∈ ℕ0)
4946, 48ifclda 4097 . . . . . . . . . 10 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
5043a1i 11 . . . . . . . . . . . 12 ((𝜑𝑁𝐵) → 2 ∈ ℕ0)
515adantr 481 . . . . . . . . . . . 12 ((𝜑𝑁𝐵) → 𝑁 ∈ ℕ0)
5250, 51nn0expcld 12978 . . . . . . . . . . 11 ((𝜑𝑁𝐵) → (2↑𝑁) ∈ ℕ0)
5347a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝑁𝐵) → 0 ∈ ℕ0)
5452, 53ifclda 4097 . . . . . . . . . 10 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
5549, 54nn0addcld 11306 . . . . . . . . 9 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℕ0)
5655nn0red 11303 . . . . . . . 8 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
5756ad2antrr 761 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
58 sadcaddlem.1 . . . . . . . . 9 (𝜑 → (∅ ∈ (𝐶𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))
5958biimpa 501 . . . . . . . 8 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
6059adantr 481 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
616nnnn0d 11302 . . . . . . . . . . . . 13 (𝜑 → (2↑𝑁) ∈ ℕ0)
62 ifcl 4107 . . . . . . . . . . . . 13 (((2↑𝑁) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
6361, 47, 62sylancl 693 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℕ0)
6463nn0ge0d 11305 . . . . . . . . . . 11 (𝜑 → 0 ≤ if(𝑁𝐵, (2↑𝑁), 0))
657adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑁𝐵) → (2↑𝑁) ∈ ℝ)
66 0red 9992 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑁𝐵) → 0 ∈ ℝ)
6765, 66ifclda 4097 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℝ)
687, 67addge01d 10566 . . . . . . . . . . 11 (𝜑 → (0 ≤ if(𝑁𝐵, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0))))
6964, 68mpbid 222 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
7069ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (2↑𝑁) ≤ ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
71 iftrue 4069 . . . . . . . . . . 11 (𝑁𝐴 → if(𝑁𝐴, (2↑𝑁), 0) = (2↑𝑁))
7271adantl 482 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → if(𝑁𝐴, (2↑𝑁), 0) = (2↑𝑁))
7372oveq1d 6625 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + if(𝑁𝐵, (2↑𝑁), 0)))
7470, 73breqtrrd 4646 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐴) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
75 ifcl 4107 . . . . . . . . . . . . 13 (((2↑𝑁) ∈ ℕ0 ∧ 0 ∈ ℕ0) → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
7661, 47, 75sylancl 693 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℕ0)
7776nn0ge0d 11305 . . . . . . . . . . 11 (𝜑 → 0 ≤ if(𝑁𝐴, (2↑𝑁), 0))
787adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑁𝐴) → (2↑𝑁) ∈ ℝ)
79 0red 9992 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑁𝐴) → 0 ∈ ℝ)
8078, 79ifclda 4097 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℝ)
817, 80addge02d 10567 . . . . . . . . . . 11 (𝜑 → (0 ≤ if(𝑁𝐴, (2↑𝑁), 0) ↔ (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁))))
8277, 81mpbid 222 . . . . . . . . . 10 (𝜑 → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
8382ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
84 iftrue 4069 . . . . . . . . . . 11 (𝑁𝐵 → if(𝑁𝐵, (2↑𝑁), 0) = (2↑𝑁))
8584adantl 482 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → if(𝑁𝐵, (2↑𝑁), 0) = (2↑𝑁))
8685oveq2d 6626 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (if(𝑁𝐴, (2↑𝑁), 0) + (2↑𝑁)))
8783, 86breqtrrd 4646 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ 𝑁𝐵) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
8874, 87jaodan 825 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (2↑𝑁) ≤ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))
898, 8, 42, 57, 60, 88le2addd 10597 . . . . . 6 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
9089ex 450 . . . . 5 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
91 ioran 511 . . . . . 6 (¬ (𝑁𝐴𝑁𝐵) ↔ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵))
92 iffalse 4072 . . . . . . . . . . . . . 14 𝑁𝐴 → if(𝑁𝐴, (2↑𝑁), 0) = 0)
9392ad2antrl 763 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐴, (2↑𝑁), 0) = 0)
94 iffalse 4072 . . . . . . . . . . . . . 14 𝑁𝐵 → if(𝑁𝐵, (2↑𝑁), 0) = 0)
9594ad2antll 764 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐵, (2↑𝑁), 0) = 0)
9693, 95oveq12d 6628 . . . . . . . . . . . 12 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (0 + 0))
97 00id 10162 . . . . . . . . . . . 12 (0 + 0) = 0
9896, 97syl6eq 2671 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = 0)
9998oveq2d 6626 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0))
10029nn0red 11303 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
101100ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
10239nn0red 11303 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
103102ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
104101, 103readdcld 10020 . . . . . . . . . . . 12 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
105104recnd 10019 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℂ)
106105addid1d 10187 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + 0) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
10799, 106eqtrd 2655 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
10822fveq1i 6154 . . . . . . . . . . . . . . . 16 (𝐾‘(𝐴 ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))
109108fveq2i 6156 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁))))
110 fvres 6169 . . . . . . . . . . . . . . . 16 ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))))
11129, 110syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))))
112 f1ocnvfv2 6493 . . . . . . . . . . . . . . . 16 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
11319, 18, 112sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
114109, 111, 1133eqtr3a 2679 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) = (𝐴 ∩ (0..^𝑁)))
115114, 14syl6eqss 3639 . . . . . . . . . . . . 13 (𝜑 → (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
11629nn0zd 11431 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ)
117 bitsfzo 15088 . . . . . . . . . . . . . 14 (((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
118116, 5, 117syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐴 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
119115, 118mpbird 247 . . . . . . . . . . . 12 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
120 elfzolt2 12427 . . . . . . . . . . . 12 ((𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁))
121119, 120syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) < (2↑𝑁))
12222fveq1i 6154 . . . . . . . . . . . . . . . 16 (𝐾‘(𝐵 ∩ (0..^𝑁))) = ((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))
123122fveq2i 6156 . . . . . . . . . . . . . . 15 ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁))))
124 fvres 6169 . . . . . . . . . . . . . . . 16 ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℕ0 → ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))))
12539, 124syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))))
126 f1ocnvfv2 6493 . . . . . . . . . . . . . . . 16 (((bits ↾ ℕ0):ℕ01-1-onto→(𝒫 ℕ0 ∩ Fin) ∧ (𝐵 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0 ∩ Fin)) → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
12719, 37, 126sylancr 694 . . . . . . . . . . . . . . 15 (𝜑 → ((bits ↾ ℕ0)‘((bits ↾ ℕ0)‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
128123, 125, 1273eqtr3a 2679 . . . . . . . . . . . . . 14 (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) = (𝐵 ∩ (0..^𝑁)))
129128, 33syl6eqss 3639 . . . . . . . . . . . . 13 (𝜑 → (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁))
13039nn0zd 11431 . . . . . . . . . . . . . 14 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ)
131 bitsfzo 15088 . . . . . . . . . . . . . 14 (((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
132130, 5, 131syl2anc 692 . . . . . . . . . . . . 13 (𝜑 → ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) ↔ (bits‘(𝐾‘(𝐵 ∩ (0..^𝑁)))) ⊆ (0..^𝑁)))
133129, 132mpbird 247 . . . . . . . . . . . 12 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)))
134 elfzolt2 12427 . . . . . . . . . . . 12 ((𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ (0..^(2↑𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁))
135133, 134syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) < (2↑𝑁))
136100, 102, 7, 7, 121, 135lt2addd 10601 . . . . . . . . . 10 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁)))
137136ad2antrr 761 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < ((2↑𝑁) + (2↑𝑁)))
138107, 137eqbrtrd 4640 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)))
13980ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℝ)
14067ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℝ)
141139, 140readdcld 10020 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
142104, 141readdcld 10020 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
1437ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → (2↑𝑁) ∈ ℝ)
144143, 143readdcld 10020 . . . . . . . . 9 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
145142, 144ltnled 10135 . . . . . . . 8 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ((((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) < ((2↑𝑁) + (2↑𝑁)) ↔ ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
146138, 145mpbid 222 . . . . . . 7 (((𝜑 ∧ ∅ ∈ (𝐶𝑁)) ∧ (¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵)) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
147146ex 450 . . . . . 6 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
14891, 147syl5bi 232 . . . . 5 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (¬ (𝑁𝐴𝑁𝐵) → ¬ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
14990, 148impcon4bid 217 . . . 4 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
1502, 149bitrd 268 . . 3 ((𝜑 ∧ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
151 cad0 1553 . . . . 5 (¬ ∅ ∈ (𝐶𝑁) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
152151adantl 482 . . . 4 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ (𝑁𝐴𝑁𝐵)))
15340nn0ge0d 11305 . . . . . . . . 9 (𝜑 → 0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
1547, 7readdcld 10020 . . . . . . . . . 10 (𝜑 → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
155154, 41addge02d 10567 . . . . . . . . 9 (𝜑 → (0 ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁)))))
156153, 155mpbid 222 . . . . . . . 8 (𝜑 → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
157156ad2antrr 761 . . . . . . 7 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
15871, 84oveqan12d 6629 . . . . . . . . 9 ((𝑁𝐴𝑁𝐵) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁)))
159158adantl 482 . . . . . . . 8 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = ((2↑𝑁) + (2↑𝑁)))
160159oveq2d 6626 . . . . . . 7 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + ((2↑𝑁) + (2↑𝑁))))
161157, 160breqtrrd 4646 . . . . . 6 (((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) ∧ (𝑁𝐴𝑁𝐵)) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
162161ex 450 . . . . 5 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) → ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
163100adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℝ)
164102adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℝ)
165163, 164readdcld 10020 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
1667adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (2↑𝑁) ∈ ℝ)
1677, 41lenltd 10134 . . . . . . . . . . . 12 (𝜑 → ((2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)))
16858, 167bitrd 268 . . . . . . . . . . 11 (𝜑 → (∅ ∈ (𝐶𝑁) ↔ ¬ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁)))
169168con2bid 344 . . . . . . . . . 10 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁) ↔ ¬ ∅ ∈ (𝐶𝑁)))
170169biimpar 502 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) < (2↑𝑁))
171165, 166, 166, 170ltadd1dd 10589 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < ((2↑𝑁) + (2↑𝑁)))
172165, 166readdcld 10020 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) ∈ ℝ)
173154adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) + (2↑𝑁)) ∈ ℝ)
17441, 56readdcld 10020 . . . . . . . . . 10 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
175174adantr 481 . . . . . . . . 9 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) ∈ ℝ)
176 ltletr 10080 . . . . . . . . 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 1323 . . . . . . . 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 710 . . . . . . 7 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
17956adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ∈ ℝ)
18041adantr 481 . . . . . . . 8 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) ∈ ℝ)
181166, 179, 180ltadd2d 10144 . . . . . . 7 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ↔ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (2↑𝑁)) < (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
182178, 181sylibrd 249 . . . . . 6 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
1837, 56ltnled 10135 . . . . . . . 8 (𝜑 → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ↔ ¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
18463nn0cnd 11304 . . . . . . . . . . . . 13 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ∈ ℂ)
185184addid2d 10188 . . . . . . . . . . . 12 (𝜑 → (0 + if(𝑁𝐵, (2↑𝑁), 0)) = if(𝑁𝐵, (2↑𝑁), 0))
1867leidd 10545 . . . . . . . . . . . . 13 (𝜑 → (2↑𝑁) ≤ (2↑𝑁))
18761nn0ge0d 11305 . . . . . . . . . . . . 13 (𝜑 → 0 ≤ (2↑𝑁))
188 breq1 4621 . . . . . . . . . . . . . 14 ((2↑𝑁) = if(𝑁𝐵, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)))
189 breq1 4621 . . . . . . . . . . . . . 14 (0 = if(𝑁𝐵, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁)))
190188, 189ifboth 4101 . . . . . . . . . . . . 13 (((2↑𝑁) ≤ (2↑𝑁) ∧ 0 ≤ (2↑𝑁)) → if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))
191186, 187, 190syl2anc 692 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐵, (2↑𝑁), 0) ≤ (2↑𝑁))
192185, 191eqbrtrd 4640 . . . . . . . . . . 11 (𝜑 → (0 + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁))
19392oveq1d 6625 . . . . . . . . . . . 12 𝑁𝐴 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (0 + if(𝑁𝐵, (2↑𝑁), 0)))
194193breq1d 4628 . . . . . . . . . . 11 𝑁𝐴 → ((if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (0 + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
195192, 194syl5ibrcom 237 . . . . . . . . . 10 (𝜑 → (¬ 𝑁𝐴 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
196195con1d 139 . . . . . . . . 9 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁𝐴))
19776nn0cnd 11304 . . . . . . . . . . . . 13 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ∈ ℂ)
198197addid1d 10187 . . . . . . . . . . . 12 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + 0) = if(𝑁𝐴, (2↑𝑁), 0))
199 breq1 4621 . . . . . . . . . . . . . 14 ((2↑𝑁) = if(𝑁𝐴, (2↑𝑁), 0) → ((2↑𝑁) ≤ (2↑𝑁) ↔ if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)))
200 breq1 4621 . . . . . . . . . . . . . 14 (0 = if(𝑁𝐴, (2↑𝑁), 0) → (0 ≤ (2↑𝑁) ↔ if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁)))
201199, 200ifboth 4101 . . . . . . . . . . . . 13 (((2↑𝑁) ≤ (2↑𝑁) ∧ 0 ≤ (2↑𝑁)) → if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))
202186, 187, 201syl2anc 692 . . . . . . . . . . . 12 (𝜑 → if(𝑁𝐴, (2↑𝑁), 0) ≤ (2↑𝑁))
203198, 202eqbrtrd 4640 . . . . . . . . . . 11 (𝜑 → (if(𝑁𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁))
20494oveq2d 6626 . . . . . . . . . . . 12 𝑁𝐵 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) = (if(𝑁𝐴, (2↑𝑁), 0) + 0))
205204breq1d 4628 . . . . . . . . . . 11 𝑁𝐵 → ((if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) ↔ (if(𝑁𝐴, (2↑𝑁), 0) + 0) ≤ (2↑𝑁)))
206203, 205syl5ibrcom 237 . . . . . . . . . 10 (𝜑 → (¬ 𝑁𝐵 → (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁)))
207206con1d 139 . . . . . . . . 9 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → 𝑁𝐵))
208196, 207jcad 555 . . . . . . . 8 (𝜑 → (¬ (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) ≤ (2↑𝑁) → (𝑁𝐴𝑁𝐵)))
209183, 208sylbid 230 . . . . . . 7 (𝜑 → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) → (𝑁𝐴𝑁𝐵)))
210209adantr 481 . . . . . 6 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((2↑𝑁) < (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)) → (𝑁𝐴𝑁𝐵)))
211182, 210syld 47 . . . . 5 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))) → (𝑁𝐴𝑁𝐵)))
212162, 211impbid 202 . . . 4 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → ((𝑁𝐴𝑁𝐵) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
213152, 212bitrd 268 . . 3 ((𝜑 ∧ ¬ ∅ ∈ (𝐶𝑁)) → (cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁)) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
214150, 213pm2.61dan 831 . 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 15108 . 2 (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁𝐴, 𝑁𝐵, ∅ ∈ (𝐶𝑁))))
217 2cnd 11044 . . . . 5 (𝜑 → 2 ∈ ℂ)
218217, 5expp1d 12956 . . . 4 (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) · 2))
2196nncnd 10987 . . . . 5 (𝜑 → (2↑𝑁) ∈ ℂ)
220219times2d 11227 . . . 4 (𝜑 → ((2↑𝑁) · 2) = ((2↑𝑁) + (2↑𝑁)))
221218, 220eqtrd 2655 . . 3 (𝜑 → (2↑(𝑁 + 1)) = ((2↑𝑁) + (2↑𝑁)))
22222bitsinvp1 15102 . . . . . 6 ((𝐴 ⊆ ℕ0𝑁 ∈ ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)))
22310, 5, 222syl2anc 692 . . . . 5 (𝜑 → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)))
22422bitsinvp1 15102 . . . . . 6 ((𝐵 ⊆ ℕ0𝑁 ∈ ℕ0) → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0)))
22531, 5, 224syl2anc 692 . . . . 5 (𝜑 → (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0)))
226223, 225oveq12d 6628 . . . 4 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0))))
22729nn0cnd 11304 . . . . 5 (𝜑 → (𝐾‘(𝐴 ∩ (0..^𝑁))) ∈ ℂ)
22839nn0cnd 11304 . . . . 5 (𝜑 → (𝐾‘(𝐵 ∩ (0..^𝑁))) ∈ ℂ)
229227, 197, 228, 184add4d 10215 . . . 4 (𝜑 → (((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁𝐴, (2↑𝑁), 0)) + ((𝐾‘(𝐵 ∩ (0..^𝑁))) + if(𝑁𝐵, (2↑𝑁), 0))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
230226, 229eqtrd 2655 . . 3 (𝜑 → ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0))))
231221, 230breq12d 4631 . 2 (𝜑 → ((2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))) ↔ ((2↑𝑁) + (2↑𝑁)) ≤ (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) + (if(𝑁𝐴, (2↑𝑁), 0) + if(𝑁𝐵, (2↑𝑁), 0)))))
232214, 216, 2313bitr4d 300 1 (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  caddwcad 1542  wcel 1987  cin 3558  wss 3559  c0 3896  ifcif 4063  𝒫 cpw 4135   class class class wbr 4618  cmpt 4678  ccnv 5078  cres 5081  wf 5848  1-1-ontowf1o 5851  cfv 5852  (class class class)co 6610  cmpt2 6612  1𝑜c1o 7505  2𝑜c2o 7506  Fincfn 7906  cr 9886  0cc0 9887  1c1 9888   + caddc 9890   · cmul 9892   < clt 10025  cle 10026  cmin 10217  cn 10971  2c2 11021  0cn0 11243  cz 11328  ..^cfzo 12413  seqcseq 12748  cexp 12807  bitscbits 15072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-xor 1462  df-tru 1483  df-fal 1486  df-cad 1543  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-pm 7812  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-n0 11244  df-xnn0 11315  df-z 11329  df-uz 11639  df-rp 11784  df-fz 12276  df-fzo 12414  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-clim 14160  df-sum 14358  df-dvds 14915  df-bits 15075
This theorem is referenced by:  sadcadd  15111
  Copyright terms: Public domain W3C validator