Step | Hyp | Ref
| Expression |
1 | | simpll 527 |
. . . . . 6
      
  |
2 | 1 | recnd 7963 |
. . . . 5
      
  |
3 | | ax-icn 7884 |
. . . . . . 7
 |
4 | 3 | a1i 9 |
. . . . . 6
         |
5 | | simplr 528 |
. . . . . . 7
      
  |
6 | 5 | recnd 7963 |
. . . . . 6
      
  |
7 | 4, 6 | mulcld 7955 |
. . . . 5
           |
8 | 2, 7 | addcld 7954 |
. . . 4
             |
9 | | simprl 529 |
. . . . . 6
      
  |
10 | 9 | recnd 7963 |
. . . . 5
      
  |
11 | | simprr 531 |
. . . . . . 7
      
  |
12 | 11 | recnd 7963 |
. . . . . 6
      
  |
13 | 4, 12 | mulcld 7955 |
. . . . 5
           |
14 | 10, 13 | addcld 7954 |
. . . 4
             |
15 | | eqeq1 2184 |
. . . . . . . . 9
  
      
           |
16 | 15 | anbi1d 465 |
. . . . . . . 8
  
                              |
17 | 16 | anbi1d 465 |
. . . . . . 7
  
               #ℝ #ℝ                  
#ℝ
#ℝ      |
18 | 17 | 2rexbidv 2502 |
. . . . . 6
  
   
             #ℝ
#ℝ  
                 
#ℝ
#ℝ      |
19 | 18 | 2rexbidv 2502 |
. . . . 5
  
   
 
            
#ℝ
#ℝ  
                   
#ℝ
#ℝ      |
20 | | eqeq1 2184 |
. . . . . . . . 9
  
      
           |
21 | 20 | anbi2d 464 |
. . . . . . . 8
  
     
                                |
22 | 21 | anbi1d 465 |
. . . . . . 7
  
                   #ℝ #ℝ             
         #ℝ #ℝ      |
23 | 22 | 2rexbidv 2502 |
. . . . . 6
  
   
    
            #ℝ
#ℝ  
            
         #ℝ #ℝ      |
24 | 23 | 2rexbidv 2502 |
. . . . 5
  
   
 
                
#ℝ
#ℝ  
              
         #ℝ #ℝ      |
25 | | df-ap 8516 |
. . . . 5
#       
            
#ℝ
#ℝ     |
26 | 19, 24, 25 | brabg 4265 |
. . . 4
      

        #     
 
           
         #ℝ #ℝ      |
27 | 8, 14, 26 | syl2anc 411 |
. . 3
         
  #    
              
         #ℝ #ℝ      |
28 | | simprr 531 |
. . . . . . 7
     
                    

        #ℝ #ℝ     #ℝ #ℝ    |
29 | 1 | ad3antrrr 492 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
30 | 9 | ad3antrrr 492 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
31 | | apreap 8521 |
. . . . . . . . . 10
 
  #
#ℝ
   |
32 | 29, 30, 31 | syl2anc 411 |
. . . . . . . . 9
     
                    

        #ℝ #ℝ     # #ℝ    |
33 | 5 | ad3antrrr 492 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
34 | 11 | ad3antrrr 492 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
35 | | apreap 8521 |
. . . . . . . . . 10
 
  #
#ℝ
   |
36 | 33, 34, 35 | syl2anc 411 |
. . . . . . . . 9
     
                    

        #ℝ #ℝ     # #ℝ    |
37 | 32, 36 | orbi12d 793 |
. . . . . . . 8
     
                    

        #ℝ #ℝ      # #   #ℝ #ℝ     |
38 | | simprll 537 |
. . . . . . . . . . . 12
     
                    

        #ℝ #ℝ     
        |
39 | | simpllr 534 |
. . . . . . . . . . . . 13
     
                    

        #ℝ #ℝ        |
40 | | cru 8536 |
. . . . . . . . . . . . 13
         
           |
41 | 29, 33, 39, 40 | syl21anc 1237 |
. . . . . . . . . . . 12
     
                    

        #ℝ #ℝ                  |
