ostth2lem2

	Ref	Expression
Hypotheses	qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
	qabsabv.a	$⊢ A = AbsVal (Q)$
	padic.j	$⊢ J = (q \in ℙ ⟼ (x \in ℚ ⟼ if (x = 0, 0, q^{- (q pCnt x)})))$
	ostth.k	$⊢ K = (x \in ℚ ⟼ if (x = 0, 0, 1))$
	ostth.1	$⊢ φ \to F \in A$
	ostth2.2	$⊢ φ \to N \in ℤ_{\geq 2}$
	ostth2.3	$⊢ φ \to 1 < F (N)$
	ostth2.4	$⊢ R = \frac{\log F (N)}{\log N}$
	ostth2.5	$⊢ φ \to M \in ℤ_{\geq 2}$
	ostth2.6	$⊢ S = \frac{\log F (M)}{\log M}$
	ostth2.7	$⊢ T = if (F (M) \leq 1, 1, F (M))$
Assertion	ostth2lem2	$⊢ (φ \land X \in ℕ_{0} \land Y \in (0 \dots M^{X} - 1)) \to F (Y) \leq M X T^{X}$

Proof

Step	Hyp	Ref	Expression
1		qrng.q	$⊢ Q = ℂ_{fld} ↾_{𝑠} ℚ$
2		qabsabv.a	$⊢ A = AbsVal (Q)$
3		padic.j	$⊢ J = (q \in ℙ ⟼ (x \in ℚ ⟼ if (x = 0, 0, q^{- (q pCnt x)})))$
4		ostth.k	$⊢ K = (x \in ℚ ⟼ if (x = 0, 0, 1))$
5		ostth.1	$⊢ φ \to F \in A$
6		ostth2.2	$⊢ φ \to N \in ℤ_{\geq 2}$
7		ostth2.3	$⊢ φ \to 1 < F (N)$
8		ostth2.4	$⊢ R = \frac{\log F (N)}{\log N}$
9		ostth2.5	$⊢ φ \to M \in ℤ_{\geq 2}$
10		ostth2.6	$⊢ S = \frac{\log F (M)}{\log M}$
11		ostth2.7	$⊢ T = if (F (M) \leq 1, 1, F (M))$
12		oveq2	$⊢ x = 0 \to M^{x} = M^{0}$
13	12	oveq1d	$⊢ x = 0 \to M^{x} - 1 = M^{0} - 1$
14	13	oveq2d	$⊢ x = 0 \to (0 \dots M^{x} - 1) = (0 \dots M^{0} - 1)$
15		oveq2	$⊢ x = 0 \to M x = M \cdot 0$
16		oveq2	$⊢ x = 0 \to T^{x} = T^{0}$
17	15 16	oveq12d	$⊢ x = 0 \to M x T^{x} = M \cdot 0 T^{0}$
18	17	breq2d	$⊢ x = 0 \to (F (k) \leq M x T^{x} \leftrightarrow F (k) \leq M \cdot 0 T^{0})$
19	14 18	raleqbidv	$⊢ x = 0 \to (\forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x} \leftrightarrow \forall k \in (0 \dots M^{0} - 1) F (k) \leq M \cdot 0 T^{0})$
20	19	imbi2d	$⊢ x = 0 \to ((φ \to \forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x}) \leftrightarrow (φ \to \forall k \in (0 \dots M^{0} - 1) F (k) \leq M \cdot 0 T^{0}))$
21		oveq2	$⊢ x = n \to M^{x} = M^{n}$
22	21	oveq1d	$⊢ x = n \to M^{x} - 1 = M^{n} - 1$
23	22	oveq2d	$⊢ x = n \to (0 \dots M^{x} - 1) = (0 \dots M^{n} - 1)$
24		oveq2	$⊢ x = n \to M x = M n$
25		oveq2	$⊢ x = n \to T^{x} = T^{n}$
26	24 25	oveq12d	$⊢ x = n \to M x T^{x} = M n T^{n}$
27	26	breq2d	$⊢ x = n \to (F (k) \leq M x T^{x} \leftrightarrow F (k) \leq M n T^{n})$
28	23 27	raleqbidv	$⊢ x = n \to (\forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x} \leftrightarrow \forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n})$
29	28	imbi2d	$⊢ x = n \to ((φ \to \forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x}) \leftrightarrow (φ \to \forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n}))$
30		oveq2	$⊢ x = n + 1 \to M^{x} = M^{n + 1}$
31	30	oveq1d	$⊢ x = n + 1 \to M^{x} - 1 = M^{n + 1} - 1$
32	31	oveq2d	$⊢ x = n + 1 \to (0 \dots M^{x} - 1) = (0 \dots M^{n + 1} - 1)$
33		oveq2	$⊢ x = n + 1 \to M x = M (n + 1)$
34		oveq2	$⊢ x = n + 1 \to T^{x} = T^{n + 1}$
35	33 34	oveq12d	$⊢ x = n + 1 \to M x T^{x} = M (n + 1) T^{n + 1}$
36	35	breq2d	$⊢ x = n + 1 \to (F (k) \leq M x T^{x} \leftrightarrow F (k) \leq M (n + 1) T^{n + 1})$
37	32 36	raleqbidv	$⊢ x = n + 1 \to (\forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x} \leftrightarrow \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1})$
38	37	imbi2d	$⊢ x = n + 1 \to ((φ \to \forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x}) \leftrightarrow (φ \to \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1}))$
39		oveq2	$⊢ x = X \to M^{x} = M^{X}$
40	39	oveq1d	$⊢ x = X \to M^{x} - 1 = M^{X} - 1$
41	40	oveq2d	$⊢ x = X \to (0 \dots M^{x} - 1) = (0 \dots M^{X} - 1)$
42		oveq2	$⊢ x = X \to M x = M X$
43		oveq2	$⊢ x = X \to T^{x} = T^{X}$
44	42 43	oveq12d	$⊢ x = X \to M x T^{x} = M X T^{X}$
45	44	breq2d	$⊢ x = X \to (F (k) \leq M x T^{x} \leftrightarrow F (k) \leq M X T^{X})$
46	41 45	raleqbidv	$⊢ x = X \to (\forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x} \leftrightarrow \forall k \in (0 \dots M^{X} - 1) F (k) \leq M X T^{X})$
47	46	imbi2d	$⊢ x = X \to ((φ \to \forall k \in (0 \dots M^{x} - 1) F (k) \leq M x T^{x}) \leftrightarrow (φ \to \forall k \in (0 \dots M^{X} - 1) F (k) \leq M X T^{X}))$
48		eluz2nn	$⊢ M \in ℤ_{\geq 2} \to M \in ℕ$
49	9 48	syl	$⊢ φ \to M \in ℕ$
50	49	nncnd	$⊢ φ \to M \in ℂ$
51	50	exp0d	$⊢ φ \to M^{0} = 1$
52	51	oveq1d	$⊢ φ \to M^{0} - 1 = 1 - 1$
53		1m1e0	$⊢ 1 - 1 = 0$
54	52 53	eqtrdi	$⊢ φ \to M^{0} - 1 = 0$
55	54	oveq2d	$⊢ φ \to (0 \dots M^{0} - 1) = (0 \dots 0)$
56	55	eleq2d	$⊢ φ \to (k \in (0 \dots M^{0} - 1) \leftrightarrow k \in (0 \dots 0))$
57		0le0	$⊢ 0 \leq 0$
58	57	a1i	$⊢ φ \to 0 \leq 0$
59	1	qrng0	$⊢ 0 = 0_{Q}$
60	2 59	abv0	$⊢ F \in A \to F (0) = 0$
61	5 60	syl	$⊢ φ \to F (0) = 0$
62	50	mul01d	$⊢ φ \to M \cdot 0 = 0$
63	62	oveq1d	$⊢ φ \to M \cdot 0 T^{0} = 0 \cdot T^{0}$
64		1re	$⊢ 1 \in ℝ$
65		nnq	$⊢ M \in ℕ \to M \in ℚ$
66	49 65	syl	$⊢ φ \to M \in ℚ$
67	1	qrngbas	$⊢ ℚ = {Base}_{Q}$
68	2 67	abvcl	$⊢ (F \in A \land M \in ℚ) \to F (M) \in ℝ$
69	5 66 68	syl2anc	$⊢ φ \to F (M) \in ℝ$
70		ifcl	$⊢ (1 \in ℝ \land F (M) \in ℝ) \to if (F (M) \leq 1, 1, F (M)) \in ℝ$
71	64 69 70	sylancr	$⊢ φ \to if (F (M) \leq 1, 1, F (M)) \in ℝ$
72	11 71	eqeltrid	$⊢ φ \to T \in ℝ$
73	72	recnd	$⊢ φ \to T \in ℂ$
74		0nn0	$⊢ 0 \in ℕ_{0}$
75		expcl	$⊢ (T \in ℂ \land 0 \in ℕ_{0}) \to T^{0} \in ℂ$
76	73 74 75	sylancl	$⊢ φ \to T^{0} \in ℂ$
77	76	mul02d	$⊢ φ \to 0 \cdot T^{0} = 0$
78	63 77	eqtrd	$⊢ φ \to M \cdot 0 T^{0} = 0$
79	58 61 78	3brtr4d	$⊢ φ \to F (0) \leq M \cdot 0 T^{0}$
80		elfz1eq	$⊢ k \in (0 \dots 0) \to k = 0$
81	80	fveq2d	$⊢ k \in (0 \dots 0) \to F (k) = F (0)$
82	81	breq1d	$⊢ k \in (0 \dots 0) \to (F (k) \leq M \cdot 0 T^{0} \leftrightarrow F (0) \leq M \cdot 0 T^{0})$
83	79 82	syl5ibrcom	$⊢ φ \to (k \in (0 \dots 0) \to F (k) \leq M \cdot 0 T^{0})$
84	56 83	sylbid	$⊢ φ \to (k \in (0 \dots M^{0} - 1) \to F (k) \leq M \cdot 0 T^{0})$
85	84	ralrimiv	$⊢ φ \to \forall k \in (0 \dots M^{0} - 1) F (k) \leq M \cdot 0 T^{0}$
86		fveq2	$⊢ k = j \to F (k) = F (j)$
87	86	breq1d	$⊢ k = j \to (F (k) \leq M n T^{n} \leftrightarrow F (j) \leq M n T^{n})$
88	87	cbvralvw	$⊢ \forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n} \leftrightarrow \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n}$
89	5	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F \in A$
90		elfzelz	$⊢ k \in (0 \dots M^{n + 1} - 1) \to k \in ℤ$
91	90	ad2antrl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \in ℤ$
92		zq	$⊢ k \in ℤ \to k \in ℚ$
93	91 92	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \in ℚ$
94	2 67	abvcl	$⊢ (F \in A \land k \in ℚ) \to F (k) \in ℝ$
95	89 93 94	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k) \in ℝ$
96	49	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℕ$
97		simplr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n \in ℕ_{0}$
98	96 97	nnexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} \in ℕ$
99	91 98	zmodcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \mod M^{n} \in ℕ_{0}$
100	99	nn0zd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \mod M^{n} \in ℤ$
101		zq	$⊢ k \mod M^{n} \in ℤ \to k \mod M^{n} \in ℚ$
102	100 101	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \mod M^{n} \in ℚ$
103	2 67	abvcl	$⊢ (F \in A \land k \mod M^{n} \in ℚ) \to F (k \mod M^{n}) \in ℝ$
104	89 102 103	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) \in ℝ$
105	96 65	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℚ$
106	89 105 68	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M) \in ℝ$
107	106 97	reexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} \in ℝ$
108	91	zred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \in ℝ$
109	108 98	nndivred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to \frac{k}{M^{n}} \in ℝ$
110	109	flcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ \in ℤ$
111		zq	$⊢ ⌊\frac{k}{M^{n}}⌋ \in ℤ \to ⌊\frac{k}{M^{n}}⌋ \in ℚ$
112	110 111	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ \in ℚ$
113	2 67	abvcl	$⊢ (F \in A \land ⌊\frac{k}{M^{n}}⌋ \in ℚ) \to F (⌊\frac{k}{M^{n}}⌋) \in ℝ$
114	89 112 113	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (⌊\frac{k}{M^{n}}⌋) \in ℝ$
115	107 114	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \in ℝ$
116	104 115	readdcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \in ℝ$
117	96	nnred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℝ$
118		nn0p1nn	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ$
119	118	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n + 1 \in ℕ$
120	119	nnred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n + 1 \in ℝ$
121	117 120	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) \in ℝ$
122	72	ad2antrr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to T \in ℝ$
123		peano2nn0	$⊢ n \in ℕ_{0} \to n + 1 \in ℕ_{0}$
124	123	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n + 1 \in ℕ_{0}$
125	122 124	reexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to T^{n + 1} \in ℝ$
126	121 125	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) T^{n + 1} \in ℝ$
127		nnq	$⊢ M^{n} \in ℕ \to M^{n} \in ℚ$
128	98 127	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} \in ℚ$
129		qmulcl	$⊢ (M^{n} \in ℚ \land ⌊\frac{k}{M^{n}}⌋ \in ℚ) \to M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℚ$
130	128 112 129	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℚ$
131		qex	$⊢ ℚ \in V$
132		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
133	1 132	ressplusg	$⊢ ℚ \in V \to + = +_{Q}$
134	131 133	ax-mp	$⊢ + = +_{Q}$
135	2 67 134	abvtri	$⊢ (F \in A \land k \mod M^{n} \in ℚ \land M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℚ) \to F ((k \mod M^{n}) + M^{n} ⌊\frac{k}{M^{n}}⌋) \leq F (k \mod M^{n}) + F (M^{n} ⌊\frac{k}{M^{n}}⌋)$
136	89 102 130 135	syl3anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F ((k \mod M^{n}) + M^{n} ⌊\frac{k}{M^{n}}⌋) \leq F (k \mod M^{n}) + F (M^{n} ⌊\frac{k}{M^{n}}⌋)$
137	98	nnrpd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} \in ℝ^{+}$
138		modval	$⊢ (k \in ℝ \land M^{n} \in ℝ^{+}) \to k \mod M^{n} = k - M^{n} ⌊\frac{k}{M^{n}}⌋$
139	108 137 138	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \mod M^{n} = k - M^{n} ⌊\frac{k}{M^{n}}⌋$
140	139	oveq1d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (k \mod M^{n}) + M^{n} ⌊\frac{k}{M^{n}}⌋ = k - M^{n} ⌊\frac{k}{M^{n}}⌋ + M^{n} ⌊\frac{k}{M^{n}}⌋$
141	108	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \in ℂ$
142		qcn	$⊢ M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℚ \to M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℂ$
143	130 142	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} ⌊\frac{k}{M^{n}}⌋ \in ℂ$
144	141 143	npcand	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k - M^{n} ⌊\frac{k}{M^{n}}⌋ + M^{n} ⌊\frac{k}{M^{n}}⌋ = k$
145	140 144	eqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (k \mod M^{n}) + M^{n} ⌊\frac{k}{M^{n}}⌋ = k$
146	145	fveq2d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F ((k \mod M^{n}) + M^{n} ⌊\frac{k}{M^{n}}⌋) = F (k)$
147		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
148	1 147	ressmulr	$⊢ ℚ \in V \to \times = \cdot_{Q}$
149	131 148	ax-mp	$⊢ \times = \cdot_{Q}$
150	2 67 149	abvmul	$⊢ (F \in A \land M^{n} \in ℚ \land ⌊\frac{k}{M^{n}}⌋ \in ℚ) \to F (M^{n} ⌊\frac{k}{M^{n}}⌋) = F (M^{n}) F (⌊\frac{k}{M^{n}}⌋)$
151	89 128 112 150	syl3anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M^{n} ⌊\frac{k}{M^{n}}⌋) = F (M^{n}) F (⌊\frac{k}{M^{n}}⌋)$
152	1 2	qabvexp	$⊢ (F \in A \land M \in ℚ \land n \in ℕ_{0}) \to F (M^{n}) = {F (M)}^{n}$
153	89 105 97 152	syl3anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M^{n}) = {F (M)}^{n}$
154	153	oveq1d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M^{n}) F (⌊\frac{k}{M^{n}}⌋) = {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋)$
155	151 154	eqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M^{n} ⌊\frac{k}{M^{n}}⌋) = {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋)$
156	155	oveq2d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) + F (M^{n} ⌊\frac{k}{M^{n}}⌋) = F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋)$
157	136 146 156	3brtr3d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k) \leq F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋)$
158	122 97	reexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to T^{n} \in ℝ$
159	121 158	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) T^{n} \in ℝ$
160		nn0re	$⊢ n \in ℕ_{0} \to n \in ℝ$
161	160	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n \in ℝ$
162	117 161	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M n \in ℝ$
163	162 158	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M n T^{n} \in ℝ$
164	117 158	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M T^{n} \in ℝ$
165		fveq2	$⊢ j = k \mod M^{n} \to F (j) = F (k \mod M^{n})$
166	165	breq1d	$⊢ j = k \mod M^{n} \to (F (j) \leq M n T^{n} \leftrightarrow F (k \mod M^{n}) \leq M n T^{n})$
167		simprr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n}$
168		zmodfz	$⊢ (k \in ℤ \land M^{n} \in ℕ) \to k \mod M^{n} \in (0 \dots M^{n} - 1)$
169	91 98 168	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \mod M^{n} \in (0 \dots M^{n} - 1)$
170	166 167 169	rspcdva	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) \leq M n T^{n}$
171	117 107	remulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M {F (M)}^{n} \in ℝ$
172	107	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} \in ℂ$
173	114	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (⌊\frac{k}{M^{n}}⌋) \in ℂ$
174	172 173	mulcomd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) = F (⌊\frac{k}{M^{n}}⌋) {F (M)}^{n}$
175	2 67	abvge0	$⊢ (F \in A \land M \in ℚ) \to 0 \leq F (M)$
176	89 105 175	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 \leq F (M)$
177	106 97 176	expge0d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 \leq {F (M)}^{n}$
178	110	zred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ \in ℝ$
179		elfzle1	$⊢ k \in (0 \dots M^{n + 1} - 1) \to 0 \leq k$
180	179	ad2antrl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 \leq k$
181	98	nnred	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n} \in ℝ$
182	98	nngt0d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 < M^{n}$
183		divge0	$⊢ ((k \in ℝ \land 0 \leq k) \land (M^{n} \in ℝ \land 0 < M^{n})) \to 0 \leq \frac{k}{M^{n}}$
184	108 180 181 182 183	syl22anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 \leq \frac{k}{M^{n}}$
185		flge0nn0	$⊢ (\frac{k}{M^{n}} \in ℝ \land 0 \leq \frac{k}{M^{n}}) \to ⌊\frac{k}{M^{n}}⌋ \in ℕ_{0}$
186	109 184 185	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ \in ℕ_{0}$
187	1 2	qabvle	$⊢ (F \in A \land ⌊\frac{k}{M^{n}}⌋ \in ℕ_{0}) \to F (⌊\frac{k}{M^{n}}⌋) \leq ⌊\frac{k}{M^{n}}⌋$
188	89 186 187	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (⌊\frac{k}{M^{n}}⌋) \leq ⌊\frac{k}{M^{n}}⌋$
189		simprl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k \in (0 \dots M^{n + 1} - 1)$
190		0z	$⊢ 0 \in ℤ$
191	96 124	nnexpcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n + 1} \in ℕ$
192	191	nnzd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n + 1} \in ℤ$
193		elfzm11	$⊢ (0 \in ℤ \land M^{n + 1} \in ℤ) \to (k \in (0 \dots M^{n + 1} - 1) \leftrightarrow (k \in ℤ \land 0 \leq k \land k < M^{n + 1}))$
194	190 192 193	sylancr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (k \in (0 \dots M^{n + 1} - 1) \leftrightarrow (k \in ℤ \land 0 \leq k \land k < M^{n + 1}))$
195	189 194	mpbid	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (k \in ℤ \land 0 \leq k \land k < M^{n + 1})$
196	195	simp3d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k < M^{n + 1}$
197	96	nncnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℂ$
198	197 97	expp1d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M^{n + 1} = M^{n} \cdot M$
199	196 198	breqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to k < M^{n} \cdot M$
200		ltdivmul	$⊢ (k \in ℝ \land M \in ℝ \land (M^{n} \in ℝ \land 0 < M^{n})) \to (\frac{k}{M^{n}} < M \leftrightarrow k < M^{n} \cdot M)$
201	108 117 181 182 200	syl112anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (\frac{k}{M^{n}} < M \leftrightarrow k < M^{n} \cdot M)$
202	199 201	mpbird	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to \frac{k}{M^{n}} < M$
203	96	nnzd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℤ$
204		fllt	$⊢ (\frac{k}{M^{n}} \in ℝ \land M \in ℤ) \to (\frac{k}{M^{n}} < M \leftrightarrow ⌊\frac{k}{M^{n}}⌋ < M)$
205	109 203 204	syl2anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (\frac{k}{M^{n}} < M \leftrightarrow ⌊\frac{k}{M^{n}}⌋ < M)$
206	202 205	mpbid	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ < M$
207	178 117 206	ltled	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to ⌊\frac{k}{M^{n}}⌋ \leq M$
208	114 178 117 188 207	letrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (⌊\frac{k}{M^{n}}⌋) \leq M$
209	114 117 107 177 208	lemul1ad	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (⌊\frac{k}{M^{n}}⌋) {F (M)}^{n} \leq M {F (M)}^{n}$
210	174 209	eqbrtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \leq M {F (M)}^{n}$
211	96	nnnn0d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \in ℕ_{0}$
212	211	nn0ge0d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 \leq M$
213		max1	$⊢ (F (M) \in ℝ \land 1 \in ℝ) \to F (M) \leq if (F (M) \leq 1, 1, F (M))$
214	106 64 213	sylancl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M) \leq if (F (M) \leq 1, 1, F (M))$
215	214 11	breqtrrdi	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (M) \leq T$
216		leexp1a	$⊢ ((F (M) \in ℝ \land T \in ℝ \land n \in ℕ_{0}) \land (0 \leq F (M) \land F (M) \leq T)) \to {F (M)}^{n} \leq T^{n}$
217	106 122 97 176 215 216	syl32anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} \leq T^{n}$
218	107 158 117 212 217	lemul2ad	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M {F (M)}^{n} \leq M T^{n}$
219	115 171 164 210 218	letrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \leq M T^{n}$
220	104 115 163 164 170 219	le2addd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \leq M n T^{n} + M T^{n}$
221		nn0cn	$⊢ n \in ℕ_{0} \to n \in ℂ$
222	221	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n \in ℂ$
223		1cnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 1 \in ℂ$
224	197 222 223	adddid	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) = M n + M \cdot 1$
225	197	mulid1d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M \cdot 1 = M$
226	225	oveq2d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M n + M \cdot 1 = M n + M$
227	224 226	eqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) = M n + M$
228	227	oveq1d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) T^{n} = (M n + M) T^{n}$
229	197 222	mulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M n \in ℂ$
230	158	recnd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to T^{n} \in ℂ$
231	229 197 230	adddird	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (M n + M) T^{n} = M n T^{n} + M T^{n}$
232	228 231	eqtrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) T^{n} = M n T^{n} + M T^{n}$
233	220 232	breqtrrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \leq M (n + 1) T^{n}$
234		max2	$⊢ (F (M) \in ℝ \land 1 \in ℝ) \to 1 \leq if (F (M) \leq 1, 1, F (M))$
235	106 64 234	sylancl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 1 \leq if (F (M) \leq 1, 1, F (M))$
236	235 11	breqtrrdi	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 1 \leq T$
237		nn0z	$⊢ n \in ℕ_{0} \to n \in ℤ$
238	237	ad2antlr	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n \in ℤ$
239		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
240	238 239	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n \in ℤ_{\geq n}$
241		peano2uz	$⊢ n \in ℤ_{\geq n} \to n + 1 \in ℤ_{\geq n}$
242	240 241	syl	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to n + 1 \in ℤ_{\geq n}$
243	122 236 242	leexp2ad	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to T^{n} \leq T^{n + 1}$
244	96 119	nnmulcld	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) \in ℕ$
245	244	nngt0d	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to 0 < M (n + 1)$
246		lemul2	$⊢ (T^{n} \in ℝ \land T^{n + 1} \in ℝ \land (M (n + 1) \in ℝ \land 0 < M (n + 1))) \to (T^{n} \leq T^{n + 1} \leftrightarrow M (n + 1) T^{n} \leq M (n + 1) T^{n + 1})$
247	158 125 121 245 246	syl112anc	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to (T^{n} \leq T^{n + 1} \leftrightarrow M (n + 1) T^{n} \leq M (n + 1) T^{n + 1})$
248	243 247	mpbid	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to M (n + 1) T^{n} \leq M (n + 1) T^{n + 1}$
249	116 159 126 233 248	letrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k \mod M^{n}) + {F (M)}^{n} F (⌊\frac{k}{M^{n}}⌋) \leq M (n + 1) T^{n + 1}$
250	95 116 126 157 249	letrd	$⊢ ((φ \land n \in ℕ_{0}) \land (k \in (0 \dots M^{n + 1} - 1) \land \forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n})) \to F (k) \leq M (n + 1) T^{n + 1}$
251	250	expr	$⊢ ((φ \land n \in ℕ_{0}) \land k \in (0 \dots M^{n + 1} - 1)) \to (\forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n} \to F (k) \leq M (n + 1) T^{n + 1})$
252	251	ralrimdva	$⊢ (φ \land n \in ℕ_{0}) \to (\forall j \in (0 \dots M^{n} - 1) F (j) \leq M n T^{n} \to \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1})$
253	88 252	syl5bi	$⊢ (φ \land n \in ℕ_{0}) \to (\forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n} \to \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1})$
254	253	expcom	$⊢ n \in ℕ_{0} \to (φ \to (\forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n} \to \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1}))$
255	254	a2d	$⊢ n \in ℕ_{0} \to ((φ \to \forall k \in (0 \dots M^{n} - 1) F (k) \leq M n T^{n}) \to (φ \to \forall k \in (0 \dots M^{n + 1} - 1) F (k) \leq M (n + 1) T^{n + 1}))$
256	20 29 38 47 85 255	nn0ind	$⊢ X \in ℕ_{0} \to (φ \to \forall k \in (0 \dots M^{X} - 1) F (k) \leq M X T^{X})$
257	256	impcom	$⊢ (φ \land X \in ℕ_{0}) \to \forall k \in (0 \dots M^{X} - 1) F (k) \leq M X T^{X}$
258		fveq2	$⊢ k = Y \to F (k) = F (Y)$
259	258	breq1d	$⊢ k = Y \to (F (k) \leq M X T^{X} \leftrightarrow F (Y) \leq M X T^{X})$
260	259	rspccv	$⊢ \forall k \in (0 \dots M^{X} - 1) F (k) \leq M X T^{X} \to (Y \in (0 \dots M^{X} - 1) \to F (Y) \leq M X T^{X})$
261	257 260	syl	$⊢ (φ \land X \in ℕ_{0}) \to (Y \in (0 \dots M^{X} - 1) \to F (Y) \leq M X T^{X})$
262	261	3impia	$⊢ (φ \land X \in ℕ_{0} \land Y \in (0 \dots M^{X} - 1)) \to F (Y) \leq M X T^{X}$

Metamath Proof Explorer

Theorem ostth2lem2

Proof