Step | Hyp | Ref
| Expression |
1 | | madjusmdet.n |
. . . . . . . . . . . 12
   |
2 | | nnuz 11194 |
. . . . . . . . . . . 12
     |
3 | 1, 2 | syl6eleq 2539 |
. . . . . . . . . . 11
       |
4 | | eluzfz2 11807 |
. . . . . . . . . . 11
    
      |
5 | 3, 4 | syl 17 |
. . . . . . . . . 10
       |
6 | | eqid 2451 |
. . . . . . . . . . 11
         |
7 | | madjusmdetlem2.s |
. . . . . . . . . . 11
                   |
8 | | eqid 2451 |
. . . . . . . . . . 11
                 |
9 | | eqid 2451 |
. . . . . . . . . . 11
                         |
10 | 6, 7, 8, 9 | fzto1st 28616 |
. . . . . . . . . 10
                   |
11 | 5, 10 | syl 17 |
. . . . . . . . 9
               |
12 | 8, 9 | symgbasf1o 17024 |
. . . . . . . . 9
                           |
13 | 11, 12 | syl 17 |
. . . . . . . 8
               |
14 | 13 | adantr 467 |
. . . . . . 7
 
   
                 |
15 | | fznatpl1 11850 |
. . . . . . . 8
 
               |
16 | 1, 15 | sylan 474 |
. . . . . . 7
 
   
   
       |
17 | | eqeq1 2455 |
. . . . . . . . . . . . 13
     |
18 | | breq1 4405 |
. . . . . . . . . . . . . 14
 
   |
19 | | oveq1 6297 |
. . . . . . . . . . . . . 14
       |
20 | | id 22 |
. . . . . . . . . . . . . 14
   |
21 | 18, 19, 20 | ifbieq12d 3908 |
. . . . . . . . . . . . 13
         
       |
22 | 17, 21 | ifbieq2d 3906 |
. . . . . . . . . . . 12
                  
        |
23 | 22 | cbvmptv 4495 |
. . . . . . . . . . 11
          
                 
        |
24 | 7, 23 | eqtri 2473 |
. . . . . . . . . 10
                   |
25 | 24 | a1i 11 |
. . . . . . . . 9
 
   
              
        |
26 | | simpr 463 |
. . . . . . . . . . . . 13
      
     
    |
27 | | 1red 9658 |
. . . . . . . . . . . . . . 15
      
        |
28 | | fz1ssnn 11830 |
. . . . . . . . . . . . . . . . . . 19
       |
29 | | simpr 463 |
. . . . . . . . . . . . . . . . . . 19
 
   
      
    |
30 | 28, 29 | sseldi 3430 |
. . . . . . . . . . . . . . . . . 18
 
   
     |
31 | 30 | nnrpd 11339 |
. . . . . . . . . . . . . . . . 17
 
   
     |
32 | 31 | adantr 467 |
. . . . . . . . . . . . . . . 16
      
     
  |
33 | 27, 32 | ltaddrp2d 11372 |
. . . . . . . . . . . . . . 15
      
     
    |
34 | 27, 33 | ltned 9771 |
. . . . . . . . . . . . . 14
      
          |
35 | 34 | necomd 2679 |
. . . . . . . . . . . . 13
      
          |
36 | 26, 35 | eqnetrd 2691 |
. . . . . . . . . . . 12
      
        |
37 | 36 | neneqd 2629 |
. . . . . . . . . . 11
      
     
  |
38 | 37 | iffalsed 3892 |
. . . . . . . . . 10
      
           
       
       |
39 | 1 | adantr 467 |
. . . . . . . . . . . . . 14
 
   
     |
40 | 30 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
 
   
     |
41 | 39 | nnnn0d 10925 |
. . . . . . . . . . . . . . 15
 
   
     |
42 | | elfzle2 11803 |
. . . . . . . . . . . . . . . 16
           |
43 | 29, 42 | syl 17 |
. . . . . . . . . . . . . . 15
 
   
       |
44 | | nn0ltlem1 10996 |
. . . . . . . . . . . . . . . 16
 
       |
