Proof of Theorem harmonicbnd4
Step | Hyp | Ref
| Expression |
1 | | fzfid 12224 |
. . . . . 6

          |
2 | | elfznn 11854 |
. . . . . . . 8
           |
3 | 2 | adantl 473 |
. . . . . . 7
          
  |
4 | 3 | nnrecred 10677 |
. . . . . 6
          
    |
5 | 1, 4 | fsumrecl 13877 |
. . . . 5

              |
6 | 5 | recnd 9687 |
. . . 4

              |
7 | | relogcl 23604 |
. . . . 5

      |
8 | 7 | recnd 9687 |
. . . 4

      |
9 | | emre 24010 |
. . . . . 6
 |
10 | 9 | a1i 11 |
. . . . 5

  |
11 | 10 | recnd 9687 |
. . . 4

  |
12 | 6, 8, 11 | subsub4d 10036 |
. . 3

  
                                       |
13 | 12 | fveq2d 5883 |
. 2

                                                  |
14 | | rpreccl 11349 |
. . . . . 6

    |
15 | 14 | rpred 11364 |
. . . . 5

    |
16 | | resubcl 9958 |
. . . . 5
           |
17 | 9, 15, 16 | sylancr 676 |
. . . 4

      |
18 | | rprege0 11339 |
. . . . . . . . 9

    |
19 | | flge0nn0 12087 |
. . . . . . . . 9
         |
20 | 18, 19 | syl 17 |
. . . . . . . 8

      |
21 | | nn0p1nn 10933 |
. . . . . . . 8
    
        |
22 | 20, 21 | syl 17 |
. . . . . . 7

        |
23 | 22 | nnrpd 11362 |
. . . . . 6

        |
24 | | relogcl 23604 |
. . . . . 6
      
            |
25 | 23, 24 | syl 17 |
. . . . 5

            |
26 | 5, 25 | resubcld 10068 |
. . . 4

                          |
27 | 5, 7 | resubcld 10068 |
. . . 4

                    |
28 | 22 | nnrecred 10677 |
. . . . . 6

          |
29 | | fzfid 12224 |
. . . . . . . 8

            |
30 | | elfznn 11854 |
. . . . . . . . . 10
             |
31 | 30 | adantl 473 |
. . . . . . . . 9
               |
32 | 31 | nnrecred 10677 |
. . . . . . . 8
                 |
33 | 29, 32 | fsumrecl 13877 |
. . . . . . 7

                |
34 | 33, 25 | resubcld 10068 |
. . . . . 6

                            |
35 | | harmonicbnd 24008 |
. . . . . . . 8
                                   ![[,] [,]](_icc.gif)    |
36 | 22, 35 | syl 17 |
. . . . . . 7

                            ![[,] [,]](_icc.gif)    |
37 | | 1re 9660 |
. . . . . . . . 9
 |
38 | 9, 37 | elicc2i 11725 |
. . . . . . . 8
  
                          ![[,] [,]](_icc.gif) 
                                                                                  |
39 | 38 | simp2bi 1046 |
. . . . . . 7
  
                          ![[,] [,]](_icc.gif)                              |
40 | 36, 39 | syl 17 |
. . . . . 6

                            |
41 | | rpre 11331 |
. . . . . . . 8

  |
42 | | fllep1 12070 |
. . . . . . . 8
         |
43 | 41, 42 | syl 17 |
. . . . . . 7

        |
44 | | rpregt0 11338 |
. . . . . . . 8

    |
45 | 22 | nnred 10646 |
. . . . . . . 8

        |
46 | 22 | nngt0d 10675 |
. . . . . . . 8

        |
47 | | lerec 10511 |
. . . . . . . 8
                                 
     |
48 | 44, 45, 46, 47 | syl12anc 1290 |
. . . . . . 7

      
             |
49 | 43, 48 | mpbid 215 |
. . . . . 6

            |
