eulerpartlems

	Ref	Expression
Hypotheses	eulerpartlems.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
	eulerpartlems.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
Assertion	eulerpartlems	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℤ_{\geq (S (A) + 1)}) \to A (t) = 0$

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
2		eulerpartlems.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
3	1 2	eulerpartlemsf	$⊢ S : ({ℕ_{0}}^{ℕ}) \cap R ⟶ ℕ_{0}$
4	3	ffvelrni	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) \in ℕ_{0}$
5		nndiffz1	$⊢ S (A) \in ℕ_{0} \to ℕ ∖ (1 \dots S (A)) = ℤ_{\geq (S (A) + 1)}$
6	5	eleq2d	$⊢ S (A) \in ℕ_{0} \to (t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow t \in ℤ_{\geq (S (A) + 1)})$
7	4 6	syl	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow t \in ℤ_{\geq (S (A) + 1)})$
8	7	pm5.32i	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \leftrightarrow (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℤ_{\geq (S (A) + 1)})$
9		simpr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to t \in (ℕ ∖ (1 \dots S (A)))$
10		eldif	$⊢ t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow (t \in ℕ \land \neg t \in (1 \dots S (A)))$
11	9 10	sylib	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to (t \in ℕ \land \neg t \in (1 \dots S (A)))$
12	11	simpld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to t \in ℕ$
13	1 2	eulerpartlemelr	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (A : ℕ ⟶ ℕ_{0} \land A^{-1} [ℕ] \in Fin)$
14	13	simpld	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to A : ℕ ⟶ ℕ_{0}$
15	14	ffvelrnda	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to A (t) \in ℕ_{0}$
16	12 15	syldan	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) \in ℕ_{0}$
17		simpl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A \in (({ℕ_{0}}^{ℕ}) \cap R)$
18	4	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to S (A) \in ℕ_{0}$
19	11	simprd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to \neg t \in (1 \dots S (A))$
20		simpl	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to t \in ℕ$
21		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
22	20 21	eleqtrdi	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to t \in ℤ_{\geq 1}$
23		simpr	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to S (A) \in ℕ_{0}$
24	23	nn0zd	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to S (A) \in ℤ$
25		elfz5	$⊢ (t \in ℤ_{\geq 1} \land S (A) \in ℤ) \to (t \in (1 \dots S (A)) \leftrightarrow t \leq S (A))$
26	22 24 25	syl2anc	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to (t \in (1 \dots S (A)) \leftrightarrow t \leq S (A))$
27	26	notbid	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to (\neg t \in (1 \dots S (A)) \leftrightarrow \neg t \leq S (A))$
28	23	nn0red	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to S (A) \in ℝ$
29	20	nnred	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to t \in ℝ$
30	28 29	ltnled	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to (S (A) < t \leftrightarrow \neg t \leq S (A))$
31	27 30	bitr4d	$⊢ (t \in ℕ \land S (A) \in ℕ_{0}) \to (\neg t \in (1 \dots S (A)) \leftrightarrow S (A) < t)$
32	31	biimpa	$⊢ ((t \in ℕ \land S (A) \in ℕ_{0}) \land \neg t \in (1 \dots S (A))) \to S (A) < t$
33	12 18 19 32	syl21anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to S (A) < t$
34	1 2	eulerpartlemsv1	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) = \sum_{k \in ℕ} A (k) k$
35		fveq2	$⊢ k = t \to A (k) = A (t)$
36		id	$⊢ k = t \to k = t$
37	35 36	oveq12d	$⊢ k = t \to A (k) k = A (t) t$
38	37	cbvsumv	$⊢ \sum_{k \in ℕ} A (k) k = \sum_{t \in ℕ} A (t) t$
39	34 38	eqtr2di	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to \sum_{t \in ℕ} A (t) t = S (A)$
40		breq2	$⊢ t = l \to (S (A) < t \leftrightarrow S (A) < l)$
41		fveq2	$⊢ t = l \to A (t) = A (l)$
42	41	breq2d	$⊢ t = l \to (0 < A (t) \leftrightarrow 0 < A (l))$
43	40 42	anbi12d	$⊢ t = l \to ((S (A) < t \land 0 < A (t)) \leftrightarrow (S (A) < l \land 0 < A (l)))$
44	43	cbvrexvw	$⊢ \exists t \in ℕ (S (A) < t \land 0 < A (t)) \leftrightarrow \exists l \in ℕ (S (A) < l \land 0 < A (l))$
45	4	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land \exists l \in ℕ (S (A) < l \land 0 < A (l))) \to S (A) \in ℕ_{0}$
46	45	nn0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land \exists l \in ℕ (S (A) < l \land 0 < A (l))) \to S (A) \in ℝ$
47	4	ad2antrr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to S (A) \in ℕ_{0}$
48	47	nn0red	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to S (A) \in ℝ$
49		simpr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to l \in ℕ$
50	49	adantr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to l \in ℕ$
51	50	nnred	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to l \in ℝ$
52		1zzd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to 1 \in ℤ$
53	14	ad2antrr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to A : ℕ ⟶ ℕ_{0}$
54		simpr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to t \in ℕ$
55		eqidd	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to (m \in ℕ ⟼ A (m) m) = (m \in ℕ ⟼ A (m) m)$
56		simpr	$⊢ ((A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \land m = t) \to m = t$
57	56	fveq2d	$⊢ ((A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \land m = t) \to A (m) = A (t)$
58	57 56	oveq12d	$⊢ ((A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \land m = t) \to A (m) m = A (t) t$
59		simpr	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to t \in ℕ$
60		ffvelrn	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to A (t) \in ℕ_{0}$
61	59	nnnn0d	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to t \in ℕ_{0}$
62	60 61	nn0mulcld	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to A (t) t \in ℕ_{0}$
63	55 58 59 62	fvmptd	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ) \to (m \in ℕ ⟼ A (m) m) (t) = A (t) t$
64	53 54 63	syl2anc	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to (m \in ℕ ⟼ A (m) m) (t) = A (t) t$
65	14	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A : ℕ ⟶ ℕ_{0}$
66	65	ffvelrnda	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to A (t) \in ℕ_{0}$
67	54	nnnn0d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to t \in ℕ_{0}$
68	66 67	nn0mulcld	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to A (t) t \in ℕ_{0}$
69	68	nn0red	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to A (t) t \in ℝ$
70		fveq2	$⊢ m = t \to A (m) = A (t)$
71		id	$⊢ m = t \to m = t$
72	70 71	oveq12d	$⊢ m = t \to A (m) m = A (t) t$
73	72	cbvmptv	$⊢ (m \in ℕ ⟼ A (m) m) = (t \in ℕ ⟼ A (t) t)$
74	68 73	fmptd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to (m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℕ_{0}$
75		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
76		fss	$⊢ ((m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℕ_{0} \land ℕ_{0} \subseteq ℂ) \to (m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℂ$
77	74 75 76	sylancl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to (m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℂ$
78		nnex	$⊢ ℕ \in V$
79		0nn0	$⊢ 0 \in ℕ_{0}$
80		eqid	$⊢ ℂ ∖ \{0\} = ℂ ∖ \{0\}$
81	80	ffs2	$⊢ (ℕ \in V \land 0 \in ℕ_{0} \land (m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℂ) \to (m \in ℕ ⟼ A (m) m) supp 0 = {(m \in ℕ ⟼ A (m) m)}^{-1} [ℂ ∖ \{0\}]$
82	78 79 81	mp3an12	$⊢ (m \in ℕ ⟼ A (m) m) : ℕ ⟶ ℂ \to (m \in ℕ ⟼ A (m) m) supp 0 = {(m \in ℕ ⟼ A (m) m)}^{-1} [ℂ ∖ \{0\}]$
83	77 82	syl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to (m \in ℕ ⟼ A (m) m) supp 0 = {(m \in ℕ ⟼ A (m) m)}^{-1} [ℂ ∖ \{0\}]$
84		frnnn0supp	$⊢ (ℕ \in V \land A : ℕ ⟶ ℕ_{0}) \to A supp 0 = A^{-1} [ℕ]$
85	78 65 84	sylancr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A supp 0 = A^{-1} [ℕ]$
86	13	simprd	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to A^{-1} [ℕ] \in Fin$
87	86	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A^{-1} [ℕ] \in Fin$
88	85 87	eqeltrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A supp 0 \in Fin$
89	78	a1i	$⊢ A : ℕ ⟶ ℕ_{0} \to ℕ \in V$
90	79	a1i	$⊢ A : ℕ ⟶ ℕ_{0} \to 0 \in ℕ_{0}$
91		ffn	$⊢ A : ℕ ⟶ ℕ_{0} \to A Fn ℕ$
92		simp3	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to A (t) = 0$
93	92	oveq1d	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to A (t) t = 0 \cdot t$
94		simp2	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to t \in ℕ$
95	94	nncnd	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to t \in ℂ$
96	95	mul02d	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to 0 \cdot t = 0$
97	93 96	eqtrd	$⊢ (A : ℕ ⟶ ℕ_{0} \land t \in ℕ \land A (t) = 0) \to A (t) t = 0$
98	73 89 90 91 97	suppss3	$⊢ A : ℕ ⟶ ℕ_{0} \to (m \in ℕ ⟼ A (m) m) supp 0 \subseteq A supp 0$
99	65 98	syl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to (m \in ℕ ⟼ A (m) m) supp 0 \subseteq A supp 0$
100		ssfi	$⊢ (A supp 0 \in Fin \land (m \in ℕ ⟼ A (m) m) supp 0 \subseteq A supp 0) \to (m \in ℕ ⟼ A (m) m) supp 0 \in Fin$
101	88 99 100	syl2anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to (m \in ℕ ⟼ A (m) m) supp 0 \in Fin$
102	83 101	eqeltrrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to {(m \in ℕ ⟼ A (m) m)}^{-1} [ℂ ∖ \{0\}] \in Fin$
103	21 52 77 102	fsumcvg4	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to seq 1 (+ (m \in ℕ ⟼ A (m) m)) \in dom ⇝$
104	21 52 64 69 103	isumrecl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to \sum_{t \in ℕ} A (t) t \in ℝ$
105	104	adantr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to \sum_{t \in ℕ} A (t) t \in ℝ$
106		simprl	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to S (A) < l$
107	14	ffvelrnda	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A (l) \in ℕ_{0}$
108	107	adantr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to A (l) \in ℕ_{0}$
109	108	nn0red	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to A (l) \in ℝ$
110	109 51	remulcld	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to A (l) l \in ℝ$
111	50	nnnn0d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to l \in ℕ_{0}$
112	111	nn0ge0d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to 0 \leq l$
113		simprr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to 0 < A (l)$
114		elnnnn0b	$⊢ A (l) \in ℕ \leftrightarrow (A (l) \in ℕ_{0} \land 0 < A (l))$
115		nnge1	$⊢ A (l) \in ℕ \to 1 \leq A (l)$
116	114 115	sylbir	$⊢ (A (l) \in ℕ_{0} \land 0 < A (l)) \to 1 \leq A (l)$
117	108 113 116	syl2anc	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to 1 \leq A (l)$
118	51 109 112 117	lemulge12d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to l \leq A (l) l$
119	107	nn0cnd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A (l) \in ℂ$
120	49	nncnd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to l \in ℂ$
121	119 120	mulcld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A (l) l \in ℂ$
122		id	$⊢ t = l \to t = l$
123	41 122	oveq12d	$⊢ t = l \to A (t) t = A (l) l$
124	123	sumsn	$⊢ (l \in ℕ \land A (l) l \in ℂ) \to \sum_{t \in \{l\}} A (t) t = A (l) l$
125	49 121 124	syl2anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to \sum_{t \in \{l\}} A (t) t = A (l) l$
126		snfi	$⊢ \{l\} \in Fin$
127	126	a1i	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to \{l\} \in Fin$
128	49	snssd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to \{l\} \subseteq ℕ$
129	68	nn0ge0d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land t \in ℕ) \to 0 \leq A (t) t$
130	21 52 127 128 64 69 129 103	isumless	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to \sum_{t \in \{l\}} A (t) t \leq \sum_{t \in ℕ} A (t) t$
131	125 130	eqbrtrrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \to A (l) l \leq \sum_{t \in ℕ} A (t) t$
132	131	adantr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to A (l) l \leq \sum_{t \in ℕ} A (t) t$
133	51 110 105 118 132	letrd	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to l \leq \sum_{t \in ℕ} A (t) t$
134	48 51 105 106 133	ltletrd	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land l \in ℕ) \land (S (A) < l \land 0 < A (l))) \to S (A) < \sum_{t \in ℕ} A (t) t$
135	134	r19.29an	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land \exists l \in ℕ (S (A) < l \land 0 < A (l))) \to S (A) < \sum_{t \in ℕ} A (t) t$
136	46 135	gtned	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land \exists l \in ℕ (S (A) < l \land 0 < A (l))) \to \sum_{t \in ℕ} A (t) t \neq S (A)$
137	136	ex	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (\exists l \in ℕ (S (A) < l \land 0 < A (l)) \to \sum_{t \in ℕ} A (t) t \neq S (A))$
138	44 137	syl5bi	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (\exists t \in ℕ (S (A) < t \land 0 < A (t)) \to \sum_{t \in ℕ} A (t) t \neq S (A))$
139	138	necon2bd	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (\sum_{t \in ℕ} A (t) t = S (A) \to \neg \exists t \in ℕ (S (A) < t \land 0 < A (t)))$
140	39 139	mpd	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to \neg \exists t \in ℕ (S (A) < t \land 0 < A (t))$
141		ralnex	$⊢ \forall t \in ℕ \neg (S (A) < t \land 0 < A (t)) \leftrightarrow \neg \exists t \in ℕ (S (A) < t \land 0 < A (t))$
142	140 141	sylibr	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to \forall t \in ℕ \neg (S (A) < t \land 0 < A (t))$
143		imnan	$⊢ (S (A) < t \to \neg 0 < A (t)) \leftrightarrow \neg (S (A) < t \land 0 < A (t))$
144	143	ralbii	$⊢ \forall t \in ℕ (S (A) < t \to \neg 0 < A (t)) \leftrightarrow \forall t \in ℕ \neg (S (A) < t \land 0 < A (t))$
145	142 144	sylibr	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to \forall t \in ℕ (S (A) < t \to \neg 0 < A (t))$
146	145	r19.21bi	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to (S (A) < t \to \neg 0 < A (t))$
147	146	imp	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \land S (A) < t) \to \neg 0 < A (t)$
148	17 12 33 147	syl21anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to \neg 0 < A (t)$
149		nn0re	$⊢ A (t) \in ℕ_{0} \to A (t) \in ℝ$
150		0red	$⊢ A (t) \in ℕ_{0} \to 0 \in ℝ$
151	149 150	lenltd	$⊢ A (t) \in ℕ_{0} \to (A (t) \leq 0 \leftrightarrow \neg 0 < A (t))$
152		nn0le0eq0	$⊢ A (t) \in ℕ_{0} \to (A (t) \leq 0 \leftrightarrow A (t) = 0)$
153	151 152	bitr3d	$⊢ A (t) \in ℕ_{0} \to (\neg 0 < A (t) \leftrightarrow A (t) = 0)$
154	153	biimpa	$⊢ (A (t) \in ℕ_{0} \land \neg 0 < A (t)) \to A (t) = 0$
155	16 148 154	syl2anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) = 0$
156	8 155	sylbir	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℤ_{\geq (S (A) + 1)}) \to A (t) = 0$

Metamath Proof Explorer

Theorem eulerpartlems

Proof