45 | 44 | biimpar 488 |
. . . . . . . . . . . . . . 15
   
     |
46 | 40, 41, 43, 45 | syl21anc 1267 |
. . . . . . . . . . . . . 14
 
   
     |
47 | | nnltp1le 10992 |
. . . . . . . . . . . . . . 15
 
       |
48 | 47 | biimpa 487 |
. . . . . . . . . . . . . 14
    
    |
49 | 30, 39, 46, 48 | syl21anc 1267 |
. . . . . . . . . . . . 13
 
   
   
   |
50 | 49 | adantr 467 |
. . . . . . . . . . . 12
      
       
  |
51 | 26, 50 | eqbrtrd 4423 |
. . . . . . . . . . 11
      
        |
52 | 51 | iftrued 3889 |
. . . . . . . . . 10
      
                 |
53 | 26 | oveq1d 6305 |
. . . . . . . . . . 11
      
              |
54 | 30 | nncnd 10625 |
. . . . . . . . . . . . 13
 
   
     |
55 | | 1cnd 9659 |
. . . . . . . . . . . . 13
 
   
     |
56 | 54, 55 | pncand 9987 |
. . . . . . . . . . . 12
 
   
         |
57 | 56 | adantr 467 |
. . . . . . . . . . 11
      
            |
58 | 53, 57 | eqtrd 2485 |
. . . . . . . . . 10
      
          |
59 | 38, 52, 58 | 3eqtrd 2489 |
. . . . . . . . 9
      
           
        |
60 | 25, 59, 16, 29 | fvmptd 5954 |
. . . . . . . 8
 
   
           |
61 | 60 | idi 2 |
. . . . . . 7
 
   
           |
62 | | f1ocnvfv 6177 |
. . . . . . . 8
              
            
          |
63 | 62 | imp 431 |
. . . . . . 7
                                      |
64 | 14, 16, 61, 63 | syl21anc 1267 |
. . . . . 6
 
   
            |
65 | 64 | fveq2d 5869 |
. . . . 5
 
   
                    |
66 | 65 | adantr 467 |
. . . 4
      
                     |
67 | | madjusmdetlem2.p |
. . . . . . 7
           
       |
68 | 20 | breq1d 4412 |
. . . . . . . . . 10
 
   |
69 | 68, 19, 20 | ifbieq12d 3908 |
. . . . . . . . 9
         
       |
70 | 17, 69 | ifbieq2d 3906 |
. . . . . . . 8
                  
        |
71 | 70 | cbvmptv 4495 |
. . . . . . 7
          
                 
        |
72 | 67, 71 | eqtri 2473 |
. . . . . 6
           
       |
73 | 72 | a1i 11 |
. . . . 5
      
               
        |
74 | 33, 26 | breqtrrd 4429 |
. . . . . . . . . . 11
      
     
  |
75 | 27, 74 | ltned 9771 |
. . . . . . . . . 10
      
        |
76 | 75 | necomd 2679 |
. . . . . . . . 9
      
        |
77 | 76 | neneqd 2629 |
. . . . . . . 8
      
     
  |
78 | 77 | iffalsed 3892 |
. . . . . . 7
      
           
       
       |
79 | 78 | adantlr 721 |
. . . . . 6
   
       

   
   
       
       |
80 | | simpr 463 |
. . . . . . . 8
   
       

      |
81 | 30 | ad2antrr 732 |
. . . . . . . . 9
   
       

    |
82 | | fz1ssnn 11830 |
. . . . . . . . . . 11
     |
83 | | madjusmdet.i |
. . . . . . . . . . 11
       |
84 | 82, 83 | sseldi 3430 |
. . . . . . . . . 10
   |
85 | 84 | ad3antrrr 736 |
. . . . . . . . 9
   
       

    |
86 | | simplr 762 |
. . . . . . . . 9
   
       

    |
87 | | nnltp1le 10992 |
. . . . . . . . . 10
 
       |
88 | 87 | biimpa 487 |
. . . . . . . . 9
    
    |
