Step | Hyp | Ref
| Expression |
1 | | cnre 6821 |
. . 3
 
       |
2 | 1 | 3ad2ant3 926 |
. 2
 
 
       |
3 | | cnre 6821 |
. . . . . . 7
 
       |
4 | 3 | 3ad2ant2 925 |
. . . . . 6
 
 
       |
5 | 4 | ad2antrr 457 |
. . . . 5
             
       |
6 | | cnre 6821 |
. . . . . . . . . . 11
 
       |
7 | 6 | 3ad2ant1 924 |
. . . . . . . . . 10
 
 
       |
8 | 7 | ad2antrr 457 |
. . . . . . . . 9
             
       |
9 | 8 | ad2antrr 457 |
. . . . . . . 8
     
 
 
     
 
     
       |
10 | | simplrl 487 |
. . . . . . . . . . . 12
                 
 
     
 
       |
11 | | simplrr 488 |
. . . . . . . . . . . 12
                 
 
     
 
       |
12 | | simprl 483 |
. . . . . . . . . . . . 13
      
 
     
 
  |
13 | 12 | ad3antrrr 461 |
. . . . . . . . . . . 12
                 
 
     
 
       |
14 | | simprr 484 |
. . . . . . . . . . . . 13
      
 
     
 
  |
15 | 14 | ad3antrrr 461 |
. . . . . . . . . . . 12
                 
 
     
 
       |
16 | | apreim 7387 |
. . . . . . . . . . . 12
            #      #
#     |
17 | 10, 11, 13, 15, 16 | syl22anc 1135 |
. . . . . . . . . . 11
                 
 
     
 
      
   #      #
#     |
18 | | simpr 103 |
. . . . . . . . . . . 12
                 
 
     
 
           |
19 | | simpllr 486 |
. . . . . . . . . . . 12
                 
 
     
 
           |
20 | 18, 19 | breq12d 3768 |
. . . . . . . . . . 11
                 
 
     
 
      #  
  #
       |
21 | | simprl 483 |
. . . . . . . . . . . . . . . 16
  
      |
22 | 21 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
      
 
     
 
  |
23 | 22 | ad3antrrr 461 |
. . . . . . . . . . . . . 14
                 
 
     
 
       |
24 | 10, 23 | readdcld 6852 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   |
25 | | simprr 484 |
. . . . . . . . . . . . . . . 16
  
      |
26 | 25 | ad2antrr 457 |
. . . . . . . . . . . . . . 15
      
 
     
 
  |
27 | 26 | ad3antrrr 461 |
. . . . . . . . . . . . . 14
                 
 
     
 
       |
28 | 11, 27 | readdcld 6852 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   |
29 | 13, 23 | readdcld 6852 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   |
30 | 15, 27 | readdcld 6852 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   |
31 | | apreim 7387 |
. . . . . . . . . . . . 13
    
     
       
     #   
        #     #
      |
32 | 24, 28, 29, 30, 31 | syl22anc 1135 |
. . . . . . . . . . . 12
                 
 
     
 
        
     #   
        #     #
      |
33 | 10 | recnd 6851 |
. . . . . . . . . . . . . . 15
                 
 
     
 
       |
34 | | ax-icn 6778 |
. . . . . . . . . . . . . . . . 17
 |
35 | 34 | a1i 9 |
. . . . . . . . . . . . . . . 16
                 
 
     
 
       |
36 | 11 | recnd 6851 |
. . . . . . . . . . . . . . . 16
                 
 
     
 
       |
37 | 35, 36 | mulcld 6845 |
. . . . . . . . . . . . . . 15
                 
 
     
 
         |
38 | 23 | recnd 6851 |
. . . . . . . . . . . . . . 15
                 
 
     
 
       |
39 | 27 | recnd 6851 |
. . . . . . . . . . . . . . . 16
                 
 
     
 
       |
