Step | Hyp | Ref
| Expression |
1 | | simpll1 1025 |
. . . 4
|
2 | | simpll2 1026 |
. . . . 5
|
3 | 2 | nn0zd 9303 |
. . . 4
|
4 | | simpll3 1027 |
. . . . 5
|
5 | 4 | nn0zd 9303 |
. . . 4
|
6 | | simplr 520 |
. . . 4
|
7 | | simpr 109 |
. . . 4
|
8 | | ltexp2a 10498 |
. . . 4
|
9 | 1, 3, 5, 6, 7, 8 | syl32anc 1235 |
. . 3
|
10 | 9 | ex 114 |
. 2
|
11 | | oveq2 5845 |
. . . . 5
|
12 | 11 | breq1d 3987 |
. . . 4
|
13 | | breq1 3980 |
. . . 4
|
14 | 12, 13 | imbi12d 233 |
. . 3
|
15 | | simpl3 991 |
. . . 4
|
16 | | simpl1 989 |
. . . 4
|
17 | | simpr 109 |
. . . 4
|
18 | | oveq2 5845 |
. . . . . . . . . 10
|
19 | 18 | breq2d 3989 |
. . . . . . . . 9
|
20 | | breq2 3981 |
. . . . . . . . 9
|
21 | 19, 20 | imbi12d 233 |
. . . . . . . 8
|
22 | 21 | ralbidv 2464 |
. . . . . . 7
|
23 | 22 | imbi2d 229 |
. . . . . 6
|
24 | | oveq2 5845 |
. . . . . . . . . 10
|
25 | 24 | breq2d 3989 |
. . . . . . . . 9
|
26 | | breq2 3981 |
. . . . . . . . 9
|
27 | 25, 26 | imbi12d 233 |
. . . . . . . 8
|
28 | 27 | ralbidv 2464 |
. . . . . . 7
|
29 | 28 | imbi2d 229 |
. . . . . 6
|
30 | | oveq2 5845 |
. . . . . . . . . 10
|
31 | 30 | breq2d 3989 |
. . . . . . . . 9
|
32 | | breq2 3981 |
. . . . . . . . 9
|
33 | 31, 32 | imbi12d 233 |
. . . . . . . 8
|
34 | 33 | ralbidv 2464 |
. . . . . . 7
|
35 | 34 | imbi2d 229 |
. . . . . 6
|
36 | | oveq2 5845 |
. . . . . . . . . 10
|
37 | 36 | breq2d 3989 |
. . . . . . . . 9
|
38 | | breq2 3981 |
. . . . . . . . 9
|
39 | 37, 38 | imbi12d 233 |
. . . . . . . 8
|
40 | 39 | ralbidv 2464 |
. . . . . . 7
|
41 | 40 | imbi2d 229 |
. . . . . 6
|
42 | | recn 7878 |
. . . . . . . . . . . 12
|
43 | 42 | ad2antrr 480 |
. . . . . . . . . . 11
|
44 | 43 | exp0d 10572 |
. . . . . . . . . 10
|
45 | | 1re 7890 |
. . . . . . . . . 10
|
46 | 44, 45 | eqeltrdi 2255 |
. . . . . . . . 9
|
47 | | simpll 519 |
. . . . . . . . . 10
|
48 | | simpr 109 |
. . . . . . . . . 10
|
49 | 47, 48 | reexpcld 10595 |
. . . . . . . . 9
|
50 | | 1red 7906 |
. . . . . . . . . . . 12
|
51 | | simplr 520 |
. . . . . . . . . . . 12
|
52 | 50, 47, 51 | ltled 8009 |
. . . . . . . . . . 11
|
53 | 47, 48, 52 | expge1d 10597 |
. . . . . . . . . 10
|
54 | 44, 53 | eqbrtrd 3999 |
. . . . . . . . 9
|
55 | 46, 49, 54 | lensymd 8012 |
. . . . . . . 8
|
56 | 55 | pm2.21d 609 |
. . . . . . 7
|
57 | 56 | ralrimiva 2537 |
. . . . . 6
|
58 | | oveq2 5845 |
. . . . . . . . . . . 12
|
59 | 58 | breq1d 3987 |
. . . . . . . . . . 11
|
60 | | breq1 3980 |
. . . . . . . . . . 11
|
61 | 59, 60 | imbi12d 233 |
. . . . . . . . . 10
|
62 | 61 | cbvralv 2690 |
. . . . . . . . 9
|
63 | | simplr 520 |
. . . . . . . . . . . . . . . . . 18
|
64 | | simprl 521 |
. . . . . . . . . . . . . . . . . . . . 21
|
65 | 64 | ad4antr 486 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | 65 | recnd 7919 |
. . . . . . . . . . . . . . . . . . 19
|
67 | | simpr 109 |
. . . . . . . . . . . . . . . . . . 19
|
68 | | expm1t 10474 |
. . . . . . . . . . . . . . . . . . 19
|
69 | 66, 67, 68 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
|
70 | | simp-5l 533 |
. . . . . . . . . . . . . . . . . . 19
|
71 | 66, 70 | expp1d 10579 |
. . . . . . . . . . . . . . . . . 18
|
72 | 63, 69, 71 | 3brtr3d 4008 |
. . . . . . . . . . . . . . . . 17
|
73 | | nnm1nn0 9147 |
. . . . . . . . . . . . . . . . . . . 20
|
74 | 73 | adantl 275 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 65, 74 | reexpcld 10595 |
. . . . . . . . . . . . . . . . . 18
|
76 | 65, 70 | reexpcld 10595 |
. . . . . . . . . . . . . . . . . 18
|
77 | | 0red 7892 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | | 1red 7906 |
. . . . . . . . . . . . . . . . . . . . 21
|
79 | | 0lt1 8017 |
. . . . . . . . . . . . . . . . . . . . . 22
|
80 | 79 | a1i 9 |
. . . . . . . . . . . . . . . . . . . . 21
|
81 | | simprr 522 |
. . . . . . . . . . . . . . . . . . . . 21
|
82 | 77, 78, 64, 80, 81 | lttrd 8016 |
. . . . . . . . . . . . . . . . . . . 20
|
83 | 64, 82 | elrpd 9621 |
. . . . . . . . . . . . . . . . . . 19
|
84 | 83 | ad4antr 486 |
. . . . . . . . . . . . . . . . . 18
|
85 | 75, 76, 84 | ltmul1d 9666 |
. . . . . . . . . . . . . . . . 17
|
86 | 72, 85 | mpbird 166 |
. . . . . . . . . . . . . . . 16
|
87 | | oveq2 5845 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 87 | breq1d 3987 |
. . . . . . . . . . . . . . . . . 18
|
89 | | breq1 3980 |
. . . . . . . . . . . . . . . . . 18
|
90 | 88, 89 | imbi12d 233 |
. . . . . . . . . . . . . . . . 17
|
91 | | simp-4r 532 |
. . . . . . . . . . . . . . . . 17
|
92 | 90, 91, 74 | rspcdva 2831 |
. . . . . . . . . . . . . . . 16
|
93 | 86, 92 | mpd 13 |
. . . . . . . . . . . . . . 15
|
94 | | nnz 9202 |
. . . . . . . . . . . . . . . . 17
|
95 | 94 | adantl 275 |
. . . . . . . . . . . . . . . 16
|
96 | 70 | nn0zd 9303 |
. . . . . . . . . . . . . . . 16
|
97 | | zlem1lt 9239 |
. . . . . . . . . . . . . . . 16
|
98 | 95, 96, 97 | syl2anc 409 |
. . . . . . . . . . . . . . 15
|
99 | 93, 98 | mpbird 166 |
. . . . . . . . . . . . . 14
|
100 | | zleltp1 9238 |
. . . . . . . . . . . . . . 15
|
101 | 95, 96, 100 | syl2anc 409 |
. . . . . . . . . . . . . 14
|
102 | 99, 101 | mpbid 146 |
. . . . . . . . . . . . 13
|
103 | | simpr 109 |
. . . . . . . . . . . . . 14
|
104 | | nn0p1gt0 9135 |
. . . . . . . . . . . . . . 15
|
105 | 104 | ad5antr 488 |
. . . . . . . . . . . . . 14
|
106 | 103, 105 | eqbrtrd 3999 |
. . . . . . . . . . . . 13
|
107 | | simplr 520 |
. . . . . . . . . . . . . 14
|
108 | | elnn0 9108 |
. . . . . . . . . . . . . 14
|
109 | 107, 108 | sylib 121 |
. . . . . . . . . . . . 13
|
110 | 102, 106,
109 | mpjaodan 788 |
. . . . . . . . . . . 12
|
111 | 110 | ex 114 |
. . . . . . . . . . 11
|
112 | 111 | ralrimiva 2537 |
. . . . . . . . . 10
|
113 | 112 | ex 114 |
. . . . . . . . 9
|
114 | 62, 113 | syl5bir 152 |
. . . . . . . 8
|
115 | 114 | ex 114 |
. . . . . . 7
|
116 | 115 | a2d 26 |
. . . . . 6
|
117 | 23, 29, 35, 41, 57, 116 | nn0ind 9297 |
. . . . 5
|
118 | 117 | imp 123 |
. . . 4
|
119 | 15, 16, 17, 118 | syl12anc 1225 |
. . 3
|
120 | | simpl2 990 |
. . 3
|
121 | 14, 119, 120 | rspcdva 2831 |
. 2
|
122 | 10, 121 | impbid 128 |
1
|