Step Hyp Ref
Expression 1 elznn0nn 10903 . . 3
2 elznn0nn 10903 . . . 4
3 expmul 12211 . . . . . . . 8
4 3 3expia 1198 . . . . . . 7
5 4 adantlr 714 . . . . . 6
6 simp2l 1022 . . . . . . . . . . . . . 14
7 6 recnd 9643 . . . . . . . . . . . . 13
8 simp3 998 . . . . . . . . . . . . . 14
9 8 nn0cnd 10879 . . . . . . . . . . . . 13
10 7 , 9 mulneg1d 10034 . . . . . . . . . . . 12
11 10 oveq2d 6312 . . . . . . . . . . 11
12 simp1l 1020 . . . . . . . . . . . 12
13 simp2r 1023 . . . . . . . . . . . . 13
14 13 nnnn0d 10877 . . . . . . . . . . . 12
15 expmul 12211 . . . . . . . . . . . 12
16 12 , 14 , 8 , 15 syl3anc 1228 . . . . . . . . . . 11
17 11 , 16 eqtr3d 2500 . . . . . . . . . 10
18 17 oveq2d 6312 . . . . . . . . 9
19 expcl 12184 . . . . . . . . . . 11
20 12 , 14 , 19 syl2anc 661 . . . . . . . . . 10
21 simp1r 1021 . . . . . . . . . . 11
22 13 nnzd 10993 . . . . . . . . . . 11
23 expne0i 12198 . . . . . . . . . . 11
24 12 , 21 , 22 , 23 syl3anc 1228 . . . . . . . . . 10
25 8 nn0zd 10992 . . . . . . . . . 10
26 exprec 12207 . . . . . . . . . 10
27 20 , 24 , 25 , 26 syl3anc 1228 . . . . . . . . 9
28 18 , 27 eqtr4d 2501 . . . . . . . 8
29 7 , 9 mulcld 9637 . . . . . . . . 9
30 14 , 8 nn0mulcld 10882 . . . . . . . . . 10
31 10 , 30 eqeltrrd 2546 . . . . . . . . 9
32 expneg2 12175 . . . . . . . . 9
33 12 , 29 , 31 , 32 syl3anc 1228 . . . . . . . 8
34 expneg2 12175 . . . . . . . . . 10
35 12 , 7 , 14 , 34 syl3anc 1228 . . . . . . . . 9
36 35 oveq1d 6311 . . . . . . . 8
37 28 , 33 , 36 3eqtr4d 2508 . . . . . . 7
38 37 3expia 1198 . . . . . 6
39 5 , 38 jaodan 785 . . . . 5
40 simp2 997 . . . . . . . . . . . . 13
41 40 nn0cnd 10879 . . . . . . . . . . . 12
42 simp3l 1024 . . . . . . . . . . . . 13
43 42 recnd 9643 . . . . . . . . . . . 12
44 41 , 43 mulneg2d 10035 . . . . . . . . . . 11
45 44 oveq2d 6312 . . . . . . . . . 10
46 simp1l 1020 . . . . . . . . . . 11
47 simp3r 1025 . . . . . . . . . . . 12
48 47 nnnn0d 10877 . . . . . . . . . . 11
49 expmul 12211 . . . . . . . . . . 11
50 46 , 40 , 48 , 49 syl3anc 1228 . . . . . . . . . 10
51 45 , 50 eqtr3d 2500 . . . . . . . . 9
52 51 oveq2d 6312 . . . . . . . 8
53 41 , 43 mulcld 9637 . . . . . . . . 9
54 40 , 48 nn0mulcld 10882 . . . . . . . . . 10
55 44 , 54 eqeltrrd 2546 . . . . . . . . 9
56 46 , 53 , 55 , 32 syl3anc 1228 . . . . . . . 8
57 expcl 12184 . . . . . . . . . 10
58 46 , 40 , 57 syl2anc 661 . . . . . . . . 9
59 expneg2 12175 . . . . . . . . 9
60 58 , 43 , 48 , 59 syl3anc 1228 . . . . . . . 8
61 52 , 56 , 60 3eqtr4d 2508 . . . . . . 7
62 61 3expia 1198 . . . . . 6
63 simp1l 1020 . . . . . . . . . 10
64 simp2l 1022 . . . . . . . . . . 11
65 64 recnd 9643 . . . . . . . . . 10
66 simp2r 1023 . . . . . . . . . . 11
67 66 nnnn0d 10877 . . . . . . . . . 10
68 63 , 65 , 67 , 34 syl3anc 1228 . . . . . . . . 9
69 68 oveq1d 6311 . . . . . . . 8
70 63 , 67 , 19 syl2anc 661 . . . . . . . . . 10
71 simp1r 1021 . . . . . . . . . . 11
72 66 nnzd 10993 . . . . . . . . . . 11
73 63 , 71 , 72 , 23 syl3anc 1228 . . . . . . . . . 10
74 70 , 73 reccld 10338 . . . . . . . . 9
75 simp3l 1024 . . . . . . . . . 10
76 75 recnd 9643 . . . . . . . . 9
77 simp3r 1025 . . . . . . . . . 10
78 77 nnnn0d 10877 . . . . . . . . 9
79 expneg2 12175 . . . . . . . . 9
80 74 , 76 , 78 , 79 syl3anc 1228 . . . . . . . 8
81 77 nnzd 10993 . . . . . . . . . . 11
82 exprec 12207 . . . . . . . . . . 11
83 70 , 73 , 81 , 82 syl3anc 1228 . . . . . . . . . 10
84 83 oveq2d 6312 . . . . . . . . 9
85 expcl 12184 . . . . . . . . . . 11
86 70 , 78 , 85 syl2anc 661 . . . . . . . . . 10
87 expne0i 12198 . . . . . . . . . . 11
88 70 , 73 , 81 , 87 syl3anc 1228 . . . . . . . . . 10
89 86 , 88 recrecd 10342 . . . . . . . . 9
90 expmul 12211 . . . . . . . . . . 11
91 63 , 67 , 78 , 90 syl3anc 1228 . . . . . . . . . 10
92 65 , 76 mul2negd 10036 . . . . . . . . . . 11
93 92 oveq2d 6312 . . . . . . . . . 10
94 91 , 93 eqtr3d 2500 . . . . . . . . 9
95 84 , 89 , 94 3eqtrd 2502 . . . . . . . 8
96 69 , 80 , 95 3eqtrrd 2503 . . . . . . 7
97 96 3expia 1198 . . . . . 6
98 62 , 97 jaodan 785 . . . . 5
99 39 , 98 jaod 380 . . . 4
100 2 , 99 sylan2b 475 . . 3
101 1 , 100 syl5bi 217 . 2
102 101 impr 619 1
