MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ostth2lem2 Structured version   Visualization version   GIF version

Theorem ostth2lem2 25040
Description: Lemma for ostth2 25043. (Contributed by Mario Carneiro, 10-Sep-2014.)
Hypotheses
Ref Expression
qrng.q 𝑄 = (ℂflds ℚ)
qabsabv.a 𝐴 = (AbsVal‘𝑄)
padic.j 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))
ostth.k 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))
ostth.1 (𝜑𝐹𝐴)
ostth2.2 (𝜑𝑁 ∈ (ℤ‘2))
ostth2.3 (𝜑 → 1 < (𝐹𝑁))
ostth2.4 𝑅 = ((log‘(𝐹𝑁)) / (log‘𝑁))
ostth2.5 (𝜑𝑀 ∈ (ℤ‘2))
ostth2.6 𝑆 = ((log‘(𝐹𝑀)) / (log‘𝑀))
ostth2.7 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
Assertion
Ref Expression
ostth2lem2 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Distinct variable groups:   𝑥,𝑀   𝑥,𝑞,𝜑   𝑥,𝑇   𝑥,𝑋   𝐴,𝑞,𝑥   𝑥,𝑁   𝑥,𝑄   𝐹,𝑞   𝑅,𝑞   𝑥,𝐹
Allowed substitution hints:   𝑄(𝑞)   𝑅(𝑥)   𝑆(𝑥,𝑞)   𝑇(𝑞)   𝐽(𝑥,𝑞)   𝐾(𝑥,𝑞)   𝑀(𝑞)   𝑁(𝑞)   𝑋(𝑞)   𝑌(𝑥,𝑞)