42 | 38, 41 | mpbid 147 |
. . . . . . . . . . 11
     
                    

        #ℝ #ℝ        |
43 | 42 | simpld 112 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
44 | | simprlr 538 |
. . . . . . . . . . . 12
     
                    

        #ℝ #ℝ     
        |
45 | | simplr 528 |
. . . . . . . . . . . . 13
     
                    

        #ℝ #ℝ        |
46 | | cru 8536 |
. . . . . . . . . . . . 13
         
           |
47 | 30, 34, 45, 46 | syl21anc 1237 |
. . . . . . . . . . . 12
     
                    

        #ℝ #ℝ                  |
48 | 44, 47 | mpbid 147 |
. . . . . . . . . . 11
     
                    

        #ℝ #ℝ        |
49 | 48 | simpld 112 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
50 | 43, 49 | breq12d 4013 |
. . . . . . . . 9
     
                    

        #ℝ #ℝ     #ℝ
#ℝ
   |
51 | 42 | simprd 114 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
52 | 48 | simprd 114 |
. . . . . . . . . 10
     
                    

        #ℝ #ℝ      |
53 | 51, 52 | breq12d 4013 |
. . . . . . . . 9
     
                    

        #ℝ #ℝ     #ℝ
#ℝ
   |
54 | 50, 53 | orbi12d 793 |
. . . . . . . 8
     
                    

        #ℝ #ℝ      #ℝ
#ℝ 
 #ℝ
#ℝ     |
55 | 37, 54 | bitrd 188 |
. . . . . . 7
     
                    

        #ℝ #ℝ      # #   #ℝ #ℝ     |
56 | 28, 55 | mpbird 167 |
. . . . . 6
     
                    

        #ℝ #ℝ     #
#    |
57 | 56 | ex 115 |
. . . . 5
      
                   
         #ℝ #ℝ  
 #
#     |
58 | 57 | rexlimdvva 2602 |
. . . 4
     
    
 
           
         #ℝ #ℝ  
 #
#     |
59 | 58 | rexlimdvva 2602 |
. . 3
                      
         #ℝ #ℝ  
 #
#     |
60 | 27, 59 | sylbid 150 |
. 2
         
  #      # #     |
61 | 31 | ad2ant2r 509 |
. . . . . 6
        #
#ℝ
   |
62 | 35 | ad2ant2l 508 |
. . . . . 6
        #
#ℝ
   |
63 | 61, 62 | orbi12d 793 |
. . . . 5
         #
#   #ℝ #ℝ     |
64 | 63 | pm5.32i 454 |
. . . 4
     
   #
#  
       
#ℝ
#ℝ     |
65 | | eqid 2177 |
. . . . . . . . . . . 12
         |
66 | | eqid 2177 |
. . . . . . . . . . . 12
         |
67 | 65, 66 | pm3.2i 272 |
. . . . . . . . . . 11
      
  
         |
68 | 67 | biantrur 303 |
. . . . . . . . . 10
  #ℝ #ℝ                      #ℝ
#ℝ
    |
69 | | oveq1 5875 |
. . . . . . . . . . . . . 14
      
    |
70 | 69 | eqeq2d 2189 |
. . . . . . . . . . . . 13
         
           |
71 | 70 | anbi2d 464 |
. . . . . . . . . . . 12
    
       
                            |
72 | | breq2 4004 |
. . . . . . . . . . . . 13
  #ℝ #ℝ    |
73 | 72 | orbi1d 791 |
. . . . . . . . . . . 12
  
#ℝ
#ℝ   #ℝ #ℝ     |
74 | 71, 73 | anbi12d 473 |
. . . . . . . . . . 11
                      #ℝ
#ℝ
         
  
         #ℝ
#ℝ
     |
75 | | oveq2 5876 |
. . . . . . . . . . . . . . 15
 
     |
76 | 75 | oveq2d 5884 |
. . . . . . . . . . . . . 14
 
         |
