Step | Hyp | Ref
| Expression |
1 | | nnex 11026 |
. . . 4
|
2 | 1, 1 | xpex 6962 |
. . 3
|
3 | | opabssxp 5193 |
. . 3
|
4 | 2, 3 | ssexi 4803 |
. 2
|
5 | | simprl 794 |
. . . . . . . 8
denom |
6 | | simprrl 804 |
. . . . . . . 8
denom |
7 | | qgt0numnn 15459 |
. . . . . . . 8
numer |
8 | 5, 6, 7 | syl2anc 693 |
. . . . . . 7
denom numer |
9 | | qdencl 15449 |
. . . . . . . 8
denom |
10 | 5, 9 | syl 17 |
. . . . . . 7
denom denom |
11 | 8, 10 | jca 554 |
. . . . . 6
denom numer denom |
12 | | simpll 790 |
. . . . . . 7
denom |
13 | | simplr 792 |
. . . . . . 7
denom |
14 | | pellexlem1 37393 |
. . . . . . 7
numer denom numer denom |
15 | 12, 8, 10, 13, 14 | syl31anc 1329 |
. . . . . 6
denom numer denom |
16 | | simprrr 805 |
. . . . . . . 8
denom denom |
17 | | qeqnumdivden 15454 |
. . . . . . . . . . . 12
numer denom |
18 | 17 | oveq1d 6665 |
. . . . . . . . . . 11
numer denom |
19 | 18 | fveq2d 6195 |
. . . . . . . . . 10
numer denom |
20 | 19 | breq1d 4663 |
. . . . . . . . 9
denom numer denom denom |
21 | 5, 20 | syl 17 |
. . . . . . . 8
denom denom numer denom denom |
22 | 16, 21 | mpbid 222 |
. . . . . . 7
denom numer denom denom |
23 | | pellexlem2 37394 |
. . . . . . 7
numer denom numer denom denom numer denom |
24 | 12, 8, 10, 22, 23 | syl31anc 1329 |
. . . . . 6
denom numer denom |
25 | 11, 15, 24 | jca32 558 |
. . . . 5
denom numer denom numer denom numer denom |
26 | 25 | ex 450 |
. . . 4
denom numer denom numer denom numer denom |
27 | | breq2 4657 |
. . . . . 6
|
28 | | oveq1 6657 |
. . . . . . . 8
|
29 | 28 | fveq2d 6195 |
. . . . . . 7
|
30 | | fveq2 6191 |
. . . . . . . 8
denom denom |
31 | 30 | oveq1d 6665 |
. . . . . . 7
denom denom |
32 | 29, 31 | breq12d 4666 |
. . . . . 6
denom denom |
33 | 27, 32 | anbi12d 747 |
. . . . 5
denom
denom |
34 | 33 | elrab 3363 |
. . . 4
denom denom |
35 | | fvex 6201 |
. . . . 5
numer |
36 | | fvex 6201 |
. . . . 5
denom |
37 | | eleq1 2689 |
. . . . . . 7
numer
numer |
38 | 37 | anbi1d 741 |
. . . . . 6
numer
numer |
39 | | oveq1 6657 |
. . . . . . . . 9
numer
numer |
40 | 39 | oveq1d 6665 |
. . . . . . . 8
numer
numer |
41 | 40 | neeq1d 2853 |
. . . . . . 7
numer
numer
|
42 | 40 | fveq2d 6195 |
. . . . . . . 8
numer
numer
|
43 | 42 | breq1d 4663 |
. . . . . . 7
numer
numer |
44 | 41, 43 | anbi12d 747 |
. . . . . 6
numer
numer numer |
45 | 38, 44 | anbi12d 747 |
. . . . 5
numer
numer numer
numer |
46 | | eleq1 2689 |
. . . . . . 7
denom
denom |
47 | 46 | anbi2d 740 |
. . . . . 6
denom
numer
numer denom |
48 | | oveq1 6657 |
. . . . . . . . . 10
denom
denom |
49 | 48 | oveq2d 6666 |
. . . . . . . . 9
denom
denom |
50 | 49 | oveq2d 6666 |
. . . . . . . 8
denom
numer
numer denom |
51 | 50 | neeq1d 2853 |
. . . . . . 7
denom
numer numer denom |
52 | 50 | fveq2d 6195 |
. . . . . . . 8
denom
numer numer denom |
53 | 52 | breq1d 4663 |
. . . . . . 7
denom
numer
numer denom |
54 | 51, 53 | anbi12d 747 |
. . . . . 6
denom
numer numer numer denom numer denom |
55 | 47, 54 | anbi12d 747 |
. . . . 5
denom
numer
numer numer numer denom numer denom numer denom |
56 | 35, 36, 45, 55 | opelopab 4997 |
. . . 4
numer denom
numer denom numer
denom numer denom |
57 | 26, 34, 56 | 3imtr4g 285 |
. . 3
denom numer denom
|
58 | | ssrab2 3687 |
. . . . . 6
denom
|
59 | | simprl 794 |
. . . . . 6
denom
denom denom |
60 | 58, 59 | sseldi 3601 |
. . . . 5
denom
denom |
61 | | simprr 796 |
. . . . . 6
denom
denom denom |
62 | 58, 61 | sseldi 3601 |
. . . . 5
denom
denom |
63 | 35, 36 | opth 4945 |
. . . . . . 7
numer denom numer denom
numer numer denom denom |
64 | | simprl 794 |
. . . . . . . . . 10
numer numer denom denom numer numer |
65 | | simprr 796 |
. . . . . . . . . 10
numer numer denom denom denom denom |
66 | 64, 65 | oveq12d 6668 |
. . . . . . . . 9
numer numer denom denom numer denom numer denom |
67 | | simpll 790 |
. . . . . . . . . 10
numer numer denom denom |
68 | 67, 17 | syl 17 |
. . . . . . . . 9
numer numer denom denom numer denom |
69 | | simplr 792 |
. . . . . . . . . 10
numer numer denom denom |
70 | | qeqnumdivden 15454 |
. . . . . . . . . 10
numer denom |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
numer numer denom denom numer denom |
72 | 66, 68, 71 | 3eqtr4d 2666 |
. . . . . . . 8
numer numer denom denom |
73 | 72 | ex 450 |
. . . . . . 7
numer numer denom denom |
74 | 63, 73 | syl5bi 232 |
. . . . . 6
numer denom numer denom |
75 | | fveq2 6191 |
. . . . . . 7
numer numer |
76 | | fveq2 6191 |
. . . . . . 7
denom denom |
77 | 75, 76 | opeq12d 4410 |
. . . . . 6
numer denom numer denom |
78 | 74, 77 | impbid1 215 |
. . . . 5
numer denom numer denom
|
79 | 60, 62, 78 | syl2anc 693 |
. . . 4
denom
denom numer denom numer denom
|
80 | 79 | ex 450 |
. . 3
denom
denom numer denom numer denom
|
81 | 57, 80 | dom2d 7996 |
. 2
denom
|
82 | 4, 81 | mpi 20 |
1
denom
|