Step | Hyp | Ref
| Expression |
1 | | eqeq1 2184 |
. . . . . . . 8
     
       |
2 | 1 | anbi1d 465 |
. . . . . . 7
                         |
3 | 2 | anbi1d 465 |
. . . . . 6
              #ℝ #ℝ              
#ℝ
#ℝ      |
4 | 3 | 2rexbidv 2502 |
. . . . 5
  
             #ℝ
#ℝ  
             
#ℝ
#ℝ      |
5 | 4 | 2rexbidv 2502 |
. . . 4
  
 
            
#ℝ
#ℝ  
               
#ℝ
#ℝ      |
6 | | eqeq1 2184 |
. . . . . . . 8
     
       |
7 | 6 | anbi2d 464 |
. . . . . . 7
                         |
8 | 7 | anbi1d 465 |
. . . . . 6
              #ℝ #ℝ              
#ℝ
#ℝ      |
9 | 8 | 2rexbidv 2502 |
. . . . 5
  
             #ℝ
#ℝ  
             
#ℝ
#ℝ      |
10 | 9 | 2rexbidv 2502 |
. . . 4
  
 
            
#ℝ
#ℝ  
               
#ℝ
#ℝ      |
11 | | df-ap 8538 |
. . . 4
#       
            
#ℝ
#ℝ     |
12 | 5, 10, 11 | brabg 4269 |
. . 3
 
  #
               
#ℝ
#ℝ      |
13 | | simplll 533 |
. . . . . . . . . . . . 13
     
 
  
  |
14 | 13 | adantr 276 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
15 | | simplrl 535 |
. . . . . . . . . . . . 13
     
 
     |
16 | 15 | adantr 276 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
17 | | simplrr 536 |
. . . . . . . . . . . . 13
     
 
     |
18 | 17 | adantr 276 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
19 | | simprll 537 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ          |
20 | | rereim 8542 |
. . . . . . . . . . . 12
               |
21 | 14, 16, 18, 19, 20 | syl22anc 1239 |
. . . . . . . . . . 11
      
 
               #ℝ #ℝ    
   |
22 | 21 | simprd 114 |
. . . . . . . . . 10
      
 
               #ℝ #ℝ      |
23 | | simpllr 534 |
. . . . . . . . . . . . 13
     
 
  
  |
24 | 23 | adantr 276 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
25 | | simplrl 535 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
26 | | simplrr 536 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ      |
27 | | simprlr 538 |
. . . . . . . . . . . 12
      
 
               #ℝ #ℝ          |
28 | | rereim 8542 |
. . . . . . . . . . . 12
               |
29 | 24, 25, 26, 27, 28 | syl22anc 1239 |
. . . . . . . . . . 11
      
 
               #ℝ #ℝ    
   |
30 | 29 | simprd 114 |
. . . . . . . . . 10
      
 
               #ℝ #ℝ      |
31 | 22, 30 | eqtr4d 2213 |
. . . . . . . . 9
      
 
               #ℝ #ℝ      |
32 | | reapti 8535 |
. . . . . . . . . 10
 
 
#ℝ    |
33 | 18, 26, 32 | syl2anc 411 |
. . . . . . . . 9
      
 
               #ℝ #ℝ    
#ℝ    |
34 | 31, 33 | mpbid 147 |
. . . . . . . 8
      
 
               #ℝ #ℝ    #ℝ   |
35 | | simprr 531 |
. . . . . . . 8
      
 
               #ℝ #ℝ     #ℝ #ℝ    |
36 | 34, 35 | ecased 1349 |
. . . . . . 7
      
 
               #ℝ #ℝ    #ℝ   |
37 | 21 | simpld 112 |
. . . . . . 7
      
 
               #ℝ #ℝ      |
38 | 29 | simpld 112 |
. . . . . . 7
      
 
               #ℝ #ℝ      |
39 | 36, 37, 38 | 3brtr3d 4034 |
. . . . . 6
      
 
               #ℝ #ℝ    #ℝ   |
