Step | Hyp | Ref
| Expression |
1 | | elex 3056 |
. . . 4
   |
2 | 1 | adantr 467 |
. . 3
  chr  
  |
3 | | qqhval2.1 |
. . . 4
/r   |
4 | | eqid 2453 |
. . . 4
         |
5 | | qqhval2.2 |
. . . 4
 RHom   |
6 | 3, 4, 5 | qqhval 28790 |
. . 3
 QQHom  

    Unit                     |
7 | 2, 6 | syl 17 |
. 2
  chr  
QQHom        Unit                     |
8 | | eqidd 2454 |
. . . 4
  chr  
  |
9 | | qqhval2.0 |
. . . . 5
     |
10 | | eqid 2453 |
. . . . 5
         |
11 | 9, 5, 10 | zrhunitpreima 28794 |
. . . 4
  chr  
    Unit         |
12 | | mpt2eq12 6356 |
. . . 4
      Unit              Unit           
                     
         |
13 | 8, 11, 12 | syl2anc 667 |
. . 3
  chr  
      Unit           
                     
         |
14 | 13 | rneqd 5065 |
. 2
  chr  
      Unit           
                     
         |
15 | | nfv 1763 |
. . . 4
   chr    |
16 | | nfab1 2596 |
. . . 4
   
              
        |
17 | | nfcv 2594 |
. . . 4
     
     numer      denom       |
18 | | simpr 463 |
. . . . . . . . . 10
    chr                         
                 |
19 | | zssq 11278 |
. . . . . . . . . . . 12
 |
20 | | simplrl 771 |
. . . . . . . . . . . 12
    chr                         
  |
21 | 19, 20 | sseldi 3432 |
. . . . . . . . . . 11
    chr                         
  |
22 | | simplrr 772 |
. . . . . . . . . . . . 13
    chr                         

     |
23 | 22 | eldifad 3418 |
. . . . . . . . . . . 12
    chr                         
  |
24 | 19, 23 | sseldi 3432 |
. . . . . . . . . . 11
    chr                         
  |
25 | 22 | eldifbd 3419 |
. . . . . . . . . . . 12
    chr                         
    |
26 | | elsn 3984 |
. . . . . . . . . . . . 13
     |
27 | 26 | necon3bbii 2673 |
. . . . . . . . . . . 12
     |
28 | 25, 27 | sylib 200 |
. . . . . . . . . . 11
    chr                         
  |
29 | | qdivcl 11292 |
. . . . . . . . . . 11
 
     |
30 | 21, 24, 28, 29 | syl3anc 1269 |
. . . . . . . . . 10
    chr                         
    |
31 | | simplll 769 |
. . . . . . . . . . 11
    chr                         
  |
32 | | simpllr 770 |
. . . . . . . . . . 11
    chr                         
chr    |
33 | 9, 3, 5 | qqhval2lem 28797 |
. . . . . . . . . . . 12
   chr   
      numer        denom                  |
34 | 33 | eqcomd 2459 |
. . . . . . . . . . 11
   chr   
                numer 
      denom 
      |
35 | 31, 32, 20, 23, 28, 34 | syl23anc 1276 |
. . . . . . . . . 10
    chr                         
              numer        denom 
      |
36 | | ovex 6323 |
. . . . . . . . . . 11
   |
37 | | ovex 6323 |
. . . . . . . . . . 11
           |
38 | | opeq12 4171 |
. . . . . . . . . . . . 13
   
                      
        |
39 | 38 | eqeq2d 2463 |
. . . . . . . . . . . 12
   
              
                  |
40 | | simpl 459 |
. . . . . . . . . . . . . 14
   
               |
41 | 40 | eleq1d 2515 |
. . . . . . . . . . . . 13
   
                 |
42 | | simpr 463 |
. . . . . . . . . . . . . 14
   
                       |
43 | 40 | fveq2d 5874 |
. . . . . . . . . . . . . . . 16
   
           numer  numer      |
44 | 43 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
   
              numer      numer       |
45 | 40 | fveq2d 5874 |
. . . . . . . . . . . . . . . 16
   
           denom  denom      |
46 | 45 | fveq2d 5874 |
. . . . . . . . . . . . . . 15
   
              denom      denom       |
47 | 44, 46 | oveq12d 6313 |
. . . . . . . . . . . . . 14
   
               numer      denom        numer 
      denom 
      |
48 | 42, 47 | eqeq12d 2468 |
. . . . . . . . . . . . 13
   
                numer      denom                  numer 
      denom 
       |
49 | 41, 48 | anbi12d 718 |
. . . . . . . . . . . 12
   
                 numer      denom    
       
         numer        denom          |
50 | 39, 49 | anbi12d 718 |
. . . . . . . . . . 11
   
                     numer      denom     
         
                       numer 
      denom 
         |
51 | 36, 37, 50 | spc2ev 3144 |
. . . . . . . . . 10
                
                 numer 
      denom 
                   numer      denom        |
