Step | Hyp | Ref
| Expression |
1 | | cnre 7950 |
. . 3
         |
2 | 1 | 3ad2ant3 1020 |
. 2
 
         |
3 | | cnre 7950 |
. . . . . . 7
         |
4 | 3 | 3ad2ant2 1019 |
. . . . . 6
 
         |
5 | 4 | ad2antrr 488 |
. . . . 5
     
 


           |
6 | | cnre 7950 |
. . . . . . . . . . 11
         |
7 | 6 | 3ad2ant1 1018 |
. . . . . . . . . 10
 
         |
8 | 7 | adantr 276 |
. . . . . . . . 9
  
   
        |
9 | 8 | ad3antrrr 492 |
. . . . . . . 8
     
 
 


   
 
             |
10 | | simplrl 535 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
11 | 10 | recnd 7982 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


     |
12 | | simprl 529 |
. . . . . . . . . . . . . . . . . . 19
  
   
  |
13 | 12 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . 18
      
 


   
 
  |
14 | 13 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
15 | 14 | recnd 7982 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


     |
16 | 11, 15 | mulcld 7974 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
17 | | simplrr 536 |
. . . . . . . . . . . . . . . . . 18
         
 


   
 
     
 


     |
18 | 17 | recnd 7982 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
19 | | simprr 531 |
. . . . . . . . . . . . . . . . . . . 20
  
   
  |
20 | 19 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
      
 


   
 
  |
21 | 20 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
         
 


   
 
     
 


     |
22 | 21 | recnd 7982 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
23 | 18, 22 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
24 | 23 | negcld 8251 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


        |
25 | | simprl 529 |
. . . . . . . . . . . . . . . . . 18
      
 


   
 
  |
26 | 25 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
27 | 26 | recnd 7982 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


     |
28 | 27, 15 | mulcld 7974 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
29 | | simprr 531 |
. . . . . . . . . . . . . . . . . . 19
      
 


   
 
  |
30 | 29 | ad3antrrr 492 |
. . . . . . . . . . . . . . . . . 18
         
 


   
 
     
 


     |
31 | 30 | recnd 7982 |
. . . . . . . . . . . . . . . . 17
         
 


   
 
     
 


     |
32 | 31, 22 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
33 | 32 | negcld 8251 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


        |
34 | | addext 8563 |
. . . . . . . . . . . . . . 15
                         #       
   #      #        |
35 | 16, 24, 28, 33, 34 | syl22anc 1239 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


           #           #      #        |
36 | | remulext1 8552 |
. . . . . . . . . . . . . . . 16
 
    #   #    |
37 | 10, 26, 14, 36 | syl3anc 1238 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


      #   #    |
38 | | apneg 8564 |
. . . . . . . . . . . . . . . . 17
    
     #      #       |
39 | 23, 32, 38 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


      #  
   #  
    |
40 | | remulext1 8552 |
. . . . . . . . . . . . . . . . 17
 
    #   #    |
41 | 17, 30, 21, 40 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


      #   #    |
42 | 39, 41 | sylbird 170 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       #    #    |
43 | 37, 42 | orim12d 786 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


       #      #      # #     |
44 | 35, 43 | syld 45 |
. . . . . . . . . . . . 13
         
 


   
 
     
 


           #         # #     |
45 | 15, 18 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
46 | 22, 11 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
47 | 15, 31 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
48 | 22, 27 | mulcld 7974 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
49 | | addext 8563 |
. . . . . . . . . . . . . . . 16
                      #          #     #       |
50 | 45, 46, 47, 48, 49 | syl22anc 1239 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


          #          #     #       |
51 | | remulext2 8553 |
. . . . . . . . . . . . . . . . 17
 
    #   #    |
52 | 17, 30, 14, 51 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


      #   #    |
53 | | remulext2 8553 |
. . . . . . . . . . . . . . . . 17
 
    #   #    |
54 | 10, 26, 21, 53 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


      #   #    |
55 | 52, 54 | orim12d 786 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       #     #     # #     |
56 | 50, 55 | syld 45 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


          #        # #     |
57 | | orcom 728 |
. . . . . . . . . . . . . 14
  # # 
 #
