Step | Hyp | Ref
| Expression |
1 | | cnre 7944 |
. . 3
         |
2 | | recexaplem2 8598 |
. . . . . . . . 9
 
    #        #   |
3 | 2 | 3expia 1205 |
. . . . . . . 8
 
      #       #    |
4 | | remulcl 7930 |
. . . . . . . . . . . 12
 
     |
5 | 4 | anidms 397 |
. . . . . . . . . . 11
     |
6 | | remulcl 7930 |
. . . . . . . . . . . 12
 
     |
7 | 6 | anidms 397 |
. . . . . . . . . . 11
     |
8 | | readdcl 7928 |
. . . . . . . . . . 11
               |
9 | 5, 7, 8 | syl2an 289 |
. . . . . . . . . 10
 
         |
10 | | 0re 7948 |
. . . . . . . . . 10
 |
11 | | apreap 8534 |
. . . . . . . . . 10
       
        #       #ℝ    |
12 | 9, 10, 11 | sylancl 413 |
. . . . . . . . 9
 
        #       #ℝ    |
13 | | recexre 8525 |
. . . . . . . . . . . 12
              #ℝ             |
14 | 9, 13 | sylan 283 |
. . . . . . . . . . 11
         
#ℝ  
          |
15 | | recn 7935 |
. . . . . . . . . . . . 13
   |
16 | | recn 7935 |
. . . . . . . . . . . . 13
   |
17 | | recn 7935 |
. . . . . . . . . . . . . . 15
   |
18 | | ax-icn 7897 |
. . . . . . . . . . . . . . . . . . . . 21
 |
19 | | mulcl 7929 |
. . . . . . . . . . . . . . . . . . . . 21
 
     |
20 | 18, 19 | mpan 424 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
21 | | subcl 8146 |
. . . . . . . . . . . . . . . . . . . 20
  
   
    |
22 | 20, 21 | sylan2 286 |
. . . . . . . . . . . . . . . . . . 19
 
  
    |
23 | | mulcl 7929 |
. . . . . . . . . . . . . . . . . . 19
   
 
   
     |
24 | 22, 23 | sylan 283 |
. . . . . . . . . . . . . . . . . 18
             |
25 | 24 | adantr 276 |
. . . . . . . . . . . . . . . . 17
                 
     |
26 | | addcl 7927 |
. . . . . . . . . . . . . . . . . . . . . 22
  
        |
27 | 20, 26 | sylan2 286 |
. . . . . . . . . . . . . . . . . . . . 21
 
       |
28 | 27 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
           |
29 | 22 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
      
    |
30 | | simpr 110 |
. . . . . . . . . . . . . . . . . . . 20
       |
31 | 28, 29, 30 | mulassd 7971 |
. . . . . . . . . . . . . . . . . . 19
            
                  |
32 | | recextlem1 8597 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   |
33 | 32 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
           
           |
34 | 33 | oveq1d 5884 |
. . . . . . . . . . . . . . . . . . 19
            
              |
35 | 31, 34 | eqtr3d 2212 |
. . . . . . . . . . . . . . . . . 18
            
              |
36 | | id 19 |
. . . . . . . . . . . . . . . . . 18
                   |
37 | 35, 36 | sylan9eq 2230 |
. . . . . . . . . . . . . . . . 17
                      
      |
38 | | oveq2 5877 |
. . . . . . . . . . . . . . . . . . 19
                    
      |
39 | 38 | eqeq1d 2186 |
. . . . . . . . . . . . . . . . . 18
                             |
40 | 39 | rspcev 2841 |
. . . . . . . . . . . . . . . . 17
    
          
              |
41 | 25, 37, 40 | syl2anc 411 |
. . . . . . . . . . . . . . . 16
               
        |
42 | 41 | exp31 364 |
. . . . . . . . . . . . . . 15
 
                      |
43 | 17, 42 | syl5 32 |
. . . . . . . . . . . . . 14
 
                      |
44 | 43 | rexlimdv 2593 |
. . . . . . . . . . . . 13
 
                     |
45 | 15, 16, 44 | syl2an 289 |
. . . . . . . . . . . 12
 
                     |
46 | 45 | adantr 276 |
. . . . . . . . . . 11
         
#ℝ                      |
47 | 14, 46 | mpd 13 |
. . . . . . . . . 10
         
#ℝ  
        |
48 | 47 | ex 115 |
. . . . . . . . 9
 
       
#ℝ           |
49 | 12, 48 | sylbid 150 |
. . . . . . . 8
 
        # 
         |
50 | 3, 49 | syld 45 |
. . . . . . 7
 
      # 
         |
51 | 50 | adantr 276 |
. . . . . 6
        
     #
          |
52 | | breq1 4003 |
. . . . . . 7
      #
    #    |
53 | 52 | adantl 277 |
. . . . . 6
        
 #     #    |
54 | | oveq1 5876 |
. . . . . . . . 9
     
         |
55 | 54 | eqeq1d 2186 |
. . . . . . . 8
                 |
56 | 55 | rexbidv 2478 |
. . . . . . 7
      

 
         |
57 | 56 | adantl 277 |
. . . . . 6
        
 


          |
58 | 51, 53, 57 | 3imtr4d 203 |
. . . . 5
        
 #  
    |
59 | 58 | ex 115 |
. . . 4
 
       #  
     |
60 | 59 | rexlimivv 2600 |
. . 3
  
     #
      |
61 | 1, 60 | syl 14 |
. 2
  #
      |
62 | 61 | imp 124 |
1
  #       |