50 | 10, 28, 34, 15, 40, 49 | le2subd 10254 |
. . . . 5

                                          |
51 | 33 | recnd 9687 |
. . . . . . 7

                |
52 | 25 | recnd 9687 |
. . . . . . 7

            |
53 | 28 | recnd 9687 |
. . . . . . 7

          |
54 | 51, 52, 53 | sub32d 10037 |
. . . . . 6

  
                                   
                                   |
55 | | nnuz 11218 |
. . . . . . . . . . . 12
     |
56 | 22, 55 | syl6eleq 2559 |
. . . . . . . . . . 11

            |
57 | 32 | recnd 9687 |
. . . . . . . . . . 11
                 |
58 | | oveq2 6316 |
. . . . . . . . . . 11
                   |
59 | 56, 57, 58 | fsumm1 13889 |
. . . . . . . . . 10

               
                          |
60 | 20 | nn0cnd 10951 |
. . . . . . . . . . . . . 14

      |
61 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
62 | | pncan 9901 |
. . . . . . . . . . . . . 14
     
               |
63 | 60, 61, 62 | sylancl 675 |
. . . . . . . . . . . . 13

              |
64 | 63 | oveq2d 6324 |
. . . . . . . . . . . 12

                      |
65 | 64 | sumeq1d 13844 |
. . . . . . . . . . 11

                              |
66 | 65 | oveq1d 6323 |
. . . . . . . . . 10

                           
                      |
67 | 59, 66 | eqtrd 2505 |
. . . . . . . . 9

               
                      |
68 | 67 | oveq1d 6323 |
. . . . . . . 8

                                                          |
69 | 6, 53 | pncand 10006 |
. . . . . . . 8

  
                                           |
70 | 68, 69 | eqtrd 2505 |
. . . . . . 7

                                      |
71 | 70 | oveq1d 6323 |
. . . . . 6

  
                                                           |
72 | 54, 71 | eqtrd 2505 |
. . . . 5

  
                                                           |
73 | 50, 72 | breqtrd 4420 |
. . . 4

                              |
74 | | logleb 23631 |
. . . . . . 7
               
                 |
75 | 23, 74 | mpdan 681 |
. . . . . 6

      
                 |
76 | 43, 75 | mpbid 215 |
. . . . 5

                |
77 | 7, 25, 5, 76 | lesub2dd 10251 |
. . . 4

                       
                    |
78 | 17, 26, 27, 73, 77 | letrd 9809 |
. . 3

                        |
79 | 27, 15 | resubcld 10068 |
. . . . 5

  
                     |
80 | 15 | recnd 9687 |
. . . . . . 7

    |
81 | 6, 8, 80 | subsub4d 10036 |
. . . . . 6

  
                                           |
82 | 7, 15 | readdcld 9688 |
. . . . . . 7

          |
83 | | id 22 |
. . . . . . . . . 10

  |
84 | 23, 83 | relogdivd 23654 |
. . . . . . . . 9

                              |
85 | | rerpdivcl 11353 |
. . . . . . . . . . . . 13
       
           |
86 | 45, 85 | mpancom 682 |
. . . . . . . . . . . 12

          |
87 | 37 | a1i 11 |
. . . . . . . . . . . . 13

  |
88 | 87, 15 | readdcld 9688 |
. . . . . . . . . . . 12

      |
89 | 15 | reefcld 14219 |
. . . . . . . . . . . 12

        |
90 | 61 | a1i 11 |
. . . . . . . . . . . . . 14

  |
91 | | rpcnne0 11342 |
. . . . . . . . . . . . . 14

    |
92 | | divdir 10315 |
. . . . . . . . . . . . . 14
     

                      |
93 | 60, 90, 91, 92 | syl3anc 1292 |
. . . . . . . . . . . . 13

                    |
94 | | reflcl 12065 |
. . . . . . . . . . . . . . . 16
       |
95 | 41, 94 | syl 17 |
. . . . . . . . . . . . . . 15

      |
