MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lgsquad2lem2 Structured version   Visualization version   GIF version

Theorem lgsquad2lem2 27234
Description: Lemma for lgsquad2 27235. (Contributed by Mario Carneiro, 19-Jun-2015.)
Hypotheses
Ref Expression
lgsquad2.1 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
lgsquad2.2 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘€)
lgsquad2.3 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
lgsquad2.4 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘)
lgsquad2.5 (๐œ‘ โ†’ (๐‘€ gcd ๐‘) = 1)
lgsquad2lem2.f ((๐œ‘ โˆง (๐‘š โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘š gcd ๐‘) = 1)) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
lgsquad2lem2.s (๐œ“ โ†” โˆ€๐‘ฅ โˆˆ (1...๐‘˜)((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
Assertion
Ref Expression
lgsquad2lem2 (๐œ‘ โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
Distinct variable groups:   ๐‘š,๐‘€   ๐‘ฅ,๐‘š,๐‘   ๐œ‘,๐‘š,๐‘ฅ
Allowed substitution hints:   ๐œ‘(๐‘˜)   ๐œ“(๐‘ฅ,๐‘˜,๐‘š)   ๐‘€(๐‘ฅ,๐‘˜)   ๐‘(๐‘˜)

Proof of Theorem lgsquad2lem2
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 lgsquad2.1 . . . 4 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„•)
2 2nn 12282 . . . . 5 2 โˆˆ โ„•
32a1i 11 . . . 4 (๐œ‘ โ†’ 2 โˆˆ โ„•)
4 lgsquad2.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
51nnzd 12582 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
6 2z 12591 . . . . . 6 2 โˆˆ โ„ค
7 gcdcom 16451 . . . . . 6 ((๐‘€ โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ (๐‘€ gcd 2) = (2 gcd ๐‘€))
85, 6, 7sylancl 585 . . . . 5 (๐œ‘ โ†’ (๐‘€ gcd 2) = (2 gcd ๐‘€))
9 lgsquad2.2 . . . . . 6 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘€)
10 2prm 16626 . . . . . . 7 2 โˆˆ โ„™
11 coprm 16645 . . . . . . 7 ((2 โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค) โ†’ (ยฌ 2 โˆฅ ๐‘€ โ†” (2 gcd ๐‘€) = 1))
1210, 5, 11sylancr 586 . . . . . 6 (๐œ‘ โ†’ (ยฌ 2 โˆฅ ๐‘€ โ†” (2 gcd ๐‘€) = 1))
139, 12mpbid 231 . . . . 5 (๐œ‘ โ†’ (2 gcd ๐‘€) = 1)
148, 13eqtrd 2764 . . . 4 (๐œ‘ โ†’ (๐‘€ gcd 2) = 1)
15 rpmulgcd 16495 . . . 4 (((๐‘€ โˆˆ โ„• โˆง 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘€ gcd 2) = 1) โ†’ (๐‘€ gcd (2 ยท ๐‘)) = (๐‘€ gcd ๐‘))
161, 3, 4, 14, 15syl31anc 1370 . . 3 (๐œ‘ โ†’ (๐‘€ gcd (2 ยท ๐‘)) = (๐‘€ gcd ๐‘))
17 lgsquad2.5 . . 3 (๐œ‘ โ†’ (๐‘€ gcd ๐‘) = 1)
1816, 17eqtrd 2764 . 2 (๐œ‘ โ†’ (๐‘€ gcd (2 ยท ๐‘)) = 1)
19 oveq1 7408 . . . . . . . 8 (๐‘š = 1 โ†’ (๐‘š /L ๐‘) = (1 /L ๐‘))
20 oveq2 7409 . . . . . . . 8 (๐‘š = 1 โ†’ (๐‘ /L ๐‘š) = (๐‘ /L 1))
2119, 20oveq12d 7419 . . . . . . 7 (๐‘š = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((1 /L ๐‘) ยท (๐‘ /L 1)))
22 oveq1 7408 . . . . . . . . . . . 12 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = (1 โˆ’ 1))
23 1m1e0 12281 . . . . . . . . . . . 12 (1 โˆ’ 1) = 0
2422, 23eqtrdi 2780 . . . . . . . . . . 11 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = 0)
2524oveq1d 7416 . . . . . . . . . 10 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1) / 2) = (0 / 2))
26 2cn 12284 . . . . . . . . . . 11 2 โˆˆ โ„‚
27 2ne0 12313 . . . . . . . . . . 11 2 โ‰  0
2826, 27div0i 11945 . . . . . . . . . 10 (0 / 2) = 0
2925, 28eqtrdi 2780 . . . . . . . . 9 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1) / 2) = 0)
3029oveq1d 7416 . . . . . . . 8 (๐‘š = 1 โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (0 ยท ((๐‘ โˆ’ 1) / 2)))
3130oveq2d 7417 . . . . . . 7 (๐‘š = 1 โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))))
3221, 31eqeq12d 2740 . . . . . 6 (๐‘š = 1 โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2)))))
3332imbi2d 340 . . . . 5 (๐‘š = 1 โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))))))
3433imbi2d 340 . . . 4 (๐‘š = 1 โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2)))))))
35 oveq1 7408 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘ฅ gcd (2 ยท ๐‘)))
3635eqeq1d 2726 . . . . . 6 (๐‘š = ๐‘ฅ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘ฅ gcd (2 ยท ๐‘)) = 1))
37 oveq1 7408 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (๐‘š /L ๐‘) = (๐‘ฅ /L ๐‘))
38 oveq2 7409 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘ฅ))
3937, 38oveq12d 7419 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)))
40 oveq1 7408 . . . . . . . . . 10 (๐‘š = ๐‘ฅ โ†’ (๐‘š โˆ’ 1) = (๐‘ฅ โˆ’ 1))
4140oveq1d 7416 . . . . . . . . 9 (๐‘š = ๐‘ฅ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘ฅ โˆ’ 1) / 2))
4241oveq1d 7416 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
4342oveq2d 7417 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
4439, 43eqeq12d 2740 . . . . . 6 (๐‘š = ๐‘ฅ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
4536, 44imbi12d 344 . . . . 5 (๐‘š = ๐‘ฅ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
4645imbi2d 340 . . . 4 (๐‘š = ๐‘ฅ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
47 oveq1 7408 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘ฆ gcd (2 ยท ๐‘)))
4847eqeq1d 2726 . . . . . 6 (๐‘š = ๐‘ฆ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘ฆ gcd (2 ยท ๐‘)) = 1))
49 oveq1 7408 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (๐‘š /L ๐‘) = (๐‘ฆ /L ๐‘))
50 oveq2 7409 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘ฆ))
5149, 50oveq12d 7419 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)))
52 oveq1 7408 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ (๐‘š โˆ’ 1) = (๐‘ฆ โˆ’ 1))
5352oveq1d 7416 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘ฆ โˆ’ 1) / 2))
5453oveq1d 7416 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
5554oveq2d 7417 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
5651, 55eqeq12d 2740 . . . . . 6 (๐‘š = ๐‘ฆ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
5748, 56imbi12d 344 . . . . 5 (๐‘š = ๐‘ฆ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
5857imbi2d 340 . . . 4 (๐‘š = ๐‘ฆ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
59 oveq1 7408 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š gcd (2 ยท ๐‘)) = ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)))
6059eqeq1d 2726 . . . . . 6 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1))
61 oveq1 7408 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š /L ๐‘) = ((๐‘ฅ ยท ๐‘ฆ) /L ๐‘))
62 oveq2 7409 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘ /L ๐‘š) = (๐‘ /L (๐‘ฅ ยท ๐‘ฆ)))
6361, 62oveq12d 7419 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))))
64 oveq1 7408 . . . . . . . . . 10 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š โˆ’ 1) = ((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1))
6564oveq1d 7416 . . . . . . . . 9 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š โˆ’ 1) / 2) = (((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2))
6665oveq1d 7416 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = ((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
6766oveq2d 7417 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
6863, 67eqeq12d 2740 . . . . . 6 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
6960, 68imbi12d 344 . . . . 5 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
7069imbi2d 340 . . . 4 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
71 oveq1 7408 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘€ gcd (2 ยท ๐‘)))
7271eqeq1d 2726 . . . . . 6 (๐‘š = ๐‘€ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘€ gcd (2 ยท ๐‘)) = 1))
73 oveq1 7408 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (๐‘š /L ๐‘) = (๐‘€ /L ๐‘))
74 oveq2 7409 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘€))
7573, 74oveq12d 7419 . . . . . . 7 (๐‘š = ๐‘€ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)))
76 oveq1 7408 . . . . . . . . . 10 (๐‘š = ๐‘€ โ†’ (๐‘š โˆ’ 1) = (๐‘€ โˆ’ 1))
7776oveq1d 7416 . . . . . . . . 9 (๐‘š = ๐‘€ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘€ โˆ’ 1) / 2))
7877oveq1d 7416 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
7978oveq2d 7417 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
8075, 79eqeq12d 2740 . . . . . 6 (๐‘š = ๐‘€ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
8172, 80imbi12d 344 . . . . 5 (๐‘š = ๐‘€ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
8281imbi2d 340 . . . 4 (๐‘š = ๐‘€ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
83 1t1e1 12371 . . . . . . 7 (1 ยท 1) = 1
84 neg1cn 12323 . . . . . . . 8 -1 โˆˆ โ„‚
85 exp0 14028 . . . . . . . 8 (-1 โˆˆ โ„‚ โ†’ (-1โ†‘0) = 1)
8684, 85ax-mp 5 . . . . . . 7 (-1โ†‘0) = 1
8783, 86eqtr4i 2755 . . . . . 6 (1 ยท 1) = (-1โ†‘0)
88 sq1 14156 . . . . . . . . 9 (1โ†‘2) = 1
8988oveq1i 7411 . . . . . . . 8 ((1โ†‘2) /L ๐‘) = (1 /L ๐‘)
90 1z 12589 . . . . . . . . . 10 1 โˆˆ โ„ค
91 ax-1ne0 11175 . . . . . . . . . 10 1 โ‰  0
9290, 91pm3.2i 470 . . . . . . . . 9 (1 โˆˆ โ„ค โˆง 1 โ‰  0)
934nnzd 12582 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
94 1gcd 16472 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ (1 gcd ๐‘) = 1)
9593, 94syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (1 gcd ๐‘) = 1)
96 lgssq 27186 . . . . . . . . 9 (((1 โˆˆ โ„ค โˆง 1 โ‰  0) โˆง ๐‘ โˆˆ โ„ค โˆง (1 gcd ๐‘) = 1) โ†’ ((1โ†‘2) /L ๐‘) = 1)
9792, 93, 95, 96mp3an2i 1462 . . . . . . . 8 (๐œ‘ โ†’ ((1โ†‘2) /L ๐‘) = 1)
9889, 97eqtr3id 2778 . . . . . . 7 (๐œ‘ โ†’ (1 /L ๐‘) = 1)
9988oveq2i 7412 . . . . . . . 8 (๐‘ /L (1โ†‘2)) = (๐‘ /L 1)
100 1nn 12220 . . . . . . . . . 10 1 โˆˆ โ„•
101100a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ 1 โˆˆ โ„•)
102 gcd1 16466 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ (๐‘ gcd 1) = 1)
10393, 102syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ gcd 1) = 1)
104 lgssq2 27187 . . . . . . . . 9 ((๐‘ โˆˆ โ„ค โˆง 1 โˆˆ โ„• โˆง (๐‘ gcd 1) = 1) โ†’ (๐‘ /L (1โ†‘2)) = 1)
10593, 101, 103, 104syl3anc 1368 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ /L (1โ†‘2)) = 1)
10699, 105eqtr3id 2778 . . . . . . 7 (๐œ‘ โ†’ (๐‘ /L 1) = 1)
10798, 106oveq12d 7419 . . . . . 6 (๐œ‘ โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (1 ยท 1))
108 nnm1nn0 12510 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
1094, 108syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
110109nn0cnd 12531 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„‚)
111110halfcld 12454 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ โˆ’ 1) / 2) โˆˆ โ„‚)
112111mul02d 11409 . . . . . . 7 (๐œ‘ โ†’ (0 ยท ((๐‘ โˆ’ 1) / 2)) = 0)
113112oveq2d 7417 . . . . . 6 (๐œ‘ โ†’ (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘0))
11487, 107, 1133eqtr4a 2790 . . . . 5 (๐œ‘ โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))))
115114a1d 25 . . . 4 (๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2)))))
116 simprl 768 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„™)
117 prmz 16609 . . . . . . . . . . . 12 (๐‘š โˆˆ โ„™ โ†’ ๐‘š โˆˆ โ„ค)
118117ad2antrl 725 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„ค)
1196a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆˆ โ„ค)
1204adantr 480 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘ โˆˆ โ„•)
121120nnzd 12582 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘ โˆˆ โ„ค)
122 zmulcl 12608 . . . . . . . . . . . 12 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
1236, 121, 122sylancr 586 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
124 simprr 770 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd (2 ยท ๐‘)) = 1)
125 dvdsmul1 16218 . . . . . . . . . . . 12 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ 2 โˆฅ (2 ยท ๐‘))
1266, 121, 125sylancr 586 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆฅ (2 ยท ๐‘))
127 rpdvds 16594 . . . . . . . . . . 11 (((๐‘š โˆˆ โ„ค โˆง 2 โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โˆง ((๐‘š gcd (2 ยท ๐‘)) = 1 โˆง 2 โˆฅ (2 ยท ๐‘))) โ†’ (๐‘š gcd 2) = 1)
128118, 119, 123, 124, 126, 127syl32anc 1375 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd 2) = 1)
129 prmrp 16646 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„™ โˆง 2 โˆˆ โ„™) โ†’ ((๐‘š gcd 2) = 1 โ†” ๐‘š โ‰  2))
130116, 10, 129sylancl 585 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ((๐‘š gcd 2) = 1 โ†” ๐‘š โ‰  2))
131128, 130mpbid 231 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โ‰  2)
132 eldifsn 4782 . . . . . . . . 9 (๐‘š โˆˆ (โ„™ โˆ– {2}) โ†” (๐‘š โˆˆ โ„™ โˆง ๐‘š โ‰  2))
133116, 131, 132sylanbrc 582 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ (โ„™ โˆ– {2}))
134 prmnn 16608 . . . . . . . . . . 11 (๐‘š โˆˆ โ„™ โ†’ ๐‘š โˆˆ โ„•)
135134ad2antrl 725 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„•)
1362a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆˆ โ„•)
137 rpmulgcd 16495 . . . . . . . . . 10 (((๐‘š โˆˆ โ„• โˆง 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘š gcd 2) = 1) โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘š gcd ๐‘))
138135, 136, 120, 128, 137syl31anc 1370 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘š gcd ๐‘))
139138, 124eqtr3d 2766 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd ๐‘) = 1)
140133, 139jca 511 . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘š gcd ๐‘) = 1))
141 lgsquad2lem2.f . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘š gcd ๐‘) = 1)) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
142140, 141syldan 590 . . . . . 6 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
143142exp32 420 . . . . 5 (๐œ‘ โ†’ (๐‘š โˆˆ โ„™ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
144143com12 32 . . . 4 (๐‘š โˆˆ โ„™ โ†’ (๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
145 jcab 517 . . . . 5 ((๐œ‘ โ†’ (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))) โ†” ((๐œ‘ โ†’ ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โˆง (๐œ‘ โ†’ ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
146 simplrl 774 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2))
147 eluz2nn 12865 . . . . . . . . . . . 12 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„•)
148146, 147syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ๐‘ฅ โˆˆ โ„•)
149 simplrr 775 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))
150 eluz2nn 12865 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฆ โˆˆ โ„•)
151149, 150syl 17 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ๐‘ฆ โˆˆ โ„•)
152148, 151nnmulcld 12262 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„•)
153 n2dvds1 16308 . . . . . . . . . . . 12 ยฌ 2 โˆฅ 1
15493ad2antrr 723 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ โˆˆ โ„ค)
1556, 154, 125sylancr 586 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ 2 โˆฅ (2 ยท ๐‘))
156 eluzelz 12829 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„ค)
157 eluzelz 12829 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฆ โˆˆ โ„ค)
158156, 157anim12i 612 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค))
159158ad2antlr 724 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค))
160 zmulcl 12608 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค)
161159, 160syl 17 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค)
1626, 154, 122sylancr 586 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
163 dvdsgcd 16483 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โ†’ ((2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โˆง 2 โˆฅ (2 ยท ๐‘)) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
1646, 161, 162, 163mp3an2i 1462 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โˆง 2 โˆฅ (2 ยท ๐‘)) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
165155, 164mpan2d 691 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
166 simpr 484 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1)
167166breq2d 5150 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) โ†” 2 โˆฅ 1))
168165, 167sylibd 238 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โ†’ 2 โˆฅ 1))
169153, 168mtoi 198 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ยฌ 2 โˆฅ (๐‘ฅ ยท ๐‘ฆ))
170169adantrr 714 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ยฌ 2 โˆฅ (๐‘ฅ ยท ๐‘ฆ))
1714ad2antrr 723 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ๐‘ โˆˆ โ„•)
172 lgsquad2.4 . . . . . . . . . . 11 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘)
173172ad2antrr 723 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ยฌ 2 โˆฅ ๐‘)
174 dvdsmul2 16219 . . . . . . . . . . . . 13 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (2 ยท ๐‘))
1756, 154, 174sylancr 586 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ โˆฅ (2 ยท ๐‘))
176 rpdvds 16594 . . . . . . . . . . . 12 ((((๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง ๐‘ โˆฅ (2 ยท ๐‘))) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd ๐‘) = 1)
177161, 154, 162, 166, 175, 176syl32anc 1375 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd ๐‘) = 1)
178177adantrr 714 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd ๐‘) = 1)
179 eqidd 2725 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ (๐‘ฅ ยท ๐‘ฆ) = (๐‘ฅ ยท ๐‘ฆ))
180159simpld 494 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฅ โˆˆ โ„ค)
181180, 162gcdcomd 16452 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ gcd (2 ยท ๐‘)) = ((2 ยท ๐‘) gcd ๐‘ฅ))
182162, 161gcdcomd 16452 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)))
183182, 166eqtrd 2764 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1)
184 dvdsmul1 16218 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
185159, 184syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
186 rpdvds 16594 . . . . . . . . . . . . . 14 ((((2 ยท ๐‘) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค) โˆง (((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1 โˆง ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))) โ†’ ((2 ยท ๐‘) gcd ๐‘ฅ) = 1)
187162, 180, 161, 183, 185, 186syl32anc 1375 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd ๐‘ฅ) = 1)
188181, 187eqtrd 2764 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ gcd (2 ยท ๐‘)) = 1)
189188adantrr 714 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ (๐‘ฅ gcd (2 ยท ๐‘)) = 1)
190 simprrl 778 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
191189, 190mpd 15 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
192159simprd 495 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฆ โˆˆ โ„ค)
193192, 162gcdcomd 16452 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฆ gcd (2 ยท ๐‘)) = ((2 ยท ๐‘) gcd ๐‘ฆ))
194 dvdsmul2 16219 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
195159, 194syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
196 rpdvds 16594 . . . . . . . . . . . . . 14 ((((2 ยท ๐‘) โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค) โˆง (((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1 โˆง ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))) โ†’ ((2 ยท ๐‘) gcd ๐‘ฆ) = 1)
197162, 192, 161, 183, 195, 196syl32anc 1375 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd ๐‘ฆ) = 1)
198193, 197eqtrd 2764 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฆ gcd (2 ยท ๐‘)) = 1)
199198adantrr 714 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ (๐‘ฆ gcd (2 ยท ๐‘)) = 1)
200 simprrr 779 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
201199, 200mpd 15 . . . . . . . . . 10 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
202152, 170, 171, 173, 178, 148, 151, 179, 191, 201lgsquad2lem1 27233 . . . . . . . . 9 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))) โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
203202exp32 420 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ ((((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
204203com23 86 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โ†’ ((((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
205204expcom 413 . . . . . 6 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐œ‘ โ†’ ((((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
206205a2d 29 . . . . 5 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ ((๐œ‘ โ†’ (((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โˆง ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))) โ†’ (๐œ‘ โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
207145, 206biimtrrid 242 . . . 4 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (((๐œ‘ โ†’ ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โˆง (๐œ‘ โ†’ ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))) โ†’ (๐œ‘ โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
20834, 46, 58, 70, 82, 115, 144, 207prmind 16620 . . 3 (๐‘€ โˆˆ โ„• โ†’ (๐œ‘ โ†’ ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
2091, 208mpcom 38 . 2 (๐œ‘ โ†’ ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
21018, 209mpd 15 1 (๐œ‘ โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 395   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2932  โˆ€wral 3053   โˆ– cdif 3937  {csn 4620   class class class wbr 5138  โ€˜cfv 6533  (class class class)co 7401  โ„‚cc 11104  0cc0 11106  1c1 11107   ยท cmul 11111   โˆ’ cmin 11441  -cneg 11442   / cdiv 11868  โ„•cn 12209  2c2 12264  โ„•0cn0 12469  โ„คcz 12555  โ„คโ‰ฅcuz 12819  ...cfz 13481  โ†‘cexp 14024   โˆฅ cdvds 16194   gcd cgcd 16432  โ„™cprime 16605   /L clgs 27143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-int 4941  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-2o 8462  df-oadd 8465  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-dju 9892  df-card 9930  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-uz 12820  df-q 12930  df-rp 12972  df-fz 13482  df-fzo 13625  df-fl 13754  df-mod 13832  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-dvds 16195  df-gcd 16433  df-prm 16606  df-phi 16698  df-pc 16769  df-lgs 27144
This theorem is referenced by:  lgsquad2  27235
  Copyright terms: Public domain W3C validator