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 ) : ℕ01-1-onto→ ( 𝒫 ℕ0 ∩ Fin )
24 f1ocnv ( ( bits ↾ ℕ0 ) : ℕ01-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 ffvelrni ( ( 𝐴 ∩ ( 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 ffvelrni ( ( 𝐵 ∩ ( 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 addid1d ( ( ( 𝜑 ∧ ∅ ∈ ( 𝐶𝑁 ) ) ∧ ( ¬ 𝑁𝐴 ∧ ¬ 𝑁𝐵 ) ) → ( ( ( 𝐾 ‘ ( 𝐴 ∩ ( 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 ) : ℕ01-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 ) : ℕ01-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 syl5bi ( ( 𝜑 ∧ ∅ ∈ ( 𝐶𝑁 ) ) → ( ¬ ( 𝑁𝐴𝑁𝐵 ) → ¬ ( ( 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 addid2d ( 𝜑 → ( 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 addid1d ( 𝜑 → ( 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 ) ) ) ) ) ) )