Proof of Theorem qqhval2lem
Step | Hyp | Ref
| Expression |
1 | | drngring 18060 |
. . . . 5
   |
2 | | qqhval2.2 |
. . . . . 6
 RHom   |
3 | 2 | zrhrhm 19160 |
. . . . 5

ℤring RingHom    |
4 | 1, 3 | syl 17 |
. . . 4
 ℤring RingHom    |
5 | 4 | ad2antrr 740 |
. . 3
   chr   
 
ℤring
RingHom    |
6 | | simpr1 1036 |
. . . . . 6
   chr   
 
  |
7 | | simpr2 1037 |
. . . . . 6
   chr   
 
  |
8 | 6, 7 | gcdcld 14561 |
. . . . 5
   chr   
      |
9 | 8 | nn0zd 11061 |
. . . 4
   chr   
      |
10 | | simpr3 1038 |
. . . . 5
   chr   
    |
11 | | gcdeq0 14564 |
. . . . . . . . 9
 
    
    |
12 | 11 | simplbda 636 |
. . . . . . . 8
         |
13 | 12 | ex 441 |
. . . . . . 7
 
   
   |
14 | 13 | necon3d 2664 |
. . . . . 6
 
       |
15 | 14 | imp 436 |
. . . . 5
    
    |
16 | 6, 7, 10, 15 | syl21anc 1291 |
. . . 4
   chr   
      |
17 | | gcddvds 14556 |
. . . . . 6
 
    
    |
18 | 6, 7, 17 | syl2anc 673 |
. . . . 5
   chr   
     
    |
19 | 18 | simpld 466 |
. . . 4
   chr   
   
  |
20 | | dvdsval2 14385 |
. . . . 5
    
    
       |
21 | 20 | biimpa 492 |
. . . 4
     
           |
22 | 9, 16, 6, 19, 21 | syl31anc 1295 |
. . 3
   chr   
        |
23 | 18 | simprd 470 |
. . . 4
   chr   
   
  |
24 | | dvdsval2 14385 |
. . . . 5
    
    
       |
25 | 24 | biimpa 492 |
. . . 4
     
           |
26 | 9, 16, 7, 23, 25 | syl31anc 1295 |
. . 3
   chr   
        |
27 | | zringbas 19122 |
. . . . . . 7
  ℤring |
28 | | qqhval2.0 |
. . . . . . 7
     |
29 | 27, 28 | rhmf 18032 |
. . . . . 6
 ℤring RingHom        |
30 | 5, 29 | syl 17 |
. . . . 5
   chr   
        |
31 | 30, 26 | ffvelrnd 6038 |
. . . 4
   chr   
            |
32 | | ffn 5739 |
. . . . . 6
    
  |
33 | 30, 32 | syl 17 |
. . . . 5
   chr   
 
  |
34 | 7 | zcnd 11064 |
. . . . . . . 8
   chr   
 
  |
35 | 9 | zcnd 11064 |
. . . . . . . 8
   chr   
      |
36 | 34, 35, 10, 16 | divne0d 10421 |
. . . . . . 7
   chr   
        |
37 | | ovex 6336 |
. . . . . . . . 9
     |
38 | 37 | elsnc 3984 |
. . . . . . . 8
             |
39 | 38 | necon3bbii 2690 |
. . . . . . 7
             |
40 | 36, 39 | sylibr 217 |
. . . . . 6
   chr   
          |
41 | 1 | ad2antrr 740 |
. . . . . . 7
   chr   
 
  |
42 | | simplr 770 |
. . . . . . 7
   chr   
  chr    |
43 | | eqid 2471 |
. . . . . . . . 9
         |
44 | 28, 2, 43 | zrhker 28855 |
. . . . . . . 8

 chr                  |
45 | 44 | biimpa 492 |
. . . . . . 7
  chr  
               |
46 | 41, 42, 45 | syl2anc 673 |
. . . . . 6
   chr   
                 |
47 | 40, 46 | neleqtrrd 2571 |
. . . . 5
   chr   
                   |
48 | | elpreima 6017 |
. . . . . . . . 9
                                        |
49 | 48 | baibd 923 |
. . . . . . . 8
  
                   
                 |
50 | 49 | biimprd 231 |
. . . . . . 7
  
        
         
                  |
51 | 50 | con3dimp 448 |
. . . . . 6
                       
                |
52 | | fvex 5889 |
. . . . . . . 8
         |