89 | 81, 85, 86, 88 | syl21anc 1267 |
. . . . . . . 8
   
       

  
   |
90 | 80, 89 | eqbrtrd 4423 |
. . . . . . 7
   
       

    |
91 | 90 | iftrued 3889 |
. . . . . 6
   
       

   
         |
92 | 58 | adantlr 721 |
. . . . . 6
   
       

      |
93 | 79, 91, 92 | 3eqtrd 2489 |
. . . . 5
   
       

   
   
        |
94 | 16 | adantr 467 |
. . . . 5
      
    
       |
95 | | simplr 762 |
. . . . 5
      
       
    |
96 | 73, 93, 94, 95 | fvmptd 5954 |
. . . 4
      
            |
97 | 66, 96 | eqtr2d 2486 |
. . 3
      
               |
98 | 65 | adantr 467 |
. . . 4
      
                     |
99 | 72 | a1i 11 |
. . . . 5
      
   
           
        |
100 | 78 | adantlr 721 |
. . . . . 6
   
                
       
       |
101 | 30 | ad2antrr 732 |
. . . . . . . . . . . . 13
   
             |
102 | 84 | ad3antrrr 736 |
. . . . . . . . . . . . 13
   
             |
103 | 26 | adantr 467 |
. . . . . . . . . . . . . 14
   
               |
104 | | simpr 463 |
. . . . . . . . . . . . . 14
   
             |
105 | 103, 104 | eqbrtrrd 4425 |
. . . . . . . . . . . . 13
   
           
   |
106 | 87 | biimpar 488 |
. . . . . . . . . . . . 13
      
  |
107 | 101, 102,
105, 106 | syl21anc 1267 |
. . . . . . . . . . . 12
   
             |
108 | 107 | ex 436 |
. . . . . . . . . . 11
      
          |
109 | 108 | con3d 139 |
. . . . . . . . . 10
      
      
   |
110 | 109 | imp 431 |
. . . . . . . . 9
   
             |
111 | 110 | an32s 813 |
. . . . . . . 8
   
          
  |
112 | 111 | iffalsed 3892 |
. . . . . . 7
   
                    |
113 | | simpr 463 |
. . . . . . 7
   
          
    |
114 | 112, 113 | eqtrd 2485 |
. . . . . 6
   
                      |
115 | 100, 114 | eqtrd 2485 |
. . . . 5
   
                
          |
116 | 16 | adantr 467 |
. . . . 5
      
            |
117 | 99, 115, 116, 116 | fvmptd 5954 |
. . . 4
      
       
      |
118 | 98, 117 | eqtr2d 2486 |
. . 3
      
                 |
119 | 97, 118 | ifeqda 3914 |
. 2
 
   
    
                |
120 | | f1ocnv 5826 |
. . . . . 6
            
               |
121 | 11, 12, 120 | 3syl 18 |
. . . . 5
                |
122 | | f1ofun 5816 |
. . . . 5
                 |
123 | 121, 122 | syl 17 |
. . . 4
    |
124 | 123 | adantr 467 |
. . 3
 
   
      |
125 | | fzdif2 28369 |
. . . . . . . 8
    
           
    |
126 | 3, 125 | syl 17 |
. . . . . . 7
                 |
127 | | difss 3560 |
. . . . . . 7
       
     |
128 | 126, 127 | syl6eqssr 3483 |
. . . . . 6
    
 
      |
129 | | f1odm 5818 |
. . . . . . 7
              
      |
130 | 121, 129 | syl 17 |
. . . . . 6
        |
131 | 128, 130 | sseqtr4d 3469 |
. . . . 5
    
 
   |
132 | 131 | adantr 467 |
. . . 4
 
   
            |
133 | 132, 29 | sseldd 3433 |
. . 3
 
   
      |
134 | | fvco 5941 |
. . 3
  
 
 
                |
135 | 124, 133,
134 | syl2anc 667 |
. 2
 
   
                     |
136 | 119, 135 | eqtr4d 2488 |
1
 
   
    
              |