40 | 39 | ex 115 |
. . . . 5
     
 
               
#ℝ
#ℝ   #ℝ    |
41 | 40 | rexlimdvva 2602 |
. . . 4
                     
#ℝ
#ℝ   #ℝ    |
42 | 41 | rexlimdvva 2602 |
. . 3
 
                 
#ℝ
#ℝ   #ℝ    |
43 | 12, 42 | sylbid 150 |
. 2
 
  # #ℝ    |
44 | | ax-icn 7905 |
. . . . . . . 8
 |
45 | 44 | mul01i 8347 |
. . . . . . 7
   |
46 | 45 | oveq2i 5885 |
. . . . . 6
       |
47 | | simp1 997 |
. . . . . . . 8
 
#ℝ 
  |
48 | 47 | recnd 7985 |
. . . . . . 7
 
#ℝ 
  |
49 | 48 | addid1d 8105 |
. . . . . 6
 
#ℝ 
    |
50 | 46, 49 | eqtr2id 2223 |
. . . . 5
 
#ℝ 


    |
51 | 45 | oveq2i 5885 |
. . . . . 6
       |
52 | | simp2 998 |
. . . . . . . 8
 
#ℝ 
  |
53 | 52 | recnd 7985 |
. . . . . . 7
 
#ℝ 
  |
54 | 53 | addid1d 8105 |
. . . . . 6
 
#ℝ 
    |
55 | 51, 54 | eqtr2id 2223 |
. . . . 5
 
#ℝ 


    |
56 | | olc 711 |
. . . . . . 7
 #ℝ  #ℝ #ℝ    |
57 | 56 | 3ad2ant3 1020 |
. . . . . 6
 
#ℝ 
 #ℝ
#ℝ    |
58 | 57 | orcomd 729 |
. . . . 5
 
#ℝ 
 #ℝ
#ℝ    |
59 | 50, 55, 58 | jca31 309 |
. . . 4
 
#ℝ 
 
   
      #ℝ #ℝ     |
60 | | 0red 7957 |
. . . . . . . 8
 
#ℝ 
  |
61 | | simpr 110 |
. . . . . . . . . . . . 13
   #ℝ  
  |
62 | 61 | oveq2d 5890 |
. . . . . . . . . . . 12
   #ℝ         |
63 | 62 | oveq2d 5890 |
. . . . . . . . . . 11
   #ℝ             |
64 | 63 | eqeq2d 2189 |
. . . . . . . . . 10
   #ℝ               |
65 | 64 | anbi2d 464 |
. . . . . . . . 9
   #ℝ             
  
   
      |
66 | 61 | breq2d 4015 |
. . . . . . . . . 10
   #ℝ   
#ℝ
#ℝ    |
67 | 66 | orbi2d 790 |
. . . . . . . . 9
   #ℝ     #ℝ #ℝ 
 #ℝ
#ℝ     |
68 | 65, 67 | anbi12d 473 |
. . . . . . . 8
   #ℝ       
   
   
#ℝ
#ℝ  
 
   
      #ℝ #ℝ      |
69 | 60, 68 | rspcedv 2845 |
. . . . . . 7
 
#ℝ 
             #ℝ
#ℝ                #ℝ
#ℝ      |
70 | | simpr 110 |
. . . . . . . . . . . . 13
   #ℝ     |
71 | 70 | oveq1d 5889 |
. . . . . . . . . . . 12
   #ℝ        
    |
72 | 71 | eqeq2d 2189 |
. . . . . . . . . . 11
   #ℝ   
   


     |
73 | 72 | anbi2d 464 |
. . . . . . . . . 10
   #ℝ                           |
74 | 70 | breq2d 4015 |
. . . . . . . . . . 11
   #ℝ    #ℝ #ℝ    |
75 | 74 | orbi1d 791 |
. . . . . . . . . 10
   #ℝ    
#ℝ
#ℝ   #ℝ #ℝ     |
76 | 73, 75 | anbi12d 473 |
. . . . . . . . 9
   #ℝ                #ℝ
