| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (0...𝑄) ∈ Fin) | 
| 2 |  | elfznn0 13660 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑄) → 𝑘 ∈ ℕ0) | 
| 3 |  | eirr.1 | . . . . . . . . . . . 12
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 /
(!‘𝑛))) | 
| 4 |  | nn0z 12638 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℤ) | 
| 5 |  | 1exp 14132 | . . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ →
(1↑𝑛) =
1) | 
| 6 | 4, 5 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ0
→ (1↑𝑛) =
1) | 
| 7 | 6 | oveq1d 7446 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ0
→ ((1↑𝑛) /
(!‘𝑛)) = (1 /
(!‘𝑛))) | 
| 8 | 7 | mpteq2ia 5245 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
↦ ((1↑𝑛) /
(!‘𝑛))) = (𝑛 ∈ ℕ0
↦ (1 / (!‘𝑛))) | 
| 9 | 3, 8 | eqtr4i 2768 | . . . . . . . . . . 11
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
((1↑𝑛) /
(!‘𝑛))) | 
| 10 | 9 | eftval 16112 | . . . . . . . . . 10
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = ((1↑𝑘) / (!‘𝑘))) | 
| 11 | 10 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = ((1↑𝑘) / (!‘𝑘))) | 
| 12 |  | ax-1cn 11213 | . . . . . . . . . . 11
⊢ 1 ∈
ℂ | 
| 13 | 12 | a1i 11 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℂ) | 
| 14 |  | eftcl 16109 | . . . . . . . . . 10
⊢ ((1
∈ ℂ ∧ 𝑘
∈ ℕ0) → ((1↑𝑘) / (!‘𝑘)) ∈ ℂ) | 
| 15 | 13, 14 | sylan 580 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
((1↑𝑘) /
(!‘𝑘)) ∈
ℂ) | 
| 16 | 11, 15 | eqeltrd 2841 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈ ℂ) | 
| 17 | 2, 16 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (𝐹‘𝑘) ∈ ℂ) | 
| 18 | 1, 17 | fsumcl 15769 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘) ∈ ℂ) | 
| 19 |  | nn0uz 12920 | . . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) | 
| 20 |  | eqid 2737 | . . . . . . . . 9
⊢
(ℤ≥‘(𝑄 + 1)) =
(ℤ≥‘(𝑄 + 1)) | 
| 21 |  | eirr.3 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℕ) | 
| 22 | 21 | peano2nnd 12283 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄 + 1) ∈ ℕ) | 
| 23 | 22 | nnnn0d 12587 | . . . . . . . . 9
⊢ (𝜑 → (𝑄 + 1) ∈
ℕ0) | 
| 24 |  | eqidd 2738 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐹‘𝑘)) | 
| 25 |  | fveq2 6906 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘)) | 
| 26 | 25 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘))) | 
| 27 |  | ovex 7464 | . . . . . . . . . . . 12
⊢ (1 /
(!‘𝑘)) ∈
V | 
| 28 | 26, 3, 27 | fvmpt 7016 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (𝐹‘𝑘) = (1 / (!‘𝑘))) | 
| 29 | 28 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (1 / (!‘𝑘))) | 
| 30 |  | faccl 14322 | . . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) | 
| 31 | 30 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(!‘𝑘) ∈
ℕ) | 
| 32 | 31 | nnrpd 13075 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) →
(!‘𝑘) ∈
ℝ+) | 
| 33 | 32 | rpreccld 13087 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (1 /
(!‘𝑘)) ∈
ℝ+) | 
| 34 | 29, 33 | eqeltrd 2841 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) ∈
ℝ+) | 
| 35 | 9 | efcllem 16113 | . . . . . . . . . 10
⊢ (1 ∈
ℂ → seq0( + , 𝐹)
∈ dom ⇝ ) | 
| 36 | 13, 35 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐹) ∈ dom ⇝
) | 
| 37 | 19, 20, 23, 24, 34, 36 | isumrpcl 15879 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ∈
ℝ+) | 
| 38 | 37 | rpred 13077 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ∈ ℝ) | 
| 39 | 38 | recnd 11289 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ∈ ℂ) | 
| 40 |  | esum 16116 | . . . . . . . . 9
⊢ e =
Σ𝑘 ∈
ℕ0 (1 / (!‘𝑘)) | 
| 41 | 28 | sumeq2i 15734 | . . . . . . . . 9
⊢
Σ𝑘 ∈
ℕ0 (𝐹‘𝑘) = Σ𝑘 ∈ ℕ0 (1 /
(!‘𝑘)) | 
| 42 | 40, 41 | eqtr4i 2768 | . . . . . . . 8
⊢ e =
Σ𝑘 ∈
ℕ0 (𝐹‘𝑘) | 
| 43 | 19, 20, 23, 24, 16, 36 | isumsplit 15876 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ℕ0 (𝐹‘𝑘) = (Σ𝑘 ∈ (0...((𝑄 + 1) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 44 | 42, 43 | eqtrid 2789 | . . . . . . 7
⊢ (𝜑 → e = (Σ𝑘 ∈ (0...((𝑄 + 1) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 45 | 21 | nncnd 12282 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ ℂ) | 
| 46 |  | pncan 11514 | . . . . . . . . . . 11
⊢ ((𝑄 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑄 + 1)
− 1) = 𝑄) | 
| 47 | 45, 12, 46 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑄 + 1) − 1) = 𝑄) | 
| 48 | 47 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (0...((𝑄 + 1) − 1)) = (0...𝑄)) | 
| 49 | 48 | sumeq1d 15736 | . . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (0...((𝑄 + 1) − 1))(𝐹‘𝑘) = Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)) | 
| 50 | 49 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → (Σ𝑘 ∈ (0...((𝑄 + 1) − 1))(𝐹‘𝑘) + Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) = (Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘) + Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 51 | 44, 50 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → e = (Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘) + Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 52 | 18, 39, 51 | mvrladdd 11676 | . . . . 5
⊢ (𝜑 → (e − Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) | 
| 53 | 52 | oveq2d 7447 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · (e −
Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘))) = ((!‘𝑄) · Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 54 | 21 | nnnn0d 12587 | . . . . . . 7
⊢ (𝜑 → 𝑄 ∈
ℕ0) | 
| 55 | 54 | faccld 14323 | . . . . . 6
⊢ (𝜑 → (!‘𝑄) ∈ ℕ) | 
| 56 | 55 | nncnd 12282 | . . . . 5
⊢ (𝜑 → (!‘𝑄) ∈ ℂ) | 
| 57 |  | ere 16125 | . . . . . . 7
⊢ e ∈
ℝ | 
| 58 | 57 | recni 11275 | . . . . . 6
⊢ e ∈
ℂ | 
| 59 | 58 | a1i 11 | . . . . 5
⊢ (𝜑 → e ∈
ℂ) | 
| 60 | 56, 59, 18 | subdid 11719 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · (e −
Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘))) = (((!‘𝑄) · e) − ((!‘𝑄) · Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)))) | 
| 61 | 53, 60 | eqtr3d 2779 | . . 3
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) = (((!‘𝑄) · e) − ((!‘𝑄) · Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)))) | 
| 62 |  | eirr.4 | . . . . . . 7
⊢ (𝜑 → e = (𝑃 / 𝑄)) | 
| 63 | 62 | oveq2d 7447 | . . . . . 6
⊢ (𝜑 → ((!‘𝑄) · e) = ((!‘𝑄) · (𝑃 / 𝑄))) | 
| 64 |  | eirr.2 | . . . . . . . 8
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 65 | 64 | zcnd 12723 | . . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 66 | 21 | nnne0d 12316 | . . . . . . 7
⊢ (𝜑 → 𝑄 ≠ 0) | 
| 67 | 56, 65, 45, 66 | div12d 12079 | . . . . . 6
⊢ (𝜑 → ((!‘𝑄) · (𝑃 / 𝑄)) = (𝑃 · ((!‘𝑄) / 𝑄))) | 
| 68 | 63, 67 | eqtrd 2777 | . . . . 5
⊢ (𝜑 → ((!‘𝑄) · e) = (𝑃 · ((!‘𝑄) / 𝑄))) | 
| 69 | 21 | nnred 12281 | . . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ ℝ) | 
| 70 | 69 | leidd 11829 | . . . . . . . 8
⊢ (𝜑 → 𝑄 ≤ 𝑄) | 
| 71 |  | facdiv 14326 | . . . . . . . 8
⊢ ((𝑄 ∈ ℕ0
∧ 𝑄 ∈ ℕ
∧ 𝑄 ≤ 𝑄) → ((!‘𝑄) / 𝑄) ∈ ℕ) | 
| 72 | 54, 21, 70, 71 | syl3anc 1373 | . . . . . . 7
⊢ (𝜑 → ((!‘𝑄) / 𝑄) ∈ ℕ) | 
| 73 | 72 | nnzd 12640 | . . . . . 6
⊢ (𝜑 → ((!‘𝑄) / 𝑄) ∈ ℤ) | 
| 74 | 64, 73 | zmulcld 12728 | . . . . 5
⊢ (𝜑 → (𝑃 · ((!‘𝑄) / 𝑄)) ∈ ℤ) | 
| 75 | 68, 74 | eqeltrd 2841 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · e) ∈
ℤ) | 
| 76 | 1, 56, 17 | fsummulc2 15820 | . . . . 5
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)) = Σ𝑘 ∈ (0...𝑄)((!‘𝑄) · (𝐹‘𝑘))) | 
| 77 | 2 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → 𝑘 ∈ ℕ0) | 
| 78 | 77, 28 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (𝐹‘𝑘) = (1 / (!‘𝑘))) | 
| 79 | 78 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) · (𝐹‘𝑘)) = ((!‘𝑄) · (1 / (!‘𝑘)))) | 
| 80 | 56 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (!‘𝑄) ∈ ℂ) | 
| 81 | 2, 31 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (!‘𝑘) ∈ ℕ) | 
| 82 | 81 | nncnd 12282 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (!‘𝑘) ∈ ℂ) | 
| 83 |  | facne0 14325 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ≠
0) | 
| 84 | 77, 83 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → (!‘𝑘) ≠ 0) | 
| 85 | 80, 82, 84 | divrecd 12046 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) / (!‘𝑘)) = ((!‘𝑄) · (1 / (!‘𝑘)))) | 
| 86 | 79, 85 | eqtr4d 2780 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) · (𝐹‘𝑘)) = ((!‘𝑄) / (!‘𝑘))) | 
| 87 |  | permnn 14365 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑄) → ((!‘𝑄) / (!‘𝑘)) ∈ ℕ) | 
| 88 | 87 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) / (!‘𝑘)) ∈ ℕ) | 
| 89 | 86, 88 | eqeltrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) · (𝐹‘𝑘)) ∈ ℕ) | 
| 90 | 89 | nnzd 12640 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑄)) → ((!‘𝑄) · (𝐹‘𝑘)) ∈ ℤ) | 
| 91 | 1, 90 | fsumzcl 15771 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑄)((!‘𝑄) · (𝐹‘𝑘)) ∈ ℤ) | 
| 92 | 76, 91 | eqeltrd 2841 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘)) ∈ ℤ) | 
| 93 | 75, 92 | zsubcld 12727 | . . 3
⊢ (𝜑 → (((!‘𝑄) · e) −
((!‘𝑄) ·
Σ𝑘 ∈ (0...𝑄)(𝐹‘𝑘))) ∈ ℤ) | 
| 94 | 61, 93 | eqeltrd 2841 | . 2
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ∈ ℤ) | 
| 95 |  | 0zd 12625 | . . 3
⊢ (𝜑 → 0 ∈
ℤ) | 
| 96 | 55 | nnrpd 13075 | . . . . 5
⊢ (𝜑 → (!‘𝑄) ∈
ℝ+) | 
| 97 | 96, 37 | rpmulcld 13093 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ∈
ℝ+) | 
| 98 | 97 | rpgt0d 13080 | . . 3
⊢ (𝜑 → 0 < ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 99 | 22 | peano2nnd 12283 | . . . . . . . 8
⊢ (𝜑 → ((𝑄 + 1) + 1) ∈ ℕ) | 
| 100 | 99 | nnred 12281 | . . . . . . 7
⊢ (𝜑 → ((𝑄 + 1) + 1) ∈ ℝ) | 
| 101 | 23 | faccld 14323 | . . . . . . . 8
⊢ (𝜑 → (!‘(𝑄 + 1)) ∈
ℕ) | 
| 102 | 101, 22 | nnmulcld 12319 | . . . . . . 7
⊢ (𝜑 → ((!‘(𝑄 + 1)) · (𝑄 + 1)) ∈
ℕ) | 
| 103 | 100, 102 | nndivred 12320 | . . . . . 6
⊢ (𝜑 → (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))) ∈ ℝ) | 
| 104 | 55 | nnrecred 12317 | . . . . . 6
⊢ (𝜑 → (1 / (!‘𝑄)) ∈
ℝ) | 
| 105 |  | abs1 15336 | . . . . . . . . . . . 12
⊢
(abs‘1) = 1 | 
| 106 | 105 | oveq1i 7441 | . . . . . . . . . . 11
⊢
((abs‘1)↑𝑛) = (1↑𝑛) | 
| 107 | 106 | oveq1i 7441 | . . . . . . . . . 10
⊢
(((abs‘1)↑𝑛) / (!‘𝑛)) = ((1↑𝑛) / (!‘𝑛)) | 
| 108 | 107 | mpteq2i 5247 | . . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
↦ (((abs‘1)↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦
((1↑𝑛) /
(!‘𝑛))) | 
| 109 | 9, 108 | eqtr4i 2768 | . . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦
(((abs‘1)↑𝑛) /
(!‘𝑛))) | 
| 110 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((((abs‘1)↑(𝑄 + 1)) / (!‘(𝑄 + 1))) · ((1 / ((𝑄 + 1) + 1))↑𝑛))) = (𝑛 ∈ ℕ0 ↦
((((abs‘1)↑(𝑄 +
1)) / (!‘(𝑄 + 1)))
· ((1 / ((𝑄 + 1) +
1))↑𝑛))) | 
| 111 |  | 1le1 11891 | . . . . . . . . . 10
⊢ 1 ≤
1 | 
| 112 | 105, 111 | eqbrtri 5164 | . . . . . . . . 9
⊢
(abs‘1) ≤ 1 | 
| 113 | 112 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (abs‘1) ≤
1) | 
| 114 | 9, 109, 110, 22, 13, 113 | eftlub 16145 | . . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ≤ (((abs‘1)↑(𝑄 + 1)) · (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))))) | 
| 115 | 37 | rprege0d 13084 | . . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘))) | 
| 116 |  | absid 15335 | . . . . . . . 8
⊢
((Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ∈ ℝ ∧ 0 ≤ Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) | 
| 117 | 115, 116 | syl 17 | . . . . . . 7
⊢ (𝜑 → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) = Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) | 
| 118 | 105 | oveq1i 7441 | . . . . . . . . . 10
⊢
((abs‘1)↑(𝑄 + 1)) = (1↑(𝑄 + 1)) | 
| 119 | 22 | nnzd 12640 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄 + 1) ∈ ℤ) | 
| 120 |  | 1exp 14132 | . . . . . . . . . . 11
⊢ ((𝑄 + 1) ∈ ℤ →
(1↑(𝑄 + 1)) =
1) | 
| 121 | 119, 120 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (1↑(𝑄 + 1)) = 1) | 
| 122 | 118, 121 | eqtrid 2789 | . . . . . . . . 9
⊢ (𝜑 → ((abs‘1)↑(𝑄 + 1)) = 1) | 
| 123 | 122 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 →
(((abs‘1)↑(𝑄 +
1)) · (((𝑄 + 1) + 1)
/ ((!‘(𝑄 + 1))
· (𝑄 + 1)))) = (1
· (((𝑄 + 1) + 1) /
((!‘(𝑄 + 1)) ·
(𝑄 +
1))))) | 
| 124 | 103 | recnd 11289 | . . . . . . . . 9
⊢ (𝜑 → (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))) ∈ ℂ) | 
| 125 | 124 | mullidd 11279 | . . . . . . . 8
⊢ (𝜑 → (1 · (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1)))) = (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1)))) | 
| 126 | 123, 125 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 →
(((abs‘1)↑(𝑄 +
1)) · (((𝑄 + 1) + 1)
/ ((!‘(𝑄 + 1))
· (𝑄 + 1)))) =
(((𝑄 + 1) + 1) /
((!‘(𝑄 + 1)) ·
(𝑄 + 1)))) | 
| 127 | 114, 117,
126 | 3brtr3d 5174 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) ≤ (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1)))) | 
| 128 | 22 | nnred 12281 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄 + 1) ∈ ℝ) | 
| 129 | 128, 128 | readdcld 11290 | . . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) + (𝑄 + 1)) ∈ ℝ) | 
| 130 | 128, 128 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) · (𝑄 + 1)) ∈ ℝ) | 
| 131 |  | 1red 11262 | . . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℝ) | 
| 132 | 21 | nnge1d 12314 | . . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 𝑄) | 
| 133 |  | 1nn 12277 | . . . . . . . . . . . 12
⊢ 1 ∈
ℕ | 
| 134 |  | nnleltp1 12673 | . . . . . . . . . . . 12
⊢ ((1
∈ ℕ ∧ 𝑄
∈ ℕ) → (1 ≤ 𝑄 ↔ 1 < (𝑄 + 1))) | 
| 135 | 133, 21, 134 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → (1 ≤ 𝑄 ↔ 1 < (𝑄 + 1))) | 
| 136 | 132, 135 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → 1 < (𝑄 + 1)) | 
| 137 | 131, 128,
128, 136 | ltadd2dd 11420 | . . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) + 1) < ((𝑄 + 1) + (𝑄 + 1))) | 
| 138 | 22 | nncnd 12282 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑄 + 1) ∈ ℂ) | 
| 139 | 138 | 2timesd 12509 | . . . . . . . . . 10
⊢ (𝜑 → (2 · (𝑄 + 1)) = ((𝑄 + 1) + (𝑄 + 1))) | 
| 140 |  | df-2 12329 | . . . . . . . . . . . 12
⊢ 2 = (1 +
1) | 
| 141 | 131, 69, 131, 132 | leadd1dd 11877 | . . . . . . . . . . . 12
⊢ (𝜑 → (1 + 1) ≤ (𝑄 + 1)) | 
| 142 | 140, 141 | eqbrtrid 5178 | . . . . . . . . . . 11
⊢ (𝜑 → 2 ≤ (𝑄 + 1)) | 
| 143 |  | 2re 12340 | . . . . . . . . . . . . 13
⊢ 2 ∈
ℝ | 
| 144 | 143 | a1i 11 | . . . . . . . . . . . 12
⊢ (𝜑 → 2 ∈
ℝ) | 
| 145 | 22 | nngt0d 12315 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 < (𝑄 + 1)) | 
| 146 |  | lemul1 12119 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ ∧ (𝑄 +
1) ∈ ℝ ∧ ((𝑄
+ 1) ∈ ℝ ∧ 0 < (𝑄 + 1))) → (2 ≤ (𝑄 + 1) ↔ (2 · (𝑄 + 1)) ≤ ((𝑄 + 1) · (𝑄 + 1)))) | 
| 147 | 144, 128,
128, 145, 146 | syl112anc 1376 | . . . . . . . . . . 11
⊢ (𝜑 → (2 ≤ (𝑄 + 1) ↔ (2 · (𝑄 + 1)) ≤ ((𝑄 + 1) · (𝑄 + 1)))) | 
| 148 | 142, 147 | mpbid 232 | . . . . . . . . . 10
⊢ (𝜑 → (2 · (𝑄 + 1)) ≤ ((𝑄 + 1) · (𝑄 + 1))) | 
| 149 | 139, 148 | eqbrtrrd 5167 | . . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) + (𝑄 + 1)) ≤ ((𝑄 + 1) · (𝑄 + 1))) | 
| 150 | 100, 129,
130, 137, 149 | ltletrd 11421 | . . . . . . . 8
⊢ (𝜑 → ((𝑄 + 1) + 1) < ((𝑄 + 1) · (𝑄 + 1))) | 
| 151 |  | facp1 14317 | . . . . . . . . . . . . 13
⊢ (𝑄 ∈ ℕ0
→ (!‘(𝑄 + 1)) =
((!‘𝑄) ·
(𝑄 + 1))) | 
| 152 | 54, 151 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (!‘(𝑄 + 1)) = ((!‘𝑄) · (𝑄 + 1))) | 
| 153 | 152 | oveq1d 7446 | . . . . . . . . . . 11
⊢ (𝜑 → ((!‘(𝑄 + 1)) / (!‘𝑄)) = (((!‘𝑄) · (𝑄 + 1)) / (!‘𝑄))) | 
| 154 | 101 | nncnd 12282 | . . . . . . . . . . . 12
⊢ (𝜑 → (!‘(𝑄 + 1)) ∈
ℂ) | 
| 155 | 55 | nnne0d 12316 | . . . . . . . . . . . 12
⊢ (𝜑 → (!‘𝑄) ≠ 0) | 
| 156 | 154, 56, 155 | divrecd 12046 | . . . . . . . . . . 11
⊢ (𝜑 → ((!‘(𝑄 + 1)) / (!‘𝑄)) = ((!‘(𝑄 + 1)) · (1 /
(!‘𝑄)))) | 
| 157 | 138, 56, 155 | divcan3d 12048 | . . . . . . . . . . 11
⊢ (𝜑 → (((!‘𝑄) · (𝑄 + 1)) / (!‘𝑄)) = (𝑄 + 1)) | 
| 158 | 153, 156,
157 | 3eqtr3rd 2786 | . . . . . . . . . 10
⊢ (𝜑 → (𝑄 + 1) = ((!‘(𝑄 + 1)) · (1 / (!‘𝑄)))) | 
| 159 | 158 | oveq1d 7446 | . . . . . . . . 9
⊢ (𝜑 → ((𝑄 + 1) · (𝑄 + 1)) = (((!‘(𝑄 + 1)) · (1 / (!‘𝑄))) · (𝑄 + 1))) | 
| 160 | 104 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → (1 / (!‘𝑄)) ∈
ℂ) | 
| 161 | 154, 160,
138 | mul32d 11471 | . . . . . . . . 9
⊢ (𝜑 → (((!‘(𝑄 + 1)) · (1 /
(!‘𝑄))) ·
(𝑄 + 1)) =
(((!‘(𝑄 + 1))
· (𝑄 + 1)) ·
(1 / (!‘𝑄)))) | 
| 162 | 159, 161 | eqtrd 2777 | . . . . . . . 8
⊢ (𝜑 → ((𝑄 + 1) · (𝑄 + 1)) = (((!‘(𝑄 + 1)) · (𝑄 + 1)) · (1 / (!‘𝑄)))) | 
| 163 | 150, 162 | breqtrd 5169 | . . . . . . 7
⊢ (𝜑 → ((𝑄 + 1) + 1) < (((!‘(𝑄 + 1)) · (𝑄 + 1)) · (1 /
(!‘𝑄)))) | 
| 164 | 102 | nnred 12281 | . . . . . . . 8
⊢ (𝜑 → ((!‘(𝑄 + 1)) · (𝑄 + 1)) ∈
ℝ) | 
| 165 | 102 | nngt0d 12315 | . . . . . . . 8
⊢ (𝜑 → 0 < ((!‘(𝑄 + 1)) · (𝑄 + 1))) | 
| 166 |  | ltdivmul 12143 | . . . . . . . 8
⊢ ((((𝑄 + 1) + 1) ∈ ℝ ∧
(1 / (!‘𝑄)) ∈
ℝ ∧ (((!‘(𝑄
+ 1)) · (𝑄 + 1))
∈ ℝ ∧ 0 < ((!‘(𝑄 + 1)) · (𝑄 + 1)))) → ((((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))) < (1 / (!‘𝑄)) ↔ ((𝑄 + 1) + 1) < (((!‘(𝑄 + 1)) · (𝑄 + 1)) · (1 /
(!‘𝑄))))) | 
| 167 | 100, 104,
164, 165, 166 | syl112anc 1376 | . . . . . . 7
⊢ (𝜑 → ((((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))) < (1 / (!‘𝑄)) ↔ ((𝑄 + 1) + 1) < (((!‘(𝑄 + 1)) · (𝑄 + 1)) · (1 /
(!‘𝑄))))) | 
| 168 | 163, 167 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (((𝑄 + 1) + 1) / ((!‘(𝑄 + 1)) · (𝑄 + 1))) < (1 / (!‘𝑄))) | 
| 169 | 38, 103, 104, 127, 168 | lelttrd 11419 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) < (1 / (!‘𝑄))) | 
| 170 | 38, 131, 96 | ltmuldiv2d 13125 | . . . . 5
⊢ (𝜑 → (((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) < 1 ↔ Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘) < (1 / (!‘𝑄)))) | 
| 171 | 169, 170 | mpbird 257 | . . . 4
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) < 1) | 
| 172 |  | 0p1e1 12388 | . . . 4
⊢ (0 + 1) =
1 | 
| 173 | 171, 172 | breqtrrdi 5185 | . . 3
⊢ (𝜑 → ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) < (0 + 1)) | 
| 174 |  | btwnnz 12694 | . . 3
⊢ ((0
∈ ℤ ∧ 0 < ((!‘𝑄) · Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ∧ ((!‘𝑄) · Σ𝑘 ∈ (ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) < (0 + 1)) → ¬ ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ∈ ℤ) | 
| 175 | 95, 98, 173, 174 | syl3anc 1373 | . 2
⊢ (𝜑 → ¬ ((!‘𝑄) · Σ𝑘 ∈
(ℤ≥‘(𝑄 + 1))(𝐹‘𝑘)) ∈ ℤ) | 
| 176 | 94, 175 | pm2.65i 194 | 1
⊢  ¬
𝜑 |