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

Metamath Proof Explorer

Theorem eulerpartlems

Proof