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
|
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 ) : ℕ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
|
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 ) ) ) ) ) ) ) |