#ℝ      
   
   
#ℝ
#ℝ      |
77 | 76 | rexbidv 2478 |
. . . . . . . 8
   #ℝ    
            #ℝ
#ℝ                #ℝ
#ℝ      |
78 | 52, 77 | rspcedv 2845 |
. . . . . . 7
 
#ℝ 
 
            #ℝ
#ℝ   
             #ℝ
#ℝ      |
79 | 69, 78 | syld 45 |
. . . . . 6
 
#ℝ 
             #ℝ
#ℝ                 #ℝ
#ℝ      |
80 | | simpr 110 |
. . . . . . . . . . . . 13
   #ℝ     |
81 | 80 | oveq2d 5890 |
. . . . . . . . . . . 12
   #ℝ         |
82 | 81 | oveq2d 5890 |
. . . . . . . . . . 11
   #ℝ             |
83 | 82 | eqeq2d 2189 |
. . . . . . . . . 10
   #ℝ               |
84 | 83 | anbi1d 465 |
. . . . . . . . 9
   #ℝ             
  
          |
85 | 80 | breq1d 4013 |
. . . . . . . . . 10
   #ℝ   
#ℝ
#ℝ    |
86 | 85 | orbi2d 790 |
. . . . . . . . 9
   #ℝ     #ℝ #ℝ 
 #ℝ
#ℝ     |
87 | 84, 86 | anbi12d 473 |
. . . . . . . 8
   #ℝ       
       
#ℝ
#ℝ  
 
   
      #ℝ #ℝ      |
88 | 87 | 2rexbidv 2502 |
. . . . . . 7
   #ℝ         
       
#ℝ
#ℝ  
     
       
#ℝ
#ℝ      |
89 | 60, 88 | rspcedv 2845 |
. . . . . 6
 
#ℝ 
 
    
       
#ℝ
#ℝ         
       
#ℝ
#ℝ      |
90 | | simpr 110 |
. . . . . . . . . . . . 13
   #ℝ     |
91 | 90 | oveq1d 5889 |
. . . . . . . . . . . 12
   #ℝ        
    |
92 | 91 | eqeq2d 2189 |
. . . . . . . . . . 11
   #ℝ   
   


     |
93 | 92 | anbi1d 465 |
. . . . . . . . . 10
   #ℝ                           |
94 | 90 | breq1d 4013 |
. . . . . . . . . . 11
   #ℝ    #ℝ
#ℝ    |
95 | 94 | orbi1d 791 |
. . . . . . . . . 10
   #ℝ    
#ℝ
#ℝ   #ℝ #ℝ     |
96 | 93, 95 | anbi12d 473 |
. . . . . . . . 9
   #ℝ                #ℝ #ℝ      
       
#ℝ
#ℝ      |
97 | 96 | rexbidv 2478 |
. . . . . . . 8
   #ℝ    
            #ℝ #ℝ                #ℝ
#ℝ
     |
98 | 97 | 2rexbidv 2502 |
. . . . . . 7
   #ℝ    
 
            #ℝ
#ℝ  
      
       
#ℝ
#ℝ      |
99 | 47, 98 | rspcedv 2845 |
. . . . . 6
 
#ℝ 
 
     
       
#ℝ
#ℝ                  
#ℝ
#ℝ      |
100 | 79, 89, 99 | 3syld 57 |
. . . . 5
 
#ℝ 
             #ℝ
#ℝ     
            
#ℝ
#ℝ      |
101 | 12 | 3adant3 1017 |
. . . . 5
 
#ℝ 
 #   
            
#ℝ
#ℝ      |
102 | 100, 101 | sylibrd 169 |
. . . 4
 
#ℝ 
             #ℝ
#ℝ   #    |
103 | 59, 102 | mpd 13 |
. . 3
 
#ℝ 
#   |
104 | 103 | 3expia 1205 |
. 2
 
 
#ℝ
#    |
105 | 43, 104 | impbid 129 |
1
 
  #
#ℝ
   |