77 | 76 | eqeq2d 2189 |
. . . . . . . . . . . . 13
         
           |
78 | 77 | anbi2d 464 |
. . . . . . . . . . . 12
    
       
                            |
79 | | breq2 4004 |
. . . . . . . . . . . . 13
  #ℝ #ℝ    |
80 | 79 | orbi2d 790 |
. . . . . . . . . . . 12
  
#ℝ
#ℝ   #ℝ #ℝ     |
81 | 78, 80 | anbi12d 473 |
. . . . . . . . . . 11
                      #ℝ
#ℝ
         
  
         #ℝ
#ℝ
     |
82 | 74, 81 | rspc2ev 2856 |
. . . . . . . . . 10
 
   
       
        #ℝ
#ℝ         
       
        #ℝ
#ℝ     |
83 | 68, 82 | syl3an3b 1276 |
. . . . . . . . 9
 
 #ℝ
#ℝ
 
         
  
         #ℝ
#ℝ
    |
84 | 83 | 3expa 1203 |
. . . . . . . 8
     #ℝ #ℝ   
    
       
        #ℝ
#ℝ     |
85 | | oveq1 5875 |
. . . . . . . . . . . . 13
      
    |
86 | 85 | eqeq2d 2189 |
. . . . . . . . . . . 12
         
           |
87 | 86 | anbi1d 465 |
. . . . . . . . . . 11
    
       
                            |
88 | | breq1 4003 |
. . . . . . . . . . . 12
  #ℝ
#ℝ    |
89 | 88 | orbi1d 791 |
. . . . . . . . . . 11
  
#ℝ
#ℝ   #ℝ #ℝ     |
90 | 87, 89 | anbi12d 473 |
. . . . . . . . . 10
                      #ℝ #ℝ          
  
         #ℝ
#ℝ
     |
91 | 90 | 2rexbidv 2502 |
. . . . . . . . 9
  
    
       
        #ℝ
#ℝ  
         
  
         #ℝ
#ℝ
     |
92 | | oveq2 5876 |
. . . . . . . . . . . . . 14
 
     |
93 | 92 | oveq2d 5884 |
. . . . . . . . . . . . 13
 
         |
94 | 93 | eqeq2d 2189 |
. . . . . . . . . . . 12
         
           |
95 | 94 | anbi1d 465 |
. . . . . . . . . . 11
    
       
                            |
96 | | breq1 4003 |
. . . . . . . . . . . 12
  #ℝ
#ℝ    |
97 | 96 | orbi2d 790 |
. . . . . . . . . . 11
  
#ℝ
#ℝ   #ℝ #ℝ     |
98 | 95, 97 | anbi12d 473 |
. . . . . . . . . 10
                      #ℝ
#ℝ
         
  
         #ℝ
#ℝ
     |
99 | 98 | 2rexbidv 2502 |
. . . . . . . . 9
  
    
       
        #ℝ
#ℝ  
         
  
         #ℝ
#ℝ
     |
100 | 91, 99 | rspc2ev 2856 |
. . . . . . . 8
 

        
  
         #ℝ
#ℝ
                 
         #ℝ #ℝ     |
101 | 84, 100 | syl3an3 1273 |
. . . . . . 7
 
    #ℝ #ℝ      
           
         #ℝ #ℝ     |
102 | 101 | 3expa 1203 |
. . . . . 6
        #ℝ
#ℝ
                 
         #ℝ #ℝ     |
103 | 102 | anassrs 400 |
. . . . 5
     
  
#ℝ
#ℝ                 
         #ℝ #ℝ     |
104 | 27 | adantr 276 |
. . . . 5
     
  
#ℝ
#ℝ        #  
 
              
         #ℝ #ℝ      |
105 | 103, 104 | mpbird 167 |
. . . 4
     
  
#ℝ
#ℝ   
   #       |
106 | 64, 105 | sylbi 121 |
. . 3
     
   #
#       #  
    |
107 | 106 | ex 115 |
. 2
         #
#      #  
     |
108 | 60, 107 | impbid 129 |
1
         
  #    
 #
#     |