40 | 35, 39 | mulcld 6845 |
. . . . . . . . . . . . . . 15
                 
 
     
 
         |
41 | 33, 37, 38, 40 | add4d 6977 |
. . . . . . . . . . . . . 14
                 
 
     
 
      
    
     
   
     |
42 | | simplr 482 |
. . . . . . . . . . . . . . . 16
      
 
     
        |
43 | 42 | ad3antrrr 461 |
. . . . . . . . . . . . . . 15
                 
 
     
 
           |
44 | 18, 43 | oveq12d 5473 |
. . . . . . . . . . . . . 14
                 
 
     
 
     
   
 

      |
45 | 35, 36, 39 | adddid 6849 |
. . . . . . . . . . . . . . 15
                 
 
     
 
           
     |
46 | 45 | oveq2d 5471 |
. . . . . . . . . . . . . 14
                 
 
     
 
      

       
 

      |
47 | 41, 44, 46 | 3eqtr4d 2079 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   
       |
48 | 13 | recnd 6851 |
. . . . . . . . . . . . . . 15
                 
 
     
 
       |
49 | 15 | recnd 6851 |
. . . . . . . . . . . . . . . 16
                 
 
     
 
       |
50 | 35, 49 | mulcld 6845 |
. . . . . . . . . . . . . . 15
                 
 
     
 
         |
51 | 48, 50, 38, 40 | add4d 6977 |
. . . . . . . . . . . . . 14
                 
 
     
 
      
    
     
   
     |
52 | 19, 43 | oveq12d 5473 |
. . . . . . . . . . . . . 14
                 
 
     
 
     
   
 

      |
53 | 35, 49, 39 | adddid 6849 |
. . . . . . . . . . . . . . 15
                 
 
     
 
           
     |
54 | 53 | oveq2d 5471 |
. . . . . . . . . . . . . 14
                 
 
     
 
      

       
 

      |
55 | 51, 52, 54 | 3eqtr4d 2079 |
. . . . . . . . . . . . 13
                 
 
     
 
     
   
       |
56 | 47, 55 | breq12d 3768 |
. . . . . . . . . . . 12
                 
 
     
 
      
 #     
     #   
        |
57 | | reapadd1 7380 |
. . . . . . . . . . . . . 14
 
  #
  #      |
58 | 10, 13, 23, 57 | syl3anc 1134 |
. . . . . . . . . . . . 13
                 
 
     
 
      #
  #      |
59 | | reapadd1 7380 |
. . . . . . . . . . . . . 14
 
  #   #
     |
60 | 11, 15, 27, 59 | syl3anc 1134 |
. . . . . . . . . . . . 13
                 
 
     
 
      #   #
     |
61 | 58, 60 | orbi12d 706 |
. . . . . . . . . . . 12
                 
 
     
 
       #
#     #     #
      |
62 | 32, 56, 61 | 3bitr4d 209 |
. . . . . . . . . . 11
                 
 
     
 
      
 #    # #     |
63 | 17, 20, 62 | 3bitr4d 209 |
. . . . . . . . . 10
                 
 
     
 
      #   #
     |
64 | 63 | ex 108 |
. . . . . . . . 9
      
         
 
     
  

   
#   #       |
65 | 64 | rexlimdvva 2434 |
. . . . . . . 8
     
 
 
     
 
      
      #   #       |
66 | 9, 65 | mpd 13 |
. . . . . . 7
     
 
 
     
 
      #   #
     |
67 | 66 | ex 108 |
. . . . . 6
      
 
     
  

   
#   #       |
68 | 67 | rexlimdvva 2434 |
. . . . 5
              
      #   #       |
69 | 5, 68 | mpd 13 |
. . . 4
              #   #
     |
70 | 69 | ex 108 |
. . 3
  
      
 
 #   #
      |
71 | 70 | rexlimdvva 2434 |
. 2
 
  
      #   #       |
72 | 2, 71 | mpd 13 |
1
 
  #   #
     |