Metamath Proof Explorer

Theorem sadcaddlem

Description: Lemma for sadcadd . (Contributed by Mario Carneiro, 8-Sep-2016)

Ref Expression
Hypotheses sadval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
sadval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
sadval.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
sadcp1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sadcadd.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
sadcaddlem.1 ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) ↔ ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
Assertion sadcaddlem ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sadval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ0 )
2 sadval.b ⊢ ( 𝜑 → 𝐵 ⊆ ℕ0 )
3 sadval.c ⊢ 𝐶 = seq 0 ( ( 𝑐 ∈ 2o , 𝑚 ∈ ℕ0 ↦ if ( cadd ( 𝑚 ∈ 𝐴 , 𝑚 ∈ 𝐵 , ∅ ∈ 𝑐 ) , 1o , ∅ ) ) , ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ∅ , ( 𝑛 − 1 ) ) ) )
4 sadcp1.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5 sadcadd.k ⊢ 𝐾 = ◡ ( bits ↾ ℕ0 )
6 sadcaddlem.1 ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) ↔ ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ) )
7 cad1 ⊢ ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) )
9 2nn ⊢ 2 ∈ ℕ
10 9 a1i ⊢ ( 𝜑 → 2 ∈ ℕ )
11 10 4 nnexpcld ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ )
12 11 nnred ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℝ )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
14 inss1 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐴
15 14 1 sstrid ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
16 fzofi ⊢ ( 0 ..^ 𝑁 ) ∈ Fin
17 16 a1i ⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
18 inss2 ⊢ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
19 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
20 17 18 19 sylancl ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
21 elfpw ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
22 15 20 21 sylanbrc ⊢ ( 𝜑 → ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
23 bitsf1o ⊢ ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
24 f1ocnv ⊢ ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) → ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
25 23 24 ax-mp ⊢ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0
26 f1oeq1 ⊢ ( 𝐾 = ◡ ( bits ↾ ℕ0 ) → ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ↔ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ) )
27 5 26 ax-mp ⊢ ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 ↔ ◡ ( bits ↾ ℕ0 ) : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 )
28 25 27 mpbir ⊢ 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0
29 f1of ⊢ ( 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) –1-1-onto→ ℕ0 → 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0 )
30 28 29 ax-mp ⊢ 𝐾 : ( 𝒫 ℕ0 ∩ Fin ) ⟶ ℕ0
31 30 ffvelcdmi ⊢ ( ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
32 22 31 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
33 inss1 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ 𝐵
34 33 2 sstrid ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 )
35 inss2 ⊢ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 )
36 ssfi ⊢ ( ( ( 0 ..^ 𝑁 ) ∈ Fin ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ( 0 ..^ 𝑁 ) ) → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
37 17 35 36 sylancl ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin )
38 elfpw ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ⊆ ℕ0 ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ Fin ) )
39 34 37 38 sylanbrc ⊢ ( 𝜑 → ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) )
40 30 ffvelcdmi ⊢ ( ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
41 39 40 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℕ0 )
42 32 41 nn0addcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℕ0 )
43 42 nn0red ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
45 2nn0 ⊢ 2 ∈ ℕ0
46 45 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) → 2 ∈ ℕ0 )
47 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) → 𝑁 ∈ ℕ0 )
48 46 47 nn0expcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
49 0nn0 ⊢ 0 ∈ ℕ0
50 49 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ 𝐴 ) → 0 ∈ ℕ0 )
51 48 50 ifclda ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
52 45 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐵 ) → 2 ∈ ℕ0 )
53 4 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐵 ) → 𝑁 ∈ ℕ0 )
54 52 53 nn0expcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐵 ) → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
55 49 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ 𝐵 ) → 0 ∈ ℕ0 )
56 54 55 ifclda ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
57 51 56 nn0addcld ⊢ ( 𝜑 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℕ0 )
58 57 nn0red ⊢ ( 𝜑 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℝ )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℝ )
60 6 biimpa ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
62 11 nnnn0d ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℕ0 )
63 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
64 62 49 63 sylancl ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
65 64 nn0ge0d ⊢ ( 𝜑 → 0 ≤ if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) )
66 12 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐵 ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
67 0red ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ 𝐵 ) → 0 ∈ ℝ )
68 66 67 ifclda ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℝ )
69 12 68 addge01d ⊢ ( 𝜑 → ( 0 ≤ if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ↔ ( 2 ↑ 𝑁 ) ≤ ( ( 2 ↑ 𝑁 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
70 65 69 mpbid ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( ( 2 ↑ 𝑁 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
71 70 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐴 ) → ( 2 ↑ 𝑁 ) ≤ ( ( 2 ↑ 𝑁 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
72 iftrue ⊢ ( 𝑁 ∈ 𝐴 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) = ( 2 ↑ 𝑁 ) )
73 72 adantl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐴 ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) = ( 2 ↑ 𝑁 ) )
74 73 oveq1d ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐴 ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 2 ↑ 𝑁 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
75 71 74 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐴 ) → ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
76 ifcl ⊢ ( ( ( 2 ↑ 𝑁 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
77 62 49 76 sylancl ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℕ0 )
78 77 nn0ge0d ⊢ ( 𝜑 → 0 ≤ if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) )
79 12 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ 𝐴 ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
80 0red ⊢ ( ( 𝜑 ∧ ¬ 𝑁 ∈ 𝐴 ) → 0 ∈ ℝ )
81 79 80 ifclda ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℝ )
82 12 81 addge02d ⊢ ( 𝜑 → ( 0 ≤ if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ↔ ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + ( 2 ↑ 𝑁 ) ) ) )
83 78 82 mpbid ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + ( 2 ↑ 𝑁 ) ) )
84 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐵 ) → ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + ( 2 ↑ 𝑁 ) ) )
85 iftrue ⊢ ( 𝑁 ∈ 𝐵 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) = ( 2 ↑ 𝑁 ) )
86 85 adantl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐵 ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) = ( 2 ↑ 𝑁 ) )
87 86 oveq2d ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐵 ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + ( 2 ↑ 𝑁 ) ) )
88 84 87 breqtrrd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑁 ∈ 𝐵 ) → ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
89 75 88 jaodan ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( 2 ↑ 𝑁 ) ≤ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
90 13 13 44 59 61 89 le2addd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
91 90 ex ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
92 ioran ⊢ ( ¬ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ↔ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) )
93 iffalse ⊢ ( ¬ 𝑁 ∈ 𝐴 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) = 0 )
94 93 ad2antrl ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) = 0 )
95 iffalse ⊢ ( ¬ 𝑁 ∈ 𝐵 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) = 0 )
96 95 ad2antll ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) = 0 )
97 94 96 oveq12d ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( 0 + 0 ) )
98 00id ⊢ ( 0 + 0 ) = 0
99 97 98 eqtrdi ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = 0 )
100 99 oveq2d ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + 0 ) )
101 32 nn0red ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
102 101 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
103 41 nn0red ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
104 103 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
105 102 104 readdcld ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
106 105 recnd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℂ )
107 106 addridd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + 0 ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
108 100 107 eqtrd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
109 5 fveq1i ⊢ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) )
110 109 fveq2i ⊢ ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) )
111 32 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
112 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) )
113 23 22 112 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) )
114 110 111 113 3eqtr3a ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) )
115 114 18 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
116 32 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
117 bitsfzo ⊢ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
118 116 4 117 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
119 115 118 mpbird ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
120 elfzolt2 ⊢ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
121 119 120 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
122 5 fveq1i ⊢ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) = ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
123 122 fveq2i ⊢ ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) )
124 41 fvresd ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( bits ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
125 f1ocnvfv2 ⊢ ( ( ( bits ↾ ℕ0 ) : ℕ0 –1-1-onto→ ( 𝒫 ℕ0 ∩ Fin ) ∧ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ∈ ( 𝒫 ℕ0 ∩ Fin ) ) → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
126 23 39 125 sylancr ⊢ ( 𝜑 → ( ( bits ↾ ℕ0 ) ‘ ( ◡ ( bits ↾ ℕ0 ) ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
127 123 124 126 3eqtr3a ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) = ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) )
128 127 35 eqsstrdi ⊢ ( 𝜑 → ( bits ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) )
129 41 nn0zd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ )
130 bitsfzo ⊢ ( ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
131 129 4 130 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) ↔ ( bits ‘ ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ⊆ ( 0 ..^ 𝑁 ) ) )
132 128 131 mpbird ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) )
133 elfzolt2 ⊢ ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ( 0 ..^ ( 2 ↑ 𝑁 ) ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
134 132 133 syl ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) < ( 2 ↑ 𝑁 ) )
135 101 103 12 12 121 134 lt2addd ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
136 135 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
137 108 136 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
138 81 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℝ )
139 68 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℝ )
140 138 139 readdcld ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℝ )
141 105 140 readdcld ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ∈ ℝ )
142 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
143 142 142 readdcld ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ∈ ℝ )
144 141 143 ltnled ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ( ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) < ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ↔ ¬ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
145 137 144 mpbid ⊢ ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) ) → ¬ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
146 145 ex ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ¬ 𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ 𝐵 ) → ¬ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
147 92 146 biimtrid ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ¬ ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) → ¬ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
148 91 147 impcon4bid ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝑁 ∈ 𝐴 ∨ 𝑁 ∈ 𝐵 ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
149 8 148 bitrd ⊢ ( ( 𝜑 ∧ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
150 cad0 ⊢ ( ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
151 150 adantl ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
152 42 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) )
153 12 12 readdcld ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ∈ ℝ )
154 153 43 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ) ) )
155 152 154 mpbid ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ) )
156 155 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ) )
157 72 85 oveqan12d ⊢ ( ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
158 157 adantl ⊢ ( ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
159 158 oveq2d ⊢ ( ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ) )
160 156 159 breqtrrd ⊢ ( ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
161 160 ex ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
162 101 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
163 103 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℝ )
164 162 163 readdcld ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
165 12 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 2 ↑ 𝑁 ) ∈ ℝ )
166 12 43 lenltd ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ↔ ¬ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( 2 ↑ 𝑁 ) ) )
167 6 166 bitrd ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ 𝑁 ) ↔ ¬ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( 2 ↑ 𝑁 ) ) )
168 167 con2bid ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( 2 ↑ 𝑁 ) ↔ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) )
169 168 biimpar ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) < ( 2 ↑ 𝑁 ) )
170 164 165 165 169 ltadd1dd ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 2 ↑ 𝑁 ) ) < ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
171 164 165 readdcld ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 2 ↑ 𝑁 ) ) ∈ ℝ )
172 153 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ∈ ℝ )
173 43 58 readdcld ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ∈ ℝ )
174 173 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ∈ ℝ )
175 ltletr ⊢ ( ( ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 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 ) ) ) ) )
176 171 172 174 175 syl3anc ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 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 170 176 mpand ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 2 ↑ 𝑁 ) ) < ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
178 58 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ∈ ℝ )
179 43 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) ∈ ℝ )
180 165 178 179 ltadd2d ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 2 ↑ 𝑁 ) < ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ↔ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( 2 ↑ 𝑁 ) ) < ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
181 177 180 sylibrd ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) → ( 2 ↑ 𝑁 ) < ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
182 12 58 ltnled ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) < ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ↔ ¬ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ) )
183 64 nn0cnd ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
184 183 addlidd ⊢ ( 𝜑 → ( 0 + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) )
185 12 leidd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ≤ ( 2 ↑ 𝑁 ) )
186 62 nn0ge0d ⊢ ( 𝜑 → 0 ≤ ( 2 ↑ 𝑁 ) )
187 breq1 ⊢ ( ( 2 ↑ 𝑁 ) = if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) → ( ( 2 ↑ 𝑁 ) ≤ ( 2 ↑ 𝑁 ) ↔ if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) ) )
188 breq1 ⊢ ( 0 = if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) → ( 0 ≤ ( 2 ↑ 𝑁 ) ↔ if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) ) )
189 187 188 ifboth ⊢ ( ( ( 2 ↑ 𝑁 ) ≤ ( 2 ↑ 𝑁 ) ∧ 0 ≤ ( 2 ↑ 𝑁 ) ) → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) )
190 185 186 189 syl2anc ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) )
191 184 190 eqbrtrd ⊢ ( 𝜑 → ( 0 + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) )
192 93 oveq1d ⊢ ( ¬ 𝑁 ∈ 𝐴 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( 0 + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
193 192 breq1d ⊢ ( ¬ 𝑁 ∈ 𝐴 → ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ↔ ( 0 + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ) )
194 191 193 syl5ibrcom ⊢ ( 𝜑 → ( ¬ 𝑁 ∈ 𝐴 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ) )
195 194 con1d ⊢ ( 𝜑 → ( ¬ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) → 𝑁 ∈ 𝐴 ) )
196 77 nn0cnd ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ∈ ℂ )
197 196 addridd ⊢ ( 𝜑 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + 0 ) = if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) )
198 breq1 ⊢ ( ( 2 ↑ 𝑁 ) = if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) → ( ( 2 ↑ 𝑁 ) ≤ ( 2 ↑ 𝑁 ) ↔ if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) ) )
199 breq1 ⊢ ( 0 = if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) → ( 0 ≤ ( 2 ↑ 𝑁 ) ↔ if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) ) )
200 198 199 ifboth ⊢ ( ( ( 2 ↑ 𝑁 ) ≤ ( 2 ↑ 𝑁 ) ∧ 0 ≤ ( 2 ↑ 𝑁 ) ) → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) )
201 185 186 200 syl2anc ⊢ ( 𝜑 → if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ≤ ( 2 ↑ 𝑁 ) )
202 197 201 eqbrtrd ⊢ ( 𝜑 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + 0 ) ≤ ( 2 ↑ 𝑁 ) )
203 95 oveq2d ⊢ ( ¬ 𝑁 ∈ 𝐵 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) = ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + 0 ) )
204 203 breq1d ⊢ ( ¬ 𝑁 ∈ 𝐵 → ( ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ↔ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + 0 ) ≤ ( 2 ↑ 𝑁 ) ) )
205 202 204 syl5ibrcom ⊢ ( 𝜑 → ( ¬ 𝑁 ∈ 𝐵 → ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) ) )
206 205 con1d ⊢ ( 𝜑 → ( ¬ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) → 𝑁 ∈ 𝐵 ) )
207 195 206 jcad ⊢ ( 𝜑 → ( ¬ ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ≤ ( 2 ↑ 𝑁 ) → ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
208 182 207 sylbid ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) < ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) → ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
209 208 adantr ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 2 ↑ 𝑁 ) < ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) → ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
210 181 209 syld ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) → ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ) )
211 161 210 impbid ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( 𝑁 ∈ 𝐴 ∧ 𝑁 ∈ 𝐵 ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
212 151 211 bitrd ⊢ ( ( 𝜑 ∧ ¬ ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
213 149 212 pm2.61dan ⊢ ( 𝜑 → ( cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
214 1 2 3 4 sadcp1 ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ cadd ( 𝑁 ∈ 𝐴 , 𝑁 ∈ 𝐵 , ∅ ∈ ( 𝐶 ‘ 𝑁 ) ) ) )
215 2cnd ⊢ ( 𝜑 → 2 ∈ ℂ )
216 215 4 expp1d ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) · 2 ) )
217 11 nncnd ⊢ ( 𝜑 → ( 2 ↑ 𝑁 ) ∈ ℂ )
218 217 times2d ⊢ ( 𝜑 → ( ( 2 ↑ 𝑁 ) · 2 ) = ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
219 216 218 eqtrd ⊢ ( 𝜑 → ( 2 ↑ ( 𝑁 + 1 ) ) = ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) )
220 5 bitsinvp1 ⊢ ( ( 𝐴 ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )
221 1 4 220 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) )
222 5 bitsinvp1 ⊢ ( ( 𝐵 ⊆ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
223 2 4 222 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) = ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) )
224 221 223 oveq12d ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) + ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
225 32 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
226 41 nn0cnd ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ∈ ℂ )
227 225 196 226 183 add4d ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) ) + ( ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
228 224 227 eqtrd ⊢ ( 𝜑 → ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) = ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) )
229 219 228 breq12d ⊢ ( 𝜑 → ( ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) ↔ ( ( 2 ↑ 𝑁 ) + ( 2 ↑ 𝑁 ) ) ≤ ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ 𝑁 ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ 𝑁 ) ) ) ) + ( if ( 𝑁 ∈ 𝐴 , ( 2 ↑ 𝑁 ) , 0 ) + if ( 𝑁 ∈ 𝐵 , ( 2 ↑ 𝑁 ) , 0 ) ) ) ) )
230 213 214 229 3bitr4d ⊢ ( 𝜑 → ( ∅ ∈ ( 𝐶 ‘ ( 𝑁 + 1 ) ) ↔ ( 2 ↑ ( 𝑁 + 1 ) ) ≤ ( ( 𝐾 ‘ ( 𝐴 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) + ( 𝐾 ‘ ( 𝐵 ∩ ( 0 ..^ ( 𝑁 + 1 ) ) ) ) ) ) )