| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3z 12650 | . . 3
⊢ 3 ∈
ℤ | 
| 2 | 1 | a1i 11 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) → 3
∈ ℤ) | 
| 3 |  | fzfid 14014 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) →
(0...𝑁) ∈
Fin) | 
| 4 |  | ffvelcdm 7101 | . . . . 5
⊢ ((𝐹:(0...𝑁)⟶ℤ ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℤ) | 
| 5 | 4 | adantll 714 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℤ) | 
| 6 |  | 10nn 12749 | . . . . . 6
⊢ ;10 ∈ ℕ | 
| 7 | 6 | nnzi 12641 | . . . . 5
⊢ ;10 ∈ ℤ | 
| 8 |  | elfznn0 13660 | . . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) | 
| 9 | 8 | adantl 481 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) | 
| 10 |  | zexpcl 14117 | . . . . 5
⊢ ((;10 ∈ ℤ ∧ 𝑘 ∈ ℕ0)
→ (;10↑𝑘) ∈
ℤ) | 
| 11 | 7, 9, 10 | sylancr 587 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (;10↑𝑘) ∈ ℤ) | 
| 12 | 5, 11 | zmulcld 12728 | . . 3
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ) | 
| 13 | 3, 12 | fsumzcl 15771 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) →
Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ) | 
| 14 | 3, 5 | fsumzcl 15771 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) →
Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘) ∈ ℤ) | 
| 15 | 12, 5 | zsubcld 12727 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)) ∈ ℤ) | 
| 16 |  | ax-1cn 11213 | . . . . . . . . . . . 12
⊢ 1 ∈
ℂ | 
| 17 | 6 | nncni 12276 | . . . . . . . . . . . 12
⊢ ;10 ∈ ℂ | 
| 18 | 16, 17 | negsubdi2i 11595 | . . . . . . . . . . 11
⊢ -(1
− ;10) = (;10 − 1) | 
| 19 |  | 9p1e10 12735 | . . . . . . . . . . . . 13
⊢ (9 + 1) =
;10 | 
| 20 | 19 | eqcomi 2746 | . . . . . . . . . . . 12
⊢ ;10 = (9 + 1) | 
| 21 | 20 | oveq1i 7441 | . . . . . . . . . . 11
⊢ (;10 − 1) = ((9 + 1) −
1) | 
| 22 |  | 9cn 12366 | . . . . . . . . . . . 12
⊢ 9 ∈
ℂ | 
| 23 | 22, 16 | pncan3oi 11524 | . . . . . . . . . . 11
⊢ ((9 + 1)
− 1) = 9 | 
| 24 | 18, 21, 23 | 3eqtri 2769 | . . . . . . . . . 10
⊢ -(1
− ;10) = 9 | 
| 25 |  | 3t3e9 12433 | . . . . . . . . . 10
⊢ (3
· 3) = 9 | 
| 26 | 24, 25 | eqtr4i 2768 | . . . . . . . . 9
⊢ -(1
− ;10) = (3 ·
3) | 
| 27 | 17 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ;10 ∈
ℂ) | 
| 28 |  | 1re 11261 | . . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ | 
| 29 |  | 1lt10 12872 | . . . . . . . . . . . . . . . . 17
⊢ 1 <
;10 | 
| 30 | 28, 29 | gtneii 11373 | . . . . . . . . . . . . . . . 16
⊢ ;10 ≠ 1 | 
| 31 | 30 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ;10 ≠
1) | 
| 32 |  | id 22 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ 𝑘 ∈
ℕ0) | 
| 33 | 27, 31, 32 | geoser 15903 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ Σ𝑗 ∈
(0...(𝑘 − 1))(;10↑𝑗) = ((1 − (;10↑𝑘)) / (1 − ;10))) | 
| 34 |  | fzfid 14014 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (0...(𝑘 − 1))
∈ Fin) | 
| 35 |  | elfznn0 13660 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(𝑘 − 1)) → 𝑗 ∈ ℕ0) | 
| 36 | 35 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 ∈ (0...(𝑘 − 1))) → 𝑗 ∈
ℕ0) | 
| 37 |  | zexpcl 14117 | . . . . . . . . . . . . . . . 16
⊢ ((;10 ∈ ℤ ∧ 𝑗 ∈ ℕ0)
→ (;10↑𝑗) ∈
ℤ) | 
| 38 | 7, 36, 37 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ℕ0
∧ 𝑗 ∈ (0...(𝑘 − 1))) → (;10↑𝑗) ∈ ℤ) | 
| 39 | 34, 38 | fsumzcl 15771 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ Σ𝑗 ∈
(0...(𝑘 − 1))(;10↑𝑗) ∈ ℤ) | 
| 40 | 33, 39 | eqeltrrd 2842 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ) | 
| 41 |  | 1z 12647 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ | 
| 42 |  | zsubcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℤ ∧ ;10 ∈
ℤ) → (1 − ;10)
∈ ℤ) | 
| 43 | 41, 7, 42 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ (1
− ;10) ∈
ℤ | 
| 44 | 28, 29 | ltneii 11374 | . . . . . . . . . . . . . . 15
⊢ 1 ≠
;10 | 
| 45 | 16, 17 | subeq0i 11589 | . . . . . . . . . . . . . . . 16
⊢ ((1
− ;10) = 0 ↔ 1 = ;10) | 
| 46 | 45 | necon3bii 2993 | . . . . . . . . . . . . . . 15
⊢ ((1
− ;10) ≠ 0 ↔ 1 ≠
;10) | 
| 47 | 44, 46 | mpbir 231 | . . . . . . . . . . . . . 14
⊢ (1
− ;10) ≠
0 | 
| 48 | 7, 32, 10 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ (;10↑𝑘) ∈
ℤ) | 
| 49 |  | zsubcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℤ ∧ (;10↑𝑘) ∈ ℤ) → (1 − (;10↑𝑘)) ∈ ℤ) | 
| 50 | 41, 48, 49 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ (1 − (;10↑𝑘)) ∈
ℤ) | 
| 51 |  | dvdsval2 16293 | . . . . . . . . . . . . . 14
⊢ (((1
− ;10) ∈ ℤ ∧
(1 − ;10) ≠ 0 ∧ (1
− (;10↑𝑘)) ∈ ℤ) → ((1
− ;10) ∥ (1 −
(;10↑𝑘)) ↔ ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ)) | 
| 52 | 43, 47, 50, 51 | mp3an12i 1467 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ ((1 − ;10) ∥ (1
− (;10↑𝑘)) ↔ ((1 − (;10↑𝑘)) / (1 − ;10)) ∈ ℤ)) | 
| 53 | 40, 52 | mpbird 257 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ (1 − ;10) ∥ (1
− (;10↑𝑘))) | 
| 54 | 48 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (;10↑𝑘) ∈
ℂ) | 
| 55 |  | negsubdi2 11568 | . . . . . . . . . . . . 13
⊢ (((;10↑𝑘) ∈ ℂ ∧ 1 ∈ ℂ)
→ -((;10↑𝑘) − 1) = (1 − (;10↑𝑘))) | 
| 56 | 54, 16, 55 | sylancl 586 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ -((;10↑𝑘) − 1) = (1 − (;10↑𝑘))) | 
| 57 | 53, 56 | breqtrrd 5171 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (1 − ;10) ∥
-((;10↑𝑘) − 1)) | 
| 58 |  | peano2zm 12660 | . . . . . . . . . . . . 13
⊢ ((;10↑𝑘) ∈ ℤ → ((;10↑𝑘) − 1) ∈ ℤ) | 
| 59 | 48, 58 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ0
→ ((;10↑𝑘) − 1) ∈
ℤ) | 
| 60 |  | dvdsnegb 16311 | . . . . . . . . . . . 12
⊢ (((1
− ;10) ∈ ℤ ∧
((;10↑𝑘) − 1) ∈ ℤ) → ((1
− ;10) ∥ ((;10↑𝑘) − 1) ↔ (1 − ;10) ∥ -((;10↑𝑘) − 1))) | 
| 61 | 43, 59, 60 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ ((1 − ;10) ∥
((;10↑𝑘) − 1) ↔ (1 − ;10) ∥ -((;10↑𝑘) − 1))) | 
| 62 | 57, 61 | mpbird 257 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (1 − ;10) ∥
((;10↑𝑘) − 1)) | 
| 63 |  | negdvdsb 16310 | . . . . . . . . . . 11
⊢ (((1
− ;10) ∈ ℤ ∧
((;10↑𝑘) − 1) ∈ ℤ) → ((1
− ;10) ∥ ((;10↑𝑘) − 1) ↔ -(1 − ;10) ∥ ((;10↑𝑘) − 1))) | 
| 64 | 43, 59, 63 | sylancr 587 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ ((1 − ;10) ∥
((;10↑𝑘) − 1) ↔ -(1 − ;10) ∥ ((;10↑𝑘) − 1))) | 
| 65 | 62, 64 | mpbid 232 | . . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
→ -(1 − ;10) ∥
((;10↑𝑘) − 1)) | 
| 66 | 26, 65 | eqbrtrrid 5179 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ (3 · 3) ∥ ((;10↑𝑘) − 1)) | 
| 67 |  | muldvds1 16318 | . . . . . . . . 9
⊢ ((3
∈ ℤ ∧ 3 ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → ((3
· 3) ∥ ((;10↑𝑘) − 1) → 3 ∥ ((;10↑𝑘) − 1))) | 
| 68 | 1, 1, 59, 67 | mp3an12i 1467 | . . . . . . . 8
⊢ (𝑘 ∈ ℕ0
→ ((3 · 3) ∥ ((;10↑𝑘) − 1) → 3 ∥ ((;10↑𝑘) − 1))) | 
| 69 | 66, 68 | mpd 15 | . . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ 3 ∥ ((;10↑𝑘) − 1)) | 
| 70 | 9, 69 | syl 17 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ ((;10↑𝑘) − 1)) | 
| 71 | 11, 58 | syl 17 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((;10↑𝑘) − 1) ∈ ℤ) | 
| 72 |  | dvdsmultr2 16335 | . . . . . . 7
⊢ ((3
∈ ℤ ∧ (𝐹‘𝑘) ∈ ℤ ∧ ((;10↑𝑘) − 1) ∈ ℤ) → (3
∥ ((;10↑𝑘) − 1) → 3 ∥
((𝐹‘𝑘) · ((;10↑𝑘) − 1)))) | 
| 73 | 1, 5, 71, 72 | mp3an2i 1468 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (3 ∥ ((;10↑𝑘) − 1) → 3 ∥ ((𝐹‘𝑘) · ((;10↑𝑘) − 1)))) | 
| 74 | 70, 73 | mpd 15 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ ((𝐹‘𝑘) · ((;10↑𝑘) − 1))) | 
| 75 | 5 | zcnd 12723 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (𝐹‘𝑘) ∈ ℂ) | 
| 76 | 11 | zcnd 12723 | . . . . . 6
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → (;10↑𝑘) ∈ ℂ) | 
| 77 | 75, 76 | muls1d 11723 | . . . . 5
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · ((;10↑𝑘) − 1)) = (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘))) | 
| 78 | 74, 77 | breqtrd 5169 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → 3 ∥ (((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘))) | 
| 79 | 3, 2, 15, 78 | fsumdvds 16345 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) → 3
∥ Σ𝑘 ∈
(0...𝑁)(((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘))) | 
| 80 | 12 | zcnd 12723 | . . . 4
⊢ (((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) ∧ 𝑘 ∈ (0...𝑁)) → ((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℂ) | 
| 81 | 3, 80, 75 | fsumsub 15824 | . . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) →
Σ𝑘 ∈ (0...𝑁)(((𝐹‘𝑘) · (;10↑𝑘)) − (𝐹‘𝑘)) = (Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) | 
| 82 | 79, 81 | breqtrd 5169 | . 2
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) → 3
∥ (Σ𝑘 ∈
(0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) | 
| 83 |  | dvdssub2 16338 | . 2
⊢ (((3
∈ ℤ ∧ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ∈ ℤ ∧ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘) ∈ ℤ) ∧ 3 ∥
(Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) − Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) | 
| 84 | 2, 13, 14, 82, 83 | syl31anc 1375 | 1
⊢ ((𝑁 ∈ ℕ0
∧ 𝐹:(0...𝑁)⟶ℤ) → (3
∥ Σ𝑘 ∈
(0...𝑁)((𝐹‘𝑘) · (;10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) |