Metamath Proof Explorer

Theorem eirrlem

Description: Lemma for eirr . (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses eirr.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
eirr.2 ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
eirr.3 ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
eirr.4 ⊢ ( 𝜑 → e = ( 𝑃 / 𝑄 ) )
Assertion eirrlem ¬ 𝜑

Proof

Step Hyp Ref Expression
1 eirr.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
2 eirr.2 ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
3 eirr.3 ⊢ ( 𝜑 → 𝑄 ∈ ℕ )
4 eirr.4 ⊢ ( 𝜑 → e = ( 𝑃 / 𝑄 ) )
5 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑄 ) ∈ Fin )
6 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑄 ) → 𝑘 ∈ ℕ0 )
7 nn0z ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ )
8 1exp ⊢ ( 𝑛 ∈ ℤ → ( 1 ↑ 𝑛 ) = 1 )
9 7 8 syl ⊢ ( 𝑛 ∈ ℕ0 → ( 1 ↑ 𝑛 ) = 1 )
10 9 oveq1d ⊢ ( 𝑛 ∈ ℕ0 → ( ( 1 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) = ( 1 / ( ! ‘ 𝑛 ) ) )
11 10 mpteq2ia ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 1 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
12 1 11 eqtr4i ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
13 12 eftval ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
15 ax-1cn ⊢ 1 ∈ ℂ
16 15 a1i ⊢ ( 𝜑 → 1 ∈ ℂ )
17 eftcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
18 16 17 sylan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 1 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
19 14 18 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
20 6 19 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
21 5 20 fsumcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
22 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
23 eqid ⊢ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) = ( ℤ≥ ‘ ( 𝑄 + 1 ) )
24 3 peano2nnd ⊢ ( 𝜑 → ( 𝑄 + 1 ) ∈ ℕ )
25 24 nnnn0d ⊢ ( 𝜑 → ( 𝑄 + 1 ) ∈ ℕ0 )
26 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
27 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ! ‘ 𝑛 ) = ( ! ‘ 𝑘 ) )
28 27 oveq2d ⊢ ( 𝑛 = 𝑘 → ( 1 / ( ! ‘ 𝑛 ) ) = ( 1 / ( ! ‘ 𝑘 ) ) )
29 ovex ⊢ ( 1 / ( ! ‘ 𝑘 ) ) ∈ V
30 28 1 29 fvmpt ⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( 1 / ( ! ‘ 𝑘 ) ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 1 / ( ! ‘ 𝑘 ) ) )
32 faccl ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
33 32 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
34 33 nnrpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ+ )
35 34 rpreccld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1 / ( ! ‘ 𝑘 ) ) ∈ ℝ+ )
36 31 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
37 12 efcllem ⊢ ( 1 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
38 16 37 syl ⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
39 22 23 25 26 36 38 isumrpcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
40 39 rpred ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
41 40 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
42 esum ⊢ e = Σ 𝑘 ∈ ℕ0 ( 1 / ( ! ‘ 𝑘 ) )
43 30 sumeq2i ⊢ Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ℕ0 ( 1 / ( ! ‘ 𝑘 ) )
44 42 43 eqtr4i ⊢ e = Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 )
45 22 23 25 26 19 38 isumsplit ⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑄 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
46 44 45 eqtrid ⊢ ( 𝜑 → e = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑄 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
47 3 nncnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
48 pncan ⊢ ( ( 𝑄 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑄 + 1 ) − 1 ) = 𝑄 )
49 47 15 48 sylancl ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) − 1 ) = 𝑄 )
50 49 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ( 𝑄 + 1 ) − 1 ) ) = ( 0 ... 𝑄 ) )
51 50 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( 𝑄 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) )
52 51 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑄 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
53 46 52 eqtrd ⊢ ( 𝜑 → e = ( Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
54 21 41 53 mvrladdd ⊢ ( 𝜑 → ( e − Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
55 54 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · ( e − Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
56 3 nnnn0d ⊢ ( 𝜑 → 𝑄 ∈ ℕ0 )
57 56 faccld ⊢ ( 𝜑 → ( ! ‘ 𝑄 ) ∈ ℕ )
58 57 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝑄 ) ∈ ℂ )
59 ere ⊢ e ∈ ℝ
60 59 recni ⊢ e ∈ ℂ
61 60 a1i ⊢ ( 𝜑 → e ∈ ℂ )
62 58 61 21 subdid ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · ( e − Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ( ! ‘ 𝑄 ) · e ) − ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ) )
63 55 62 eqtr3d ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( ( ! ‘ 𝑄 ) · e ) − ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ) )
64 4 oveq2d ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · e ) = ( ( ! ‘ 𝑄 ) · ( 𝑃 / 𝑄 ) ) )
65 2 zcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
66 3 nnne0d ⊢ ( 𝜑 → 𝑄 ≠ 0 )
67 58 65 47 66 div12d ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · ( 𝑃 / 𝑄 ) ) = ( 𝑃 · ( ( ! ‘ 𝑄 ) / 𝑄 ) ) )
68 64 67 eqtrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · e ) = ( 𝑃 · ( ( ! ‘ 𝑄 ) / 𝑄 ) ) )
69 3 nnred ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
70 69 leidd ⊢ ( 𝜑 → 𝑄 ≤ 𝑄 )
71 facdiv ⊢ ( ( 𝑄 ∈ ℕ0 ∧ 𝑄 ∈ ℕ ∧ 𝑄 ≤ 𝑄 ) → ( ( ! ‘ 𝑄 ) / 𝑄 ) ∈ ℕ )
72 56 3 70 71 syl3anc ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) / 𝑄 ) ∈ ℕ )
73 72 nnzd ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) / 𝑄 ) ∈ ℤ )
74 2 73 zmulcld ⊢ ( 𝜑 → ( 𝑃 · ( ( ! ‘ 𝑄 ) / 𝑄 ) ) ∈ ℤ )
75 68 74 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · e ) ∈ ℤ )
76 5 58 20 fsummulc2 ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) )
77 6 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → 𝑘 ∈ ℕ0 )
78 77 30 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 1 / ( ! ‘ 𝑘 ) ) )
79 78 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) = ( ( ! ‘ 𝑄 ) · ( 1 / ( ! ‘ 𝑘 ) ) ) )
80 58 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ! ‘ 𝑄 ) ∈ ℂ )
81 6 33 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ! ‘ 𝑘 ) ∈ ℕ )
82 81 nncnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
83 facne0 ⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ≠ 0 )
84 77 83 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ! ‘ 𝑘 ) ≠ 0 )
85 80 82 84 divrecd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) / ( ! ‘ 𝑘 ) ) = ( ( ! ‘ 𝑄 ) · ( 1 / ( ! ‘ 𝑘 ) ) ) )
86 79 85 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) = ( ( ! ‘ 𝑄 ) / ( ! ‘ 𝑘 ) ) )
87 permnn ⊢ ( 𝑘 ∈ ( 0 ... 𝑄 ) → ( ( ! ‘ 𝑄 ) / ( ! ‘ 𝑘 ) ) ∈ ℕ )
88 87 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) / ( ! ‘ 𝑘 ) ) ∈ ℕ )
89 86 88 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℕ )
90 89 nnzd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑄 ) ) → ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
91 5 90 fsumzcl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( ( ! ‘ 𝑄 ) · ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
92 76 91 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
93 75 92 zsubcld ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑄 ) · e ) − ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( 0 ... 𝑄 ) ( 𝐹 ‘ 𝑘 ) ) ) ∈ ℤ )
94 63 93 eqeltrd ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
95 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
96 57 nnrpd ⊢ ( 𝜑 → ( ! ‘ 𝑄 ) ∈ ℝ+ )
97 96 39 rpmulcld ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ+ )
98 97 rpgt0d ⊢ ( 𝜑 → 0 < ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
99 24 peano2nnd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) ∈ ℕ )
100 99 nnred ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) ∈ ℝ )
101 25 faccld ⊢ ( 𝜑 → ( ! ‘ ( 𝑄 + 1 ) ) ∈ ℕ )
102 101 24 nnmulcld ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ∈ ℕ )
103 100 102 nndivred ⊢ ( 𝜑 → ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ∈ ℝ )
104 57 nnrecred ⊢ ( 𝜑 → ( 1 / ( ! ‘ 𝑄 ) ) ∈ ℝ )
105 abs1 ⊢ ( abs ‘ 1 ) = 1
106 105 oveq1i ⊢ ( ( abs ‘ 1 ) ↑ 𝑛 ) = ( 1 ↑ 𝑛 )
107 106 oveq1i ⊢ ( ( ( abs ‘ 1 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) = ( ( 1 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) )
108 107 mpteq2i ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 1 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 1 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
109 12 108 eqtr4i ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( abs ‘ 1 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
110 eqid ⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) / ( ! ‘ ( 𝑄 + 1 ) ) ) · ( ( 1 / ( ( 𝑄 + 1 ) + 1 ) ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) / ( ! ‘ ( 𝑄 + 1 ) ) ) · ( ( 1 / ( ( 𝑄 + 1 ) + 1 ) ) ↑ 𝑛 ) ) )
111 1le1 ⊢ 1 ≤ 1
112 105 111 eqbrtri ⊢ ( abs ‘ 1 ) ≤ 1
113 112 a1i ⊢ ( 𝜑 → ( abs ‘ 1 ) ≤ 1 )
114 12 109 110 24 16 113 eftlub ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ≤ ( ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) · ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ) )
115 39 rprege0d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
116 absid ⊢ ( ( Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ ∧ 0 ≤ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
117 115 116 syl ⊢ ( 𝜑 → ( abs ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) )
118 105 oveq1i ⊢ ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) = ( 1 ↑ ( 𝑄 + 1 ) )
119 24 nnzd ⊢ ( 𝜑 → ( 𝑄 + 1 ) ∈ ℤ )
120 1exp ⊢ ( ( 𝑄 + 1 ) ∈ ℤ → ( 1 ↑ ( 𝑄 + 1 ) ) = 1 )
121 119 120 syl ⊢ ( 𝜑 → ( 1 ↑ ( 𝑄 + 1 ) ) = 1 )
122 118 121 eqtrid ⊢ ( 𝜑 → ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) = 1 )
123 122 oveq1d ⊢ ( 𝜑 → ( ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) · ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ) = ( 1 · ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ) )
124 103 recnd ⊢ ( 𝜑 → ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ∈ ℂ )
125 124 mulid2d ⊢ ( 𝜑 → ( 1 · ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ) = ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) )
126 123 125 eqtrd ⊢ ( 𝜑 → ( ( ( abs ‘ 1 ) ↑ ( 𝑄 + 1 ) ) · ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) ) = ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) )
127 114 117 126 3brtr3d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ≤ ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) )
128 24 nnred ⊢ ( 𝜑 → ( 𝑄 + 1 ) ∈ ℝ )
129 128 128 readdcld ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + ( 𝑄 + 1 ) ) ∈ ℝ )
130 128 128 remulcld ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) ∈ ℝ )
131 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
132 3 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑄 )
133 1nn ⊢ 1 ∈ ℕ
134 nnleltp1 ⊢ ( ( 1 ∈ ℕ ∧ 𝑄 ∈ ℕ ) → ( 1 ≤ 𝑄 ↔ 1 < ( 𝑄 + 1 ) ) )
135 133 3 134 sylancr ⊢ ( 𝜑 → ( 1 ≤ 𝑄 ↔ 1 < ( 𝑄 + 1 ) ) )
136 132 135 mpbid ⊢ ( 𝜑 → 1 < ( 𝑄 + 1 ) )
137 131 128 128 136 ltadd2dd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) < ( ( 𝑄 + 1 ) + ( 𝑄 + 1 ) ) )
138 24 nncnd ⊢ ( 𝜑 → ( 𝑄 + 1 ) ∈ ℂ )
139 138 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝑄 + 1 ) ) = ( ( 𝑄 + 1 ) + ( 𝑄 + 1 ) ) )
140 df-2 ⊢ 2 = ( 1 + 1 )
141 131 69 131 132 leadd1dd ⊢ ( 𝜑 → ( 1 + 1 ) ≤ ( 𝑄 + 1 ) )
142 140 141 eqbrtrid ⊢ ( 𝜑 → 2 ≤ ( 𝑄 + 1 ) )
143 2re ⊢ 2 ∈ ℝ
144 143 a1i ⊢ ( 𝜑 → 2 ∈ ℝ )
145 24 nngt0d ⊢ ( 𝜑 → 0 < ( 𝑄 + 1 ) )
146 lemul1 ⊢ ( ( 2 ∈ ℝ ∧ ( 𝑄 + 1 ) ∈ ℝ ∧ ( ( 𝑄 + 1 ) ∈ ℝ ∧ 0 < ( 𝑄 + 1 ) ) ) → ( 2 ≤ ( 𝑄 + 1 ) ↔ ( 2 · ( 𝑄 + 1 ) ) ≤ ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) ) )
147 144 128 128 145 146 syl112anc ⊢ ( 𝜑 → ( 2 ≤ ( 𝑄 + 1 ) ↔ ( 2 · ( 𝑄 + 1 ) ) ≤ ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) ) )
148 142 147 mpbid ⊢ ( 𝜑 → ( 2 · ( 𝑄 + 1 ) ) ≤ ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) )
149 139 148 eqbrtrrd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + ( 𝑄 + 1 ) ) ≤ ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) )
150 100 129 130 137 149 ltletrd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) < ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) )
151 facp1 ⊢ ( 𝑄 ∈ ℕ0 → ( ! ‘ ( 𝑄 + 1 ) ) = ( ( ! ‘ 𝑄 ) · ( 𝑄 + 1 ) ) )
152 56 151 syl ⊢ ( 𝜑 → ( ! ‘ ( 𝑄 + 1 ) ) = ( ( ! ‘ 𝑄 ) · ( 𝑄 + 1 ) ) )
153 152 oveq1d ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑄 + 1 ) ) / ( ! ‘ 𝑄 ) ) = ( ( ( ! ‘ 𝑄 ) · ( 𝑄 + 1 ) ) / ( ! ‘ 𝑄 ) ) )
154 101 nncnd ⊢ ( 𝜑 → ( ! ‘ ( 𝑄 + 1 ) ) ∈ ℂ )
155 57 nnne0d ⊢ ( 𝜑 → ( ! ‘ 𝑄 ) ≠ 0 )
156 154 58 155 divrecd ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑄 + 1 ) ) / ( ! ‘ 𝑄 ) ) = ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) )
157 138 58 155 divcan3d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑄 ) · ( 𝑄 + 1 ) ) / ( ! ‘ 𝑄 ) ) = ( 𝑄 + 1 ) )
158 153 156 157 3eqtr3rd ⊢ ( 𝜑 → ( 𝑄 + 1 ) = ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) )
159 158 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) = ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) · ( 𝑄 + 1 ) ) )
160 104 recnd ⊢ ( 𝜑 → ( 1 / ( ! ‘ 𝑄 ) ) ∈ ℂ )
161 154 160 138 mul32d ⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) · ( 𝑄 + 1 ) ) = ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) )
162 159 161 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) · ( 𝑄 + 1 ) ) = ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) )
163 150 162 breqtrd ⊢ ( 𝜑 → ( ( 𝑄 + 1 ) + 1 ) < ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) )
164 102 nnred ⊢ ( 𝜑 → ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ∈ ℝ )
165 102 nngt0d ⊢ ( 𝜑 → 0 < ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) )
166 ltdivmul ⊢ ( ( ( ( 𝑄 + 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 ⊢ ( 𝜑 → ( ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) < ( 1 / ( ! ‘ 𝑄 ) ) ↔ ( ( 𝑄 + 1 ) + 1 ) < ( ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) · ( 1 / ( ! ‘ 𝑄 ) ) ) ) )
168 163 167 mpbird ⊢ ( 𝜑 → ( ( ( 𝑄 + 1 ) + 1 ) / ( ( ! ‘ ( 𝑄 + 1 ) ) · ( 𝑄 + 1 ) ) ) < ( 1 / ( ! ‘ 𝑄 ) ) )
169 40 103 104 127 168 lelttrd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 1 / ( ! ‘ 𝑄 ) ) )
170 40 131 96 ltmuldiv2d ⊢ ( 𝜑 → ( ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) < 1 ↔ Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) < ( 1 / ( ! ‘ 𝑄 ) ) ) )
171 169 170 mpbird ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) < 1 )
172 0p1e1 ⊢ ( 0 + 1 ) = 1
173 171 172 breqtrrdi ⊢ ( 𝜑 → ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) < ( 0 + 1 ) )
174 btwnnz ⊢ ( ( 0 ∈ ℤ ∧ 0 < ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ∧ ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) < ( 0 + 1 ) ) → ¬ ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
175 95 98 173 174 syl3anc ⊢ ( 𝜑 → ¬ ( ( ! ‘ 𝑄 ) · Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑄 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) ∈ ℤ )
176 94 175 pm2.65i ⊢ ¬ 𝜑