eulerpartlemgc

	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	eulerpartlemgc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} t \leq S (A)$

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		2re	$⊢ 2 \in ℝ$
4	3	a1i	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2 \in ℝ$
5		bitsss	$⊢ bits (A (t)) \subseteq ℕ_{0}$
6		simprr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to n \in bits (A (t))$
7	5 6	sselid	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to n \in ℕ_{0}$
8	4 7	reexpcld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} \in ℝ$
9		simprl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to t \in ℕ$
10	9	nnred	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to t \in ℝ$
11	8 10	remulcld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} 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	14	adantrr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to A (t) \in ℕ_{0}$
16	15	nn0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to A (t) \in ℝ$
17	16 10	remulcld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to A (t) t \in ℝ$
18	1 2	eulerpartlemsf	$⊢ S : ({ℕ_{0}}^{ℕ}) \cap R ⟶ ℕ_{0}$
19	18	ffvelcdmi	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) \in ℕ_{0}$
20	19	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to S (A) \in ℕ_{0}$
21	20	nn0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to S (A) \in ℝ$
22	14	nn0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to A (t) \in ℝ$
23	22	adantrr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to A (t) \in ℝ$
24	9	nnrpd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to t \in ℝ^{+}$
25	24	rprege0d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to (t \in ℝ \land 0 \leq t)$
26		bitsfi	$⊢ A (t) \in ℕ_{0} \to bits (A (t)) \in Fin$
27	15 26	syl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to bits (A (t)) \in Fin$
28	3	a1i	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \land i \in bits (A (t))) \to 2 \in ℝ$
29	5	a1i	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to bits (A (t)) \subseteq ℕ_{0}$
30	29	sselda	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \land i \in bits (A (t))) \to i \in ℕ_{0}$
31	28 30	reexpcld	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \land i \in bits (A (t))) \to 2^{i} \in ℝ$
32		0le2	$⊢ 0 \leq 2$
33	32	a1i	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \land i \in bits (A (t))) \to 0 \leq 2$
34	28 30 33	expge0d	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \land i \in bits (A (t))) \to 0 \leq 2^{i}$
35	6	snssd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to \{n\} \subseteq bits (A (t))$
36	27 31 34 35	fsumless	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to \sum_{i \in \{n\}} 2^{i} \leq \sum_{i \in bits (A (t))} 2^{i}$
37	8	recnd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} \in ℂ$
38		oveq2	$⊢ i = n \to 2^{i} = 2^{n}$
39	38	sumsn	$⊢ (n \in bits (A (t)) \land 2^{n} \in ℂ) \to \sum_{i \in \{n\}} 2^{i} = 2^{n}$
40	6 37 39	syl2anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to \sum_{i \in \{n\}} 2^{i} = 2^{n}$
41		bitsinv1	$⊢ A (t) \in ℕ_{0} \to \sum_{i \in bits (A (t))} 2^{i} = A (t)$
42	15 41	syl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to \sum_{i \in bits (A (t))} 2^{i} = A (t)$
43	36 40 42	3brtr3d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} \leq A (t)$
44		lemul1a	$⊢ ((2^{n} \in ℝ \land A (t) \in ℝ \land (t \in ℝ \land 0 \leq t)) \land 2^{n} \leq A (t)) \to 2^{n} t \leq A (t) t$
45	8 23 25 43 44	syl31anc	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} t \leq A (t) t$
46		fzfid	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (1 \dots S (A))) \to (1 \dots S (A)) \in Fin$
47		elfznn	$⊢ k \in (1 \dots S (A)) \to k \in ℕ$
48		ffvelcdm	$⊢ (A : ℕ ⟶ ℕ_{0} \land k \in ℕ) \to A (k) \in ℕ_{0}$
49	13 47 48	syl2an	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to A (k) \in ℕ_{0}$
50	49	nn0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to A (k) \in ℝ$
51	47	adantl	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to k \in ℕ$
52	51	nnred	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to k \in ℝ$
53	50 52	remulcld	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to A (k) k \in ℝ$
54	53	adantlr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (1 \dots S (A))) \land k \in (1 \dots S (A))) \to A (k) k \in ℝ$
55	49	nn0ge0d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to 0 \leq A (k)$
56		0red	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to 0 \in ℝ$
57	51	nngt0d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to 0 < k$
58	56 52 57	ltled	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to 0 \leq k$
59	50 52 55 58	mulge0d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land k \in (1 \dots S (A))) \to 0 \leq A (k) k$
60	59	adantlr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (1 \dots S (A))) \land k \in (1 \dots S (A))) \to 0 \leq A (k) k$
61		fveq2	$⊢ k = t \to A (k) = A (t)$
62		id	$⊢ k = t \to k = t$
63	61 62	oveq12d	$⊢ k = t \to A (k) k = A (t) t$
64		simpr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (1 \dots S (A))) \to t \in (1 \dots S (A))$
65	46 54 60 63 64	fsumge1	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (1 \dots S (A))) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
66	65	adantlr	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \land t \in (1 \dots S (A))) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
67		eldif	$⊢ t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow (t \in ℕ \land \neg t \in (1 \dots S (A)))$
68		nndiffz1	$⊢ S (A) \in ℕ_{0} \to ℕ ∖ (1 \dots S (A)) = ℤ_{\geq (S (A) + 1)}$
69	68	eleq2d	$⊢ S (A) \in ℕ_{0} \to (t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow t \in ℤ_{\geq (S (A) + 1)})$
70	19 69	syl	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (t \in (ℕ ∖ (1 \dots S (A))) \leftrightarrow t \in ℤ_{\geq (S (A) + 1)})$
71	70	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)})$
72	1 2	eulerpartlems	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℤ_{\geq (S (A) + 1)}) \to A (t) = 0$
73	71 72	sylbi	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) = 0$
74	73	oveq1d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) t = 0 \cdot t$
75		simpr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to t \in (ℕ ∖ (1 \dots S (A)))$
76	75	eldifad	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to t \in ℕ$
77	76	nncnd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to t \in ℂ$
78	77	mul02d	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to 0 \cdot t = 0$
79	74 78	eqtrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) t = 0$
80		fzfid	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to (1 \dots S (A)) \in Fin$
81	80 53 59	fsumge0	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to 0 \leq \sum_{k = 1}^{S (A)} A (k) k$
82	81	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to 0 \leq \sum_{k = 1}^{S (A)} A (k) k$
83	79 82	eqbrtrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in (ℕ ∖ (1 \dots S (A)))) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
84	67 83	sylan2br	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land \neg t \in (1 \dots S (A)))) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
85	84	anassrs	$⊢ ((A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \land \neg t \in (1 \dots S (A))) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
86	66 85	pm2.61dan	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to A (t) t \leq \sum_{k = 1}^{S (A)} A (k) k$
87	1 2	eulerpartlemsv3	$⊢ A \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (A) = \sum_{k = 1}^{S (A)} A (k) k$
88	87	adantr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to S (A) = \sum_{k = 1}^{S (A)} A (k) k$
89	86 88	breqtrrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land t \in ℕ) \to A (t) t \leq S (A)$
90	89	adantrr	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to A (t) t \leq S (A)$
91	11 17 21 45 90	letrd	$⊢ (A \in (({ℕ_{0}}^{ℕ}) \cap R) \land (t \in ℕ \land n \in bits (A (t)))) \to 2^{n} t \leq S (A)$

Metamath Proof Explorer

Theorem eulerpartlemgc

Proof