52 | 18, 30, 35, 51 | syl12anc 1267 |
. . . . . . . . 9
    chr                         
             numer      denom        |
53 | 52 | ex 436 |
. . . . . . . 8
   chr   
                     
             numer      denom         |
54 | 53 | rexlimdvva 2888 |
. . . . . . 7
  chr  
 
              
              
    numer      denom         |
55 | 54 | imp 431 |
. . . . . 6
   chr   
              
      
             numer      denom        |
56 | | 19.42vv 1838 |
. . . . . . 7
       chr       
    numer      denom      
 
chr                numer      denom         |
57 | | simprrl 775 |
. . . . . . . . . 10
   chr       
    numer      denom         |
58 | | qnumcl 14701 |
. . . . . . . . . 10
 numer    |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
   chr       
    numer      denom       numer    |
60 | | qdencl 14702 |
. . . . . . . . . . . 12
 denom    |
61 | 57, 60 | syl 17 |
. . . . . . . . . . 11
   chr       
    numer      denom       denom    |
62 | 61 | nnzd 11046 |
. . . . . . . . . 10
   chr       
    numer      denom       denom    |
63 | | nnne0 10649 |
. . . . . . . . . . 11
 denom  denom    |
64 | | elsni 3995 |
. . . . . . . . . . . 12
 denom    denom    |
65 | 64 | necon3ai 2651 |
. . . . . . . . . . 11
 denom  denom      |
66 | 61, 63, 65 | 3syl 18 |
. . . . . . . . . 10
   chr       
    numer      denom       denom      |
67 | 62, 66 | eldifd 3417 |
. . . . . . . . 9
   chr       
    numer      denom       denom        |
68 | | simprl 765 |
. . . . . . . . . 10
   chr       
    numer      denom            |
69 | | qeqnumdivden 14707 |
. . . . . . . . . . . 12
  numer  denom     |
70 | 57, 69 | syl 17 |
. . . . . . . . . . 11
   chr       
    numer      denom        numer  denom     |
71 | | simprrr 776 |
. . . . . . . . . . 11
   chr       
    numer      denom           numer      denom      |
72 | 70, 71 | opeq12d 4177 |
. . . . . . . . . 10
   chr       
    numer      denom            numer  denom        numer      denom       |
73 | 68, 72 | eqtrd 2487 |
. . . . . . . . 9
   chr       
    numer      denom         numer  denom        numer      denom       |
74 | | oveq1 6302 |
. . . . . . . . . . . 12
 numer 
   numer     |
75 | | fveq2 5870 |
. . . . . . . . . . . . 13
 numer 
       numer     |
76 | 75 | oveq1d 6310 |
. . . . . . . . . . . 12
 numer 
              numer          |
77 | 74, 76 | opeq12d 4177 |
. . . . . . . . . . 11
 numer 
                 numer        numer           |
78 | 77 | eqeq2d 2463 |
. . . . . . . . . 10
 numer 
         
        numer        numer            |
79 | | oveq2 6303 |
. . . . . . . . . . . 12
 denom 
 numer    numer  denom     |
80 | | fveq2 5870 |
. . . . . . . . . . . . 13
 denom 
       denom     |
81 | 80 | oveq2d 6311 |
. . . . . . . . . . . 12
 denom 
    numer            numer      denom      |
82 | 79, 81 | opeq12d 4177 |
. . . . . . . . . . 11
 denom 
  numer        numer        
  numer  denom        numer      denom       |
83 | 82 | eqeq2d 2463 |
. . . . . . . . . 10
 denom 
   numer        numer        
  numer  denom        numer      denom        |
84 | 78, 83 | rspc2ev 3163 |
. . . . . . . . 9
  numer  denom        numer  denom        numer      denom                     
        |
85 | 59, 67, 73, 84 | syl3anc 1269 |
. . . . . . . 8
   chr       
    numer      denom                      
        |
86 | 85 | exlimivv 1780 |
. . . . . . 7
       chr       
    numer      denom                      
        |
87 | 56, 86 | sylbir 217 |
. . . . . 6
   chr                numer      denom                               |
88 | 55, 87 | impbida 844 |
. . . . 5
  chr  
 
              
              
    numer      denom         |
89 | | abid 2441 |
. . . . 5
                        
               
        |
90 | | elopab 4712 |
. . . . 5
     
    numer      denom              
    numer      denom        |
91 | 88, 89, 90 | 3bitr4g 292 |
. . . 4
  chr  
  
              
           
    numer      denom         |
92 | 15, 16, 17, 91 | eqrd 3452 |
. . 3
  chr  
                                 numer      denom        |
93 | | eqid 2453 |
. . . 4
              
                     
        |
94 | 93 | rnmpt2 6411 |
. . 3
              
                       
        |
95 | | df-mpt 4466 |
. . 3
     numer      denom         
    numer      denom       |
96 | 92, 94, 95 | 3eqtr4g 2512 |
. 2
  chr  
              
            numer      denom       |
97 | 7, 14, 96 | 3eqtrd 2491 |
1
  chr  
QQHom       numer      denom       |