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 ) ) ) ) ) )