Step | Hyp | Ref
| Expression |
1 | | 2re 11090 |
. . . 4
|
2 | | pellfundre 37445 |
. . . 4
◻NN PellFund |
3 | | remulcl 10021 |
. . . 4
PellFund PellFund |
4 | 1, 2, 3 | sylancr 695 |
. . 3
◻NN PellFund |
5 | | 0red 10041 |
. . . . . . 7
◻NN |
6 | | 1red 10055 |
. . . . . . 7
◻NN |
7 | | 0lt1 10550 |
. . . . . . . 8
|
8 | 7 | a1i 11 |
. . . . . . 7
◻NN
|
9 | | pellfundgt1 37447 |
. . . . . . 7
◻NN
PellFund |
10 | 5, 6, 2, 8, 9 | lttrd 10198 |
. . . . . 6
◻NN
PellFund |
11 | 2, 10 | elrpd 11869 |
. . . . 5
◻NN PellFund |
12 | 2, 11 | ltaddrpd 11905 |
. . . 4
◻NN PellFund PellFund PellFund |
13 | 2 | recnd 10068 |
. . . . 5
◻NN PellFund |
14 | 13 | 2timesd 11275 |
. . . 4
◻NN PellFund PellFund PellFund |
15 | 12, 14 | breqtrrd 4681 |
. . 3
◻NN PellFund PellFund |
16 | | pellfundglb 37449 |
. . 3
◻NN PellFund PellFund PellFund Pell1QRPellFund
PellFund |
17 | 4, 15, 16 | mpd3an23 1426 |
. 2
◻NN
Pell1QRPellFund
PellFund |
18 | 2 | adantr 481 |
. . . . . 6
◻NN Pell1QR PellFund |
19 | | pell1qrss14 37432 |
. . . . . . . 8
◻NN Pell1QR Pell14QR |
20 | 19 | sselda 3603 |
. . . . . . 7
◻NN Pell1QR Pell14QR |
21 | | pell14qrre 37421 |
. . . . . . 7
◻NN Pell14QR |
22 | 20, 21 | syldan 487 |
. . . . . 6
◻NN Pell1QR |
23 | 18, 22 | leloed 10180 |
. . . . 5
◻NN Pell1QR PellFund PellFund
PellFund |
24 | | simp-4l 806 |
. . . . . . . . 9
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund
◻NN |
25 | | simp-4r 807 |
. . . . . . . . 9
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund Pell1QR |
26 | | simplr 792 |
. . . . . . . . 9
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund Pell1QR |
27 | | simprr 796 |
. . . . . . . . 9
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund
|
28 | 22 | ad3antrrr 766 |
. . . . . . . . . 10
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund |
29 | 4 | ad4antr 768 |
. . . . . . . . . 10
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund |
30 | 19 | ad4antr 768 |
. . . . . . . . . . . . 13
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund Pell1QR Pell14QR |
31 | 30, 26 | sseldd 3604 |
. . . . . . . . . . . 12
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund Pell14QR |
32 | | pell14qrre 37421 |
. . . . . . . . . . . 12
◻NN Pell14QR |
33 | 24, 31, 32 | syl2anc 693 |
. . . . . . . . . . 11
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund |
34 | | remulcl 10021 |
. . . . . . . . . . 11
|
35 | 1, 33, 34 | sylancr 695 |
. . . . . . . . . 10
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund |
36 | | simprr 796 |
. . . . . . . . . . 11
◻NN Pell1QR
PellFund
PellFund PellFund |
37 | 36 | ad2antrr 762 |
. . . . . . . . . 10
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund
PellFund |
38 | | simprl 794 |
. . . . . . . . . . 11
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund |
39 | 2 | ad4antr 768 |
. . . . . . . . . . . 12
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund |
40 | 1 | a1i 11 |
. . . . . . . . . . . 12
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund |
41 | | 2pos 11112 |
. . . . . . . . . . . . 13
|
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund
|
43 | | lemul2 10876 |
. . . . . . . . . . . 12
PellFund PellFund PellFund
|
44 | 39, 33, 40, 42, 43 | syl112anc 1330 |
. . . . . . . . . . 11
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund PellFund
|
45 | 38, 44 | mpbid 222 |
. . . . . . . . . 10
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund |
46 | 28, 29, 35, 37, 45 | ltletrd 10197 |
. . . . . . . . 9
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund
|
47 | | simp1 1061 |
. . . . . . . . . 10
◻NN Pell1QR
Pell1QR
◻NN |
48 | 19 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
Pell1QR
Pell14QR |
49 | | simp2l 1087 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
Pell1QR |
50 | 48, 49 | sseldd 3604 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
Pell14QR |
51 | | simp2r 1088 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
Pell1QR |
52 | 48, 51 | sseldd 3604 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
Pell14QR |
53 | | pell14qrdivcl 37429 |
. . . . . . . . . . 11
◻NN Pell14QR Pell14QR
Pell14QR |
54 | 47, 50, 52, 53 | syl3anc 1326 |
. . . . . . . . . 10
◻NN Pell1QR
Pell1QR
Pell14QR |
55 | 47, 52, 32 | syl2anc 693 |
. . . . . . . . . . . . . 14
◻NN Pell1QR
Pell1QR
|
56 | 55 | recnd 10068 |
. . . . . . . . . . . . 13
◻NN Pell1QR
Pell1QR
|
57 | 56 | mulid2d 10058 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
58 | | simp3l 1089 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
59 | 57, 58 | eqbrtrd 4675 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
|
60 | | 1red 10055 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
61 | 47, 50, 21 | syl2anc 693 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
62 | | pell14qrgt0 37423 |
. . . . . . . . . . . . 13
◻NN Pell14QR
|
63 | 47, 52, 62 | syl2anc 693 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
64 | | ltmuldiv 10896 |
. . . . . . . . . . . 12
|
65 | 60, 61, 55, 63, 64 | syl112anc 1330 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
|
66 | 59, 65 | mpbid 222 |
. . . . . . . . . 10
◻NN Pell1QR
Pell1QR
|
67 | | simp3r 1090 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
|
68 | 1 | a1i 11 |
. . . . . . . . . . . 12
◻NN Pell1QR
Pell1QR
|
69 | | ltdivmul2 10900 |
. . . . . . . . . . . 12
|
70 | 61, 68, 55, 63, 69 | syl112anc 1330 |
. . . . . . . . . . 11
◻NN Pell1QR
Pell1QR
|
71 | 67, 70 | mpbird 247 |
. . . . . . . . . 10
◻NN Pell1QR
Pell1QR
|
72 | | simprr 796 |
. . . . . . . . . . 11
◻NN Pell14QR
|
73 | | simpll 790 |
. . . . . . . . . . . . 13
◻NN Pell14QR
◻NN |
74 | | simplr 792 |
. . . . . . . . . . . . 13
◻NN Pell14QR
Pell14QR |
75 | | simprl 794 |
. . . . . . . . . . . . 13
◻NN Pell14QR
|
76 | | pell14qrgapw 37440 |
. . . . . . . . . . . . 13
◻NN Pell14QR |
77 | 73, 74, 75, 76 | syl3anc 1326 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
78 | | pell14qrre 37421 |
. . . . . . . . . . . . . 14
◻NN Pell14QR |
79 | 78 | adantr 481 |
. . . . . . . . . . . . 13
◻NN Pell14QR
|
80 | | ltnsym 10135 |
. . . . . . . . . . . . 13
|
81 | 1, 79, 80 | sylancr 695 |
. . . . . . . . . . . 12
◻NN Pell14QR
|
82 | 77, 81 | mpd 15 |
. . . . . . . . . . 11
◻NN Pell14QR
|
83 | 72, 82 | pm2.21dd 186 |
. . . . . . . . . 10
◻NN Pell14QR
PellFund Pell1QR |
84 | 47, 54, 66, 71, 83 | syl22anc 1327 |
. . . . . . . . 9
◻NN Pell1QR
Pell1QR
PellFund Pell1QR |
85 | 24, 25, 26, 27, 46, 84 | syl122anc 1335 |
. . . . . . . 8
◻NN
Pell1QR PellFund
PellFund Pell1QR PellFund PellFund Pell1QR |
86 | | simpll 790 |
. . . . . . . . 9
◻NN Pell1QR
PellFund
PellFund
◻NN |
87 | 22 | adantr 481 |
. . . . . . . . 9
◻NN Pell1QR
PellFund
PellFund |
88 | | simprl 794 |
. . . . . . . . 9
◻NN Pell1QR
PellFund
PellFund PellFund |
89 | | pellfundglb 37449 |
. . . . . . . . 9
◻NN PellFund Pell1QRPellFund |
90 | 86, 87, 88, 89 | syl3anc 1326 |
. . . . . . . 8
◻NN Pell1QR
PellFund
PellFund Pell1QRPellFund
|
91 | 85, 90 | r19.29a 3078 |
. . . . . . 7
◻NN Pell1QR
PellFund
PellFund PellFund Pell1QR |
92 | 91 | exp32 631 |
. . . . . 6
◻NN Pell1QR PellFund
PellFund PellFund Pell1QR |
93 | | simp2 1062 |
. . . . . . . 8
◻NN Pell1QR
PellFund PellFund PellFund |
94 | | simp1r 1086 |
. . . . . . . 8
◻NN Pell1QR
PellFund PellFund Pell1QR |
95 | 93, 94 | eqeltrd 2701 |
. . . . . . 7
◻NN Pell1QR
PellFund PellFund PellFund Pell1QR |
96 | 95 | 3exp 1264 |
. . . . . 6
◻NN Pell1QR PellFund
PellFund
PellFund Pell1QR |
97 | 92, 96 | jaod 395 |
. . . . 5
◻NN Pell1QR PellFund
PellFund
PellFund PellFund Pell1QR |
98 | 23, 97 | sylbid 230 |
. . . 4
◻NN Pell1QR PellFund
PellFund PellFund Pell1QR |
99 | 98 | impd 447 |
. . 3
◻NN Pell1QR PellFund
PellFund PellFund Pell1QR |
100 | 99 | rexlimdva 3031 |
. 2
◻NN Pell1QRPellFund PellFund PellFund Pell1QR |
101 | 17, 100 | mpd 15 |
1
◻NN PellFund Pell1QR |