Metamath Proof Explorer

Theorem fsumfldivdiaglem

Description: Lemma for fsumfldivdiag . (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypothesis fsumfldivdiag.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion fsumfldivdiaglem ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fsumfldivdiag.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 simprr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) )
3 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝐴 ∈ ℝ )
4 simprl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
5 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴 ) ) )
6 3 5 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴 ) ) )
7 4 6 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝐴 ) )
8 7 simpld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑛 ∈ ℕ )
9 3 8 nndivred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ )
10 fznnfl ⊢ ( ( 𝐴 / 𝑛 ) ∈ ℝ → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 𝐴 / 𝑛 ) ) ) )
11 9 10 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 𝐴 / 𝑛 ) ) ) )
12 2 11 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ ( 𝐴 / 𝑛 ) ) )
13 12 simpld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ∈ ℕ )
14 13 nnred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ∈ ℝ )
15 12 simprd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ≤ ( 𝐴 / 𝑛 ) )
16 3 recnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝐴 ∈ ℂ )
17 16 mulid2d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 1 · 𝐴 ) = 𝐴 )
18 8 nnge1d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 1 ≤ 𝑛 )
19 1red ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 1 ∈ ℝ )
20 8 nnred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑛 ∈ ℝ )
21 0red ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 0 ∈ ℝ )
22 8 13 nnmulcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℕ )
23 22 nnred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℝ )
24 22 nngt0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 0 < ( 𝑛 · 𝑚 ) )
25 8 nngt0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 0 < 𝑛 )
26 lemuldiv2 ⊢ ( ( 𝑚 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 𝑛 · 𝑚 ) ≤ 𝐴 ↔ 𝑚 ≤ ( 𝐴 / 𝑛 ) ) )
27 14 3 20 25 26 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( ( 𝑛 · 𝑚 ) ≤ 𝐴 ↔ 𝑚 ≤ ( 𝐴 / 𝑛 ) ) )
28 15 27 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 · 𝑚 ) ≤ 𝐴 )
29 21 23 3 24 28 ltletrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 0 < 𝐴 )
30 lemul1 ⊢ ( ( 1 ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 ≤ 𝑛 ↔ ( 1 · 𝐴 ) ≤ ( 𝑛 · 𝐴 ) ) )
31 19 20 3 29 30 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 1 ≤ 𝑛 ↔ ( 1 · 𝐴 ) ≤ ( 𝑛 · 𝐴 ) ) )
32 18 31 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 1 · 𝐴 ) ≤ ( 𝑛 · 𝐴 ) )
33 17 32 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝐴 ≤ ( 𝑛 · 𝐴 ) )
34 ledivmul ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 𝐴 / 𝑛 ) ≤ 𝐴 ↔ 𝐴 ≤ ( 𝑛 · 𝐴 ) ) )
35 3 3 20 25 34 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( ( 𝐴 / 𝑛 ) ≤ 𝐴 ↔ 𝐴 ≤ ( 𝑛 · 𝐴 ) ) )
36 33 35 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝐴 / 𝑛 ) ≤ 𝐴 )
37 14 9 3 15 36 letrd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ≤ 𝐴 )
38 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴 ) ) )
39 3 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑚 ∈ ℕ ∧ 𝑚 ≤ 𝐴 ) ) )
40 13 37 39 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
41 13 nngt0d ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 0 < 𝑚 )
42 lemuldiv ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑚 ∈ ℝ ∧ 0 < 𝑚 ) ) → ( ( 𝑛 · 𝑚 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑚 ) ) )
43 20 3 14 41 42 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( ( 𝑛 · 𝑚 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑚 ) ) )
44 28 43 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑛 ≤ ( 𝐴 / 𝑚 ) )
45 3 13 nndivred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝐴 / 𝑚 ) ∈ ℝ )
46 fznnfl ⊢ ( ( 𝐴 / 𝑚 ) ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑚 ) ) ) )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑚 ) ) ) )
48 8 44 47 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) )
49 40 48 jca ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) )
50 49 ex ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) ) )