Step |
Hyp |
Ref |
Expression |
1 |
|
2nn |
⊢ 2 ∈ ℕ |
2 |
|
1ne2 |
⊢ 1 ≠ 2 |
3 |
|
1ex |
⊢ 1 ∈ V |
4 |
|
2ex |
⊢ 2 ∈ V |
5 |
3 4 4 4
|
fpr |
⊢ ( 1 ≠ 2 → { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ { 2 , 2 } ) |
6 |
|
2prm |
⊢ 2 ∈ ℙ |
7 |
6 6
|
pm3.2i |
⊢ ( 2 ∈ ℙ ∧ 2 ∈ ℙ ) |
8 |
4 4
|
prss |
⊢ ( ( 2 ∈ ℙ ∧ 2 ∈ ℙ ) ↔ { 2 , 2 } ⊆ ℙ ) |
9 |
7 8
|
mpbi |
⊢ { 2 , 2 } ⊆ ℙ |
10 |
|
fss |
⊢ ( ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ { 2 , 2 } ∧ { 2 , 2 } ⊆ ℙ ) → { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ ℙ ) |
11 |
9 10
|
mpan2 |
⊢ ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ { 2 , 2 } → { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ ℙ ) |
12 |
2 5 11
|
mp2b |
⊢ { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ ℙ |
13 |
|
prmex |
⊢ ℙ ∈ V |
14 |
|
prex |
⊢ { 1 , 2 } ∈ V |
15 |
13 14
|
elmap |
⊢ ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ∈ ( ℙ ↑m { 1 , 2 } ) ↔ { 〈 1 , 2 〉 , 〈 2 , 2 〉 } : { 1 , 2 } ⟶ ℙ ) |
16 |
12 15
|
mpbir |
⊢ { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ∈ ( ℙ ↑m { 1 , 2 } ) |
17 |
|
2re |
⊢ 2 ∈ ℝ |
18 |
|
3re |
⊢ 3 ∈ ℝ |
19 |
|
2lt3 |
⊢ 2 < 3 |
20 |
17 18 19
|
ltleii |
⊢ 2 ≤ 3 |
21 |
|
2cn |
⊢ 2 ∈ ℂ |
22 |
|
fveq2 |
⊢ ( 𝑘 = 1 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 1 ) ) |
23 |
3 4
|
fvpr1 |
⊢ ( 1 ≠ 2 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 1 ) = 2 ) |
24 |
2 23
|
ax-mp |
⊢ ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 1 ) = 2 |
25 |
22 24
|
eqtrdi |
⊢ ( 𝑘 = 1 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = 2 ) |
26 |
|
fveq2 |
⊢ ( 𝑘 = 2 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 2 ) ) |
27 |
4 4
|
fvpr2 |
⊢ ( 1 ≠ 2 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 2 ) = 2 ) |
28 |
2 27
|
ax-mp |
⊢ ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 2 ) = 2 |
29 |
26 28
|
eqtrdi |
⊢ ( 𝑘 = 2 → ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = 2 ) |
30 |
|
id |
⊢ ( 2 ∈ ℂ → 2 ∈ ℂ ) |
31 |
30
|
ancri |
⊢ ( 2 ∈ ℂ → ( 2 ∈ ℂ ∧ 2 ∈ ℂ ) ) |
32 |
3
|
jctl |
⊢ ( 2 ∈ ℂ → ( 1 ∈ V ∧ 2 ∈ ℂ ) ) |
33 |
2
|
a1i |
⊢ ( 2 ∈ ℂ → 1 ≠ 2 ) |
34 |
25 29 31 32 33
|
sumpr |
⊢ ( 2 ∈ ℂ → Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = ( 2 + 2 ) ) |
35 |
21 34
|
ax-mp |
⊢ Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) = ( 2 + 2 ) |
36 |
|
2p2e4 |
⊢ ( 2 + 2 ) = 4 |
37 |
35 36
|
eqtr2i |
⊢ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) |
38 |
20 37
|
pm3.2i |
⊢ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) |
39 |
|
fveq1 |
⊢ ( 𝑓 = { 〈 1 , 2 〉 , 〈 2 , 2 〉 } → ( 𝑓 ‘ 𝑘 ) = ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) |
40 |
39
|
sumeq2sdv |
⊢ ( 𝑓 = { 〈 1 , 2 〉 , 〈 2 , 2 〉 } → Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) |
41 |
40
|
eqeq2d |
⊢ ( 𝑓 = { 〈 1 , 2 〉 , 〈 2 , 2 〉 } → ( 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ↔ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) ) |
42 |
41
|
anbi2d |
⊢ ( 𝑓 = { 〈 1 , 2 〉 , 〈 2 , 2 〉 } → ( ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) ) ) |
43 |
42
|
rspcev |
⊢ ( ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ∈ ( ℙ ↑m { 1 , 2 } ) ∧ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( { 〈 1 , 2 〉 , 〈 2 , 2 〉 } ‘ 𝑘 ) ) ) → ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) |
44 |
16 38 43
|
mp2an |
⊢ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) |
45 |
|
oveq2 |
⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = ( 1 ... 2 ) ) |
46 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
47 |
46
|
oveq2i |
⊢ ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) ) |
48 |
|
1z |
⊢ 1 ∈ ℤ |
49 |
|
fzpr |
⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } ) |
50 |
48 49
|
ax-mp |
⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } |
51 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
52 |
51
|
preq2i |
⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 } |
53 |
50 52
|
eqtri |
⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , 2 } |
54 |
47 53
|
eqtri |
⊢ ( 1 ... 2 ) = { 1 , 2 } |
55 |
45 54
|
eqtrdi |
⊢ ( 𝑑 = 2 → ( 1 ... 𝑑 ) = { 1 , 2 } ) |
56 |
55
|
oveq2d |
⊢ ( 𝑑 = 2 → ( ℙ ↑m ( 1 ... 𝑑 ) ) = ( ℙ ↑m { 1 , 2 } ) ) |
57 |
|
breq1 |
⊢ ( 𝑑 = 2 → ( 𝑑 ≤ 3 ↔ 2 ≤ 3 ) ) |
58 |
55
|
sumeq1d |
⊢ ( 𝑑 = 2 → Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) |
59 |
58
|
eqeq2d |
⊢ ( 𝑑 = 2 → ( 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ↔ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) |
60 |
57 59
|
anbi12d |
⊢ ( 𝑑 = 2 → ( ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) ) |
61 |
56 60
|
rexeqbidv |
⊢ ( 𝑑 = 2 → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ↔ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) ) |
62 |
61
|
rspcev |
⊢ ( ( 2 ∈ ℕ ∧ ∃ 𝑓 ∈ ( ℙ ↑m { 1 , 2 } ) ( 2 ≤ 3 ∧ 4 = Σ 𝑘 ∈ { 1 , 2 } ( 𝑓 ‘ 𝑘 ) ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) ) |
63 |
1 44 62
|
mp2an |
⊢ ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 4 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) |