Proof of Theorem oddpwdclemodd
Step | Hyp | Ref
| Expression |
1 | | oddpwdclemndvds 12050 |
. . 3
⊢ (𝐴 ∈ ℕ → ¬
(2↑((℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) ∥ 𝐴) |
2 | | 2cn 8905 |
. . . . 5
⊢ 2 ∈
ℂ |
3 | | pw2dvdseu 12047 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
∃!𝑧 ∈
ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) |
4 | | riotacl 5795 |
. . . . . 6
⊢
(∃!𝑧 ∈
ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴) → (℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) ∈
ℕ0) |
5 | 3, 4 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
(℩𝑧 ∈
ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) ∈
ℕ0) |
6 | | expp1 10430 |
. . . . 5
⊢ ((2
∈ ℂ ∧ (℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) ∈ ℕ0) →
(2↑((℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) = ((2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2)) |
7 | 2, 5, 6 | sylancr 411 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2↑((℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) = ((2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2)) |
8 | 7 | breq1d 3976 |
. . 3
⊢ (𝐴 ∈ ℕ →
((2↑((℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) ∥ 𝐴 ↔ ((2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥ 𝐴)) |
9 | 1, 8 | mtbid 662 |
. 2
⊢ (𝐴 ∈ ℕ → ¬
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥ 𝐴) |
10 | | nncn 8842 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℂ) |
11 | | 2nn 8995 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
12 | 11 | a1i 9 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → 2 ∈
ℕ) |
13 | 12, 5 | nnexpcld 10577 |
. . . . . . 7
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℕ) |
14 | 13 | nncnd 8848 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℂ) |
15 | 13 | nnap0d 8880 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) # 0) |
16 | 10, 14, 15 | divcanap2d 8666 |
. . . . 5
⊢ (𝐴 ∈ ℕ →
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) = 𝐴) |
17 | 16 | eqcomd 2163 |
. . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 = ((2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))) |
18 | 17 | breq2d 3978 |
. . 3
⊢ (𝐴 ∈ ℕ →
(((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥ 𝐴 ↔ ((2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))))) |
19 | 12 | nnzd 9286 |
. . . 4
⊢ (𝐴 ∈ ℕ → 2 ∈
ℤ) |
20 | | id 19 |
. . . . . 6
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ) |
21 | | oddpwdclemdvds 12049 |
. . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴) |
22 | | nndivdvds 11696 |
. . . . . . 7
⊢ ((𝐴 ∈ ℕ ∧
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℕ) →
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴 ↔ (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∈ ℕ)) |
23 | 22 | biimpa 294 |
. . . . . 6
⊢ (((𝐴 ∈ ℕ ∧
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℕ) ∧
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴) → (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∈ ℕ) |
24 | 20, 13, 21, 23 | syl21anc 1219 |
. . . . 5
⊢ (𝐴 ∈ ℕ → (𝐴 / (2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∈ ℕ) |
25 | 24 | nnzd 9286 |
. . . 4
⊢ (𝐴 ∈ ℕ → (𝐴 / (2↑(℩𝑧 ∈ ℕ0
((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∈ ℤ) |
26 | 13 | nnzd 9286 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℤ) |
27 | 13 | nnne0d 8879 |
. . . 4
⊢ (𝐴 ∈ ℕ →
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ≠ 0) |
28 | | dvdscmulr 11720 |
. . . 4
⊢ ((2
∈ ℤ ∧ (𝐴 /
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∈ ℤ ∧
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∈ ℤ ∧
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ≠ 0)) →
(((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) ↔ 2 ∥ (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))) |
29 | 19, 25, 26, 27, 28 | syl112anc 1224 |
. . 3
⊢ (𝐴 ∈ ℕ →
(((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥
((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) ↔ 2 ∥ (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))) |
30 | 18, 29 | bitrd 187 |
. 2
⊢ (𝐴 ∈ ℕ →
(((2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) · 2) ∥ 𝐴 ↔ 2 ∥ (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))) |
31 | 9, 30 | mtbid 662 |
1
⊢ (𝐴 ∈ ℕ → ¬ 2
∥ (𝐴 /
(2↑(℩𝑧
∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))) |