53 | 52 | elsnc 3984 |
. . . . . . 7
              
              |
54 | 53 | necon3bbii 2690 |
. . . . . 6
              
              |
55 | 51, 54 | sylib 201 |
. . . . 5
                       
              |
56 | 33, 26, 47, 55 | syl21anc 1291 |
. . . 4
   chr   
                |
57 | | eqid 2471 |
. . . . . 6
Unit  Unit   |
58 | 28, 57, 43 | drngunit 18058 |
. . . . 5
          Unit                           |
59 | 58 | ad2antrr 740 |
. . . 4
   chr   
      
    Unit 
                         |
60 | 31, 56, 59 | mpbir2and 936 |
. . 3
   chr   
          Unit    |
61 | 30, 9 | ffvelrnd 6038 |
. . . 4
   chr   
          |
62 | | ovex 6336 |
. . . . . . . . 9
   |
63 | 62 | elsnc 3984 |
. . . . . . . 8
         |
64 | 63 | necon3bbii 2690 |
. . . . . . 7
         |
65 | 16, 64 | sylibr 217 |
. . . . . 6
   chr   
        |
66 | 65, 46 | neleqtrrd 2571 |
. . . . 5
   chr   
                 |
67 | | elpreima 6017 |
. . . . . . . . 9
              
                   |
68 | 67 | baibd 923 |
. . . . . . . 8
  
               
               |
69 | 68 | biimprd 231 |
. . . . . . 7
  
      
       
                |
70 | 69 | con3dimp 448 |
. . . . . 6
                   
              |
71 | | fvex 5889 |
. . . . . . . 8
       |
72 | 71 | elsnc 3984 |
. . . . . . 7
                         |
73 | 72 | necon3bbii 2690 |
. . . . . 6
                         |
74 | 70, 73 | sylib 201 |
. . . . 5
                   
            |
75 | 33, 9, 66, 74 | syl21anc 1291 |
. . . 4
   chr   
              |
76 | 28, 57, 43 | drngunit 18058 |
. . . . 5
        Unit 
                     |
77 | 76 | ad2antrr 740 |
. . . 4
   chr   
      
  Unit 
                     |
78 | 61, 75, 77 | mpbir2and 936 |
. . 3
   chr   
        Unit    |
79 | | qqhval2.1 |
. . . 4
/r   |
80 | | zringmulr 19125 |
. . . 4
  ℤring |
81 | 57, 27, 79, 80 | rhmdvd 28658 |
. . 3
  ℤring
RingHom                       Unit        Unit        
   
                                     |
82 | 5, 22, 26, 9, 60, 78, 81 | syl132anc 1310 |
. 2
   chr   
      
   
                                     |
83 | | divnumden 14776 |
. . . . . . . 8
 
  numer        denom           |
84 | 6, 83 | sylan 479 |
. . . . . . 7
    chr     
  numer        denom           |
85 | 84 | simpld 466 |
. . . . . 6
    chr     
 numer          |
86 | 85 | eqcomd 2477 |
. . . . 5
    chr     
     numer      |
87 | 86 | fveq2d 5883 |
. . . 4
    chr     
            numer       |
88 | 84 | simprd 470 |
. . . . . 6
    chr     
 denom          |
89 | 88 | eqcomd 2477 |
. . . . 5
    chr     
     denom      |
90 | 89 | fveq2d 5883 |
. . . 4
    chr     
            denom       |
91 | 87, 90 | oveq12d 6326 |
. . 3
    chr     
     
   
             numer        denom 
      |
92 | 22 | adantr 472 |
. . . . . . . . 9
    chr              |
93 | 92 | zcnd 11064 |
. . . . . . . 8
    chr              |
94 | 93 | mulm1d 10091 |
. . . . . . 7
    chr                      |
95 | | neg1cn 10735 |
. . . . . . . . 9
  |
96 | 95 | a1i 11 |
. . . . . . . 8
    chr           |
97 | 96, 93 | mulcomd 9682 |
. . . . . . 7
    chr                        |
98 | 94, 97 | eqtr3d 2507 |
. . . . . 6
    chr                      |
99 | 98 | fveq2d 5883 |
. . . . 5
    chr                              |
100 | 26 | adantr 472 |
. . . . . . . . 9
    chr              |
101 | 100 | zcnd 11064 |
. . . . . . . 8
    chr              |
102 | 101 | mulm1d 10091 |
. . . . . . 7
    chr                      |