#    |
58 | 56, 57 | syl6ib 161 |
. . . . . . . . . . . . 13
         
 


   
 
     
 


          #        # #     |
59 | 44, 58 | jaod 717 |
. . . . . . . . . . . 12
         
 


   
 
     
 


            #              #       
 #
#     |
60 | | simpr 110 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


    
    |
61 | | simplr 528 |
. . . . . . . . . . . . . . . 16
      
 


   
 


    |
62 | 61 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


    
    |
63 | 60, 62 | oveq12d 5890 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


   
             |
64 | | simpllr 534 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


         |
65 | 64, 62 | oveq12d 5890 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


   
             |
66 | 63, 65 | breq12d 4015 |
. . . . . . . . . . . . 13
         
 


   
 
     
 


      #  
      
   #              |
67 | | mulreim 8557 |
. . . . . . . . . . . . . . 15
         
                          |
68 | 10, 17, 14, 21, 67 | syl22anc 1239 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


                                |
69 | | mulreim 8557 |
. . . . . . . . . . . . . . 15
                                    |
70 | 26, 30, 14, 21, 69 | syl22anc 1239 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


                                |
71 | 68, 70 | breq12d 4015 |
. . . . . . . . . . . . 13
         
 


   
 
     
 


      
       #          
                 #                     |
72 | 10, 14 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
73 | 17, 21 | remulcld 7984 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
74 | 73 | renegcld 8333 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


        |
75 | 72, 74 | readdcld 7983 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


            |
76 | 14, 17 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
77 | 21, 10 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
78 | 76, 77 | readdcld 7983 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


           |
79 | 26, 14 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
80 | 30, 21 | remulcld 7984 |
. . . . . . . . . . . . . . . 16
         
 


   
 
     
 


       |
81 | 80 | renegcld 8333 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


        |
82 | 79, 81 | readdcld 7983 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


            |
83 | 14, 30 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
84 | 21, 26 | remulcld 7984 |
. . . . . . . . . . . . . . 15
         
 


   
 
     
 


       |
85 | 83, 84 | readdcld 7983 |
. . . . . . . . . . . . . 14
         
 


   
 
     
 


           |
86 | | apreim 8556 |
. . . . . . . . . . . . . 14
                      
         
                  #                 
        #              #           |
87 | 75, 78, 82, 85, 86 | syl22anc 1239 |
. . . . . . . . . . . . 13
         
 


   
 
     
 


                     #                          #              #           |
88 | 66, 71, 87 | 3bitrd 214 |
. . . . . . . . . . . 12
         
 


   
 
     
 


      #  
        #              #           |
89 | | apreim 8556 |
. . . . . . . . . . . . 13
         
  #    
 #
#     |
90 | 10, 17, 26, 30, 89 | syl22anc 1239 |
. . . . . . . . . . . 12
         
 


   
 
     
 


        #    
 #
#     |
91 | 59, 88, 90 | 3imtr4d 203 |
. . . . . . . . . . 11
         
 


   
 
     
 


      #       #        |
92 | 60, 64 | breq12d 4015 |
. . . . . . . . . . 11
         
 


   
 
     
 


    #
 
  #        |
93 | 91, 92 | sylibrd 169 |
. . . . . . . . . 10
         
 


   
 
     
 


      #   #    |
94 | 93 | ex 115 |
. . . . . . . . 9
      
         
 
     
 
  
     #   #     |
95 | 94 | rexlimdvva 2602 |
. . . . . . . 8
     
 
 


   
 
      
  
     #   #     |
96 | 9, 95 | mpd 13 |
. . . . . . 7
     
 
 


   
 
        #   #    |
97 | 96 | ex 115 |
. . . . . 6
      
 


   
 
        #   #     |
98 | 97 | rexlimdvva 2602 |
. . . . 5
     
 


    
        #   #     |
99 | 5, 98 | mpd 13 |
. . . 4
     
 


      #   #    |
100 | 99 | ex 115 |
. . 3
  
   
  
     #   #     |
101 | 100 | rexlimdvva 2602 |
. 2
 
  
  
     #   #     |
102 | 2, 101 | mpd 13 |
1
 
    #   #    |