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

Theorem lgsquad2lem2 26736
Description: Lemma for lgsquad2 26737. (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 12227 . . . . 5 2 โˆˆ โ„•
32a1i 11 . . . 4 (๐œ‘ โ†’ 2 โˆˆ โ„•)
4 lgsquad2.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ โ„•)
51nnzd 12527 . . . . . 6 (๐œ‘ โ†’ ๐‘€ โˆˆ โ„ค)
6 2z 12536 . . . . . 6 2 โˆˆ โ„ค
7 gcdcom 16394 . . . . . 6 ((๐‘€ โˆˆ โ„ค โˆง 2 โˆˆ โ„ค) โ†’ (๐‘€ gcd 2) = (2 gcd ๐‘€))
85, 6, 7sylancl 587 . . . . 5 (๐œ‘ โ†’ (๐‘€ gcd 2) = (2 gcd ๐‘€))
9 lgsquad2.2 . . . . . 6 (๐œ‘ โ†’ ยฌ 2 โˆฅ ๐‘€)
10 2prm 16569 . . . . . . 7 2 โˆˆ โ„™
11 coprm 16588 . . . . . . 7 ((2 โˆˆ โ„™ โˆง ๐‘€ โˆˆ โ„ค) โ†’ (ยฌ 2 โˆฅ ๐‘€ โ†” (2 gcd ๐‘€) = 1))
1210, 5, 11sylancr 588 . . . . . 6 (๐œ‘ โ†’ (ยฌ 2 โˆฅ ๐‘€ โ†” (2 gcd ๐‘€) = 1))
139, 12mpbid 231 . . . . 5 (๐œ‘ โ†’ (2 gcd ๐‘€) = 1)
148, 13eqtrd 2777 . . . 4 (๐œ‘ โ†’ (๐‘€ gcd 2) = 1)
15 rpmulgcd 16438 . . . 4 (((๐‘€ โˆˆ โ„• โˆง 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘€ gcd 2) = 1) โ†’ (๐‘€ gcd (2 ยท ๐‘)) = (๐‘€ gcd ๐‘))
161, 3, 4, 14, 15syl31anc 1374 . . 3 (๐œ‘ โ†’ (๐‘€ gcd (2 ยท ๐‘)) = (๐‘€ gcd ๐‘))
17 lgsquad2.5 . . 3 (๐œ‘ โ†’ (๐‘€ gcd ๐‘) = 1)
1816, 17eqtrd 2777 . 2 (๐œ‘ โ†’ (๐‘€ gcd (2 ยท ๐‘)) = 1)
19 oveq1 7365 . . . . . . . 8 (๐‘š = 1 โ†’ (๐‘š /L ๐‘) = (1 /L ๐‘))
20 oveq2 7366 . . . . . . . 8 (๐‘š = 1 โ†’ (๐‘ /L ๐‘š) = (๐‘ /L 1))
2119, 20oveq12d 7376 . . . . . . 7 (๐‘š = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((1 /L ๐‘) ยท (๐‘ /L 1)))
22 oveq1 7365 . . . . . . . . . . . 12 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = (1 โˆ’ 1))
23 1m1e0 12226 . . . . . . . . . . . 12 (1 โˆ’ 1) = 0
2422, 23eqtrdi 2793 . . . . . . . . . . 11 (๐‘š = 1 โ†’ (๐‘š โˆ’ 1) = 0)
2524oveq1d 7373 . . . . . . . . . 10 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1) / 2) = (0 / 2))
26 2cn 12229 . . . . . . . . . . 11 2 โˆˆ โ„‚
27 2ne0 12258 . . . . . . . . . . 11 2 โ‰  0
2826, 27div0i 11890 . . . . . . . . . 10 (0 / 2) = 0
2925, 28eqtrdi 2793 . . . . . . . . 9 (๐‘š = 1 โ†’ ((๐‘š โˆ’ 1) / 2) = 0)
3029oveq1d 7373 . . . . . . . 8 (๐‘š = 1 โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (0 ยท ((๐‘ โˆ’ 1) / 2)))
3130oveq2d 7374 . . . . . . 7 (๐‘š = 1 โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))))
3221, 31eqeq12d 2753 . . . . . 6 (๐‘š = 1 โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2)))))
3332imbi2d 341 . . . . 5 (๐‘š = 1 โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))))))
3433imbi2d 341 . . . 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 7365 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘ฅ gcd (2 ยท ๐‘)))
3635eqeq1d 2739 . . . . . 6 (๐‘š = ๐‘ฅ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘ฅ gcd (2 ยท ๐‘)) = 1))
37 oveq1 7365 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (๐‘š /L ๐‘) = (๐‘ฅ /L ๐‘))
38 oveq2 7366 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘ฅ))
3937, 38oveq12d 7376 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)))
40 oveq1 7365 . . . . . . . . . 10 (๐‘š = ๐‘ฅ โ†’ (๐‘š โˆ’ 1) = (๐‘ฅ โˆ’ 1))
4140oveq1d 7373 . . . . . . . . 9 (๐‘š = ๐‘ฅ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘ฅ โˆ’ 1) / 2))
4241oveq1d 7373 . . . . . . . 8 (๐‘š = ๐‘ฅ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
4342oveq2d 7374 . . . . . . 7 (๐‘š = ๐‘ฅ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
4439, 43eqeq12d 2753 . . . . . 6 (๐‘š = ๐‘ฅ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
4536, 44imbi12d 345 . . . . 5 (๐‘š = ๐‘ฅ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
4645imbi2d 341 . . . 4 (๐‘š = ๐‘ฅ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘ฅ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฅ /L ๐‘) ยท (๐‘ /L ๐‘ฅ)) = (-1โ†‘(((๐‘ฅ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
47 oveq1 7365 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘ฆ gcd (2 ยท ๐‘)))
4847eqeq1d 2739 . . . . . 6 (๐‘š = ๐‘ฆ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘ฆ gcd (2 ยท ๐‘)) = 1))
49 oveq1 7365 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (๐‘š /L ๐‘) = (๐‘ฆ /L ๐‘))
50 oveq2 7366 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘ฆ))
5149, 50oveq12d 7376 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)))
52 oveq1 7365 . . . . . . . . . 10 (๐‘š = ๐‘ฆ โ†’ (๐‘š โˆ’ 1) = (๐‘ฆ โˆ’ 1))
5352oveq1d 7373 . . . . . . . . 9 (๐‘š = ๐‘ฆ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘ฆ โˆ’ 1) / 2))
5453oveq1d 7373 . . . . . . . 8 (๐‘š = ๐‘ฆ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
5554oveq2d 7374 . . . . . . 7 (๐‘š = ๐‘ฆ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
5651, 55eqeq12d 2753 . . . . . 6 (๐‘š = ๐‘ฆ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
5748, 56imbi12d 345 . . . . 5 (๐‘š = ๐‘ฆ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
5857imbi2d 341 . . . 4 (๐‘š = ๐‘ฆ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘ฆ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘ฆ /L ๐‘) ยท (๐‘ /L ๐‘ฆ)) = (-1โ†‘(((๐‘ฆ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
59 oveq1 7365 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š gcd (2 ยท ๐‘)) = ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)))
6059eqeq1d 2739 . . . . . 6 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1))
61 oveq1 7365 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š /L ๐‘) = ((๐‘ฅ ยท ๐‘ฆ) /L ๐‘))
62 oveq2 7366 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘ /L ๐‘š) = (๐‘ /L (๐‘ฅ ยท ๐‘ฆ)))
6361, 62oveq12d 7376 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))))
64 oveq1 7365 . . . . . . . . . 10 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (๐‘š โˆ’ 1) = ((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1))
6564oveq1d 7373 . . . . . . . . 9 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐‘š โˆ’ 1) / 2) = (((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2))
6665oveq1d 7373 . . . . . . . 8 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = ((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
6766oveq2d 7374 . . . . . . 7 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
6863, 67eqeq12d 2753 . . . . . 6 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
6960, 68imbi12d 345 . . . . 5 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
7069imbi2d 341 . . . 4 (๐‘š = (๐‘ฅ ยท ๐‘ฆ) โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โ†’ (((๐‘ฅ ยท ๐‘ฆ) /L ๐‘) ยท (๐‘ /L (๐‘ฅ ยท ๐‘ฆ))) = (-1โ†‘((((๐‘ฅ ยท ๐‘ฆ) โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
71 oveq1 7365 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘€ gcd (2 ยท ๐‘)))
7271eqeq1d 2739 . . . . . 6 (๐‘š = ๐‘€ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†” (๐‘€ gcd (2 ยท ๐‘)) = 1))
73 oveq1 7365 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (๐‘š /L ๐‘) = (๐‘€ /L ๐‘))
74 oveq2 7366 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (๐‘ /L ๐‘š) = (๐‘ /L ๐‘€))
7573, 74oveq12d 7376 . . . . . . 7 (๐‘š = ๐‘€ โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)))
76 oveq1 7365 . . . . . . . . . 10 (๐‘š = ๐‘€ โ†’ (๐‘š โˆ’ 1) = (๐‘€ โˆ’ 1))
7776oveq1d 7373 . . . . . . . . 9 (๐‘š = ๐‘€ โ†’ ((๐‘š โˆ’ 1) / 2) = ((๐‘€ โˆ’ 1) / 2))
7877oveq1d 7373 . . . . . . . 8 (๐‘š = ๐‘€ โ†’ (((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)) = (((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))
7978oveq2d 7374 . . . . . . 7 (๐‘š = ๐‘€ โ†’ (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
8075, 79eqeq12d 2753 . . . . . 6 (๐‘š = ๐‘€ โ†’ (((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))) โ†” ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))
8172, 80imbi12d 345 . . . . 5 (๐‘š = ๐‘€ โ†’ (((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))) โ†” ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))))
8281imbi2d 341 . . . 4 (๐‘š = ๐‘€ โ†’ ((๐œ‘ โ†’ ((๐‘š gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))) โ†” (๐œ‘ โ†’ ((๐‘€ gcd (2 ยท ๐‘)) = 1 โ†’ ((๐‘€ /L ๐‘) ยท (๐‘ /L ๐‘€)) = (-1โ†‘(((๐‘€ โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2)))))))
83 1t1e1 12316 . . . . . . 7 (1 ยท 1) = 1
84 neg1cn 12268 . . . . . . . 8 -1 โˆˆ โ„‚
85 exp0 13972 . . . . . . . 8 (-1 โˆˆ โ„‚ โ†’ (-1โ†‘0) = 1)
8684, 85ax-mp 5 . . . . . . 7 (-1โ†‘0) = 1
8783, 86eqtr4i 2768 . . . . . 6 (1 ยท 1) = (-1โ†‘0)
88 sq1 14100 . . . . . . . . 9 (1โ†‘2) = 1
8988oveq1i 7368 . . . . . . . 8 ((1โ†‘2) /L ๐‘) = (1 /L ๐‘)
90 1z 12534 . . . . . . . . . 10 1 โˆˆ โ„ค
91 ax-1ne0 11121 . . . . . . . . . 10 1 โ‰  0
9290, 91pm3.2i 472 . . . . . . . . 9 (1 โˆˆ โ„ค โˆง 1 โ‰  0)
934nnzd 12527 . . . . . . . . 9 (๐œ‘ โ†’ ๐‘ โˆˆ โ„ค)
94 1gcd 16415 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ (1 gcd ๐‘) = 1)
9593, 94syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (1 gcd ๐‘) = 1)
96 lgssq 26688 . . . . . . . . 9 (((1 โˆˆ โ„ค โˆง 1 โ‰  0) โˆง ๐‘ โˆˆ โ„ค โˆง (1 gcd ๐‘) = 1) โ†’ ((1โ†‘2) /L ๐‘) = 1)
9792, 93, 95, 96mp3an2i 1467 . . . . . . . 8 (๐œ‘ โ†’ ((1โ†‘2) /L ๐‘) = 1)
9889, 97eqtr3id 2791 . . . . . . 7 (๐œ‘ โ†’ (1 /L ๐‘) = 1)
9988oveq2i 7369 . . . . . . . 8 (๐‘ /L (1โ†‘2)) = (๐‘ /L 1)
100 1nn 12165 . . . . . . . . . 10 1 โˆˆ โ„•
101100a1i 11 . . . . . . . . 9 (๐œ‘ โ†’ 1 โˆˆ โ„•)
102 gcd1 16409 . . . . . . . . . 10 (๐‘ โˆˆ โ„ค โ†’ (๐‘ gcd 1) = 1)
10393, 102syl 17 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ gcd 1) = 1)
104 lgssq2 26689 . . . . . . . . 9 ((๐‘ โˆˆ โ„ค โˆง 1 โˆˆ โ„• โˆง (๐‘ gcd 1) = 1) โ†’ (๐‘ /L (1โ†‘2)) = 1)
10593, 101, 103, 104syl3anc 1372 . . . . . . . 8 (๐œ‘ โ†’ (๐‘ /L (1โ†‘2)) = 1)
10699, 105eqtr3id 2791 . . . . . . 7 (๐œ‘ โ†’ (๐‘ /L 1) = 1)
10798, 106oveq12d 7376 . . . . . 6 (๐œ‘ โ†’ ((1 /L ๐‘) ยท (๐‘ /L 1)) = (1 ยท 1))
108 nnm1nn0 12455 . . . . . . . . . . 11 (๐‘ โˆˆ โ„• โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
1094, 108syl 17 . . . . . . . . . 10 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„•0)
110109nn0cnd 12476 . . . . . . . . 9 (๐œ‘ โ†’ (๐‘ โˆ’ 1) โˆˆ โ„‚)
111110halfcld 12399 . . . . . . . 8 (๐œ‘ โ†’ ((๐‘ โˆ’ 1) / 2) โˆˆ โ„‚)
112111mul02d 11354 . . . . . . 7 (๐œ‘ โ†’ (0 ยท ((๐‘ โˆ’ 1) / 2)) = 0)
113112oveq2d 7374 . . . . . 6 (๐œ‘ โ†’ (-1โ†‘(0 ยท ((๐‘ โˆ’ 1) / 2))) = (-1โ†‘0))
11487, 107, 1133eqtr4a 2803 . . . . 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 770 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„™)
117 prmz 16552 . . . . . . . . . . . 12 (๐‘š โˆˆ โ„™ โ†’ ๐‘š โˆˆ โ„ค)
118117ad2antrl 727 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„ค)
1196a1i 11 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆˆ โ„ค)
1204adantr 482 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘ โˆˆ โ„•)
121120nnzd 12527 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘ โˆˆ โ„ค)
122 zmulcl 12553 . . . . . . . . . . . 12 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
1236, 121, 122sylancr 588 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
124 simprr 772 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd (2 ยท ๐‘)) = 1)
125 dvdsmul1 16161 . . . . . . . . . . . 12 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ 2 โˆฅ (2 ยท ๐‘))
1266, 121, 125sylancr 588 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆฅ (2 ยท ๐‘))
127 rpdvds 16537 . . . . . . . . . . 11 (((๐‘š โˆˆ โ„ค โˆง 2 โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โˆง ((๐‘š gcd (2 ยท ๐‘)) = 1 โˆง 2 โˆฅ (2 ยท ๐‘))) โ†’ (๐‘š gcd 2) = 1)
128118, 119, 123, 124, 126, 127syl32anc 1379 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd 2) = 1)
129 prmrp 16589 . . . . . . . . . . 11 ((๐‘š โˆˆ โ„™ โˆง 2 โˆˆ โ„™) โ†’ ((๐‘š gcd 2) = 1 โ†” ๐‘š โ‰  2))
130116, 10, 129sylancl 587 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ((๐‘š gcd 2) = 1 โ†” ๐‘š โ‰  2))
131128, 130mpbid 231 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โ‰  2)
132 eldifsn 4748 . . . . . . . . 9 (๐‘š โˆˆ (โ„™ โˆ– {2}) โ†” (๐‘š โˆˆ โ„™ โˆง ๐‘š โ‰  2))
133116, 131, 132sylanbrc 584 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ (โ„™ โˆ– {2}))
134 prmnn 16551 . . . . . . . . . . 11 (๐‘š โˆˆ โ„™ โ†’ ๐‘š โˆˆ โ„•)
135134ad2antrl 727 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ๐‘š โˆˆ โ„•)
1362a1i 11 . . . . . . . . . 10 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ 2 โˆˆ โ„•)
137 rpmulgcd 16438 . . . . . . . . . 10 (((๐‘š โˆˆ โ„• โˆง 2 โˆˆ โ„• โˆง ๐‘ โˆˆ โ„•) โˆง (๐‘š gcd 2) = 1) โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘š gcd ๐‘))
138135, 136, 120, 128, 137syl31anc 1374 . . . . . . . . 9 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd (2 ยท ๐‘)) = (๐‘š gcd ๐‘))
139138, 124eqtr3d 2779 . . . . . . . 8 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š gcd ๐‘) = 1)
140133, 139jca 513 . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ (๐‘š โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘š gcd ๐‘) = 1))
141 lgsquad2lem2.f . . . . . . 7 ((๐œ‘ โˆง (๐‘š โˆˆ (โ„™ โˆ– {2}) โˆง (๐‘š gcd ๐‘) = 1)) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
142140, 141syldan 592 . . . . . 6 ((๐œ‘ โˆง (๐‘š โˆˆ โ„™ โˆง (๐‘š gcd (2 ยท ๐‘)) = 1)) โ†’ ((๐‘š /L ๐‘) ยท (๐‘ /L ๐‘š)) = (-1โ†‘(((๐‘š โˆ’ 1) / 2) ยท ((๐‘ โˆ’ 1) / 2))))
143142exp32 422 . . . . 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 519 . . . . 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 776 . . . . . . . . . . . 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 12810 . . . . . . . . . . . 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 777 . . . . . . . . . . . 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 12810 . . . . . . . . . . . 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 12207 . . . . . . . . . 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 16251 . . . . . . . . . . . 12 ยฌ 2 โˆฅ 1
15493ad2antrr 725 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ โˆˆ โ„ค)
1556, 154, 125sylancr 588 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ 2 โˆฅ (2 ยท ๐‘))
156 eluzelz 12774 . . . . . . . . . . . . . . . . . 18 (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฅ โˆˆ โ„ค)
157 eluzelz 12774 . . . . . . . . . . . . . . . . . 18 (๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2) โ†’ ๐‘ฆ โˆˆ โ„ค)
158156, 157anim12i 614 . . . . . . . . . . . . . . . . 17 ((๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2)) โ†’ (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค))
159158ad2antlr 726 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค))
160 zmulcl 12553 . . . . . . . . . . . . . . . 16 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค)
161159, 160syl 17 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค)
1626, 154, 122sylancr 588 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 ยท ๐‘) โˆˆ โ„ค)
163 dvdsgcd 16426 . . . . . . . . . . . . . . 15 ((2 โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โ†’ ((2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โˆง 2 โˆฅ (2 ยท ๐‘)) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
1646, 161, 162, 163mp3an2i 1467 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โˆง 2 โˆฅ (2 ยท ๐‘)) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
165155, 164mpan2d 693 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (2 โˆฅ (๐‘ฅ ยท ๐‘ฆ) โ†’ 2 โˆฅ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘))))
166 simpr 486 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1)
167166breq2d 5118 . . . . . . . . . . . . 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 716 . . . . . . . . . 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 725 . . . . . . . . . 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 725 . . . . . . . . . 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 16162 . . . . . . . . . . . . 13 ((2 โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค) โ†’ ๐‘ โˆฅ (2 ยท ๐‘))
1756, 154, 174sylancr 588 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ โˆฅ (2 ยท ๐‘))
176 rpdvds 16537 . . . . . . . . . . . 12 ((((๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง (2 ยท ๐‘) โˆˆ โ„ค) โˆง (((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1 โˆง ๐‘ โˆฅ (2 ยท ๐‘))) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd ๐‘) = 1)
177161, 154, 162, 166, 175, 176syl32anc 1379 . . . . . . . . . . 11 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((๐‘ฅ ยท ๐‘ฆ) gcd ๐‘) = 1)
178177adantrr 716 . . . . . . . . . 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 2738 . . . . . . . . . 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 496 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฅ โˆˆ โ„ค)
181180, 162gcdcomd 16395 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ gcd (2 ยท ๐‘)) = ((2 ยท ๐‘) gcd ๐‘ฅ))
182162, 161gcdcomd 16395 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)))
183182, 166eqtrd 2777 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1)
184 dvdsmul1 16161 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
185159, 184syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
186 rpdvds 16537 . . . . . . . . . . . . . 14 ((((2 ยท ๐‘) โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค) โˆง (((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1 โˆง ๐‘ฅ โˆฅ (๐‘ฅ ยท ๐‘ฆ))) โ†’ ((2 ยท ๐‘) gcd ๐‘ฅ) = 1)
187162, 180, 161, 183, 185, 186syl32anc 1379 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd ๐‘ฅ) = 1)
188181, 187eqtrd 2777 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฅ gcd (2 ยท ๐‘)) = 1)
189188adantrr 716 . . . . . . . . . . 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 780 . . . . . . . . . . 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 497 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฆ โˆˆ โ„ค)
193192, 162gcdcomd 16395 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฆ gcd (2 ยท ๐‘)) = ((2 ยท ๐‘) gcd ๐‘ฆ))
194 dvdsmul2 16162 . . . . . . . . . . . . . . 15 ((๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค) โ†’ ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
195159, 194syl 17 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))
196 rpdvds 16537 . . . . . . . . . . . . . 14 ((((2 ยท ๐‘) โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค โˆง (๐‘ฅ ยท ๐‘ฆ) โˆˆ โ„ค) โˆง (((2 ยท ๐‘) gcd (๐‘ฅ ยท ๐‘ฆ)) = 1 โˆง ๐‘ฆ โˆฅ (๐‘ฅ ยท ๐‘ฆ))) โ†’ ((2 ยท ๐‘) gcd ๐‘ฆ) = 1)
197162, 192, 161, 183, 195, 196syl32anc 1379 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ ((2 ยท ๐‘) gcd ๐‘ฆ) = 1)
198193, 197eqtrd 2777 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐‘ฅ โˆˆ (โ„คโ‰ฅโ€˜2) โˆง ๐‘ฆ โˆˆ (โ„คโ‰ฅโ€˜2))) โˆง ((๐‘ฅ ยท ๐‘ฆ) gcd (2 ยท ๐‘)) = 1) โ†’ (๐‘ฆ gcd (2 ยท ๐‘)) = 1)
199198adantrr 716 . . . . . . . . . . 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 781 . . . . . . . . . . 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 26735 . . . . . . . . 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 422 . . . . . . . 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 415 . . . . . 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 16563 . . 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 397   = wceq 1542   โˆˆ wcel 2107   โ‰  wne 2944  โˆ€wral 3065   โˆ– cdif 3908  {csn 4587   class class class wbr 5106  โ€˜cfv 6497  (class class class)co 7358  โ„‚cc 11050  0cc0 11052  1c1 11053   ยท cmul 11057   โˆ’ cmin 11386  -cneg 11387   / cdiv 11813  โ„•cn 12154  2c2 12209  โ„•0cn0 12414  โ„คcz 12500  โ„คโ‰ฅcuz 12764  ...cfz 13425  โ†‘cexp 13968   โˆฅ cdvds 16137   gcd cgcd 16375  โ„™cprime 16548   /L clgs 26645
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-cnex 11108  ax-resscn 11109  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-addrcl 11113  ax-mulcl 11114  ax-mulrcl 11115  ax-mulcom 11116  ax-addass 11117  ax-mulass 11118  ax-distr 11119  ax-i2m1 11120  ax-1ne0 11121  ax-1rid 11122  ax-rnegex 11123  ax-rrecex 11124  ax-cnre 11125  ax-pre-lttri 11126  ax-pre-lttrn 11127  ax-pre-ltadd 11128  ax-pre-mulgt0 11129  ax-pre-sup 11130
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-1o 8413  df-2o 8414  df-oadd 8417  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-fin 8888  df-sup 9379  df-inf 9380  df-dju 9838  df-card 9876  df-pnf 11192  df-mnf 11193  df-xr 11194  df-ltxr 11195  df-le 11196  df-sub 11388  df-neg 11389  df-div 11814  df-nn 12155  df-2 12217  df-3 12218  df-4 12219  df-5 12220  df-6 12221  df-7 12222  df-8 12223  df-9 12224  df-n0 12415  df-xnn0 12487  df-z 12501  df-uz 12765  df-q 12875  df-rp 12917  df-fz 13426  df-fzo 13569  df-fl 13698  df-mod 13776  df-seq 13908  df-exp 13969  df-hash 14232  df-cj 14985  df-re 14986  df-im 14987  df-sqrt 15121  df-abs 15122  df-dvds 16138  df-gcd 16376  df-prm 16549  df-phi 16639  df-pc 16710  df-lgs 26646
This theorem is referenced by:  lgsquad2  26737
  Copyright terms: Public domain W3C validator