fsumfldivdiaglem

		Ref	Expression
	Hypothesis	fsumfldivdiag.1	$⊢ φ \to A \in ℝ$
	Assertion	fsumfldivdiaglem	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋)) \to (m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋)))$

Proof

Step	Hyp	Ref	Expression
1		fsumfldivdiag.1	$⊢ φ \to A \in ℝ$
2		simprr	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \in (1 \dots ⌊\frac{A}{n}⌋)$
3	1	adantr	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to A \in ℝ$
4		simprl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n \in (1 \dots ⌊A⌋)$
5		fznnfl	$⊢ A \in ℝ \to (n \in (1 \dots ⌊A⌋) \leftrightarrow (n \in ℕ \land n \leq A))$
6	3 5	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (n \in (1 \dots ⌊A⌋) \leftrightarrow (n \in ℕ \land n \leq A))$
7	4 6	mpbid	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (n \in ℕ \land n \leq A)$
8	7	simpld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n \in ℕ$
9	3 8	nndivred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to \frac{A}{n} \in ℝ$
10		fznnfl	$⊢ \frac{A}{n} \in ℝ \to (m \in (1 \dots ⌊\frac{A}{n}⌋) \leftrightarrow (m \in ℕ \land m \leq \frac{A}{n}))$
11	9 10	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (m \in (1 \dots ⌊\frac{A}{n}⌋) \leftrightarrow (m \in ℕ \land m \leq \frac{A}{n}))$
12	2 11	mpbid	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (m \in ℕ \land m \leq \frac{A}{n})$
13	12	simpld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \in ℕ$
14	13	nnred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \in ℝ$
15	12	simprd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \leq \frac{A}{n}$
16	3	recnd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to A \in ℂ$
17	16	mullidd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 1 A = A$
18	8	nnge1d	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 1 \leq n$
19		1red	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 1 \in ℝ$
20	8	nnred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n \in ℝ$
21		0red	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 0 \in ℝ$
22	8 13	nnmulcld	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n m \in ℕ$
23	22	nnred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n m \in ℝ$
24	22	nngt0d	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 0 < n m$
25	8	nngt0d	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 0 < n$
26		lemuldiv2	$⊢ (m \in ℝ \land A \in ℝ \land (n \in ℝ \land 0 < n)) \to (n m \leq A \leftrightarrow m \leq \frac{A}{n})$
27	14 3 20 25 26	syl112anc	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (n m \leq A \leftrightarrow m \leq \frac{A}{n})$
28	15 27	mpbird	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n m \leq A$
29	21 23 3 24 28	ltletrd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 0 < A$
30		lemul1	$⊢ (1 \in ℝ \land n \in ℝ \land (A \in ℝ \land 0 < A)) \to (1 \leq n \leftrightarrow 1 A \leq n A)$
31	19 20 3 29 30	syl112anc	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (1 \leq n \leftrightarrow 1 A \leq n A)$
32	18 31	mpbid	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 1 A \leq n A$
33	17 32	eqbrtrrd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to A \leq n A$
34		ledivmul	$⊢ (A \in ℝ \land A \in ℝ \land (n \in ℝ \land 0 < n)) \to (\frac{A}{n} \leq A \leftrightarrow A \leq n A)$
35	3 3 20 25 34	syl112anc	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (\frac{A}{n} \leq A \leftrightarrow A \leq n A)$
36	33 35	mpbird	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to \frac{A}{n} \leq A$
37	14 9 3 15 36	letrd	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \leq A$
38		fznnfl	$⊢ A \in ℝ \to (m \in (1 \dots ⌊A⌋) \leftrightarrow (m \in ℕ \land m \leq A))$
39	3 38	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (m \in (1 \dots ⌊A⌋) \leftrightarrow (m \in ℕ \land m \leq A))$
40	13 37 39	mpbir2and	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to m \in (1 \dots ⌊A⌋)$
41	13	nngt0d	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to 0 < m$
42		lemuldiv	$⊢ (n \in ℝ \land A \in ℝ \land (m \in ℝ \land 0 < m)) \to (n m \leq A \leftrightarrow n \leq \frac{A}{m})$
43	20 3 14 41 42	syl112anc	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (n m \leq A \leftrightarrow n \leq \frac{A}{m})$
44	28 43	mpbid	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n \leq \frac{A}{m}$
45	3 13	nndivred	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to \frac{A}{m} \in ℝ$
46		fznnfl	$⊢ \frac{A}{m} \in ℝ \to (n \in (1 \dots ⌊\frac{A}{m}⌋) \leftrightarrow (n \in ℕ \land n \leq \frac{A}{m}))$
47	45 46	syl	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (n \in (1 \dots ⌊\frac{A}{m}⌋) \leftrightarrow (n \in ℕ \land n \leq \frac{A}{m}))$
48	8 44 47	mpbir2and	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to n \in (1 \dots ⌊\frac{A}{m}⌋)$
49	40 48	jca	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to (m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋))$
50	49	ex	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋)) \to (m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋)))$

Metamath Proof Explorer

Theorem fsumfldivdiaglem

Proof