Step | Hyp | Ref
| Expression |
1 | | lgsquad2lem1.m |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ต) = ๐) |
2 | | lgsquad2lem1.a |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ด โ โ) |
3 | 2 | nnzd 12527 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โ โค) |
4 | 3 | zcnd 12609 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ด โ โ) |
5 | | ax-1cn 11110 |
. . . . . . . . . . . . . 14
โข 1 โ
โ |
6 | | npcan 11411 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ โง 1 โ
โ) โ ((๐ด โ
1) + 1) = ๐ด) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ด โ 1) + 1) = ๐ด) |
8 | | lgsquad2lem1.b |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โ โ) |
9 | 8 | nnzd 12527 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โ โค) |
10 | 9 | zcnd 12609 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ต โ โ) |
11 | | npcan 11411 |
. . . . . . . . . . . . . 14
โข ((๐ต โ โ โง 1 โ
โ) โ ((๐ต โ
1) + 1) = ๐ต) |
12 | 10, 5, 11 | sylancl 587 |
. . . . . . . . . . . . 13
โข (๐ โ ((๐ต โ 1) + 1) = ๐ต) |
13 | 7, 12 | oveq12d 7376 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด โ 1) + 1) ยท ((๐ต โ 1) + 1)) = (๐ด ยท ๐ต)) |
14 | | peano2zm 12547 |
. . . . . . . . . . . . . . . 16
โข (๐ด โ โค โ (๐ด โ 1) โ
โค) |
15 | 3, 14 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ด โ 1) โ โค) |
16 | 15 | zcnd 12609 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ด โ 1) โ โ) |
17 | 5 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ 1 โ
โ) |
18 | | peano2zm 12547 |
. . . . . . . . . . . . . . . 16
โข (๐ต โ โค โ (๐ต โ 1) โ
โค) |
19 | 9, 18 | syl 17 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ต โ 1) โ โค) |
20 | 19 | zcnd 12609 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ต โ 1) โ โ) |
21 | 16, 17, 20, 17 | muladdd 11614 |
. . . . . . . . . . . . 13
โข (๐ โ (((๐ด โ 1) + 1) ยท ((๐ต โ 1) + 1)) = ((((๐ด โ 1) ยท (๐ต โ 1)) + (1 ยท 1)) +
(((๐ด โ 1) ยท 1)
+ ((๐ต โ 1) ยท
1)))) |
22 | | 1t1e1 12316 |
. . . . . . . . . . . . . . . 16
โข (1
ยท 1) = 1 |
23 | 22 | a1i 11 |
. . . . . . . . . . . . . . 15
โข (๐ โ (1 ยท 1) =
1) |
24 | 23 | oveq2d 7374 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ด โ 1) ยท (๐ต โ 1)) + (1 ยท 1)) = (((๐ด โ 1) ยท (๐ต โ 1)) +
1)) |
25 | 16 | mulid1d 11173 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ด โ 1) ยท 1) = (๐ด โ 1)) |
26 | 20 | mulid1d 11173 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((๐ต โ 1) ยท 1) = (๐ต โ 1)) |
27 | 25, 26 | oveq12d 7376 |
. . . . . . . . . . . . . 14
โข (๐ โ (((๐ด โ 1) ยท 1) + ((๐ต โ 1) ยท 1)) =
((๐ด โ 1) + (๐ต โ 1))) |
28 | 24, 27 | oveq12d 7376 |
. . . . . . . . . . . . 13
โข (๐ โ ((((๐ด โ 1) ยท (๐ต โ 1)) + (1 ยท 1)) + (((๐ด โ 1) ยท 1) +
((๐ต โ 1) ยท
1))) = ((((๐ด โ 1)
ยท (๐ต โ 1)) +
1) + ((๐ด โ 1) +
(๐ต โ
1)))) |
29 | 21, 28 | eqtrd 2777 |
. . . . . . . . . . . 12
โข (๐ โ (((๐ด โ 1) + 1) ยท ((๐ต โ 1) + 1)) = ((((๐ด โ 1) ยท (๐ต โ 1)) + 1) + ((๐ด โ 1) + (๐ต โ 1)))) |
30 | 13, 29 | eqtr3d 2779 |
. . . . . . . . . . 11
โข (๐ โ (๐ด ยท ๐ต) = ((((๐ด โ 1) ยท (๐ต โ 1)) + 1) + ((๐ด โ 1) + (๐ต โ 1)))) |
31 | 1, 30 | eqtr3d 2779 |
. . . . . . . . . 10
โข (๐ โ ๐ = ((((๐ด โ 1) ยท (๐ต โ 1)) + 1) + ((๐ด โ 1) + (๐ต โ 1)))) |
32 | 31 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) = (((((๐ด โ 1) ยท (๐ต โ 1)) + 1) + ((๐ด โ 1) + (๐ต โ 1))) โ 1)) |
33 | 16, 20 | mulcld 11176 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด โ 1) ยท (๐ต โ 1)) โ
โ) |
34 | | addcl 11134 |
. . . . . . . . . . 11
โข ((((๐ด โ 1) ยท (๐ต โ 1)) โ โ
โง 1 โ โ) โ (((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ
โ) |
35 | 33, 5, 34 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ (((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ
โ) |
36 | 16, 20 | addcld 11175 |
. . . . . . . . . 10
โข (๐ โ ((๐ด โ 1) + (๐ต โ 1)) โ
โ) |
37 | 35, 36, 17 | addsubd 11534 |
. . . . . . . . 9
โข (๐ โ (((((๐ด โ 1) ยท (๐ต โ 1)) + 1) + ((๐ด โ 1) + (๐ต โ 1))) โ 1) = (((((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ 1) +
((๐ด โ 1) + (๐ต โ 1)))) |
38 | | pncan 11408 |
. . . . . . . . . . 11
โข ((((๐ด โ 1) ยท (๐ต โ 1)) โ โ
โง 1 โ โ) โ ((((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ 1) = ((๐ด โ 1) ยท (๐ต โ 1))) |
39 | 33, 5, 38 | sylancl 587 |
. . . . . . . . . 10
โข (๐ โ ((((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ 1) = ((๐ด โ 1) ยท (๐ต โ 1))) |
40 | 39 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ (((((๐ด โ 1) ยท (๐ต โ 1)) + 1) โ 1) + ((๐ด โ 1) + (๐ต โ 1))) = (((๐ด โ 1) ยท (๐ต โ 1)) + ((๐ด โ 1) + (๐ต โ 1)))) |
41 | 32, 37, 40 | 3eqtrd 2781 |
. . . . . . . 8
โข (๐ โ (๐ โ 1) = (((๐ด โ 1) ยท (๐ต โ 1)) + ((๐ด โ 1) + (๐ต โ 1)))) |
42 | 41 | oveq1d 7373 |
. . . . . . 7
โข (๐ โ ((๐ โ 1) / 2) = ((((๐ด โ 1) ยท (๐ต โ 1)) + ((๐ด โ 1) + (๐ต โ 1))) / 2)) |
43 | | 2cnd 12232 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
44 | | 2ne0 12258 |
. . . . . . . . 9
โข 2 โ
0 |
45 | 44 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ 0) |
46 | 33, 36, 43, 45 | divdird 11970 |
. . . . . . 7
โข (๐ โ ((((๐ด โ 1) ยท (๐ต โ 1)) + ((๐ด โ 1) + (๐ต โ 1))) / 2) = ((((๐ด โ 1) ยท (๐ต โ 1)) / 2) + (((๐ด โ 1) + (๐ต โ 1)) / 2))) |
47 | 16, 20, 43, 45 | divassd 11967 |
. . . . . . . . 9
โข (๐ โ (((๐ด โ 1) ยท (๐ต โ 1)) / 2) = ((๐ด โ 1) ยท ((๐ต โ 1) / 2))) |
48 | 16, 43, 45 | divcan2d 11934 |
. . . . . . . . . 10
โข (๐ โ (2 ยท ((๐ด โ 1) / 2)) = (๐ด โ 1)) |
49 | 48 | oveq1d 7373 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ((๐ด โ 1) / 2)) ยท
((๐ต โ 1) / 2)) =
((๐ด โ 1) ยท
((๐ต โ 1) /
2))) |
50 | | lgsquad2.2 |
. . . . . . . . . . . . . 14
โข (๐ โ ยฌ 2 โฅ ๐) |
51 | | dvdsmul1 16161 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ด โฅ (๐ด ยท ๐ต)) |
52 | 3, 9, 51 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ด โฅ (๐ด ยท ๐ต)) |
53 | 52, 1 | breqtrd 5132 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ด โฅ ๐) |
54 | | 2z 12536 |
. . . . . . . . . . . . . . . 16
โข 2 โ
โค |
55 | | lgsquad2.1 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ ๐ โ โ) |
56 | 55 | nnzd 12527 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ โ โค) |
57 | | dvdstr 16177 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โค โง ๐ด
โ โค โง ๐
โ โค) โ ((2 โฅ ๐ด โง ๐ด โฅ ๐) โ 2 โฅ ๐)) |
58 | 54, 3, 56, 57 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 โฅ ๐ด โง ๐ด โฅ ๐) โ 2 โฅ ๐)) |
59 | 53, 58 | mpan2d 693 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 โฅ ๐ด โ 2 โฅ ๐)) |
60 | 50, 59 | mtod 197 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ 2 โฅ ๐ด) |
61 | | 1zzd 12535 |
. . . . . . . . . . . . 13
โข (๐ โ 1 โ
โค) |
62 | | 2prm 16569 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
63 | | nprmdvds1 16583 |
. . . . . . . . . . . . . 14
โข (2 โ
โ โ ยฌ 2 โฅ 1) |
64 | 62, 63 | mp1i 13 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ 2 โฅ
1) |
65 | | omoe 16247 |
. . . . . . . . . . . . 13
โข (((๐ด โ โค โง ยฌ 2
โฅ ๐ด) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ด โ 1)) |
66 | 3, 60, 61, 64, 65 | syl22anc 838 |
. . . . . . . . . . . 12
โข (๐ โ 2 โฅ (๐ด โ 1)) |
67 | | dvdsval2 16140 |
. . . . . . . . . . . . 13
โข ((2
โ โค โง 2 โ 0 โง (๐ด โ 1) โ โค) โ (2
โฅ (๐ด โ 1)
โ ((๐ด โ 1) / 2)
โ โค)) |
68 | 54, 45, 15, 67 | mp3an2i 1467 |
. . . . . . . . . . . 12
โข (๐ โ (2 โฅ (๐ด โ 1) โ ((๐ด โ 1) / 2) โ
โค)) |
69 | 66, 68 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ ((๐ด โ 1) / 2) โ
โค) |
70 | 69 | zcnd 12609 |
. . . . . . . . . 10
โข (๐ โ ((๐ด โ 1) / 2) โ
โ) |
71 | | dvdsmul2 16162 |
. . . . . . . . . . . . . . . . 17
โข ((๐ด โ โค โง ๐ต โ โค) โ ๐ต โฅ (๐ด ยท ๐ต)) |
72 | 3, 9, 71 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ต โฅ (๐ด ยท ๐ต)) |
73 | 72, 1 | breqtrd 5132 |
. . . . . . . . . . . . . . 15
โข (๐ โ ๐ต โฅ ๐) |
74 | | dvdstr 16177 |
. . . . . . . . . . . . . . . 16
โข ((2
โ โค โง ๐ต
โ โค โง ๐
โ โค) โ ((2 โฅ ๐ต โง ๐ต โฅ ๐) โ 2 โฅ ๐)) |
75 | 54, 9, 56, 74 | mp3an2i 1467 |
. . . . . . . . . . . . . . 15
โข (๐ โ ((2 โฅ ๐ต โง ๐ต โฅ ๐) โ 2 โฅ ๐)) |
76 | 73, 75 | mpan2d 693 |
. . . . . . . . . . . . . 14
โข (๐ โ (2 โฅ ๐ต โ 2 โฅ ๐)) |
77 | 50, 76 | mtod 197 |
. . . . . . . . . . . . 13
โข (๐ โ ยฌ 2 โฅ ๐ต) |
78 | | omoe 16247 |
. . . . . . . . . . . . 13
โข (((๐ต โ โค โง ยฌ 2
โฅ ๐ต) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ต โ 1)) |
79 | 9, 77, 61, 64, 78 | syl22anc 838 |
. . . . . . . . . . . 12
โข (๐ โ 2 โฅ (๐ต โ 1)) |
80 | | dvdsval2 16140 |
. . . . . . . . . . . . 13
โข ((2
โ โค โง 2 โ 0 โง (๐ต โ 1) โ โค) โ (2
โฅ (๐ต โ 1)
โ ((๐ต โ 1) / 2)
โ โค)) |
81 | 54, 45, 19, 80 | mp3an2i 1467 |
. . . . . . . . . . . 12
โข (๐ โ (2 โฅ (๐ต โ 1) โ ((๐ต โ 1) / 2) โ
โค)) |
82 | 79, 81 | mpbid 231 |
. . . . . . . . . . 11
โข (๐ โ ((๐ต โ 1) / 2) โ
โค) |
83 | 82 | zcnd 12609 |
. . . . . . . . . 10
โข (๐ โ ((๐ต โ 1) / 2) โ
โ) |
84 | 43, 70, 83 | mulassd 11179 |
. . . . . . . . 9
โข (๐ โ ((2 ยท ((๐ด โ 1) / 2)) ยท
((๐ต โ 1) / 2)) = (2
ยท (((๐ด โ 1) /
2) ยท ((๐ต โ 1)
/ 2)))) |
85 | 47, 49, 84 | 3eqtr2d 2783 |
. . . . . . . 8
โข (๐ โ (((๐ด โ 1) ยท (๐ต โ 1)) / 2) = (2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) /
2)))) |
86 | 16, 20, 43, 45 | divdird 11970 |
. . . . . . . 8
โข (๐ โ (((๐ด โ 1) + (๐ต โ 1)) / 2) = (((๐ด โ 1) / 2) + ((๐ต โ 1) / 2))) |
87 | 85, 86 | oveq12d 7376 |
. . . . . . 7
โข (๐ โ ((((๐ด โ 1) ยท (๐ต โ 1)) / 2) + (((๐ด โ 1) + (๐ต โ 1)) / 2)) = ((2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))) +
(((๐ด โ 1) / 2) +
((๐ต โ 1) /
2)))) |
88 | 42, 46, 87 | 3eqtrd 2781 |
. . . . . 6
โข (๐ โ ((๐ โ 1) / 2) = ((2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))) +
(((๐ด โ 1) / 2) +
((๐ต โ 1) /
2)))) |
89 | 88 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = (((2
ยท (((๐ด โ 1) /
2) ยท ((๐ต โ 1)
/ 2))) + (((๐ด โ 1) /
2) + ((๐ต โ 1) / 2)))
ยท ((๐ โ 1) /
2))) |
90 | 54 | a1i 11 |
. . . . . . . 8
โข (๐ โ 2 โ
โค) |
91 | 69, 82 | zmulcld 12614 |
. . . . . . . 8
โข (๐ โ (((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) โ
โค) |
92 | 90, 91 | zmulcld 12614 |
. . . . . . 7
โข (๐ โ (2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2)))
โ โค) |
93 | 92 | zcnd 12609 |
. . . . . 6
โข (๐ โ (2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2)))
โ โ) |
94 | 69, 82 | zaddcld 12612 |
. . . . . . 7
โข (๐ โ (((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) โ
โค) |
95 | 94 | zcnd 12609 |
. . . . . 6
โข (๐ โ (((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) โ
โ) |
96 | | lgsquad2.3 |
. . . . . . . . . 10
โข (๐ โ ๐ โ โ) |
97 | 96 | nnzd 12527 |
. . . . . . . . 9
โข (๐ โ ๐ โ โค) |
98 | | lgsquad2.4 |
. . . . . . . . 9
โข (๐ โ ยฌ 2 โฅ ๐) |
99 | | omoe 16247 |
. . . . . . . . 9
โข (((๐ โ โค โง ยฌ 2
โฅ ๐) โง (1 โ
โค โง ยฌ 2 โฅ 1)) โ 2 โฅ (๐ โ 1)) |
100 | 97, 98, 61, 64, 99 | syl22anc 838 |
. . . . . . . 8
โข (๐ โ 2 โฅ (๐ โ 1)) |
101 | | peano2zm 12547 |
. . . . . . . . . 10
โข (๐ โ โค โ (๐ โ 1) โ
โค) |
102 | 97, 101 | syl 17 |
. . . . . . . . 9
โข (๐ โ (๐ โ 1) โ โค) |
103 | | dvdsval2 16140 |
. . . . . . . . 9
โข ((2
โ โค โง 2 โ 0 โง (๐ โ 1) โ โค) โ (2
โฅ (๐ โ 1)
โ ((๐ โ 1) / 2)
โ โค)) |
104 | 54, 45, 102, 103 | mp3an2i 1467 |
. . . . . . . 8
โข (๐ โ (2 โฅ (๐ โ 1) โ ((๐ โ 1) / 2) โ
โค)) |
105 | 100, 104 | mpbid 231 |
. . . . . . 7
โข (๐ โ ((๐ โ 1) / 2) โ
โค) |
106 | 105 | zcnd 12609 |
. . . . . 6
โข (๐ โ ((๐ โ 1) / 2) โ
โ) |
107 | 93, 95, 106 | adddird 11181 |
. . . . 5
โข (๐ โ (((2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))) +
(((๐ด โ 1) / 2) +
((๐ต โ 1) / 2)))
ยท ((๐ โ 1) /
2)) = (((2 ยท (((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2))) ยท ((๐ โ 1) / 2)) + ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) /
2)))) |
108 | 91 | zcnd 12609 |
. . . . . . 7
โข (๐ โ (((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) โ
โ) |
109 | 43, 108, 106 | mulassd 11179 |
. . . . . 6
โข (๐ โ ((2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2)))
ยท ((๐ โ 1) /
2)) = (2 ยท ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) /
2)))) |
110 | 109 | oveq1d 7373 |
. . . . 5
โข (๐ โ (((2 ยท (((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2)))
ยท ((๐ โ 1) /
2)) + ((((๐ด โ 1) / 2)
+ ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2))) = ((2 ยท ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2))) + ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) /
2)))) |
111 | 89, 107, 110 | 3eqtrd 2781 |
. . . 4
โข (๐ โ (((๐ โ 1) / 2) ยท ((๐ โ 1) / 2)) = ((2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2))) + ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)))) |
112 | 111 | oveq2d 7374 |
. . 3
โข (๐ โ (-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2))) =
(-1โ((2 ยท ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2))) + ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) /
2))))) |
113 | | neg1cn 12268 |
. . . . . 6
โข -1 โ
โ |
114 | 113 | a1i 11 |
. . . . 5
โข (๐ โ -1 โ
โ) |
115 | | neg1ne0 12270 |
. . . . . 6
โข -1 โ
0 |
116 | 115 | a1i 11 |
. . . . 5
โข (๐ โ -1 โ
0) |
117 | 91, 105 | zmulcld 12614 |
. . . . . 6
โข (๐ โ ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2)) โ
โค) |
118 | 90, 117 | zmulcld 12614 |
. . . . 5
โข (๐ โ (2 ยท ((((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2))) โ โค) |
119 | 94, 105 | zmulcld 12614 |
. . . . 5
โข (๐ โ ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2)) โ
โค) |
120 | | expaddz 14013 |
. . . . 5
โข (((-1
โ โ โง -1 โ 0) โง ((2 ยท ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2)))
โ โค โง ((((๐ด
โ 1) / 2) + ((๐ต
โ 1) / 2)) ยท ((๐ โ 1) / 2)) โ โค)) โ
(-1โ((2 ยท ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2))) + ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2)))) =
((-1โ(2 ยท ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2)))) ยท
(-1โ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2))))) |
121 | 114, 116,
118, 119, 120 | syl22anc 838 |
. . . 4
โข (๐ โ (-1โ((2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2))) + ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)))) = ((-1โ(2 ยท ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2))))
ยท (-1โ((((๐ด
โ 1) / 2) + ((๐ต
โ 1) / 2)) ยท ((๐ โ 1) / 2))))) |
122 | | expmulz 14015 |
. . . . . . 7
โข (((-1
โ โ โง -1 โ 0) โง (2 โ โค โง ((((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)) โ โค)) โ (-1โ(2 ยท ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2)))) =
((-1โ2)โ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) /
2)))) |
123 | 114, 116,
90, 117, 122 | syl22anc 838 |
. . . . . 6
โข (๐ โ (-1โ(2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2)))) = ((-1โ2)โ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) /
2)))) |
124 | | neg1sqe1 14101 |
. . . . . . . 8
โข
(-1โ2) = 1 |
125 | 124 | oveq1i 7368 |
. . . . . . 7
โข
((-1โ2)โ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2))) =
(1โ((((๐ด โ 1) /
2) ยท ((๐ต โ 1)
/ 2)) ยท ((๐ โ
1) / 2))) |
126 | | 1exp 13998 |
. . . . . . . 8
โข
(((((๐ด โ 1) /
2) ยท ((๐ต โ 1)
/ 2)) ยท ((๐ โ
1) / 2)) โ โค โ (1โ((((๐ด โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2))) =
1) |
127 | 117, 126 | syl 17 |
. . . . . . 7
โข (๐ โ (1โ((((๐ด โ 1) / 2) ยท
((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2))) = 1) |
128 | 125, 127 | eqtrid 2789 |
. . . . . 6
โข (๐ โ
((-1โ2)โ((((๐ด
โ 1) / 2) ยท ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2))) =
1) |
129 | 123, 128 | eqtrd 2777 |
. . . . 5
โข (๐ โ (-1โ(2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2)))) = 1) |
130 | 129 | oveq1d 7373 |
. . . 4
โข (๐ โ ((-1โ(2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2)))) ยท (-1โ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2)))) = (1
ยท (-1โ((((๐ด
โ 1) / 2) + ((๐ต
โ 1) / 2)) ยท ((๐ โ 1) / 2))))) |
131 | 121, 130 | eqtrd 2777 |
. . 3
โข (๐ โ (-1โ((2 ยท
((((๐ด โ 1) / 2)
ยท ((๐ต โ 1) /
2)) ยท ((๐ โ 1)
/ 2))) + ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)))) = (1 ยท (-1โ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท ((๐ โ 1) /
2))))) |
132 | 114, 116,
119 | expclzd 14057 |
. . . . 5
โข (๐ โ (-1โ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2)))
โ โ) |
133 | 132 | mulid2d 11174 |
. . . 4
โข (๐ โ (1 ยท
(-1โ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)))) = (-1โ((((๐ด
โ 1) / 2) + ((๐ต
โ 1) / 2)) ยท ((๐ โ 1) / 2)))) |
134 | 70, 83, 106 | adddird 11181 |
. . . . 5
โข (๐ โ ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท ((๐ โ 1) / 2)) = ((((๐ด โ 1) / 2) ยท
((๐ โ 1) / 2)) +
(((๐ต โ 1) / 2)
ยท ((๐ โ 1) /
2)))) |
135 | 134 | oveq2d 7374 |
. . . 4
โข (๐ โ (-1โ((((๐ด โ 1) / 2) + ((๐ต โ 1) / 2)) ยท
((๐ โ 1) / 2))) =
(-1โ((((๐ด โ 1) /
2) ยท ((๐ โ 1)
/ 2)) + (((๐ต โ 1) /
2) ยท ((๐ โ 1)
/ 2))))) |
136 | 133, 135 | eqtrd 2777 |
. . 3
โข (๐ โ (1 ยท
(-1โ((((๐ด โ 1) /
2) + ((๐ต โ 1) / 2))
ยท ((๐ โ 1) /
2)))) = (-1โ((((๐ด
โ 1) / 2) ยท ((๐ โ 1) / 2)) + (((๐ต โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
137 | 112, 131,
136 | 3eqtrd 2781 |
. 2
โข (๐ โ (-1โ(((๐ โ 1) / 2) ยท
((๐ โ 1) / 2))) =
(-1โ((((๐ด โ 1) /
2) ยท ((๐ โ 1)
/ 2)) + (((๐ต โ 1) /
2) ยท ((๐ โ 1)
/ 2))))) |
138 | | lgsquad2lem1.1 |
. . . 4
โข (๐ โ ((๐ด /L ๐) ยท (๐ /L ๐ด)) = (-1โ(((๐ด โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
139 | | lgsquad2lem1.2 |
. . . 4
โข (๐ โ ((๐ต /L ๐) ยท (๐ /L ๐ต)) = (-1โ(((๐ต โ 1) / 2) ยท ((๐ โ 1) /
2)))) |
140 | 138, 139 | oveq12d 7376 |
. . 3
โข (๐ โ (((๐ด /L ๐) ยท (๐ /L ๐ด)) ยท ((๐ต /L ๐) ยท (๐ /L ๐ต))) = ((-1โ(((๐ด โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(-1โ(((๐ต โ 1) /
2) ยท ((๐ โ 1)
/ 2))))) |
141 | 69, 105 | zmulcld 12614 |
. . . 4
โข (๐ โ (((๐ด โ 1) / 2) ยท ((๐ โ 1) / 2)) โ
โค) |
142 | 82, 105 | zmulcld 12614 |
. . . 4
โข (๐ โ (((๐ต โ 1) / 2) ยท ((๐ โ 1) / 2)) โ
โค) |
143 | | expaddz 14013 |
. . . 4
โข (((-1
โ โ โง -1 โ 0) โง ((((๐ด โ 1) / 2) ยท ((๐ โ 1) / 2)) โ โค
โง (((๐ต โ 1) / 2)
ยท ((๐ โ 1) /
2)) โ โค)) โ (-1โ((((๐ด โ 1) / 2) ยท ((๐ โ 1) / 2)) + (((๐ต โ 1) / 2) ยท
((๐ โ 1) / 2)))) =
((-1โ(((๐ด โ 1) /
2) ยท ((๐ โ 1)
/ 2))) ยท (-1โ(((๐ต โ 1) / 2) ยท ((๐ โ 1) /
2))))) |
144 | 114, 116,
141, 142, 143 | syl22anc 838 |
. . 3
โข (๐ โ (-1โ((((๐ด โ 1) / 2) ยท
((๐ โ 1) / 2)) +
(((๐ต โ 1) / 2)
ยท ((๐ โ 1) /
2)))) = ((-1โ(((๐ด
โ 1) / 2) ยท ((๐ โ 1) / 2))) ยท
(-1โ(((๐ต โ 1) /
2) ยท ((๐ โ 1)
/ 2))))) |
145 | 140, 144 | eqtr4d 2780 |
. 2
โข (๐ โ (((๐ด /L ๐) ยท (๐ /L ๐ด)) ยท ((๐ต /L ๐) ยท (๐ /L ๐ต))) = (-1โ((((๐ด โ 1) / 2) ยท ((๐ โ 1) / 2)) + (((๐ต โ 1) / 2) ยท
((๐ โ 1) /
2))))) |
146 | | lgscl 26662 |
. . . . . 6
โข ((๐ด โ โค โง ๐ โ โค) โ (๐ด /L ๐) โ
โค) |
147 | 3, 97, 146 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ด /L ๐) โ โค) |
148 | 147 | zcnd 12609 |
. . . 4
โข (๐ โ (๐ด /L ๐) โ โ) |
149 | | lgscl 26662 |
. . . . . 6
โข ((๐ต โ โค โง ๐ โ โค) โ (๐ต /L ๐) โ
โค) |
150 | 9, 97, 149 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ต /L ๐) โ โค) |
151 | 150 | zcnd 12609 |
. . . 4
โข (๐ โ (๐ต /L ๐) โ โ) |
152 | | lgscl 26662 |
. . . . . 6
โข ((๐ โ โค โง ๐ด โ โค) โ (๐ /L ๐ด) โ
โค) |
153 | 97, 3, 152 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ /L ๐ด) โ โค) |
154 | 153 | zcnd 12609 |
. . . 4
โข (๐ โ (๐ /L ๐ด) โ โ) |
155 | | lgscl 26662 |
. . . . . 6
โข ((๐ โ โค โง ๐ต โ โค) โ (๐ /L ๐ต) โ
โค) |
156 | 97, 9, 155 | syl2anc 585 |
. . . . 5
โข (๐ โ (๐ /L ๐ต) โ โค) |
157 | 156 | zcnd 12609 |
. . . 4
โข (๐ โ (๐ /L ๐ต) โ โ) |
158 | 148, 151,
154, 157 | mul4d 11368 |
. . 3
โข (๐ โ (((๐ด /L ๐) ยท (๐ต /L ๐)) ยท ((๐ /L ๐ด) ยท (๐ /L ๐ต))) = (((๐ด /L ๐) ยท (๐ /L ๐ด)) ยท ((๐ต /L ๐) ยท (๐ /L ๐ต)))) |
159 | 2 | nnne0d 12204 |
. . . . . 6
โข (๐ โ ๐ด โ 0) |
160 | 8 | nnne0d 12204 |
. . . . . 6
โข (๐ โ ๐ต โ 0) |
161 | | lgsdir 26683 |
. . . . . 6
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
162 | 3, 9, 97, 159, 160, 161 | syl32anc 1379 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ต) /L ๐) = ((๐ด /L ๐) ยท (๐ต /L ๐))) |
163 | 1 | oveq1d 7373 |
. . . . 5
โข (๐ โ ((๐ด ยท ๐ต) /L ๐) = (๐ /L ๐)) |
164 | 162, 163 | eqtr3d 2779 |
. . . 4
โข (๐ โ ((๐ด /L ๐) ยท (๐ต /L ๐)) = (๐ /L ๐)) |
165 | | lgsdi 26685 |
. . . . . 6
โข (((๐ โ โค โง ๐ด โ โค โง ๐ต โ โค) โง (๐ด โ 0 โง ๐ต โ 0)) โ (๐ /L (๐ด ยท ๐ต)) = ((๐ /L ๐ด) ยท (๐ /L ๐ต))) |
166 | 97, 3, 9, 159, 160, 165 | syl32anc 1379 |
. . . . 5
โข (๐ โ (๐ /L (๐ด ยท ๐ต)) = ((๐ /L ๐ด) ยท (๐ /L ๐ต))) |
167 | 1 | oveq2d 7374 |
. . . . 5
โข (๐ โ (๐ /L (๐ด ยท ๐ต)) = (๐ /L ๐)) |
168 | 166, 167 | eqtr3d 2779 |
. . . 4
โข (๐ โ ((๐ /L ๐ด) ยท (๐ /L ๐ต)) = (๐ /L ๐)) |
169 | 164, 168 | oveq12d 7376 |
. . 3
โข (๐ โ (((๐ด /L ๐) ยท (๐ต /L ๐)) ยท ((๐ /L ๐ด) ยท (๐ /L ๐ต))) = ((๐ /L ๐) ยท (๐ /L ๐))) |
170 | 158, 169 | eqtr3d 2779 |
. 2
โข (๐ โ (((๐ด /L ๐) ยท (๐ /L ๐ด)) ยท ((๐ต /L ๐) ยท (๐ /L ๐ต))) = ((๐ /L ๐) ยท (๐ /L ๐))) |
171 | 137, 145,
170 | 3eqtr2rd 2784 |
1
โข (๐ โ ((๐ /L ๐) ยท (๐ /L ๐)) = (-1โ(((๐ โ 1) / 2) ยท ((๐ โ 1) /
2)))) |