Proof of Theorem 2sqpwodd
Step | Hyp | Ref
| Expression |
1 | | oddpwdc.j |
. . . . . . . . 9
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧} |
2 | | oddpwdc.f |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦
((2↑𝑦) · 𝑥)) |
3 | 1, 2 | oddpwdc 12128 |
. . . . . . . 8
⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ |
4 | | f1ocnv 5455 |
. . . . . . . 8
⊢ (𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ → ◡𝐹:ℕ–1-1-onto→(𝐽 ×
ℕ0)) |
5 | | f1of 5442 |
. . . . . . . 8
⊢ (◡𝐹:ℕ–1-1-onto→(𝐽 × ℕ0) → ◡𝐹:ℕ⟶(𝐽 ×
ℕ0)) |
6 | 3, 4, 5 | mp2b 8 |
. . . . . . 7
⊢ ◡𝐹:ℕ⟶(𝐽 ×
ℕ0) |
7 | 6 | ffvelrni 5630 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (◡𝐹‘𝐴) ∈ (𝐽 ×
ℕ0)) |
8 | | xp2nd 6145 |
. . . . . 6
⊢ ((◡𝐹‘𝐴) ∈ (𝐽 × ℕ0) →
(2nd ‘(◡𝐹‘𝐴)) ∈
ℕ0) |
9 | 7, 8 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(2nd ‘(◡𝐹‘𝐴)) ∈
ℕ0) |
10 | 9 | nn0zd 9332 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2nd ‘(◡𝐹‘𝐴)) ∈ ℤ) |
11 | | 2nn 9039 |
. . . . . 6
⊢ 2 ∈
ℕ |
12 | 11 | a1i 9 |
. . . . 5
⊢ (𝐴 ∈ ℕ → 2 ∈
ℕ) |
13 | 12 | nnzd 9333 |
. . . 4
⊢ (𝐴 ∈ ℕ → 2 ∈
ℤ) |
14 | 10, 13 | zmulcld 9340 |
. . 3
⊢ (𝐴 ∈ ℕ →
((2nd ‘(◡𝐹‘𝐴)) · 2) ∈
ℤ) |
15 | | dvdsmul2 11776 |
. . . 4
⊢
(((2nd ‘(◡𝐹‘𝐴)) ∈ ℤ ∧ 2 ∈ ℤ)
→ 2 ∥ ((2nd ‘(◡𝐹‘𝐴)) · 2)) |
16 | 10, 13, 15 | syl2anc 409 |
. . 3
⊢ (𝐴 ∈ ℕ → 2 ∥
((2nd ‘(◡𝐹‘𝐴)) · 2)) |
17 | | oddp1even 11835 |
. . . . 5
⊢
(((2nd ‘(◡𝐹‘𝐴)) · 2) ∈ ℤ → (¬
2 ∥ ((2nd ‘(◡𝐹‘𝐴)) · 2) ↔ 2 ∥
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1))) |
18 | 17 | biimprd 157 |
. . . 4
⊢
(((2nd ‘(◡𝐹‘𝐴)) · 2) ∈ ℤ → (2
∥ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) → ¬ 2 ∥
((2nd ‘(◡𝐹‘𝐴)) · 2))) |
19 | 18 | con2d 619 |
. . 3
⊢
(((2nd ‘(◡𝐹‘𝐴)) · 2) ∈ ℤ → (2
∥ ((2nd ‘(◡𝐹‘𝐴)) · 2) → ¬ 2 ∥
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1))) |
20 | 14, 16, 19 | sylc 62 |
. 2
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) |
21 | | xp1st 6144 |
. . . . . . . . . . 11
⊢ ((◡𝐹‘𝐴) ∈ (𝐽 × ℕ0) →
(1st ‘(◡𝐹‘𝐴)) ∈ 𝐽) |
22 | 7, 21 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
(1st ‘(◡𝐹‘𝐴)) ∈ 𝐽) |
23 | | breq2 3993 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (1st ‘(◡𝐹‘𝐴)) → (2 ∥ 𝑧 ↔ 2 ∥ (1st
‘(◡𝐹‘𝐴)))) |
24 | 23 | notbid 662 |
. . . . . . . . . . . 12
⊢ (𝑧 = (1st ‘(◡𝐹‘𝐴)) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥
(1st ‘(◡𝐹‘𝐴)))) |
25 | 24, 1 | elrab2 2889 |
. . . . . . . . . . 11
⊢
((1st ‘(◡𝐹‘𝐴)) ∈ 𝐽 ↔ ((1st ‘(◡𝐹‘𝐴)) ∈ ℕ ∧ ¬ 2 ∥
(1st ‘(◡𝐹‘𝐴)))) |
26 | 25 | simplbi 272 |
. . . . . . . . . 10
⊢
((1st ‘(◡𝐹‘𝐴)) ∈ 𝐽 → (1st ‘(◡𝐹‘𝐴)) ∈ ℕ) |
27 | 22, 26 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(1st ‘(◡𝐹‘𝐴)) ∈ ℕ) |
28 | 27 | nnsqcld 10630 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((1st ‘(◡𝐹‘𝐴))↑2) ∈ ℕ) |
29 | 25 | simprbi 273 |
. . . . . . . . . . 11
⊢
((1st ‘(◡𝐹‘𝐴)) ∈ 𝐽 → ¬ 2 ∥ (1st
‘(◡𝐹‘𝐴))) |
30 | 22, 29 | syl 14 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ (1st ‘(◡𝐹‘𝐴))) |
31 | | 2prm 12081 |
. . . . . . . . . . 11
⊢ 2 ∈
ℙ |
32 | 27 | nnzd 9333 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(1st ‘(◡𝐹‘𝐴)) ∈ ℤ) |
33 | | euclemma 12100 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℙ ∧ (1st ‘(◡𝐹‘𝐴)) ∈ ℤ ∧ (1st
‘(◡𝐹‘𝐴)) ∈ ℤ) → (2 ∥
((1st ‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴))) ↔ (2 ∥ (1st
‘(◡𝐹‘𝐴)) ∨ 2 ∥ (1st
‘(◡𝐹‘𝐴))))) |
34 | | oridm 752 |
. . . . . . . . . . . 12
⊢ ((2
∥ (1st ‘(◡𝐹‘𝐴)) ∨ 2 ∥ (1st
‘(◡𝐹‘𝐴))) ↔ 2 ∥ (1st
‘(◡𝐹‘𝐴))) |
35 | 33, 34 | bitrdi 195 |
. . . . . . . . . . 11
⊢ ((2
∈ ℙ ∧ (1st ‘(◡𝐹‘𝐴)) ∈ ℤ ∧ (1st
‘(◡𝐹‘𝐴)) ∈ ℤ) → (2 ∥
((1st ‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴))) ↔ 2 ∥ (1st
‘(◡𝐹‘𝐴)))) |
36 | 31, 32, 32, 35 | mp3an2i 1337 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → (2
∥ ((1st ‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴))) ↔ 2 ∥ (1st
‘(◡𝐹‘𝐴)))) |
37 | 30, 36 | mtbird 668 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ ((1st ‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴)))) |
38 | 27 | nncnd 8892 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(1st ‘(◡𝐹‘𝐴)) ∈ ℂ) |
39 | 38 | sqvald 10606 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
((1st ‘(◡𝐹‘𝐴))↑2) = ((1st ‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴)))) |
40 | 39 | breq2d 4001 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → (2
∥ ((1st ‘(◡𝐹‘𝐴))↑2) ↔ 2 ∥ ((1st
‘(◡𝐹‘𝐴)) · (1st ‘(◡𝐹‘𝐴))))) |
41 | 37, 40 | mtbird 668 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ ((1st ‘(◡𝐹‘𝐴))↑2)) |
42 | | breq2 3993 |
. . . . . . . . . 10
⊢ (𝑧 = ((1st
‘(◡𝐹‘𝐴))↑2) → (2 ∥ 𝑧 ↔ 2 ∥
((1st ‘(◡𝐹‘𝐴))↑2))) |
43 | 42 | notbid 662 |
. . . . . . . . 9
⊢ (𝑧 = ((1st
‘(◡𝐹‘𝐴))↑2) → (¬ 2 ∥ 𝑧 ↔ ¬ 2 ∥
((1st ‘(◡𝐹‘𝐴))↑2))) |
44 | 43, 1 | elrab2 2889 |
. . . . . . . 8
⊢
(((1st ‘(◡𝐹‘𝐴))↑2) ∈ 𝐽 ↔ (((1st ‘(◡𝐹‘𝐴))↑2) ∈ ℕ ∧ ¬ 2
∥ ((1st ‘(◡𝐹‘𝐴))↑2))) |
45 | 28, 41, 44 | sylanbrc 415 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
((1st ‘(◡𝐹‘𝐴))↑2) ∈ 𝐽) |
46 | 12 | nnnn0d 9188 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → 2 ∈
ℕ0) |
47 | 9, 46 | nn0mulcld 9193 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((2nd ‘(◡𝐹‘𝐴)) · 2) ∈
ℕ0) |
48 | | peano2nn0 9175 |
. . . . . . . 8
⊢
(((2nd ‘(◡𝐹‘𝐴)) · 2) ∈ ℕ0
→ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) ∈
ℕ0) |
49 | 47, 48 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) ∈
ℕ0) |
50 | | opelxp 4641 |
. . . . . . 7
⊢
(〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉 ∈ (𝐽 × ℕ0)
↔ (((1st ‘(◡𝐹‘𝐴))↑2) ∈ 𝐽 ∧ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) ∈
ℕ0)) |
51 | 45, 49, 50 | sylanbrc 415 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉 ∈ (𝐽 ×
ℕ0)) |
52 | 12 | nncnd 8892 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → 2 ∈
ℂ) |
53 | 52, 47 | expp1d 10610 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
(2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) =
((2↑((2nd ‘(◡𝐹‘𝐴)) · 2)) ·
2)) |
54 | 52, 47 | expcld 10609 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(2↑((2nd ‘(◡𝐹‘𝐴)) · 2)) ∈
ℂ) |
55 | 54, 52 | mulcomd 7941 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
((2↑((2nd ‘(◡𝐹‘𝐴)) · 2)) · 2) = (2 ·
(2↑((2nd ‘(◡𝐹‘𝐴)) · 2)))) |
56 | 52, 46, 9 | expmuld 10612 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(2↑((2nd ‘(◡𝐹‘𝐴)) · 2)) = ((2↑(2nd
‘(◡𝐹‘𝐴)))↑2)) |
57 | 56 | oveq2d 5869 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → (2
· (2↑((2nd ‘(◡𝐹‘𝐴)) · 2))) = (2 ·
((2↑(2nd ‘(◡𝐹‘𝐴)))↑2))) |
58 | 53, 55, 57 | 3eqtrd 2207 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) = (2 ·
((2↑(2nd ‘(◡𝐹‘𝐴)))↑2))) |
59 | 58 | oveq1d 5868 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
((2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2)) = ((2 ·
((2↑(2nd ‘(◡𝐹‘𝐴)))↑2)) · ((1st
‘(◡𝐹‘𝐴))↑2))) |
60 | 12, 49 | nnexpcld 10631 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
(2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ∈
ℕ) |
61 | 60, 28 | nnmulcld 8927 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
((2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2)) ∈ ℕ) |
62 | | oveq2 5861 |
. . . . . . . . . 10
⊢ (𝑥 = ((1st
‘(◡𝐹‘𝐴))↑2) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · ((1st ‘(◡𝐹‘𝐴))↑2))) |
63 | | oveq2 5861 |
. . . . . . . . . . 11
⊢ (𝑦 = (((2nd
‘(◡𝐹‘𝐴)) · 2) + 1) → (2↑𝑦) = (2↑(((2nd
‘(◡𝐹‘𝐴)) · 2) + 1))) |
64 | 63 | oveq1d 5868 |
. . . . . . . . . 10
⊢ (𝑦 = (((2nd
‘(◡𝐹‘𝐴)) · 2) + 1) → ((2↑𝑦) · ((1st
‘(◡𝐹‘𝐴))↑2)) = ((2↑(((2nd
‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2))) |
65 | 62, 64, 2 | ovmpog 5987 |
. . . . . . . . 9
⊢
((((1st ‘(◡𝐹‘𝐴))↑2) ∈ 𝐽 ∧ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) ∈
ℕ0 ∧ ((2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2)) ∈ ℕ) →
(((1st ‘(◡𝐹‘𝐴))↑2)𝐹(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) =
((2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2))) |
66 | 45, 49, 61, 65 | syl3anc 1233 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ →
(((1st ‘(◡𝐹‘𝐴))↑2)𝐹(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) =
((2↑(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) ·
((1st ‘(◡𝐹‘𝐴))↑2))) |
67 | | f1ocnvfv2 5757 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ ∧ 𝐴 ∈ ℕ) → (𝐹‘(◡𝐹‘𝐴)) = 𝐴) |
68 | 3, 67 | mpan 422 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ → (𝐹‘(◡𝐹‘𝐴)) = 𝐴) |
69 | | 1st2nd2 6154 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹‘𝐴) ∈ (𝐽 × ℕ0) → (◡𝐹‘𝐴) = 〈(1st ‘(◡𝐹‘𝐴)), (2nd ‘(◡𝐹‘𝐴))〉) |
70 | 7, 69 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ ℕ → (◡𝐹‘𝐴) = 〈(1st ‘(◡𝐹‘𝐴)), (2nd ‘(◡𝐹‘𝐴))〉) |
71 | 70 | fveq2d 5500 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ → (𝐹‘(◡𝐹‘𝐴)) = (𝐹‘〈(1st ‘(◡𝐹‘𝐴)), (2nd ‘(◡𝐹‘𝐴))〉)) |
72 | 68, 71 | eqtr3d 2205 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ → 𝐴 = (𝐹‘〈(1st ‘(◡𝐹‘𝐴)), (2nd ‘(◡𝐹‘𝐴))〉)) |
73 | | df-ov 5856 |
. . . . . . . . . . . . . 14
⊢
((1st ‘(◡𝐹‘𝐴))𝐹(2nd ‘(◡𝐹‘𝐴))) = (𝐹‘〈(1st ‘(◡𝐹‘𝐴)), (2nd ‘(◡𝐹‘𝐴))〉) |
74 | 72, 73 | eqtr4di 2221 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ → 𝐴 = ((1st
‘(◡𝐹‘𝐴))𝐹(2nd ‘(◡𝐹‘𝐴)))) |
75 | 12, 9 | nnexpcld 10631 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℕ →
(2↑(2nd ‘(◡𝐹‘𝐴))) ∈ ℕ) |
76 | 75, 27 | nnmulcld 8927 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℕ →
((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴))) ∈ ℕ) |
77 | | oveq2 5861 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1st ‘(◡𝐹‘𝐴)) → ((2↑𝑦) · 𝑥) = ((2↑𝑦) · (1st ‘(◡𝐹‘𝐴)))) |
78 | | oveq2 5861 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (2nd ‘(◡𝐹‘𝐴)) → (2↑𝑦) = (2↑(2nd ‘(◡𝐹‘𝐴)))) |
79 | 78 | oveq1d 5868 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (2nd ‘(◡𝐹‘𝐴)) → ((2↑𝑦) · (1st ‘(◡𝐹‘𝐴))) = ((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))) |
80 | 77, 79, 2 | ovmpog 5987 |
. . . . . . . . . . . . . 14
⊢
(((1st ‘(◡𝐹‘𝐴)) ∈ 𝐽 ∧ (2nd ‘(◡𝐹‘𝐴)) ∈ ℕ0 ∧
((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴))) ∈ ℕ) → ((1st
‘(◡𝐹‘𝐴))𝐹(2nd ‘(◡𝐹‘𝐴))) = ((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))) |
81 | 22, 9, 76, 80 | syl3anc 1233 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℕ →
((1st ‘(◡𝐹‘𝐴))𝐹(2nd ‘(◡𝐹‘𝐴))) = ((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))) |
82 | 74, 81 | eqtrd 2203 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ → 𝐴 = ((2↑(2nd
‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))) |
83 | 82 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ → (𝐴↑2) =
(((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))↑2)) |
84 | 75 | nncnd 8892 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℕ →
(2↑(2nd ‘(◡𝐹‘𝐴))) ∈ ℂ) |
85 | 84, 38 | sqmuld 10621 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℕ →
(((2↑(2nd ‘(◡𝐹‘𝐴))) · (1st ‘(◡𝐹‘𝐴)))↑2) = (((2↑(2nd
‘(◡𝐹‘𝐴)))↑2) · ((1st
‘(◡𝐹‘𝐴))↑2))) |
86 | 83, 85 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → (𝐴↑2) =
(((2↑(2nd ‘(◡𝐹‘𝐴)))↑2) · ((1st
‘(◡𝐹‘𝐴))↑2))) |
87 | 86 | oveq2d 5869 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → (2
· (𝐴↑2)) = (2
· (((2↑(2nd ‘(◡𝐹‘𝐴)))↑2) · ((1st
‘(◡𝐹‘𝐴))↑2)))) |
88 | 56, 54 | eqeltrrd 2248 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
((2↑(2nd ‘(◡𝐹‘𝐴)))↑2) ∈ ℂ) |
89 | 28 | nncnd 8892 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℕ →
((1st ‘(◡𝐹‘𝐴))↑2) ∈ ℂ) |
90 | 52, 88, 89 | mulassd 7943 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℕ → ((2
· ((2↑(2nd ‘(◡𝐹‘𝐴)))↑2)) · ((1st
‘(◡𝐹‘𝐴))↑2)) = (2 ·
(((2↑(2nd ‘(◡𝐹‘𝐴)))↑2) · ((1st
‘(◡𝐹‘𝐴))↑2)))) |
91 | 87, 90 | eqtr4d 2206 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → (2
· (𝐴↑2)) = ((2
· ((2↑(2nd ‘(◡𝐹‘𝐴)))↑2)) · ((1st
‘(◡𝐹‘𝐴))↑2))) |
92 | 59, 66, 91 | 3eqtr4rd 2214 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ → (2
· (𝐴↑2)) =
(((1st ‘(◡𝐹‘𝐴))↑2)𝐹(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1))) |
93 | | df-ov 5856 |
. . . . . . 7
⊢
(((1st ‘(◡𝐹‘𝐴))↑2)𝐹(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) = (𝐹‘〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) |
94 | 92, 93 | eqtr2di 2220 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → (𝐹‘〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) = (2 ·
(𝐴↑2))) |
95 | | f1ocnvfv 5758 |
. . . . . . 7
⊢ ((𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ ∧ 〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉 ∈ (𝐽 × ℕ0))
→ ((𝐹‘〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) = (2 ·
(𝐴↑2)) → (◡𝐹‘(2 · (𝐴↑2))) = 〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉)) |
96 | 3, 95 | mpan 422 |
. . . . . 6
⊢
(〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉 ∈ (𝐽 × ℕ0)
→ ((𝐹‘〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) = (2 ·
(𝐴↑2)) → (◡𝐹‘(2 · (𝐴↑2))) = 〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉)) |
97 | 51, 94, 96 | sylc 62 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (◡𝐹‘(2 · (𝐴↑2))) = 〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) |
98 | 97 | fveq2d 5500 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2nd ‘(◡𝐹‘(2 · (𝐴↑2)))) = (2nd
‘〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉)) |
99 | | op2ndg 6130 |
. . . . 5
⊢
((((1st ‘(◡𝐹‘𝐴))↑2) ∈ 𝐽 ∧ (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1) ∈
ℕ0) → (2nd ‘〈((1st
‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) =
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) |
100 | 45, 49, 99 | syl2anc 409 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2nd ‘〈((1st ‘(◡𝐹‘𝐴))↑2), (((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)〉) =
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1)) |
101 | 98, 100 | eqtrd 2203 |
. . 3
⊢ (𝐴 ∈ ℕ →
(2nd ‘(◡𝐹‘(2 · (𝐴↑2)))) = (((2nd
‘(◡𝐹‘𝐴)) · 2) + 1)) |
102 | 101 | breq2d 4001 |
. 2
⊢ (𝐴 ∈ ℕ → (2
∥ (2nd ‘(◡𝐹‘(2 · (𝐴↑2)))) ↔ 2 ∥
(((2nd ‘(◡𝐹‘𝐴)) · 2) + 1))) |
103 | 20, 102 | mtbird 668 |
1
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ (2nd ‘(◡𝐹‘(2 · (𝐴↑2))))) |