103 | 96, 101 | mulcomd 9682 |
. . . . . . 7
    chr                        |
104 | 102, 103 | eqtr3d 2507 |
. . . . . 6
    chr                      |
105 | 104 | fveq2d 5883 |
. . . . 5
    chr                              |
106 | 99, 105 | oveq12d 6326 |
. . . 4
    chr                                                      |
107 | 6 | adantr 472 |
. . . . . . . 8
    chr          |
108 | 7 | adantr 472 |
. . . . . . . 8
    chr          |
109 | | simpr 468 |
. . . . . . . 8
    chr           |
110 | | divnumden2 28456 |
. . . . . . . 8
 
   numer         denom     
      |
111 | 107, 108,
109, 110 | syl3anc 1292 |
. . . . . . 7
    chr         numer 
   
   denom            |
112 | 111 | simpld 466 |
. . . . . 6
    chr        numer           |
113 | 112 | fveq2d 5883 |
. . . . 5
    chr           numer                |
114 | 111 | simprd 470 |
. . . . . 6
    chr        denom           |
115 | 114 | fveq2d 5883 |
. . . . 5
    chr           denom                |
116 | 113, 115 | oveq12d 6326 |
. . . 4
    chr            numer    
   denom                            |
117 | 5 | adantr 472 |
. . . . 5
    chr        ℤring RingHom    |
118 | | 1zzd 10992 |
. . . . . 6
    chr          |
119 | 118 | znegcld 11065 |
. . . . 5
    chr           |
120 | 60 | adantr 472 |
. . . . 5
    chr           
    Unit    |
121 | | neg1z 10997 |
. . . . . . . 8
  |
122 | | ax-1cn 9615 |
. . . . . . . . . 10
 |
123 | 122 | absnegi 13539 |
. . . . . . . . 9
          |
124 | | abs1 13437 |
. . . . . . . . 9
     |
125 | 123, 124 | eqtri 2493 |
. . . . . . . 8
      |
126 | | zringunit 19139 |
. . . . . . . 8
  Unit ℤring           |
127 | 121, 125,
126 | mpbir2an 934 |
. . . . . . 7
 Unit ℤring |
128 | 127 | a1i 11 |
. . . . . 6
    chr         Unit ℤring  |
129 | | elrhmunit 28657 |
. . . . . 6
  ℤring
RingHom   Unit ℤring
     Unit    |
130 | 117, 128,
129 | syl2anc 673 |
. . . . 5
    chr             Unit    |
131 | 57, 27, 79, 80 | rhmdvd 28658 |
. . . . 5
  ℤring
RingHom                      Unit       Unit                                                |
132 | 117, 92, 100, 119, 120, 130, 131 | syl132anc 1310 |
. . . 4
    chr                                                    |
133 | 106, 116,
132 | 3eqtr4rd 2516 |
. . 3
    chr                              numer    
   denom        |
134 | | simp3 1032 |
. . . . . 6
 
   |
135 | 134 | neneqd 2648 |
. . . . 5
 

  |
136 | | simp2 1031 |
. . . . . . . 8
 
   |
137 | | elz 10963 |
. . . . . . . 8

       |
138 | 136, 137 | sylib 201 |
. . . . . . 7
 
 

     |
139 | 138 | simprd 470 |
. . . . . 6
 
 
    |
140 | | 3orass 1010 |
. . . . . 6
           |
141 | 139, 140 | sylib 201 |
. . . . 5
 
 

     |
142 | | orel1 389 |
. . . . 5
             |
143 | 135, 141,
142 | sylc 61 |
. . . 4
 
 
    |
144 | 143 | adantl 473 |
. . 3
   chr   
       |
145 | 91, 133, 144 | mpjaodan 803 |
. 2
   chr   
      
   
             numer        denom 
      |
146 | 6 | zcnd 11064 |
. . . . 5
   chr   
 
  |
147 | 146, 35, 16 | divcan1d 10406 |
. . . 4
   chr   
            |
148 | 147 | fveq2d 5883 |
. . 3
   chr   
                    |
149 | 34, 35, 16 | divcan1d 10406 |
. . . 4
   chr   
            |
150 | 149 | fveq2d 5883 |
. . 3
   chr   
                    |
151 | 148, 150 | oveq12d 6326 |
. 2
   chr   
              
                 
       |
152 | 82, 145, 151 | 3eqtr3d 2513 |
1
   chr   
      numer        denom                  |