Proof of Theorem ostth2lem2
Dummy variables 𝑘 𝑛 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6535 . . . . . . . . 9 (𝑥 = 0 → (𝑀𝑥) = (𝑀↑0))
21oveq1d 6542 . . . . . . . 8 (𝑥 = 0 → ((𝑀𝑥) − 1) = ((𝑀↑0) − 1))
32oveq2d 6543 . . . . . . 7 (𝑥 = 0 → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑0) − 1)))
4 oveq2 6535 . . . . . . . . 9 (𝑥 = 0 → (𝑀 · 𝑥) = (𝑀 · 0))
5 oveq2 6535 . . . . . . . . 9 (𝑥 = 0 → (𝑇𝑥) = (𝑇↑0))
64, 5oveq12d 6545 . . . . . . . 8 (𝑥 = 0 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 0) · (𝑇↑0)))
76breq2d 4589 . . . . . . 7 (𝑥 = 0 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
83, 7raleqbidv 3128 . . . . . 6 (𝑥 = 0 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
98imbi2d 328 . . . . 5 (𝑥 = 0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))))
10 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀𝑥) = (𝑀𝑛))
1110oveq1d 6542 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀𝑥) − 1) = ((𝑀𝑛) − 1))
1211oveq2d 6543 . . . . . . 7 (𝑥 = 𝑛 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑛) − 1)))
13 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑀 · 𝑥) = (𝑀 · 𝑛))
14 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑛 → (𝑇𝑥) = (𝑇𝑛))
1513, 14oveq12d 6545 . . . . . . . 8 (𝑥 = 𝑛 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑛) · (𝑇𝑛)))
1615breq2d 4589 . . . . . . 7 (𝑥 = 𝑛 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1712, 16raleqbidv 3128 . . . . . 6 (𝑥 = 𝑛 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
1817imbi2d 328 . . . . 5 (𝑥 = 𝑛 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))))
19 oveq2 6535 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀𝑥) = (𝑀↑(𝑛 + 1)))
2019oveq1d 6542 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀𝑥) − 1) = ((𝑀↑(𝑛 + 1)) − 1))
2120oveq2d 6543 . . . . . . 7 (𝑥 = (𝑛 + 1) → (0...((𝑀𝑥) − 1)) = (0...((𝑀↑(𝑛 + 1)) − 1)))
22 oveq2 6535 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑀 · 𝑥) = (𝑀 · (𝑛 + 1)))
23 oveq2 6535 . . . . . . . . 9 (𝑥 = (𝑛 + 1) → (𝑇𝑥) = (𝑇↑(𝑛 + 1)))
2422, 23oveq12d 6545 . . . . . . . 8 (𝑥 = (𝑛 + 1) → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
2524breq2d 4589 . . . . . . 7 (𝑥 = (𝑛 + 1) → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2621, 25raleqbidv 3128 . . . . . 6 (𝑥 = (𝑛 + 1) → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
2726imbi2d 328 . . . . 5 (𝑥 = (𝑛 + 1) → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
28 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀𝑥) = (𝑀𝑋))
2928oveq1d 6542 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀𝑥) − 1) = ((𝑀𝑋) − 1))
3029oveq2d 6543 . . . . . . 7 (𝑥 = 𝑋 → (0...((𝑀𝑥) − 1)) = (0...((𝑀𝑋) − 1)))
31 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑀 · 𝑥) = (𝑀 · 𝑋))
32 oveq2 6535 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑇𝑥) = (𝑇𝑋))
3331, 32oveq12d 6545 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑀 · 𝑥) · (𝑇𝑥)) = ((𝑀 · 𝑋) · (𝑇𝑋)))
3433breq2d 4589 . . . . . . 7 (𝑥 = 𝑋 → ((𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ (𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3530, 34raleqbidv 3128 . . . . . 6 (𝑥 = 𝑋 → (∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥)) ↔ ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
3635imbi2d 328 . . . . 5 (𝑥 = 𝑋 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑥) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑥) · (𝑇𝑥))) ↔ (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))))
37 ostth2.5 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘2))
38 eluz2nn 11558 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘2) → 𝑀 ∈ ℕ)
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ ℕ)
4039nncnd 10883 . . . . . . . . . . . 12 (𝜑𝑀 ∈ ℂ)
4140exp0d 12819 . . . . . . . . . . 11 (𝜑 → (𝑀↑0) = 1)
4241oveq1d 6542 . . . . . . . . . 10 (𝜑 → ((𝑀↑0) − 1) = (1 − 1))
43 1m1e0 10936 . . . . . . . . . 10 (1 − 1) = 0
4442, 43syl6eq 2659 . . . . . . . . 9 (𝜑 → ((𝑀↑0) − 1) = 0)
4544oveq2d 6543 . . . . . . . 8 (𝜑 → (0...((𝑀↑0) − 1)) = (0...0))
4645eleq2d 2672 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) ↔ 𝑘 ∈ (0...0)))
47 0le0 10957 . . . . . . . . . 10 0 ≤ 0
4847a1i 11 . . . . . . . . 9 (𝜑 → 0 ≤ 0)
49 ostth.1 . . . . . . . . . 10 (𝜑𝐹𝐴)
50 qabsabv.a . . . . . . . . . . 11 𝐴 = (AbsVal‘𝑄)
51 qrng.q . . . . . . . . . . . 12 𝑄 = (ℂflds ℚ)
5251qrng0 25027 . . . . . . . . . . 11 0 = (0g𝑄)
5350, 52abv0 18600 . . . . . . . . . 10 (𝐹𝐴 → (𝐹‘0) = 0)
5449, 53syl 17 . . . . . . . . 9 (𝜑 → (𝐹‘0) = 0)
5540mul01d 10086 . . . . . . . . . . 11 (𝜑 → (𝑀 · 0) = 0)
5655oveq1d 6542 . . . . . . . . . 10 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = (0 · (𝑇↑0)))
57 ostth2.7 . . . . . . . . . . . . . 14 𝑇 = if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀))
58 1re 9895 . . . . . . . . . . . . . . 15 1 ∈ ℝ
59 nnq 11633 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℚ)
6039, 59syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℚ)
6151qrngbas 25025 . . . . . . . . . . . . . . . . 17 ℚ = (Base‘𝑄)
6250, 61abvcl 18593 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ) → (𝐹𝑀) ∈ ℝ)
6349, 60, 62syl2anc 690 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹𝑀) ∈ ℝ)
64 ifcl 4079 . . . . . . . . . . . . . . 15 ((1 ∈ ℝ ∧ (𝐹𝑀) ∈ ℝ) → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6558, 63, 64sylancr 693 . . . . . . . . . . . . . 14 (𝜑 → if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)) ∈ ℝ)
6657, 65syl5eqel 2691 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ ℝ)
6766recnd 9924 . . . . . . . . . . . 12 (𝜑𝑇 ∈ ℂ)
68 0nn0 11154 . . . . . . . . . . . 12 0 ∈ ℕ0
69 expcl 12695 . . . . . . . . . . . 12 ((𝑇 ∈ ℂ ∧ 0 ∈ ℕ0) → (𝑇↑0) ∈ ℂ)
7067, 68, 69sylancl 692 . . . . . . . . . . 11 (𝜑 → (𝑇↑0) ∈ ℂ)
7170mul02d 10085 . . . . . . . . . 10 (𝜑 → (0 · (𝑇↑0)) = 0)
7256, 71eqtrd 2643 . . . . . . . . 9 (𝜑 → ((𝑀 · 0) · (𝑇↑0)) = 0)
7348, 54, 723brtr4d 4609 . . . . . . . 8 (𝜑 → (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0)))
74 elfz1eq 12178 . . . . . . . . . 10 (𝑘 ∈ (0...0) → 𝑘 = 0)
7574fveq2d 6092 . . . . . . . . 9 (𝑘 ∈ (0...0) → (𝐹𝑘) = (𝐹‘0))
7675breq1d 4587 . . . . . . . 8 (𝑘 ∈ (0...0) → ((𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)) ↔ (𝐹‘0) ≤ ((𝑀 · 0) · (𝑇↑0))))
7773, 76syl5ibrcom 235 . . . . . . 7 (𝜑 → (𝑘 ∈ (0...0) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7846, 77sylbid 228 . . . . . 6 (𝜑 → (𝑘 ∈ (0...((𝑀↑0) − 1)) → (𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0))))
7978ralrimiv 2947 . . . . 5 (𝜑 → ∀𝑘 ∈ (0...((𝑀↑0) − 1))(𝐹𝑘) ≤ ((𝑀 · 0) · (𝑇↑0)))
80 fveq2 6088 . . . . . . . . . 10 (𝑘 = 𝑗 → (𝐹𝑘) = (𝐹𝑗))
8180breq1d 4587 . . . . . . . . 9 (𝑘 = 𝑗 → ((𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
8281cbvralv 3146 . . . . . . . 8 (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
8349ad2antrr 757 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝐹𝐴)
84 elfzelz 12168 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 𝑘 ∈ ℤ)
8584ad2antrl 759 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℤ)
86 zq 11626 . . . . . . . . . . . . 13 (𝑘 ∈ ℤ → 𝑘 ∈ ℚ)
8785, 86syl 17 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℚ)
8850, 61abvcl 18593 . . . . . . . . . . . 12 ((𝐹𝐴𝑘 ∈ ℚ) → (𝐹𝑘) ∈ ℝ)
8983, 87, 88syl2anc 690 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ∈ ℝ)
9039ad2antrr 757 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ)
91 simplr 787 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℕ0)
9290, 91nnexpcld 12847 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℕ)
9385, 92zmodcld 12508 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℕ0)
9493nn0zd 11312 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℤ)
95 zq 11626 . . . . . . . . . . . . . 14 ((𝑘 mod (𝑀𝑛)) ∈ ℤ → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9694, 95syl 17 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ ℚ)
9750, 61abvcl 18593 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9883, 96, 97syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ∈ ℝ)
9990, 59syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℚ)
10083, 99, 62syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ∈ ℝ)
101100, 91reexpcld 12842 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℝ)
10285zred 11314 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℝ)
103102, 92nndivred 10916 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) ∈ ℝ)
104103flcld 12416 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ)
105 zq 11626 . . . . . . . . . . . . . . 15 ((⌊‘(𝑘 / (𝑀𝑛))) ∈ ℤ → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
106104, 105syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ)
10750, 61abvcl 18593 . . . . . . . . . . . . . 14 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
10883, 106, 107syl2anc 690 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℝ)
109101, 108remulcld 9926 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ∈ ℝ)
11098, 109readdcld 9925 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ∈ ℝ)
11190nnred 10882 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℝ)
112 nn0p1nn 11179 . . . . . . . . . . . . . . 15 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ)
113112ad2antlr 758 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ)
114113nnred 10882 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℝ)
115111, 114remulcld 9926 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℝ)
11666ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑇 ∈ ℝ)
117 peano2nn0 11180 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
118117ad2antlr 758 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ ℕ0)
119116, 118reexpcld 12842 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇↑(𝑛 + 1)) ∈ ℝ)
120115, 119remulcld 9926 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))) ∈ ℝ)
121 nnq 11633 . . . . . . . . . . . . . . 15 ((𝑀𝑛) ∈ ℕ → (𝑀𝑛) ∈ ℚ)
12292, 121syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℚ)
123 qmulcl 11638 . . . . . . . . . . . . . 14 (((𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
124122, 106, 123syl2anc 690 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ)
125 qex 11632 . . . . . . . . . . . . . . 15 ℚ ∈ V
126 cnfldadd 19518 . . . . . . . . . . . . . . . 16 + = (+g‘ℂfld)
12751, 126ressplusg 15764 . . . . . . . . . . . . . . 15 (ℚ ∈ V → + = (+g𝑄))
128125, 127ax-mp 5 . . . . . . . . . . . . . 14 + = (+g𝑄)
12950, 61, 128abvtri 18599 . . . . . . . . . . . . 13 ((𝐹𝐴 ∧ (𝑘 mod (𝑀𝑛)) ∈ ℚ ∧ ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13083, 96, 124, 129syl3anc 1317 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))))
13192nnrpd 11702 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ+)
132 modval 12487 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℝ ∧ (𝑀𝑛) ∈ ℝ+) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
133102, 131, 132syl2anc 690 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) = (𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
134133oveq1d 6542 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))))
135102recnd 9924 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ ℂ)
136 qcn 11634 . . . . . . . . . . . . . . . 16 (((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℚ → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
137124, 136syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
138135, 137npcand 10247 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 − ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
139134, 138eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = 𝑘)
140139fveq2d 6092 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑘 mod (𝑀𝑛)) + ((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = (𝐹𝑘))
141 cnfldmul 19519 . . . . . . . . . . . . . . . . . 18 · = (.r‘ℂfld)
14251, 141ressmulr 15775 . . . . . . . . . . . . . . . . 17 (ℚ ∈ V → · = (.r𝑄))
143125, 142ax-mp 5 . . . . . . . . . . . . . . . 16 · = (.r𝑄)
14450, 61, 143abvmul 18598 . . . . . . . . . . . . . . 15 ((𝐹𝐴 ∧ (𝑀𝑛) ∈ ℚ ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℚ) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14583, 122, 106, 144syl3anc 1317 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
14651, 50qabvexp 25032 . . . . . . . . . . . . . . . 16 ((𝐹𝐴𝑀 ∈ ℚ ∧ 𝑛 ∈ ℕ0) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
14783, 99, 91, 146syl3anc 1317 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑀𝑛)) = ((𝐹𝑀)↑𝑛))
148147oveq1d 6542 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑀𝑛)) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
149145, 148eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛))))) = (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))))
150149oveq2d 6543 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (𝐹‘((𝑀𝑛) · (⌊‘(𝑘 / (𝑀𝑛)))))) = ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
151130, 140, 1503brtr3d 4608 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))))
152116, 91reexpcld 12842 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℝ)
153115, 152remulcld 9926 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ∈ ℝ)
154 nn0re 11148 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℝ)
155154ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℝ)
156111, 155remulcld 9926 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℝ)
157156, 152remulcld 9926 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) · (𝑇𝑛)) ∈ ℝ)
158111, 152remulcld 9926 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑇𝑛)) ∈ ℝ)
159 zmodfz 12509 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ ℤ ∧ (𝑀𝑛) ∈ ℕ) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
16085, 92, 159syl2anc 690 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)))
161 simprr 791 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
162 fveq2 6088 . . . . . . . . . . . . . . . . 17 (𝑗 = (𝑘 mod (𝑀𝑛)) → (𝐹𝑗) = (𝐹‘(𝑘 mod (𝑀𝑛))))
163162breq1d 4587 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑘 mod (𝑀𝑛)) → ((𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) ↔ (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
164163rspcv 3277 . . . . . . . . . . . . . . 15 ((𝑘 mod (𝑀𝑛)) ∈ (0...((𝑀𝑛) − 1)) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))))
165160, 161, 164sylc 62 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(𝑘 mod (𝑀𝑛))) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))
166111, 101remulcld 9926 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ∈ ℝ)
167101recnd 9924 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ∈ ℂ)
168108recnd 9924 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ∈ ℂ)
169167, 168mulcomd 9917 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) = ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)))
17050, 61abvge0 18594 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴𝑀 ∈ ℚ) → 0 ≤ (𝐹𝑀))
17183, 99, 170syl2anc 690 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝐹𝑀))
172100, 91, 171expge0d 12843 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ ((𝐹𝑀)↑𝑛))
173104zred 11314 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℝ)
174 elfzle1 12170 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) → 0 ≤ 𝑘)
175174ad2antrl 759 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑘)
17692nnred 10882 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀𝑛) ∈ ℝ)
17792nngt0d 10911 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀𝑛))
178 divge0 10741 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 ∈ ℝ ∧ 0 ≤ 𝑘) ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → 0 ≤ (𝑘 / (𝑀𝑛)))
179102, 175, 176, 177, 178syl22anc 1318 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ (𝑘 / (𝑀𝑛)))
180 flge0nn0 12438 . . . . . . . . . . . . . . . . . . . 20 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 0 ≤ (𝑘 / (𝑀𝑛))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
181103, 179, 180syl2anc 690 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0)
18251, 50qabvle 25031 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐴 ∧ (⌊‘(𝑘 / (𝑀𝑛))) ∈ ℕ0) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
18383, 181, 182syl2anc 690 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ (⌊‘(𝑘 / (𝑀𝑛))))
184 simprl 789 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)))
185 0z 11221 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ ℤ
18690, 118nnexpcld 12847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℕ)
187186nnzd 11313 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) ∈ ℤ)
188 elfzm11 12235 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((0 ∈ ℤ ∧ (𝑀↑(𝑛 + 1)) ∈ ℤ) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
189185, 187, 188sylancr 693 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1)))))
190184, 189mpbid 220 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘𝑘 < (𝑀↑(𝑛 + 1))))
191190simp3d 1067 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < (𝑀↑(𝑛 + 1)))
19290nncnd 10883 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℂ)
193192, 91expp1d 12826 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀↑(𝑛 + 1)) = ((𝑀𝑛) · 𝑀))
194191, 193breqtrd 4603 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑘 < ((𝑀𝑛) · 𝑀))
195 ltdivmul 10747 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ((𝑀𝑛) ∈ ℝ ∧ 0 < (𝑀𝑛))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
196102, 111, 176, 177, 195syl112anc 1321 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀𝑘 < ((𝑀𝑛) · 𝑀)))
197194, 196mpbird 245 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑘 / (𝑀𝑛)) < 𝑀)
19890nnzd 11313 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℤ)
199 fllt 12424 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘 / (𝑀𝑛)) ∈ ℝ ∧ 𝑀 ∈ ℤ) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
200103, 198, 199syl2anc 690 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑘 / (𝑀𝑛)) < 𝑀 ↔ (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀))
201197, 200mpbid 220 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) < 𝑀)
202173, 111, 201ltled 10036 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (⌊‘(𝑘 / (𝑀𝑛))) ≤ 𝑀)
203108, 173, 111, 183, 202letrd 10045 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) ≤ 𝑀)
204108, 111, 101, 172, 203lemul1ad 10812 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))) · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
205169, 204eqbrtrd 4599 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · ((𝐹𝑀)↑𝑛)))
20690nnnn0d 11198 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑀 ∈ ℕ0)
207206nn0ge0d 11201 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 ≤ 𝑀)
208 max1 11849 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
209100, 58, 208sylancl 692 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
210209, 57syl6breqr 4619 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑀) ≤ 𝑇)
211 leexp1a 12736 . . . . . . . . . . . . . . . . 17 ((((𝐹𝑀) ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑛 ∈ ℕ0) ∧ (0 ≤ (𝐹𝑀) ∧ (𝐹𝑀) ≤ 𝑇)) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
212100, 116, 91, 171, 210, 211syl32anc 1325 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹𝑀)↑𝑛) ≤ (𝑇𝑛))
213101, 152, 111, 207, 212lemul2ad 10813 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · ((𝐹𝑀)↑𝑛)) ≤ (𝑀 · (𝑇𝑛)))
214109, 166, 158, 205, 213letrd 10045 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛))))) ≤ (𝑀 · (𝑇𝑛)))
21598, 109, 157, 158, 165, 214le2addd 10495 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
216 nn0cn 11149 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ ℕ0𝑛 ∈ ℂ)
217216ad2antlr 758 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℂ)
218 1cnd 9912 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ∈ ℂ)
219192, 217, 218adddid 9920 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + (𝑀 · 1)))
220192mulid1d 9913 . . . . . . . . . . . . . . . . 17 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 1) = 𝑀)
221220oveq2d 6543 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · 𝑛) + (𝑀 · 1)) = ((𝑀 · 𝑛) + 𝑀))
222219, 221eqtrd 2643 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) = ((𝑀 · 𝑛) + 𝑀))
223222oveq1d 6542 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)))
224192, 217mulcld 9916 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · 𝑛) ∈ ℂ)
225152recnd 9924 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ∈ ℂ)
226224, 192, 225adddird 9921 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (((𝑀 · 𝑛) + 𝑀) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
227223, 226eqtrd 2643 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) = (((𝑀 · 𝑛) · (𝑇𝑛)) + (𝑀 · (𝑇𝑛))))
228215, 227breqtrrd 4605 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)))
229 max2 11851 . . . . . . . . . . . . . . . 16 (((𝐹𝑀) ∈ ℝ ∧ 1 ∈ ℝ) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
230100, 58, 229sylancl 692 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ if((𝐹𝑀) ≤ 1, 1, (𝐹𝑀)))
231230, 57syl6breqr 4619 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 1 ≤ 𝑇)
232 nn0z 11233 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
233232ad2antlr 758 . . . . . . . . . . . . . . . 16 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ ℤ)
234 uzid 11534 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℤ → 𝑛 ∈ (ℤ𝑛))
235233, 234syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 𝑛 ∈ (ℤ𝑛))
236 peano2uz 11573 . . . . . . . . . . . . . . 15 (𝑛 ∈ (ℤ𝑛) → (𝑛 + 1) ∈ (ℤ𝑛))
237235, 236syl 17 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑛 + 1) ∈ (ℤ𝑛))
238116, 231, 237leexp2ad 12858 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)))
23990, 113nnmulcld 10915 . . . . . . . . . . . . . . 15 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝑀 · (𝑛 + 1)) ∈ ℕ)
240239nngt0d 10911 . . . . . . . . . . . . . 14 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → 0 < (𝑀 · (𝑛 + 1)))
241 lemul2 10725 . . . . . . . . . . . . . 14 (((𝑇𝑛) ∈ ℝ ∧ (𝑇↑(𝑛 + 1)) ∈ ℝ ∧ ((𝑀 · (𝑛 + 1)) ∈ ℝ ∧ 0 < (𝑀 · (𝑛 + 1)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
242152, 119, 115, 240, 241syl112anc 1321 . . . . . . . . . . . . 13 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑇𝑛) ≤ (𝑇↑(𝑛 + 1)) ↔ ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
243238, 242mpbid 220 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝑀 · (𝑛 + 1)) · (𝑇𝑛)) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
244110, 153, 120, 228, 243letrd 10045 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → ((𝐹‘(𝑘 mod (𝑀𝑛))) + (((𝐹𝑀)↑𝑛) · (𝐹‘(⌊‘(𝑘 / (𝑀𝑛)))))) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
24589, 110, 120, 151, 244letrd 10045 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ0) ∧ (𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1)) ∧ ∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)))) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))
246245expr 640 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ0) ∧ 𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → (𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
247246ralrimdva 2951 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ0) → (∀𝑗 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑗) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
24882, 247syl5bi 230 . . . . . . 7 ((𝜑𝑛 ∈ ℕ0) → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1)))))
249248expcom 449 . . . . . 6 (𝑛 ∈ ℕ0 → (𝜑 → (∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛)) → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
250249a2d 29 . . . . 5 (𝑛 ∈ ℕ0 → ((𝜑 → ∀𝑘 ∈ (0...((𝑀𝑛) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑛) · (𝑇𝑛))) → (𝜑 → ∀𝑘 ∈ (0...((𝑀↑(𝑛 + 1)) − 1))(𝐹𝑘) ≤ ((𝑀 · (𝑛 + 1)) · (𝑇↑(𝑛 + 1))))))
2519, 18, 27, 36, 79, 250nn0ind 11304 . . . 4 (𝑋 ∈ ℕ0 → (𝜑 → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
252251impcom 444 . . 3 ((𝜑𝑋 ∈ ℕ0) → ∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
253 fveq2 6088 . . . . 5 (𝑘 = 𝑌 → (𝐹𝑘) = (𝐹𝑌))
254253breq1d 4587 . . . 4 (𝑘 = 𝑌 → ((𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) ↔ (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
255254rspccv 3278 . . 3 (∀𝑘 ∈ (0...((𝑀𝑋) − 1))(𝐹𝑘) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
256252, 255syl 17 . 2 ((𝜑𝑋 ∈ ℕ0) → (𝑌 ∈ (0...((𝑀𝑋) − 1)) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋))))
2572563impia 1252 1 ((𝜑𝑋 ∈ ℕ0𝑌 ∈ (0...((𝑀𝑋) − 1))) → (𝐹𝑌) ≤ ((𝑀 · 𝑋) · (𝑇𝑋)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wral 2895  Vcvv 3172  ifcif 4035   class class class wbr 4577  cmpt 4637  cfv 5790  (class class class)co 6527  cc 9790  cr 9791  0cc0 9792  1c1 9793   + caddc 9795   · cmul 9797   < clt 9930  cle 9931  cmin 10117  -cneg 10118   / cdiv 10533  cn 10867  2c2 10917  0cn0 11139  cz 11210  cuz 11519  cq 11620  +crp 11664  ...cfz 12152  cfl 12408   mod cmo 12485  cexp 12677  cprime 15169   pCnt cpc 15325  s cress 15642  +gcplusg 15714  .rcmulr 15715  AbsValcabv 18585  fldccnfld 19513  logclog 24022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869  ax-pre-sup 9870  ax-addf 9871  ax-mulf 9872
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-tpos 7216  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-sup 8208  df-inf 8209  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-div 10534  df-nn 10868  df-2 10926  df-3 10927  df-4 10928  df-5 10929  df-6 10930  df-7 10931  df-8 10932  df-9 10933  df-n0 11140  df-z 11211  df-dec 11326  df-uz 11520  df-q 11621  df-rp 11665  df-ico 12008  df-fz 12153  df-fl 12410  df-mod 12486  df-seq 12619  df-exp 12678  df-struct 15643  df-ndx 15644  df-slot 15645  df-base 15646  df-sets 15647  df-ress 15648  df-plusg 15727  df-mulr 15728  df-starv 15729  df-tset 15733  df-ple 15734  df-ds 15737  df-unif 15738  df-0g 15871  df-mgm 17011  df-sgrp 17053  df-mnd 17064  df-grp 17194  df-minusg 17195  df-subg 17360  df-cmn 17964  df-mgp 18259  df-ur 18271  df-ring 18318  df-cring 18319  df-oppr 18392  df-dvdsr 18410  df-unit 18411  df-invr 18441  df-dvr 18452  df-drng 18518  df-subrg 18547  df-abv 18586  df-cnfld 19514
This theorem is referenced by:  ostth2lem3  25041
  Copyright terms: Public domain W3C validator