Proof of Theorem fsumfldivdiaglem
Step | Hyp | Ref
| Expression |
1 | | simprr 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) |
2 | | fsumfldivdiag.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝐴 ∈ ℝ) |
4 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑛 ∈ (1...(⌊‘𝐴))) |
5 | | fznnfl 13571 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝐴))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝐴))) |
6 | 3, 5 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 ∈ (1...(⌊‘𝐴)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴))) |
7 | 4, 6 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴)) |
8 | 7 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑛 ∈ ℕ) |
9 | 3, 8 | nndivred 12016 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝐴 / 𝑛) ∈ ℝ) |
10 | | fznnfl 13571 |
. . . . . . 7
⊢ ((𝐴 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝐴 / 𝑛)))) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝐴 / 𝑛)))) |
12 | 1, 11 | mpbid 231 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝐴 / 𝑛))) |
13 | 12 | simpld 495 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ∈ ℕ) |
14 | 13 | nnred 11977 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ∈ ℝ) |
15 | 12 | simprd 496 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ≤ (𝐴 / 𝑛)) |
16 | 3 | recnd 10992 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝐴 ∈ ℂ) |
17 | 16 | mulid2d 10982 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (1 · 𝐴) = 𝐴) |
18 | 8 | nnge1d 12010 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 1 ≤ 𝑛) |
19 | | 1red 10965 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 1 ∈
ℝ) |
20 | 8 | nnred 11977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑛 ∈ ℝ) |
21 | | 0red 10967 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 0 ∈
ℝ) |
22 | 8, 13 | nnmulcld 12015 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 · 𝑚) ∈ ℕ) |
23 | 22 | nnred 11977 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 · 𝑚) ∈ ℝ) |
24 | 22 | nngt0d 12011 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 0 < (𝑛 · 𝑚)) |
25 | 8 | nngt0d 12011 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 0 < 𝑛) |
26 | | lemuldiv2 11845 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 <
𝑛)) → ((𝑛 · 𝑚) ≤ 𝐴 ↔ 𝑚 ≤ (𝐴 / 𝑛))) |
27 | 14, 3, 20, 25, 26 | syl112anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → ((𝑛 · 𝑚) ≤ 𝐴 ↔ 𝑚 ≤ (𝐴 / 𝑛))) |
28 | 15, 27 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 · 𝑚) ≤ 𝐴) |
29 | 21, 23, 3, 24, 28 | ltletrd 11124 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 0 < 𝐴) |
30 | | lemul1 11816 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 𝑛
∈ ℝ ∧ (𝐴
∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ 𝑛 ↔ (1 · 𝐴) ≤ (𝑛 · 𝐴))) |
31 | 19, 20, 3, 29, 30 | syl112anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (1 ≤ 𝑛 ↔ (1 · 𝐴) ≤ (𝑛 · 𝐴))) |
32 | 18, 31 | mpbid 231 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (1 · 𝐴) ≤ (𝑛 · 𝐴)) |
33 | 17, 32 | eqbrtrrd 5099 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝐴 ≤ (𝑛 · 𝐴)) |
34 | | ledivmul 11840 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑛 ∈ ℝ ∧ 0 <
𝑛)) → ((𝐴 / 𝑛) ≤ 𝐴 ↔ 𝐴 ≤ (𝑛 · 𝐴))) |
35 | 3, 3, 20, 25, 34 | syl112anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → ((𝐴 / 𝑛) ≤ 𝐴 ↔ 𝐴 ≤ (𝑛 · 𝐴))) |
36 | 33, 35 | mpbird 256 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝐴 / 𝑛) ≤ 𝐴) |
37 | 14, 9, 3, 15, 36 | letrd 11121 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ≤ 𝐴) |
38 | | fznnfl 13571 |
. . . . 5
⊢ (𝐴 ∈ ℝ → (𝑚 ∈
(1...(⌊‘𝐴))
↔ (𝑚 ∈ ℕ
∧ 𝑚 ≤ 𝐴))) |
39 | 3, 38 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑚 ∈ (1...(⌊‘𝐴)) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴))) |
40 | 13, 37, 39 | mpbir2and 710 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑚 ∈ (1...(⌊‘𝐴))) |
41 | 13 | nngt0d 12011 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 0 < 𝑚) |
42 | | lemuldiv 11844 |
. . . . . 6
⊢ ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 <
𝑚)) → ((𝑛 · 𝑚) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑚))) |
43 | 20, 3, 14, 41, 42 | syl112anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → ((𝑛 · 𝑚) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑚))) |
44 | 28, 43 | mpbid 231 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑛 ≤ (𝐴 / 𝑚)) |
45 | 3, 13 | nndivred 12016 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝐴 / 𝑚) ∈ ℝ) |
46 | | fznnfl 13571 |
. . . . 5
⊢ ((𝐴 / 𝑚) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑚)))) |
47 | 45, 46 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑚)))) |
48 | 8, 44, 47 | mpbir2and 710 |
. . 3
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))) |
49 | 40, 48 | jca 512 |
. 2
⊢ ((𝜑 ∧ (𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛))))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚))))) |
50 | 49 | ex 413 |
1
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘𝐴)) ∧ 𝑚 ∈ (1...(⌊‘(𝐴 / 𝑛)))) → (𝑚 ∈ (1...(⌊‘𝐴)) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑚)))))) |