Metamath Proof Explorer


Theorem fsumfldivdiaglem

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

Ref Expression
Hypothesis fsumfldivdiag.1
|- ( ph -> A e. RR )
Assertion fsumfldivdiaglem
|- ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) -> ( m e. ( 1 ... ( |_ ` A ) ) /\ n e. ( 1 ... ( |_ ` ( A / m ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fsumfldivdiag.1
 |-  ( ph -> A e. RR )
2 simprr
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m e. ( 1 ... ( |_ ` ( A / n ) ) ) )
3 1 adantr
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> A e. RR )
4 simprl
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> n e. ( 1 ... ( |_ ` A ) ) )
5 fznnfl
 |-  ( A e. RR -> ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. NN /\ n <_ A ) ) )
6 3 5 syl
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n e. ( 1 ... ( |_ ` A ) ) <-> ( n e. NN /\ n <_ A ) ) )
7 4 6 mpbid
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n e. NN /\ n <_ A ) )
8 7 simpld
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> n e. NN )
9 3 8 nndivred
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( A / n ) e. RR )
10 fznnfl
 |-  ( ( A / n ) e. RR -> ( m e. ( 1 ... ( |_ ` ( A / n ) ) ) <-> ( m e. NN /\ m <_ ( A / n ) ) ) )
11 9 10 syl
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( m e. ( 1 ... ( |_ ` ( A / n ) ) ) <-> ( m e. NN /\ m <_ ( A / n ) ) ) )
12 2 11 mpbid
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( m e. NN /\ m <_ ( A / n ) ) )
13 12 simpld
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m e. NN )
14 13 nnred
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m e. RR )
15 12 simprd
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m <_ ( A / n ) )
16 3 recnd
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> A e. CC )
17 16 mulid2d
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( 1 x. A ) = A )
18 8 nnge1d
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 1 <_ n )
19 1red
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 1 e. RR )
20 8 nnred
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> n e. RR )
21 0red
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 0 e. RR )
22 8 13 nnmulcld
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n x. m ) e. NN )
23 22 nnred
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n x. m ) e. RR )
24 22 nngt0d
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 0 < ( n x. m ) )
25 8 nngt0d
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 0 < n )
26 lemuldiv2
 |-  ( ( m e. RR /\ A e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( ( n x. m ) <_ A <-> m <_ ( A / n ) ) )
27 14 3 20 25 26 syl112anc
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( ( n x. m ) <_ A <-> m <_ ( A / n ) ) )
28 15 27 mpbird
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n x. m ) <_ A )
29 21 23 3 24 28 ltletrd
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 0 < A )
30 lemul1
 |-  ( ( 1 e. RR /\ n e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( 1 <_ n <-> ( 1 x. A ) <_ ( n x. A ) ) )
31 19 20 3 29 30 syl112anc
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( 1 <_ n <-> ( 1 x. A ) <_ ( n x. A ) ) )
32 18 31 mpbid
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( 1 x. A ) <_ ( n x. A ) )
33 17 32 eqbrtrrd
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> A <_ ( n x. A ) )
34 ledivmul
 |-  ( ( A e. RR /\ A e. RR /\ ( n e. RR /\ 0 < n ) ) -> ( ( A / n ) <_ A <-> A <_ ( n x. A ) ) )
35 3 3 20 25 34 syl112anc
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( ( A / n ) <_ A <-> A <_ ( n x. A ) ) )
36 33 35 mpbird
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( A / n ) <_ A )
37 14 9 3 15 36 letrd
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m <_ A )
38 fznnfl
 |-  ( A e. RR -> ( m e. ( 1 ... ( |_ ` A ) ) <-> ( m e. NN /\ m <_ A ) ) )
39 3 38 syl
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( m e. ( 1 ... ( |_ ` A ) ) <-> ( m e. NN /\ m <_ A ) ) )
40 13 37 39 mpbir2and
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> m e. ( 1 ... ( |_ ` A ) ) )
41 13 nngt0d
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> 0 < m )
42 lemuldiv
 |-  ( ( n e. RR /\ A e. RR /\ ( m e. RR /\ 0 < m ) ) -> ( ( n x. m ) <_ A <-> n <_ ( A / m ) ) )
43 20 3 14 41 42 syl112anc
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( ( n x. m ) <_ A <-> n <_ ( A / m ) ) )
44 28 43 mpbid
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> n <_ ( A / m ) )
45 3 13 nndivred
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( A / m ) e. RR )
46 fznnfl
 |-  ( ( A / m ) e. RR -> ( n e. ( 1 ... ( |_ ` ( A / m ) ) ) <-> ( n e. NN /\ n <_ ( A / m ) ) ) )
47 45 46 syl
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( n e. ( 1 ... ( |_ ` ( A / m ) ) ) <-> ( n e. NN /\ n <_ ( A / m ) ) ) )
48 8 44 47 mpbir2and
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> n e. ( 1 ... ( |_ ` ( A / m ) ) ) )
49 40 48 jca
 |-  ( ( ph /\ ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) ) -> ( m e. ( 1 ... ( |_ ` A ) ) /\ n e. ( 1 ... ( |_ ` ( A / m ) ) ) ) )
50 49 ex
 |-  ( ph -> ( ( n e. ( 1 ... ( |_ ` A ) ) /\ m e. ( 1 ... ( |_ ` ( A / n ) ) ) ) -> ( m e. ( 1 ... ( |_ ` A ) ) /\ n e. ( 1 ... ( |_ ` ( A / m ) ) ) ) ) )