Proof of Theorem quad2
Step | Hyp | Ref
| Expression |
1 | | 2cn 11091 |
. . . . . . . 8
|
2 | | quad.a |
. . . . . . . 8
|
3 | | mulcl 10020 |
. . . . . . . 8
|
4 | 1, 2, 3 | sylancr 695 |
. . . . . . 7
|
5 | | quad.x |
. . . . . . 7
|
6 | 4, 5 | mulcld 10060 |
. . . . . 6
|
7 | | quad.b |
. . . . . 6
|
8 | 6, 7 | addcld 10059 |
. . . . 5
|
9 | 8 | sqcld 13006 |
. . . 4
|
10 | | quad2.d |
. . . . 5
|
11 | 10 | sqcld 13006 |
. . . 4
|
12 | 9, 11 | subeq0ad 10402 |
. . 3
|
13 | 5 | sqcld 13006 |
. . . . . . 7
|
14 | 2, 13 | mulcld 10060 |
. . . . . 6
|
15 | 7, 5 | mulcld 10060 |
. . . . . . 7
|
16 | | quad.c |
. . . . . . 7
|
17 | 15, 16 | addcld 10059 |
. . . . . 6
|
18 | 14, 17 | addcld 10059 |
. . . . 5
|
19 | | 0cnd 10033 |
. . . . 5
|
20 | | 4cn 11098 |
. . . . . 6
|
21 | | mulcl 10020 |
. . . . . 6
|
22 | 20, 2, 21 | sylancr 695 |
. . . . 5
|
23 | 20 | a1i 11 |
. . . . . 6
|
24 | | 4ne0 11117 |
. . . . . . 7
|
25 | 24 | a1i 11 |
. . . . . 6
|
26 | | quad.z |
. . . . . 6
|
27 | 23, 2, 25, 26 | mulne0d 10679 |
. . . . 5
|
28 | 18, 19, 22, 27 | mulcand 10660 |
. . . 4
|
29 | 6 | sqcld 13006 |
. . . . . . . 8
|
30 | 6, 7 | mulcld 10060 |
. . . . . . . . 9
|
31 | | mulcl 10020 |
. . . . . . . . 9
|
32 | 1, 30, 31 | sylancr 695 |
. . . . . . . 8
|
33 | 2, 16 | mulcld 10060 |
. . . . . . . . 9
|
34 | | mulcl 10020 |
. . . . . . . . 9
|
35 | 20, 33, 34 | sylancr 695 |
. . . . . . . 8
|
36 | 29, 32, 35 | addassd 10062 |
. . . . . . 7
|
37 | 7 | sqcld 13006 |
. . . . . . . 8
|
38 | 29, 32 | addcld 10059 |
. . . . . . . 8
|
39 | 37, 38, 35 | pnncand 10431 |
. . . . . . 7
|
40 | 4, 5 | sqmuld 13020 |
. . . . . . . . 9
|
41 | | sq2 12960 |
. . . . . . . . . . . . 13
|
42 | 41 | a1i 11 |
. . . . . . . . . . . 12
|
43 | 2 | sqvald 13005 |
. . . . . . . . . . . 12
|
44 | 42, 43 | oveq12d 6668 |
. . . . . . . . . . 11
|
45 | | sqmul 12926 |
. . . . . . . . . . . 12
|
46 | 1, 2, 45 | sylancr 695 |
. . . . . . . . . . 11
|
47 | 23, 2, 2 | mulassd 10063 |
. . . . . . . . . . 11
|
48 | 44, 46, 47 | 3eqtr4d 2666 |
. . . . . . . . . 10
|
49 | 48 | oveq1d 6665 |
. . . . . . . . 9
|
50 | 22, 2, 13 | mulassd 10063 |
. . . . . . . . 9
|
51 | 40, 49, 50 | 3eqtrrd 2661 |
. . . . . . . 8
|
52 | 22, 15, 16 | adddid 10064 |
. . . . . . . . 9
|
53 | | 2t2e4 11177 |
. . . . . . . . . . . . . . . . 17
|
54 | 53 | oveq1i 6660 |
. . . . . . . . . . . . . . . 16
|
55 | 1 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
56 | 55, 55, 2 | mulassd 10063 |
. . . . . . . . . . . . . . . 16
|
57 | 54, 56 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
58 | 57 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
59 | 55, 4, 7 | mulassd 10063 |
. . . . . . . . . . . . . 14
|
60 | 58, 59 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
61 | 60 | oveq1d 6665 |
. . . . . . . . . . . 12
|
62 | 4, 7 | mulcld 10060 |
. . . . . . . . . . . . 13
|
63 | 55, 62, 5 | mulassd 10063 |
. . . . . . . . . . . 12
|
64 | 61, 63 | eqtrd 2656 |
. . . . . . . . . . 11
|
65 | 22, 7, 5 | mulassd 10063 |
. . . . . . . . . . 11
|
66 | 4, 7, 5 | mul32d 10246 |
. . . . . . . . . . . 12
|
67 | 66 | oveq2d 6666 |
. . . . . . . . . . 11
|
68 | 64, 65, 67 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
69 | 23, 2, 16 | mulassd 10063 |
. . . . . . . . . 10
|
70 | 68, 69 | oveq12d 6668 |
. . . . . . . . 9
|
71 | 52, 70 | eqtrd 2656 |
. . . . . . . 8
|
72 | 51, 71 | oveq12d 6668 |
. . . . . . 7
|
73 | 36, 39, 72 | 3eqtr4rd 2667 |
. . . . . 6
|
74 | 22, 14, 17 | adddid 10064 |
. . . . . 6
|
75 | | binom2 12979 |
. . . . . . . . 9
|
76 | 6, 7, 75 | syl2anc 693 |
. . . . . . . 8
|
77 | 38, 37 | addcomd 10238 |
. . . . . . . 8
|
78 | 76, 77 | eqtrd 2656 |
. . . . . . 7
|
79 | | quad2.2 |
. . . . . . 7
|
80 | 78, 79 | oveq12d 6668 |
. . . . . 6
|
81 | 73, 74, 80 | 3eqtr4d 2666 |
. . . . 5
|
82 | 22 | mul01d 10235 |
. . . . 5
|
83 | 81, 82 | eqeq12d 2637 |
. . . 4
|
84 | 28, 83 | bitr3d 270 |
. . 3
|
85 | 6, 7 | subnegd 10399 |
. . . . 5
|
86 | 85 | oveq1d 6665 |
. . . 4
|
87 | 86 | eqeq1d 2624 |
. . 3
|
88 | 12, 84, 87 | 3bitr4d 300 |
. 2
|
89 | 7 | negcld 10379 |
. . . 4
|
90 | 6, 89 | subcld 10392 |
. . 3
|
91 | | sqeqor 12978 |
. . 3
|
92 | 90, 10, 91 | syl2anc 693 |
. 2
|
93 | 6, 89, 10 | subaddd 10410 |
. . . 4
|
94 | 89, 10 | addcld 10059 |
. . . . . 6
|
95 | | 2ne0 11113 |
. . . . . . . 8
|
96 | 95 | a1i 11 |
. . . . . . 7
|
97 | 55, 2, 96, 26 | mulne0d 10679 |
. . . . . 6
|
98 | 94, 4, 5, 97 | divmuld 10823 |
. . . . 5
|
99 | | eqcom 2629 |
. . . . 5
|
100 | | eqcom 2629 |
. . . . 5
|
101 | 98, 99, 100 | 3bitr4g 303 |
. . . 4
|
102 | 93, 101 | bitr4d 271 |
. . 3
|
103 | 89, 10 | negsubd 10398 |
. . . . 5
|
104 | 103 | eqeq1d 2624 |
. . . 4
|
105 | 10 | negcld 10379 |
. . . . 5
|
106 | 6, 89, 105 | subaddd 10410 |
. . . 4
|
107 | 89, 10 | subcld 10392 |
. . . . . 6
|
108 | 107, 4, 5, 97 | divmuld 10823 |
. . . . 5
|
109 | | eqcom 2629 |
. . . . 5
|
110 | | eqcom 2629 |
. . . . 5
|
111 | 108, 109,
110 | 3bitr4g 303 |
. . . 4
|
112 | 104, 106,
111 | 3bitr4d 300 |
. . 3
|
113 | 102, 112 | orbi12d 746 |
. 2
|
114 | 88, 92, 113 | 3bitrd 294 |
1
|