Proof of Theorem pell1qrgaplem
Step | Hyp | Ref
| Expression |
1 | | nnrp 11842 |
. . . . . 6
|
2 | 1 | ad2antrr 762 |
. . . . 5
|
3 | | 1rp 11836 |
. . . . . 6
|
4 | 3 | a1i 11 |
. . . . 5
|
5 | 2, 4 | rpaddcld 11887 |
. . . 4
|
6 | 5 | rpsqrtcld 14150 |
. . 3
|
7 | 6 | rpred 11872 |
. 2
|
8 | 2 | rpsqrtcld 14150 |
. . 3
|
9 | 8 | rpred 11872 |
. 2
|
10 | | nn0re 11301 |
. . . 4
|
11 | 10 | adantr 481 |
. . 3
|
12 | 11 | ad2antlr 763 |
. 2
|
13 | | nn0re 11301 |
. . . . 5
|
14 | 13 | adantl 482 |
. . . 4
|
15 | 14 | ad2antlr 763 |
. . 3
|
16 | 9, 15 | remulcld 10070 |
. 2
|
17 | 2 | rpred 11872 |
. . . . . 6
|
18 | | 1re 10039 |
. . . . . . . 8
|
19 | 18 | a1i 11 |
. . . . . . 7
|
20 | 15 | resqcld 13035 |
. . . . . . 7
|
21 | 19, 20 | resubcld 10458 |
. . . . . 6
|
22 | 17, 21 | remulcld 10070 |
. . . . 5
|
23 | | 0red 10041 |
. . . . . 6
|
24 | 17, 23 | remulcld 10070 |
. . . . 5
|
25 | 12 | resqcld 13035 |
. . . . 5
|
26 | | sq1 12958 |
. . . . . . . . 9
|
27 | 26 | a1i 11 |
. . . . . . . 8
|
28 | | nnge1 11046 |
. . . . . . . . . . 11
|
29 | 28 | adantl 482 |
. . . . . . . . . 10
|
30 | | simplrl 800 |
. . . . . . . . . . . 12
|
31 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . 22
|
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
33 | | sq0 12955 |
. . . . . . . . . . . . . . . . . . . . 21
|
34 | 32, 33 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . 20
|
35 | 34 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . 19
|
36 | 2 | rpcnd 11874 |
. . . . . . . . . . . . . . . . . . . . 21
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
38 | 37 | mul01d 10235 |
. . . . . . . . . . . . . . . . . . 19
|
39 | 35, 38 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
40 | 39 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
|
41 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
|
42 | 12 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
|
43 | 42 | sqcld 13006 |
. . . . . . . . . . . . . . . . . . 19
|
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
45 | 44 | subid1d 10381 |
. . . . . . . . . . . . . . . . 17
|
46 | 40, 41, 45 | 3eqtr3d 2664 |
. . . . . . . . . . . . . . . 16
|
47 | 26, 46 | syl5req 2669 |
. . . . . . . . . . . . . . 15
|
48 | | nn0ge0 11318 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
50 | 49 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
|
51 | | 0le1 10551 |
. . . . . . . . . . . . . . . . . 18
|
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
53 | | sq11 12936 |
. . . . . . . . . . . . . . . . 17
|
54 | 12, 50, 19, 52, 53 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . 15
|
56 | 47, 55 | mpbid 222 |
. . . . . . . . . . . . . 14
|
57 | | simpr 477 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . 15
|
59 | 8 | rpcnd 11874 |
. . . . . . . . . . . . . . . . 17
|
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
61 | 60 | mul01d 10235 |
. . . . . . . . . . . . . . 15
|
62 | 58, 61 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
63 | 56, 62 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
64 | | 1p0e1 11133 |
. . . . . . . . . . . . 13
|
65 | 63, 64 | syl6eq 2672 |
. . . . . . . . . . . 12
|
66 | 30, 65 | breqtrd 4679 |
. . . . . . . . . . 11
|
67 | 18 | ltnri 10146 |
. . . . . . . . . . 11
|
68 | | pm2.24 121 |
. . . . . . . . . . 11
|
69 | 66, 67, 68 | mpisyl 21 |
. . . . . . . . . 10
|
70 | | simplrr 801 |
. . . . . . . . . . 11
|
71 | | elnn0 11294 |
. . . . . . . . . . 11
|
72 | 70, 71 | sylib 208 |
. . . . . . . . . 10
|
73 | 29, 69, 72 | mpjaodan 827 |
. . . . . . . . 9
|
74 | | nn0ge0 11318 |
. . . . . . . . . . . 12
|
75 | 74 | adantl 482 |
. . . . . . . . . . 11
|
76 | 75 | ad2antlr 763 |
. . . . . . . . . 10
|
77 | 19, 15, 52, 76 | le2sqd 13044 |
. . . . . . . . 9
|
78 | 73, 77 | mpbid 222 |
. . . . . . . 8
|
79 | 27, 78 | eqbrtrrd 4677 |
. . . . . . 7
|
80 | 19, 20 | suble0d 10618 |
. . . . . . 7
|
81 | 79, 80 | mpbird 247 |
. . . . . 6
|
82 | 21, 23, 2 | lemul2d 11916 |
. . . . . 6
|
83 | 81, 82 | mpbid 222 |
. . . . 5
|
84 | 22, 24, 25, 83 | leadd2dd 10642 |
. . . 4
|
85 | 5 | rpcnd 11874 |
. . . . . 6
|
86 | 85 | sqsqrtd 14178 |
. . . . 5
|
87 | | simprr 796 |
. . . . . . 7
|
88 | 87 | eqcomd 2628 |
. . . . . 6
|
89 | 88 | oveq2d 6666 |
. . . . 5
|
90 | 15 | recnd 10068 |
. . . . . . . . 9
|
91 | 90 | sqcld 13006 |
. . . . . . . 8
|
92 | 36, 91 | mulcld 10060 |
. . . . . . 7
|
93 | 36, 43, 92 | addsub12d 10415 |
. . . . . 6
|
94 | 19 | recnd 10068 |
. . . . . . . . 9
|
95 | 36, 94, 91 | subdid 10486 |
. . . . . . . 8
|
96 | 36 | mulid1d 10057 |
. . . . . . . . 9
|
97 | 96 | oveq1d 6665 |
. . . . . . . 8
|
98 | 95, 97 | eqtr2d 2657 |
. . . . . . 7
|
99 | 98 | oveq2d 6666 |
. . . . . 6
|
100 | 93, 99 | eqtrd 2656 |
. . . . 5
|
101 | 86, 89, 100 | 3eqtrd 2660 |
. . . 4
|
102 | 36 | mul01d 10235 |
. . . . . 6
|
103 | 102 | oveq2d 6666 |
. . . . 5
|
104 | 43 | addid1d 10236 |
. . . . 5
|
105 | 103, 104 | eqtr2d 2657 |
. . . 4
|
106 | 84, 101, 105 | 3brtr4d 4685 |
. . 3
|
107 | 6 | rpge0d 11876 |
. . . 4
|
108 | 7, 12, 107, 50 | le2sqd 13044 |
. . 3
|
109 | 106, 108 | mpbird 247 |
. 2
|
110 | 59 | mulid1d 10057 |
. . 3
|
111 | 19, 15, 8 | lemul2d 11916 |
. . . 4
|
112 | 73, 111 | mpbid 222 |
. . 3
|
113 | 110, 112 | eqbrtrrd 4677 |
. 2
|
114 | 7, 9, 12, 16, 109, 113 | le2addd 10646 |
1
|