96 | | rerpdivcl 11353 |
. . . . . . . . . . . . . . 15
     
         |
97 | 95, 96 | mpancom 682 |
. . . . . . . . . . . . . 14

        |
98 | | flle 12068 |
. . . . . . . . . . . . . . . . 17
       |
99 | 41, 98 | syl 17 |
. . . . . . . . . . . . . . . 16

      |
100 | | rpcn 11333 |
. . . . . . . . . . . . . . . . 17

  |
101 | 100 | mulid1d 9678 |
. . . . . . . . . . . . . . . 16

    |
102 | 99, 101 | breqtrrd 4422 |
. . . . . . . . . . . . . . 15

        |
103 | | ledivmul 10503 |
. . . . . . . . . . . . . . . 16
     

                  |
104 | 95, 87, 44, 103 | syl3anc 1292 |
. . . . . . . . . . . . . . 15

      
    
    |
105 | 102, 104 | mpbird 240 |
. . . . . . . . . . . . . 14

        |
106 | 97, 87, 15, 105 | leadd1dd 10248 |
. . . . . . . . . . . . 13

                |
107 | 93, 106 | eqbrtrd 4416 |
. . . . . . . . . . . 12

              |
108 | | efgt1p 14246 |
. . . . . . . . . . . . . 14
  
            |
109 | 14, 108 | syl 17 |
. . . . . . . . . . . . 13

            |
110 | 88, 89, 109 | ltled 9800 |
. . . . . . . . . . . 12

            |
111 | 86, 88, 89, 107, 110 | letrd 9809 |
. . . . . . . . . . 11

                |
112 | | rpdivcl 11348 |
. . . . . . . . . . . . 13
                   |
113 | 23, 112 | mpancom 682 |
. . . . . . . . . . . 12

          |
114 | 15 | rpefcld 14236 |
. . . . . . . . . . . 12

        |
115 | 113, 114 | logled 23655 |
. . . . . . . . . . 11

                          
             |
116 | 111, 115 | mpbid 215 |
. . . . . . . . . 10

                        |
117 | 15 | relogefd 23656 |
. . . . . . . . . 10

              |
118 | 116, 117 | breqtrd 4420 |
. . . . . . . . 9

                |
119 | 84, 118 | eqbrtrrd 4418 |
. . . . . . . 8

                    |
120 | 25, 7, 15 | lesubadd2d 10233 |
. . . . . . . 8

                            
           |
121 | 119, 120 | mpbid 215 |
. . . . . . 7

                    |
122 | 25, 82, 5, 121 | lesub2dd 10251 |
. . . . . 6

                     
                          |
123 | 81, 122 | eqbrtrd 4416 |
. . . . 5

  
                  
                          |
124 | | harmonicbnd3 24012 |
. . . . . . 7
    
                          ![[,] [,]](_icc.gif)    |
125 | 20, 124 | syl 17 |
. . . . . 6

                          ![[,] [,]](_icc.gif)    |
126 | | 0re 9661 |
. . . . . . . 8
 |
127 | 126, 9 | elicc2i 11725 |
. . . . . . 7
  
                        ![[,] [,]](_icc.gif)                                                                              |
128 | 127 | simp3bi 1047 |
. . . . . 6
  
                        ![[,] [,]](_icc.gif)                            |
129 | 125, 128 | syl 17 |
. . . . 5

                       
  |
130 | 79, 26, 10, 123, 129 | letrd 9809 |
. . . 4

  
                  
  |
131 | 27, 15, 10 | lesubaddd 10231 |
. . . 4

                      
                 
       |
132 | 130, 131 | mpbid 215 |
. . 3

                 
      |
133 | 27, 10, 15 | absdifled 13573 |
. . 3

      
                 
 
                                                 |
134 | 78, 132, 133 | mpbir2and 936 |
. 2

                            |
135 | 13, 134 | eqbrtrrd 4418 |
1

                            |