Step | Hyp | Ref
| Expression |
1 | | pellfundval 37444 |
. . . . . . 7
◻NN PellFund inf Pell14QR
|
2 | 1 | 3ad2ant1 1082 |
. . . . . 6
◻NN PellFund PellFund inf Pell14QR
|
3 | | simp3 1063 |
. . . . . 6
◻NN PellFund PellFund |
4 | 2, 3 | eqbrtrrd 4677 |
. . . . 5
◻NN PellFund inf Pell14QR |
5 | | pellfundre 37445 |
. . . . . . . 8
◻NN PellFund |
6 | 5 | 3ad2ant1 1082 |
. . . . . . 7
◻NN PellFund PellFund |
7 | 2, 6 | eqeltrrd 2702 |
. . . . . 6
◻NN PellFund inf Pell14QR |
8 | | simp2 1062 |
. . . . . 6
◻NN PellFund |
9 | 7, 8 | ltnled 10184 |
. . . . 5
◻NN PellFund inf Pell14QR
inf Pell14QR
|
10 | 4, 9 | mpbid 222 |
. . . 4
◻NN PellFund inf Pell14QR |
11 | | ssrab2 3687 |
. . . . . 6
Pell14QR Pell14QR |
12 | | pell14qrre 37421 |
. . . . . . . . 9
◻NN Pell14QR |
13 | 12 | ex 450 |
. . . . . . . 8
◻NN Pell14QR |
14 | 13 | ssrdv 3609 |
. . . . . . 7
◻NN Pell14QR |
15 | 14 | 3ad2ant1 1082 |
. . . . . 6
◻NN PellFund Pell14QR |
16 | 11, 15 | syl5ss 3614 |
. . . . 5
◻NN PellFund Pell14QR |
17 | | pell1qrss14 37432 |
. . . . . . . 8
◻NN Pell1QR Pell14QR |
18 | 17 | 3ad2ant1 1082 |
. . . . . . 7
◻NN PellFund Pell1QR Pell14QR |
19 | | pellqrex 37443 |
. . . . . . . 8
◻NN
Pell1QR |
20 | 19 | 3ad2ant1 1082 |
. . . . . . 7
◻NN PellFund Pell1QR
|
21 | | ssrexv 3667 |
. . . . . . 7
Pell1QR Pell14QR
Pell1QR
Pell14QR
|
22 | 18, 20, 21 | sylc 65 |
. . . . . 6
◻NN PellFund Pell14QR
|
23 | | rabn0 3958 |
. . . . . 6
Pell14QR
Pell14QR
|
24 | 22, 23 | sylibr 224 |
. . . . 5
◻NN PellFund Pell14QR |
25 | | infmrgelbi 37442 |
. . . . . 6
Pell14QR Pell14QR
Pell14QR
inf Pell14QR |
26 | 25 | ex 450 |
. . . . 5
Pell14QR Pell14QR
Pell14QR inf Pell14QR |
27 | 16, 24, 8, 26 | syl3anc 1326 |
. . . 4
◻NN PellFund
Pell14QR inf Pell14QR |
28 | 10, 27 | mtod 189 |
. . 3
◻NN PellFund Pell14QR |
29 | | rexnal 2995 |
. . 3
Pell14QR
Pell14QR |
30 | 28, 29 | sylibr 224 |
. 2
◻NN PellFund Pell14QR |
31 | | breq2 4657 |
. . . . . . . 8
|
32 | 31 | elrab 3363 |
. . . . . . 7
Pell14QR Pell14QR |
33 | | simprl 794 |
. . . . . . . . 9
◻NN PellFund
Pell14QR
Pell14QR |
34 | | 1red 10055 |
. . . . . . . . . 10
◻NN PellFund
Pell14QR |
35 | | simpl1 1064 |
. . . . . . . . . . 11
◻NN PellFund
Pell14QR
◻NN |
36 | | pell14qrre 37421 |
. . . . . . . . . . 11
◻NN Pell14QR
|
37 | 35, 33, 36 | syl2anc 693 |
. . . . . . . . . 10
◻NN PellFund
Pell14QR
|
38 | | simprr 796 |
. . . . . . . . . 10
◻NN PellFund
Pell14QR
|
39 | 34, 37, 38 | ltled 10185 |
. . . . . . . . 9
◻NN PellFund
Pell14QR
|
40 | 33, 39 | jca 554 |
. . . . . . . 8
◻NN PellFund
Pell14QR Pell14QR |
41 | | elpell1qr2 37436 |
. . . . . . . . 9
◻NN Pell1QR
Pell14QR
|
42 | 35, 41 | syl 17 |
. . . . . . . 8
◻NN PellFund
Pell14QR Pell1QR
Pell14QR
|
43 | 40, 42 | mpbird 247 |
. . . . . . 7
◻NN PellFund
Pell14QR
Pell1QR |
44 | 32, 43 | sylan2b 492 |
. . . . . 6
◻NN PellFund
Pell14QR
Pell1QR |
45 | 44 | adantrr 753 |
. . . . 5
◻NN PellFund
Pell14QR Pell1QR |
46 | | simpl1 1064 |
. . . . . . 7
◻NN PellFund
Pell14QR
◻NN |
47 | | simprl 794 |
. . . . . . . 8
◻NN PellFund
Pell14QR Pell14QR |
48 | 11, 47 | sseldi 3601 |
. . . . . . 7
◻NN PellFund
Pell14QR Pell14QR |
49 | | simpr 477 |
. . . . . . . . . . 11
Pell14QR
|
50 | 49 | a1i 11 |
. . . . . . . . . 10
◻NN PellFund Pell14QR |
51 | 32, 50 | syl5bi 232 |
. . . . . . . . 9
◻NN PellFund Pell14QR |
52 | 51 | imp 445 |
. . . . . . . 8
◻NN PellFund
Pell14QR
|
53 | 52 | adantrr 753 |
. . . . . . 7
◻NN PellFund
Pell14QR |
54 | | pellfundlb 37448 |
. . . . . . 7
◻NN Pell14QR PellFund |
55 | 46, 48, 53, 54 | syl3anc 1326 |
. . . . . 6
◻NN PellFund
Pell14QR PellFund |
56 | | simprr 796 |
. . . . . . 7
◻NN PellFund
Pell14QR
|
57 | 15 | adantr 481 |
. . . . . . . . 9
◻NN PellFund
Pell14QR Pell14QR |
58 | 57, 48 | sseldd 3604 |
. . . . . . . 8
◻NN PellFund
Pell14QR |
59 | | simpl2 1065 |
. . . . . . . 8
◻NN PellFund
Pell14QR |
60 | 58, 59 | ltnled 10184 |
. . . . . . 7
◻NN PellFund
Pell14QR
|
61 | 56, 60 | mpbird 247 |
. . . . . 6
◻NN PellFund
Pell14QR |
62 | 55, 61 | jca 554 |
. . . . 5
◻NN PellFund
Pell14QR PellFund
|
63 | 45, 62 | jca 554 |
. . . 4
◻NN PellFund
Pell14QR Pell1QR PellFund
|
64 | 63 | ex 450 |
. . 3
◻NN PellFund Pell14QR Pell1QR PellFund |
65 | 64 | reximdv2 3014 |
. 2
◻NN PellFund
Pell14QR
Pell1QRPellFund |
66 | 30, 65 | mpd 15 |
1
◻NN PellFund Pell1QRPellFund |