Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pellexlem6 Structured version   Visualization version   GIF version

Theorem pellexlem6 41874
Description: Lemma for pellex 41875. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
Hypotheses
Ref Expression
pellex.ann (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
pellex.bnn (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
pellex.cz (๐œ‘ โ†’ ๐ถ โˆˆ โ„ค)
pellex.dnn (๐œ‘ โ†’ ๐ท โˆˆ โ„•)
pellex.irr (๐œ‘ โ†’ ยฌ (โˆšโ€˜๐ท) โˆˆ โ„š)
pellex.enn (๐œ‘ โ†’ ๐ธ โˆˆ โ„•)
pellex.fnn (๐œ‘ โ†’ ๐น โˆˆ โ„•)
pellex.neq (๐œ‘ โ†’ ยฌ (๐ด = ๐ธ โˆง ๐ต = ๐น))
pellex.cn0 (๐œ‘ โ†’ ๐ถ โ‰  0)
pellex.no1 (๐œ‘ โ†’ ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) = ๐ถ)
pellex.no2 (๐œ‘ โ†’ ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) = ๐ถ)
pellex.xcg (๐œ‘ โ†’ (๐ด mod (absโ€˜๐ถ)) = (๐ธ mod (absโ€˜๐ถ)))
pellex.ycg (๐œ‘ โ†’ (๐ต mod (absโ€˜๐ถ)) = (๐น mod (absโ€˜๐ถ)))
Assertion
Ref Expression
pellexlem6 (๐œ‘ โ†’ โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘ โˆˆ โ„• ((๐‘Žโ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1)
Distinct variable groups:   ๐‘Ž,๐‘,๐ด   ๐ต,๐‘Ž,๐‘   ๐ถ,๐‘Ž,๐‘   ๐ท,๐‘Ž,๐‘   ๐ธ,๐‘Ž,๐‘   ๐น,๐‘Ž,๐‘   ๐œ‘,๐‘Ž,๐‘

Proof of Theorem pellexlem6
StepHypRef Expression
1 pellex.ann . . . . . . . . 9 (๐œ‘ โ†’ ๐ด โˆˆ โ„•)
21nncnd 12232 . . . . . . . 8 (๐œ‘ โ†’ ๐ด โˆˆ โ„‚)
3 pellex.enn . . . . . . . . 9 (๐œ‘ โ†’ ๐ธ โˆˆ โ„•)
43nncnd 12232 . . . . . . . 8 (๐œ‘ โ†’ ๐ธ โˆˆ โ„‚)
52, 4mulcld 11238 . . . . . . 7 (๐œ‘ โ†’ (๐ด ยท ๐ธ) โˆˆ โ„‚)
6 pellex.dnn . . . . . . . . 9 (๐œ‘ โ†’ ๐ท โˆˆ โ„•)
76nncnd 12232 . . . . . . . 8 (๐œ‘ โ†’ ๐ท โˆˆ โ„‚)
8 pellex.bnn . . . . . . . . . 10 (๐œ‘ โ†’ ๐ต โˆˆ โ„•)
98nncnd 12232 . . . . . . . . 9 (๐œ‘ โ†’ ๐ต โˆˆ โ„‚)
10 pellex.fnn . . . . . . . . . 10 (๐œ‘ โ†’ ๐น โˆˆ โ„•)
1110nncnd 12232 . . . . . . . . 9 (๐œ‘ โ†’ ๐น โˆˆ โ„‚)
129, 11mulcld 11238 . . . . . . . 8 (๐œ‘ โ†’ (๐ต ยท ๐น) โˆˆ โ„‚)
137, 12mulcld 11238 . . . . . . 7 (๐œ‘ โ†’ (๐ท ยท (๐ต ยท ๐น)) โˆˆ โ„‚)
145, 13subcld 11575 . . . . . 6 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) โˆˆ โ„‚)
15 pellex.cz . . . . . . 7 (๐œ‘ โ†’ ๐ถ โˆˆ โ„ค)
1615zcnd 12671 . . . . . 6 (๐œ‘ โ†’ ๐ถ โˆˆ โ„‚)
17 pellex.cn0 . . . . . 6 (๐œ‘ โ†’ ๐ถ โ‰  0)
1814, 16, 17absdivd 15406 . . . . 5 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) = ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (absโ€˜๐ถ)))
195, 13negsubd 11581 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) + -(๐ท ยท (๐ต ยท ๐น))) = ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))))
2019eqcomd 2736 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = ((๐ด ยท ๐ธ) + -(๐ท ยท (๐ต ยท ๐น))))
2120oveq1d 7426 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = (((๐ด ยท ๐ธ) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)))
221nnred 12231 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ด โˆˆ โ„)
233nnred 12231 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ธ โˆˆ โ„)
2422, 23remulcld 11248 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ด ยท ๐ธ) โˆˆ โ„)
256nnred 12231 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ท โˆˆ โ„)
268nnred 12231 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ต โˆˆ โ„)
2710nnred 12231 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐น โˆˆ โ„)
2826, 27remulcld 11248 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ต ยท ๐น) โˆˆ โ„)
2925, 28remulcld 11248 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ท ยท (๐ต ยท ๐น)) โˆˆ โ„)
3029renegcld 11645 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐ท ยท (๐ต ยท ๐น)) โˆˆ โ„)
3116, 17absrpcld 15399 . . . . . . . . . 10 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„+)
323nnzd 12589 . . . . . . . . . . . 12 (๐œ‘ โ†’ ๐ธ โˆˆ โ„ค)
33 pellex.xcg . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ด mod (absโ€˜๐ถ)) = (๐ธ mod (absโ€˜๐ถ)))
34 modmul1 13893 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ธ โˆˆ โ„) โˆง (๐ธ โˆˆ โ„ค โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง (๐ด mod (absโ€˜๐ถ)) = (๐ธ mod (absโ€˜๐ถ))) โ†’ ((๐ด ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ธ ยท ๐ธ) mod (absโ€˜๐ถ)))
3522, 23, 32, 31, 33, 34syl221anc 1379 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ธ ยท ๐ธ) mod (absโ€˜๐ถ)))
364sqcld 14113 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ธโ†‘2) โˆˆ โ„‚)
3711sqcld 14113 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐นโ†‘2) โˆˆ โ„‚)
387, 37mulcld 11238 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ท ยท (๐นโ†‘2)) โˆˆ โ„‚)
3936, 38npcand 11579 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) + (๐ท ยท (๐นโ†‘2))) = (๐ธโ†‘2))
404sqvald 14112 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ธโ†‘2) = (๐ธ ยท ๐ธ))
4139, 40eqtr2d 2771 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ธ ยท ๐ธ) = (((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) + (๐ท ยท (๐นโ†‘2))))
4241oveq1d 7426 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ธ ยท ๐ธ) mod (absโ€˜๐ถ)) = ((((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)))
4323resqcld 14094 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ธโ†‘2) โˆˆ โ„)
4427resqcld 14094 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐นโ†‘2) โˆˆ โ„)
4525, 44remulcld 11248 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท (๐นโ†‘2)) โˆˆ โ„)
4643, 45resubcld 11646 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) โˆˆ โ„)
47 0red 11221 . . . . . . . . . . . . 13 (๐œ‘ โ†’ 0 โˆˆ โ„)
4816abscld 15387 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„)
4948recnd 11246 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (absโ€˜๐ถ) โˆˆ โ„‚)
5016, 17absne0d 15398 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (absโ€˜๐ถ) โ‰  0)
5149, 50dividd 11992 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((absโ€˜๐ถ) / (absโ€˜๐ถ)) = 1)
52 1zzd 12597 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 1 โˆˆ โ„ค)
5351, 52eqeltrd 2831 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((absโ€˜๐ถ) / (absโ€˜๐ถ)) โˆˆ โ„ค)
54 mod0 13845 . . . . . . . . . . . . . . . . 17 (((absโ€˜๐ถ) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ (((absโ€˜๐ถ) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜๐ถ) / (absโ€˜๐ถ)) โˆˆ โ„ค))
5548, 31, 54syl2anc 582 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((absโ€˜๐ถ) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜๐ถ) / (absโ€˜๐ถ)) โˆˆ โ„ค))
5653, 55mpbird 256 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((absโ€˜๐ถ) mod (absโ€˜๐ถ)) = 0)
5715zred 12670 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ๐ถ โˆˆ โ„)
58 absmod0 15254 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ ((๐ถ mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜๐ถ) mod (absโ€˜๐ถ)) = 0))
5957, 31, 58syl2anc 582 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜๐ถ) mod (absโ€˜๐ถ)) = 0))
6056, 59mpbird 256 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ถ mod (absโ€˜๐ถ)) = 0)
61 pellex.no2 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) = ๐ถ)
6261oveq1d 7426 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = (๐ถ mod (absโ€˜๐ถ)))
63 0mod 13871 . . . . . . . . . . . . . . 15 ((absโ€˜๐ถ) โˆˆ โ„+ โ†’ (0 mod (absโ€˜๐ถ)) = 0)
6431, 63syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (0 mod (absโ€˜๐ถ)) = 0)
6560, 62, 643eqtr4d 2780 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ)))
66 modadd1 13877 . . . . . . . . . . . . 13 (((((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) โˆˆ โ„ โˆง 0 โˆˆ โ„) โˆง ((๐ท ยท (๐นโ†‘2)) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง (((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ))) โ†’ ((((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = ((0 + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)))
6746, 47, 45, 31, 65, 66syl221anc 1379 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = ((0 + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)))
6838addlidd 11419 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (0 + (๐ท ยท (๐นโ†‘2))) = (๐ท ยท (๐นโ†‘2)))
6911sqvald 14112 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐นโ†‘2) = (๐น ยท ๐น))
7069oveq2d 7427 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท (๐นโ†‘2)) = (๐ท ยท (๐น ยท ๐น)))
717, 11, 11mul12d 11427 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท (๐น ยท ๐น)) = (๐น ยท (๐ท ยท ๐น)))
7268, 70, 713eqtrd 2774 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (0 + (๐ท ยท (๐นโ†‘2))) = (๐น ยท (๐ท ยท ๐น)))
7372oveq1d 7426 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((0 + (๐ท ยท (๐นโ†‘2))) mod (absโ€˜๐ถ)) = ((๐น ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)))
7442, 67, 733eqtrd 2774 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ธ ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐น ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)))
756nnzd 12589 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐ท โˆˆ โ„ค)
7610nnzd 12589 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐น โˆˆ โ„ค)
7775, 76zmulcld 12676 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ท ยท ๐น) โˆˆ โ„ค)
78 pellex.ycg . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต mod (absโ€˜๐ถ)) = (๐น mod (absโ€˜๐ถ)))
7978eqcomd 2736 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐น mod (absโ€˜๐ถ)) = (๐ต mod (absโ€˜๐ถ)))
80 modmul1 13893 . . . . . . . . . . . . 13 (((๐น โˆˆ โ„ โˆง ๐ต โˆˆ โ„) โˆง ((๐ท ยท ๐น) โˆˆ โ„ค โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง (๐น mod (absโ€˜๐ถ)) = (๐ต mod (absโ€˜๐ถ))) โ†’ ((๐น ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)) = ((๐ต ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)))
8127, 26, 77, 31, 79, 80syl221anc 1379 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐น ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)) = ((๐ต ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)))
829, 7, 11mul12d 11427 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ต ยท (๐ท ยท ๐น)) = (๐ท ยท (๐ต ยท ๐น)))
8382oveq1d 7426 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((๐ต ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)) = ((๐ท ยท (๐ต ยท ๐น)) mod (absโ€˜๐ถ)))
8481, 83eqtrd 2770 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐น ยท (๐ท ยท ๐น)) mod (absโ€˜๐ถ)) = ((๐ท ยท (๐ต ยท ๐น)) mod (absโ€˜๐ถ)))
8535, 74, 843eqtrd 2774 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ท ยท (๐ต ยท ๐น)) mod (absโ€˜๐ถ)))
86 modadd1 13877 . . . . . . . . . 10 ((((๐ด ยท ๐ธ) โˆˆ โ„ โˆง (๐ท ยท (๐ต ยท ๐น)) โˆˆ โ„) โˆง (-(๐ท ยท (๐ต ยท ๐น)) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง ((๐ด ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ท ยท (๐ต ยท ๐น)) mod (absโ€˜๐ถ))) โ†’ (((๐ด ยท ๐ธ) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = (((๐ท ยท (๐ต ยท ๐น)) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)))
8724, 29, 30, 31, 85, 86syl221anc 1379 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = (((๐ท ยท (๐ต ยท ๐น)) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)))
8813negidd 11565 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น)) + -(๐ท ยท (๐ต ยท ๐น))) = 0)
8988oveq1d 7426 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ท ยท (๐ต ยท ๐น)) + -(๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ)))
9021, 87, 893eqtrd 2774 . . . . . . . 8 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ)))
9190, 64eqtrd 2770 . . . . . . 7 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = 0)
9224, 29resubcld 11646 . . . . . . . 8 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) โˆˆ โ„)
93 absmod0 15254 . . . . . . . 8 ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) mod (absโ€˜๐ถ)) = 0))
9492, 31, 93syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) mod (absโ€˜๐ถ)) = 0))
9591, 94mpbid 231 . . . . . 6 (๐œ‘ โ†’ ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) mod (absโ€˜๐ถ)) = 0)
9614abscld 15387 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆˆ โ„)
97 mod0 13845 . . . . . . 7 (((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ (((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (absโ€˜๐ถ)) โˆˆ โ„ค))
9896, 31, 97syl2anc 582 . . . . . 6 (๐œ‘ โ†’ (((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (absโ€˜๐ถ)) โˆˆ โ„ค))
9995, 98mpbid 231 . . . . 5 (๐œ‘ โ†’ ((absโ€˜((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (absโ€˜๐ถ)) โˆˆ โ„ค)
10018, 99eqeltrd 2831 . . . 4 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„ค)
10192, 57, 17redivcld 12046 . . . . 5 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„)
102 absz 15262 . . . . 5 ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ค โ†” (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„ค))
103101, 102syl 17 . . . 4 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ค โ†” (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„ค))
104100, 103mpbird 256 . . 3 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ค)
105 0lt1 11740 . . . . . . . 8 0 < 1
106 0re 11220 . . . . . . . . 9 0 โˆˆ โ„
107 1re 11218 . . . . . . . . 9 1 โˆˆ โ„
108106, 107ltnlei 11339 . . . . . . . 8 (0 < 1 โ†” ยฌ 1 โ‰ค 0)
109105, 108mpbi 229 . . . . . . 7 ยฌ 1 โ‰ค 0
1109, 4mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต ยท ๐ธ) โˆˆ โ„‚)
1112, 11mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ด ยท ๐น) โˆˆ โ„‚)
112110, 111subcld 11575 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) โˆˆ โ„‚)
113112, 16, 17divcld 11994 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„‚)
114113abscld 15387 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„)
115114resqcld 14094 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2) โˆˆ โ„)
1166nnnn0d 12536 . . . . . . . . . . 11 (๐œ‘ โ†’ ๐ท โˆˆ โ„•0)
117116nn0ge0d 12539 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค ๐ท)
118114sqge0d 14106 . . . . . . . . . 10 (๐œ‘ โ†’ 0 โ‰ค ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))
11925, 115, 117, 118mulge0d 11795 . . . . . . . . 9 (๐œ‘ โ†’ 0 โ‰ค (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2)))
12025, 115remulcld 11248 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2)) โˆˆ โ„)
12147, 120suble0d 11809 . . . . . . . . 9 (๐œ‘ โ†’ ((0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) โ‰ค 0 โ†” 0 โ‰ค (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))))
122119, 121mpbird 256 . . . . . . . 8 (๐œ‘ โ†’ (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) โ‰ค 0)
123 breq1 5150 . . . . . . . 8 (1 = (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) โ†’ (1 โ‰ค 0 โ†” (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) โ‰ค 0))
124122, 123syl5ibrcom 246 . . . . . . 7 (๐œ‘ โ†’ (1 = (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) โ†’ 1 โ‰ค 0))
125109, 124mtoi 198 . . . . . 6 (๐œ‘ โ†’ ยฌ 1 = (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))))
126 absresq 15253 . . . . . . . . . . . 12 ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ โ†’ ((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) = ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)โ†‘2))
127101, 126syl 17 . . . . . . . . . . 11 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) = ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)โ†‘2))
12814, 16, 17sqdivd 14128 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)โ†‘2) = ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))โ†‘2) / (๐ถโ†‘2)))
12914sqvald 14112 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))โ†‘2) = (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))))
130129oveq1d 7426 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))โ†‘2) / (๐ถโ†‘2)) = ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (๐ถโ†‘2)))
131127, 128, 1303eqtrd 2774 . . . . . . . . . 10 (๐œ‘ โ†’ ((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) = ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (๐ถโ†‘2)))
13226, 23remulcld 11248 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ต ยท ๐ธ) โˆˆ โ„)
13322, 27remulcld 11248 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ด ยท ๐น) โˆˆ โ„)
134132, 133resubcld 11646 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) โˆˆ โ„)
135134, 57, 17redivcld 12046 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„)
136 absresq 15253 . . . . . . . . . . . . . 14 ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ โ†’ ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2) = ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)โ†‘2))
137135, 136syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2) = ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)โ†‘2))
138112, 16, 17sqdivd 14128 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)โ†‘2) = ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) / (๐ถโ†‘2)))
139137, 138eqtrd 2770 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2) = ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) / (๐ถโ†‘2)))
140139oveq2d 7427 . . . . . . . . . . 11 (๐œ‘ โ†’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2)) = (๐ท ยท ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) / (๐ถโ†‘2))))
141112sqcld 14113 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) โˆˆ โ„‚)
14216sqcld 14113 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ถโ†‘2) โˆˆ โ„‚)
143 sqne0 14092 . . . . . . . . . . . . . 14 (๐ถ โˆˆ โ„‚ โ†’ ((๐ถโ†‘2) โ‰  0 โ†” ๐ถ โ‰  0))
14416, 143syl 17 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ถโ†‘2) โ‰  0 โ†” ๐ถ โ‰  0))
14517, 144mpbird 256 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ถโ†‘2) โ‰  0)
1467, 141, 142, 145divassd 12029 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2)) / (๐ถโ†‘2)) = (๐ท ยท ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) / (๐ถโ†‘2))))
147112sqvald 14112 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2) = (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))))
148147oveq2d 7427 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2)) = (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))))
149148oveq1d 7426 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))โ†‘2)) / (๐ถโ†‘2)) = ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) / (๐ถโ†‘2)))
150140, 146, 1493eqtr2d 2776 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2)) = ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) / (๐ถโ†‘2)))
151131, 150oveq12d 7429 . . . . . . . . 9 (๐œ‘ โ†’ (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (๐ถโ†‘2)) โˆ’ ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) / (๐ถโ†‘2))))
15214, 14mulcld 11238 . . . . . . . . . 10 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆˆ โ„‚)
153112, 112mulcld 11238 . . . . . . . . . . 11 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) โˆˆ โ„‚)
1547, 153mulcld 11238 . . . . . . . . . 10 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) โˆˆ โ„‚)
155152, 154, 142, 145divsubdird 12033 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))))) / (๐ถโ†‘2)) = (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) / (๐ถโ†‘2)) โˆ’ ((๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) / (๐ถโ†‘2))))
1565, 13, 5, 13mulsubd 11677 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) = ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))))
157110, 111, 110, 111mulsubd 11677 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) = ((((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))) โˆ’ (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))
158157oveq2d 7427 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) = (๐ท ยท ((((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))) โˆ’ (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))))
159110, 110mulcld 11238 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) โˆˆ โ„‚)
160111, 111mulcld 11238 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)) โˆˆ โ„‚)
161159, 160addcld 11237 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))) โˆˆ โ„‚)
162110, 111mulcld 11238 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) โˆˆ โ„‚)
163162, 162addcld 11237 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) โˆˆ โ„‚)
1647, 161, 163subdid 11674 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ท ยท ((((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))) โˆ’ (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))) = ((๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))))
1657, 159, 160adddid 11242 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) = ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))))
1667, 162, 162adddid 11242 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))) = ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))
167165, 166oveq12d 7429 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)) + ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)) + ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))) = (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))))
168158, 164, 1673eqtrd 2774 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))) = (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))))
169156, 168oveq12d 7429 . . . . . . . . . . 11 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))))) = (((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))))
170169oveq1d 7426 . . . . . . . . . 10 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))))) / (๐ถโ†‘2)) = ((((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))) / (๐ถโ†‘2)))
1715, 13mulcomd 11239 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) = ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ด ยท ๐ธ)))
1727, 12, 5mulassd 11241 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ด ยท ๐ธ)) = (๐ท ยท ((๐ต ยท ๐น) ยท (๐ด ยท ๐ธ))))
1732, 4mulcomd 11239 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐ด ยท ๐ธ) = (๐ธ ยท ๐ด))
174173oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ต ยท ๐น) ยท (๐ด ยท ๐ธ)) = ((๐ต ยท ๐น) ยท (๐ธ ยท ๐ด)))
1759, 11, 4, 2mul4d 11430 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ต ยท ๐น) ยท (๐ธ ยท ๐ด)) = ((๐ต ยท ๐ธ) ยท (๐น ยท ๐ด)))
17611, 2mulcomd 11239 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ (๐น ยท ๐ด) = (๐ด ยท ๐น))
177176oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) ยท (๐น ยท ๐ด)) = ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))
178174, 175, 1773eqtrd 2774 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ต ยท ๐น) ยท (๐ด ยท ๐ธ)) = ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))
179178oveq2d 7427 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐น) ยท (๐ด ยท ๐ธ))) = (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))
180171, 172, 1793eqtrd 2774 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) = (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))
181180, 180oveq12d 7429 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น)))) = ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))
182181oveq2d 7427 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) = ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))))
183182oveq1d 7426 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))) = (((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))))
1845, 5mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) โˆˆ โ„‚)
18513, 13mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น))) โˆˆ โ„‚)
186184, 185addcld 11237 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆˆ โ„‚)
1877, 159mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) โˆˆ โ„‚)
1887, 160mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))) โˆˆ โ„‚)
189187, 188addcld 11237 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆˆ โ„‚)
1907, 162mulcld 11238 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) โˆˆ โ„‚)
191190, 190addcld 11237 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))) โˆˆ โ„‚)
192186, 189, 191nnncan2d 11610 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))) = ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))))
193184, 185, 187, 188addsub4d 11622 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))) = ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)))) + (((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น))) โˆ’ (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))))
1945sqvald 14112 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ด ยท ๐ธ)โ†‘2) = ((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)))
195110sqvald 14112 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ต ยท ๐ธ)โ†‘2) = ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)))
196195oveq2d 7427 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2)) = (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))))
197194, 196oveq12d 7429 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ด ยท ๐ธ)โ†‘2) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2))) = (((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)))))
19813sqvald 14112 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น))โ†‘2) = ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น))))
199111sqvald 14112 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ด ยท ๐น)โ†‘2) = ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))
200199oveq2d 7427 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)) = (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))
201198, 200oveq12d 7429 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (((๐ท ยท (๐ต ยท ๐น))โ†‘2) โˆ’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2))) = (((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น))) โˆ’ (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))))
202197, 201oveq12d 7429 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ)โ†‘2) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2))) + (((๐ท ยท (๐ต ยท ๐น))โ†‘2) โˆ’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)))) = ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ)))) + (((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น))) โˆ’ (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))))
2032, 4sqmuld 14127 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ด ยท ๐ธ)โ†‘2) = ((๐ดโ†‘2) ยท (๐ธโ†‘2)))
2049, 4sqmuld 14127 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ต ยท ๐ธ)โ†‘2) = ((๐ตโ†‘2) ยท (๐ธโ†‘2)))
205204oveq2d 7427 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2)) = (๐ท ยท ((๐ตโ†‘2) ยท (๐ธโ†‘2))))
2069sqcld 14113 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
2077, 206, 36mulassd 11241 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2)) = (๐ท ยท ((๐ตโ†‘2) ยท (๐ธโ†‘2))))
208205, 207eqtr4d 2773 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2)) = ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2)))
209203, 208oveq12d 7429 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ด ยท ๐ธ)โ†‘2) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2))) = (((๐ดโ†‘2) ยท (๐ธโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2))))
2107sqvald 14112 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ทโ†‘2) = (๐ท ยท ๐ท))
2119, 11sqmuld 14127 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ต ยท ๐น)โ†‘2) = ((๐ตโ†‘2) ยท (๐นโ†‘2)))
212210, 211oveq12d 7429 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ทโ†‘2) ยท ((๐ต ยท ๐น)โ†‘2)) = ((๐ท ยท ๐ท) ยท ((๐ตโ†‘2) ยท (๐นโ†‘2))))
2137, 12sqmuld 14127 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น))โ†‘2) = ((๐ทโ†‘2) ยท ((๐ต ยท ๐น)โ†‘2)))
2147, 7mulcld 11238 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ท ยท ๐ท) โˆˆ โ„‚)
215214, 206, 37mulassd 11241 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) = ((๐ท ยท ๐ท) ยท ((๐ตโ†‘2) ยท (๐นโ†‘2))))
216212, 213, 2153eqtr4d 2780 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ท ยท (๐ต ยท ๐น))โ†‘2) = (((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)))
2172, 11sqmuld 14127 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ด ยท ๐น)โ†‘2) = ((๐ดโ†‘2) ยท (๐นโ†‘2)))
218217oveq2d 7427 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)) = (๐ท ยท ((๐ดโ†‘2) ยท (๐นโ†‘2))))
2192sqcld 14113 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
2207, 219, 37mulassd 11241 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2)) = (๐ท ยท ((๐ดโ†‘2) ยท (๐นโ†‘2))))
221218, 220eqtr4d 2773 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)) = ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2)))
222216, 221oveq12d 7429 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ท ยท (๐ต ยท ๐น))โ†‘2) โˆ’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2))) = ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) โˆ’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2))))
223209, 222oveq12d 7429 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ)โ†‘2) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2))) + (((๐ท ยท (๐ต ยท ๐น))โ†‘2) โˆ’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)))) = ((((๐ดโ†‘2) ยท (๐ธโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2))) + ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) โˆ’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2)))))
2247, 206mulcld 11238 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚)
225219, 224, 36subdird 11675 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) ยท (๐ธโ†‘2)) = (((๐ดโ†‘2) ยท (๐ธโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2))))
226 pellex.no1 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) = ๐ถ)
227226oveq1d 7426 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) ยท (๐ธโ†‘2)) = (๐ถ ยท (๐ธโ†‘2)))
228225, 227eqtr3d 2772 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (((๐ดโ†‘2) ยท (๐ธโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2))) = (๐ถ ยท (๐ธโ†‘2)))
2297, 7, 206mulassd 11241 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) = (๐ท ยท (๐ท ยท (๐ตโ†‘2))))
230229oveq1d 7426 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) โˆ’ (๐ท ยท (๐ดโ†‘2))) = ((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))))
231230oveq1d 7426 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) โˆ’ (๐ท ยท (๐ดโ†‘2))) ยท (๐นโ†‘2)) = (((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))) ยท (๐นโ†‘2)))
232214, 206mulcld 11238 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) โˆˆ โ„‚)
2337, 219mulcld 11238 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ท ยท (๐ดโ†‘2)) โˆˆ โ„‚)
234232, 233, 37subdird 11675 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) โˆ’ (๐ท ยท (๐ดโ†‘2))) ยท (๐นโ†‘2)) = ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) โˆ’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2))))
235 subdi 11651 . . . . . . . . . . . . . . . . . . . 20 ((๐ท โˆˆ โ„‚ โˆง (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚ โˆง (๐ดโ†‘2) โˆˆ โ„‚) โ†’ (๐ท ยท ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2))) = ((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))))
236235eqcomd 2736 . . . . . . . . . . . . . . . . . . 19 ((๐ท โˆˆ โ„‚ โˆง (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚ โˆง (๐ดโ†‘2) โˆˆ โ„‚) โ†’ ((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))) = (๐ท ยท ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2))))
2377, 224, 219, 236syl3anc 1369 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))) = (๐ท ยท ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2))))
238 negsubdi2 11523 . . . . . . . . . . . . . . . . . . . . . 22 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚) โ†’ -((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) = ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2)))
239238eqcomd 2736 . . . . . . . . . . . . . . . . . . . . 21 (((๐ดโ†‘2) โˆˆ โ„‚ โˆง (๐ท ยท (๐ตโ†‘2)) โˆˆ โ„‚) โ†’ ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2)) = -((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
240219, 224, 239syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2)) = -((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
241226negeqd 11458 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ -((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) = -๐ถ)
242240, 241eqtrd 2770 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2)) = -๐ถ)
243242oveq2d 7427 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ท ยท ((๐ท ยท (๐ตโ†‘2)) โˆ’ (๐ดโ†‘2))) = (๐ท ยท -๐ถ))
2447, 16mulneg2d 11672 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ท ยท -๐ถ) = -(๐ท ยท ๐ถ))
245237, 243, 2443eqtrd 2774 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ ((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))) = -(๐ท ยท ๐ถ))
246245oveq1d 7426 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (((๐ท ยท (๐ท ยท (๐ตโ†‘2))) โˆ’ (๐ท ยท (๐ดโ†‘2))) ยท (๐นโ†‘2)) = (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2)))
247231, 234, 2463eqtr3d 2778 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) โˆ’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2))) = (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2)))
248228, 247oveq12d 7429 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((((๐ดโ†‘2) ยท (๐ธโ†‘2)) โˆ’ ((๐ท ยท (๐ตโ†‘2)) ยท (๐ธโ†‘2))) + ((((๐ท ยท ๐ท) ยท (๐ตโ†‘2)) ยท (๐นโ†‘2)) โˆ’ ((๐ท ยท (๐ดโ†‘2)) ยท (๐นโ†‘2)))) = ((๐ถ ยท (๐ธโ†‘2)) + (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2))))
2497, 16mulcld 11238 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐ท ยท ๐ถ) โˆˆ โ„‚)
250249, 37mulneg1d 11671 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2)) = -((๐ท ยท ๐ถ) ยท (๐นโ†‘2)))
2517, 16mulcomd 11239 . . . . . . . . . . . . . . . . . . . 20 (๐œ‘ โ†’ (๐ท ยท ๐ถ) = (๐ถ ยท ๐ท))
252251oveq1d 7426 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ท ยท ๐ถ) ยท (๐นโ†‘2)) = ((๐ถ ยท ๐ท) ยท (๐นโ†‘2)))
25316, 7, 37mulassd 11241 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐ถ ยท ๐ท) ยท (๐นโ†‘2)) = (๐ถ ยท (๐ท ยท (๐นโ†‘2))))
254252, 253eqtrd 2770 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ท ยท ๐ถ) ยท (๐นโ†‘2)) = (๐ถ ยท (๐ท ยท (๐นโ†‘2))))
255254negeqd 11458 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ -((๐ท ยท ๐ถ) ยท (๐นโ†‘2)) = -(๐ถ ยท (๐ท ยท (๐นโ†‘2))))
256250, 255eqtrd 2770 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2)) = -(๐ถ ยท (๐ท ยท (๐นโ†‘2))))
257256oveq2d 7427 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ ยท (๐ธโ†‘2)) + (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2))) = ((๐ถ ยท (๐ธโ†‘2)) + -(๐ถ ยท (๐ท ยท (๐นโ†‘2)))))
25816, 36mulcld 11238 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ถ ยท (๐ธโ†‘2)) โˆˆ โ„‚)
25916, 38mulcld 11238 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ถ ยท (๐ท ยท (๐นโ†‘2))) โˆˆ โ„‚)
260258, 259negsubd 11581 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ ยท (๐ธโ†‘2)) + -(๐ถ ยท (๐ท ยท (๐นโ†‘2)))) = ((๐ถ ยท (๐ธโ†‘2)) โˆ’ (๐ถ ยท (๐ท ยท (๐นโ†‘2)))))
26161oveq2d 7427 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ถ ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))) = (๐ถ ยท ๐ถ))
262 subdi 11651 . . . . . . . . . . . . . . . . . 18 ((๐ถ โˆˆ โ„‚ โˆง (๐ธโ†‘2) โˆˆ โ„‚ โˆง (๐ท ยท (๐นโ†‘2)) โˆˆ โ„‚) โ†’ (๐ถ ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))) = ((๐ถ ยท (๐ธโ†‘2)) โˆ’ (๐ถ ยท (๐ท ยท (๐นโ†‘2)))))
263262eqcomd 2736 . . . . . . . . . . . . . . . . 17 ((๐ถ โˆˆ โ„‚ โˆง (๐ธโ†‘2) โˆˆ โ„‚ โˆง (๐ท ยท (๐นโ†‘2)) โˆˆ โ„‚) โ†’ ((๐ถ ยท (๐ธโ†‘2)) โˆ’ (๐ถ ยท (๐ท ยท (๐นโ†‘2)))) = (๐ถ ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))))
26416, 36, 38, 263syl3anc 1369 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ ((๐ถ ยท (๐ธโ†‘2)) โˆ’ (๐ถ ยท (๐ท ยท (๐นโ†‘2)))) = (๐ถ ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))))
26516sqvald 14112 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ถโ†‘2) = (๐ถ ยท ๐ถ))
266261, 264, 2653eqtr4d 2780 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ถ ยท (๐ธโ†‘2)) โˆ’ (๐ถ ยท (๐ท ยท (๐นโ†‘2)))) = (๐ถโ†‘2))
267257, 260, 2663eqtrd 2774 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ((๐ถ ยท (๐ธโ†‘2)) + (-(๐ท ยท ๐ถ) ยท (๐นโ†‘2))) = (๐ถโ†‘2))
268223, 248, 2673eqtrd 2774 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ)โ†‘2) โˆ’ (๐ท ยท ((๐ต ยท ๐ธ)โ†‘2))) + (((๐ท ยท (๐ต ยท ๐น))โ†‘2) โˆ’ (๐ท ยท ((๐ด ยท ๐น)โ†‘2)))) = (๐ถโ†‘2))
269193, 202, 2683eqtr2d 2776 . . . . . . . . . . . 12 (๐œ‘ โ†’ ((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น))))) = (๐ถโ†‘2))
270183, 192, 2693eqtrd 2774 . . . . . . . . . . 11 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))) = (๐ถโ†‘2))
271270oveq1d 7426 . . . . . . . . . 10 (๐œ‘ โ†’ ((((((๐ด ยท ๐ธ) ยท (๐ด ยท ๐ธ)) + ((๐ท ยท (๐ต ยท ๐น)) ยท (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))) + ((๐ด ยท ๐ธ) ยท (๐ท ยท (๐ต ยท ๐น))))) โˆ’ (((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ต ยท ๐ธ))) + (๐ท ยท ((๐ด ยท ๐น) ยท (๐ด ยท ๐น)))) โˆ’ ((๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น))) + (๐ท ยท ((๐ต ยท ๐ธ) ยท (๐ด ยท ๐น)))))) / (๐ถโ†‘2)) = ((๐ถโ†‘2) / (๐ถโ†‘2)))
272142, 145dividd 11992 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ถโ†‘2) / (๐ถโ†‘2)) = 1)
273170, 271, 2723eqtrd 2774 . . . . . . . . 9 (๐œ‘ โ†’ (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) ยท ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น)))) โˆ’ (๐ท ยท (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) ยท ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))))) / (๐ถโ†‘2)) = 1)
274151, 155, 2733eqtr2d 2776 . . . . . . . 8 (๐œ‘ โ†’ (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = 1)
275274adantr 479 . . . . . . 7 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = 1)
276 simpr 483 . . . . . . . . . . 11 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0)
277276fvoveq1d 7433 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) = (absโ€˜(0 / ๐ถ)))
27816, 17div0d 11993 . . . . . . . . . . . 12 (๐œ‘ โ†’ (0 / ๐ถ) = 0)
279278abs00bd 15242 . . . . . . . . . . 11 (๐œ‘ โ†’ (absโ€˜(0 / ๐ถ)) = 0)
280279adantr 479 . . . . . . . . . 10 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ (absโ€˜(0 / ๐ถ)) = 0)
281277, 280eqtrd 2770 . . . . . . . . 9 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) = 0)
282281sq0id 14162 . . . . . . . 8 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ ((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) = 0)
283282oveq1d 7426 . . . . . . 7 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))))
284275, 283eqtr3d 2772 . . . . . 6 ((๐œ‘ โˆง ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0) โ†’ 1 = (0 โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))))
285125, 284mtand 812 . . . . 5 (๐œ‘ โ†’ ยฌ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) = 0)
286285neqned 2945 . . . 4 (๐œ‘ โ†’ ((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) โ‰  0)
28714, 16, 286, 17divne0d 12010 . . 3 (๐œ‘ โ†’ (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โ‰  0)
288 nnabscl 15276 . . 3 (((((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โˆˆ โ„ค โˆง (((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ) โ‰  0) โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„•)
289104, 287, 288syl2anc 582 . 2 (๐œ‘ โ†’ (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„•)
290112, 16, 17absdivd 15406 . . . . 5 (๐œ‘ โ†’ (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) = ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) / (absโ€˜๐ถ)))
291 negsub 11512 . . . . . . . . . . . 12 (((๐ต ยท ๐ธ) โˆˆ โ„‚ โˆง (๐ด ยท ๐น) โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)) = ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)))
292291eqcomd 2736 . . . . . . . . . . 11 (((๐ต ยท ๐ธ) โˆˆ โ„‚ โˆง (๐ด ยท ๐น) โˆˆ โ„‚) โ†’ ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) = ((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)))
293110, 111, 292syl2anc 582 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) = ((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)))
294293oveq1d 7426 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = (((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)))
295133renegcld 11645 . . . . . . . . . 10 (๐œ‘ โ†’ -(๐ด ยท ๐น) โˆˆ โ„)
29611, 4mulcomd 11239 . . . . . . . . . . . 12 (๐œ‘ โ†’ (๐น ยท ๐ธ) = (๐ธ ยท ๐น))
297296oveq1d 7426 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐น ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ธ ยท ๐น) mod (absโ€˜๐ถ)))
298 modmul1 13893 . . . . . . . . . . . 12 (((๐ต โˆˆ โ„ โˆง ๐น โˆˆ โ„) โˆง (๐ธ โˆˆ โ„ค โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง (๐ต mod (absโ€˜๐ถ)) = (๐น mod (absโ€˜๐ถ))) โ†’ ((๐ต ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐น ยท ๐ธ) mod (absโ€˜๐ถ)))
29926, 27, 32, 31, 78, 298syl221anc 1379 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐น ยท ๐ธ) mod (absโ€˜๐ถ)))
300 modmul1 13893 . . . . . . . . . . . 12 (((๐ด โˆˆ โ„ โˆง ๐ธ โˆˆ โ„) โˆง (๐น โˆˆ โ„ค โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง (๐ด mod (absโ€˜๐ถ)) = (๐ธ mod (absโ€˜๐ถ))) โ†’ ((๐ด ยท ๐น) mod (absโ€˜๐ถ)) = ((๐ธ ยท ๐น) mod (absโ€˜๐ถ)))
30122, 23, 76, 31, 33, 300syl221anc 1379 . . . . . . . . . . 11 (๐œ‘ โ†’ ((๐ด ยท ๐น) mod (absโ€˜๐ถ)) = ((๐ธ ยท ๐น) mod (absโ€˜๐ถ)))
302297, 299, 3013eqtr4d 2780 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ด ยท ๐น) mod (absโ€˜๐ถ)))
303 modadd1 13877 . . . . . . . . . 10 ((((๐ต ยท ๐ธ) โˆˆ โ„ โˆง (๐ด ยท ๐น) โˆˆ โ„) โˆง (-(๐ด ยท ๐น) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โˆง ((๐ต ยท ๐ธ) mod (absโ€˜๐ถ)) = ((๐ด ยท ๐น) mod (absโ€˜๐ถ))) โ†’ (((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = (((๐ด ยท ๐น) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)))
304132, 133, 295, 31, 302, 303syl221anc 1379 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = (((๐ด ยท ๐น) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)))
305111negidd 11565 . . . . . . . . . 10 (๐œ‘ โ†’ ((๐ด ยท ๐น) + -(๐ด ยท ๐น)) = 0)
306305oveq1d 7426 . . . . . . . . 9 (๐œ‘ โ†’ (((๐ด ยท ๐น) + -(๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ)))
307294, 304, 3063eqtrd 2774 . . . . . . . 8 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = (0 mod (absโ€˜๐ถ)))
308307, 64eqtrd 2770 . . . . . . 7 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = 0)
309 absmod0 15254 . . . . . . . 8 ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) mod (absโ€˜๐ถ)) = 0))
310134, 31, 309syl2anc 582 . . . . . . 7 (๐œ‘ โ†’ ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) mod (absโ€˜๐ถ)) = 0))
311308, 310mpbid 231 . . . . . 6 (๐œ‘ โ†’ ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) mod (absโ€˜๐ถ)) = 0)
312112abscld 15387 . . . . . . 7 (๐œ‘ โ†’ (absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) โˆˆ โ„)
313 mod0 13845 . . . . . . 7 (((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) โˆˆ โ„ โˆง (absโ€˜๐ถ) โˆˆ โ„+) โ†’ (((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) / (absโ€˜๐ถ)) โˆˆ โ„ค))
314312, 31, 313syl2anc 582 . . . . . 6 (๐œ‘ โ†’ (((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) mod (absโ€˜๐ถ)) = 0 โ†” ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) / (absโ€˜๐ถ)) โˆˆ โ„ค))
315311, 314mpbid 231 . . . . 5 (๐œ‘ โ†’ ((absโ€˜((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น))) / (absโ€˜๐ถ)) โˆˆ โ„ค)
316290, 315eqeltrd 2831 . . . 4 (๐œ‘ โ†’ (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„ค)
317 absz 15262 . . . . 5 ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ โ†’ ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ค โ†” (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„ค))
318135, 317syl 17 . . . 4 (๐œ‘ โ†’ ((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ค โ†” (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„ค))
319316, 318mpbird 256 . . 3 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ค)
320 pellex.neq . . . . . . 7 (๐œ‘ โ†’ ยฌ (๐ด = ๐ธ โˆง ๐ต = ๐น))
32110nnne0d 12266 . . . . . . . . 9 (๐œ‘ โ†’ ๐น โ‰  0)
3223nnne0d 12266 . . . . . . . . 9 (๐œ‘ โ†’ ๐ธ โ‰  0)
3239, 11, 2, 4, 321, 322divmuleqd 12040 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต / ๐น) = (๐ด / ๐ธ) โ†” (๐ต ยท ๐ธ) = (๐ด ยท ๐น)))
32461adantr 479 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))) = ๐ถ)
325324eqcomd 2736 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ถ = ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2))))
326325oveq2d 7427 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท ๐ถ) = (((๐ต / ๐น)โ†‘2) ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))))
3279, 11, 321divcld 11994 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ต / ๐น) โˆˆ โ„‚)
328327sqcld 14113 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต / ๐น)โ†‘2) โˆˆ โ„‚)
329328adantr 479 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ต / ๐น)โ†‘2) โˆˆ โ„‚)
33036adantr 479 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ธโ†‘2) โˆˆ โ„‚)
33138adantr 479 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ท ยท (๐นโ†‘2)) โˆˆ โ„‚)
332329, 330, 331subdid 11674 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท ((๐ธโ†‘2) โˆ’ (๐ท ยท (๐นโ†‘2)))) = ((((๐ต / ๐น)โ†‘2) ยท (๐ธโ†‘2)) โˆ’ (((๐ต / ๐น)โ†‘2) ยท (๐ท ยท (๐นโ†‘2)))))
333 oveq1 7418 . . . . . . . . . . . . . . . . 17 ((๐ต / ๐น) = (๐ด / ๐ธ) โ†’ ((๐ต / ๐น)โ†‘2) = ((๐ด / ๐ธ)โ†‘2))
334333oveq1d 7426 . . . . . . . . . . . . . . . 16 ((๐ต / ๐น) = (๐ด / ๐ธ) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐ธโ†‘2)) = (((๐ด / ๐ธ)โ†‘2) ยท (๐ธโ†‘2)))
335334adantl 480 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐ธโ†‘2)) = (((๐ด / ๐ธ)โ†‘2) ยท (๐ธโ†‘2)))
3362adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ด โˆˆ โ„‚)
3374adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ธ โˆˆ โ„‚)
338322adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ธ โ‰  0)
339336, 337, 338sqdivd 14128 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ด / ๐ธ)โ†‘2) = ((๐ดโ†‘2) / (๐ธโ†‘2)))
340339oveq1d 7426 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ด / ๐ธ)โ†‘2) ยท (๐ธโ†‘2)) = (((๐ดโ†‘2) / (๐ธโ†‘2)) ยท (๐ธโ†‘2)))
341219adantr 479 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ดโ†‘2) โˆˆ โ„‚)
342 sqne0 14092 . . . . . . . . . . . . . . . . . . 19 (๐ธ โˆˆ โ„‚ โ†’ ((๐ธโ†‘2) โ‰  0 โ†” ๐ธ โ‰  0))
3434, 342syl 17 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ((๐ธโ†‘2) โ‰  0 โ†” ๐ธ โ‰  0))
344322, 343mpbird 256 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ (๐ธโ†‘2) โ‰  0)
345344adantr 479 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ธโ†‘2) โ‰  0)
346341, 330, 345divcan1d 11995 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ดโ†‘2) / (๐ธโ†‘2)) ยท (๐ธโ†‘2)) = (๐ดโ†‘2))
347335, 340, 3463eqtrd 2774 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐ธโ†‘2)) = (๐ดโ†‘2))
3487adantr 479 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ท โˆˆ โ„‚)
34937adantr 479 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐นโ†‘2) โˆˆ โ„‚)
350329, 348, 349mul12d 11427 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐ท ยท (๐นโ†‘2))) = (๐ท ยท (((๐ต / ๐น)โ†‘2) ยท (๐นโ†‘2))))
3519adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ต โˆˆ โ„‚)
35211adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐น โˆˆ โ„‚)
353321adantr 479 . . . . . . . . . . . . . . . . . 18 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐น โ‰  0)
354351, 352, 353sqdivd 14128 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ต / ๐น)โ†‘2) = ((๐ตโ†‘2) / (๐นโ†‘2)))
355354oveq1d 7426 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐นโ†‘2)) = (((๐ตโ†‘2) / (๐นโ†‘2)) ยท (๐นโ†‘2)))
356355oveq2d 7427 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ท ยท (((๐ต / ๐น)โ†‘2) ยท (๐นโ†‘2))) = (๐ท ยท (((๐ตโ†‘2) / (๐นโ†‘2)) ยท (๐นโ†‘2))))
357206adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ตโ†‘2) โˆˆ โ„‚)
358 sqne0 14092 . . . . . . . . . . . . . . . . . . . 20 (๐น โˆˆ โ„‚ โ†’ ((๐นโ†‘2) โ‰  0 โ†” ๐น โ‰  0))
35911, 358syl 17 . . . . . . . . . . . . . . . . . . 19 (๐œ‘ โ†’ ((๐นโ†‘2) โ‰  0 โ†” ๐น โ‰  0))
360321, 359mpbird 256 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ (๐นโ†‘2) โ‰  0)
361360adantr 479 . . . . . . . . . . . . . . . . 17 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐นโ†‘2) โ‰  0)
362357, 349, 361divcan1d 11995 . . . . . . . . . . . . . . . 16 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ตโ†‘2) / (๐นโ†‘2)) ยท (๐นโ†‘2)) = (๐ตโ†‘2))
363362oveq2d 7427 . . . . . . . . . . . . . . 15 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ท ยท (((๐ตโ†‘2) / (๐นโ†‘2)) ยท (๐นโ†‘2))) = (๐ท ยท (๐ตโ†‘2)))
364350, 356, 3633eqtrd 2774 . . . . . . . . . . . . . 14 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท (๐ท ยท (๐นโ†‘2))) = (๐ท ยท (๐ตโ†‘2)))
365347, 364oveq12d 7429 . . . . . . . . . . . . 13 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((((๐ต / ๐น)โ†‘2) ยท (๐ธโ†‘2)) โˆ’ (((๐ต / ๐น)โ†‘2) ยท (๐ท ยท (๐นโ†‘2)))) = ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
366326, 332, 3653eqtrd 2774 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) ยท ๐ถ) = ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
367226eqcomd 2736 . . . . . . . . . . . . 13 (๐œ‘ โ†’ ๐ถ = ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
368367adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ถ = ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))))
369366, 368oveq12d 7429 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((((๐ต / ๐น)โ†‘2) ยท ๐ถ) / ๐ถ) = (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))))
37016adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ถ โˆˆ โ„‚)
37117adantr 479 . . . . . . . . . . . 12 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ๐ถ โ‰  0)
372329, 370, 371divcan4d 12000 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((((๐ต / ๐น)โ†‘2) ยท ๐ถ) / ๐ถ) = ((๐ต / ๐น)โ†‘2))
373226, 226oveq12d 7429 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) = (๐ถ / ๐ถ))
37416, 17dividd 11992 . . . . . . . . . . . . 13 (๐œ‘ โ†’ (๐ถ / ๐ถ) = 1)
375373, 374eqtrd 2770 . . . . . . . . . . . 12 (๐œ‘ โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) = 1)
376375adantr 479 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2))) / ((๐ดโ†‘2) โˆ’ (๐ท ยท (๐ตโ†‘2)))) = 1)
377369, 372, 3763eqtr3d 2778 . . . . . . . . . 10 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ต / ๐น)โ†‘2) = 1)
37826, 27, 321redivcld 12046 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ (๐ต / ๐น) โˆˆ โ„)
3798nnnn0d 12536 . . . . . . . . . . . . . . . . . 18 (๐œ‘ โ†’ ๐ต โˆˆ โ„•0)
380379nn0ge0d 12539 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 0 โ‰ค ๐ต)
38110nngt0d 12265 . . . . . . . . . . . . . . . . 17 (๐œ‘ โ†’ 0 < ๐น)
382 divge0 12087 . . . . . . . . . . . . . . . . 17 (((๐ต โˆˆ โ„ โˆง 0 โ‰ค ๐ต) โˆง (๐น โˆˆ โ„ โˆง 0 < ๐น)) โ†’ 0 โ‰ค (๐ต / ๐น))
38326, 380, 27, 381, 382syl22anc 835 . . . . . . . . . . . . . . . 16 (๐œ‘ โ†’ 0 โ‰ค (๐ต / ๐น))
384378, 383sqrtsqd 15370 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (โˆšโ€˜((๐ต / ๐น)โ†‘2)) = (๐ต / ๐น))
385384eqcomd 2736 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ (๐ต / ๐น) = (โˆšโ€˜((๐ต / ๐น)โ†‘2)))
386385ad2antrr 722 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง ((๐ต / ๐น)โ†‘2) = 1) โ†’ (๐ต / ๐น) = (โˆšโ€˜((๐ต / ๐น)โ†‘2)))
387 fveq2 6890 . . . . . . . . . . . . . 14 (((๐ต / ๐น)โ†‘2) = 1 โ†’ (โˆšโ€˜((๐ต / ๐น)โ†‘2)) = (โˆšโ€˜1))
388387adantl 480 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง ((๐ต / ๐น)โ†‘2) = 1) โ†’ (โˆšโ€˜((๐ต / ๐น)โ†‘2)) = (โˆšโ€˜1))
389 sqrt1 15222 . . . . . . . . . . . . . 14 (โˆšโ€˜1) = 1
390389a1i 11 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง ((๐ต / ๐น)โ†‘2) = 1) โ†’ (โˆšโ€˜1) = 1)
391386, 388, 3903eqtrd 2774 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง ((๐ต / ๐น)โ†‘2) = 1) โ†’ (๐ต / ๐น) = 1)
392391ex 411 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) = 1 โ†’ (๐ต / ๐น) = 1))
393 simplr 765 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (๐ต / ๐น) = (๐ด / ๐ธ))
394 simpr 483 . . . . . . . . . . . . . . . 16 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (๐ต / ๐น) = 1)
395393, 394eqtr3d 2772 . . . . . . . . . . . . . . 15 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (๐ด / ๐ธ) = 1)
396395oveq1d 7426 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ((๐ด / ๐ธ) ยท ๐ธ) = (1 ยท ๐ธ))
3972, 4, 322divcan1d 11995 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ด / ๐ธ) ยท ๐ธ) = ๐ด)
398397ad2antrr 722 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ((๐ด / ๐ธ) ยท ๐ธ) = ๐ด)
3994mullidd 11236 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ยท ๐ธ) = ๐ธ)
400399ad2antrr 722 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (1 ยท ๐ธ) = ๐ธ)
401396, 398, 4003eqtr3d 2778 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ๐ด = ๐ธ)
402394oveq1d 7426 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ((๐ต / ๐น) ยท ๐น) = (1 ยท ๐น))
4039, 11, 321divcan1d 11995 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ ((๐ต / ๐น) ยท ๐น) = ๐ต)
404403ad2antrr 722 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ((๐ต / ๐น) ยท ๐น) = ๐ต)
40511mullidd 11236 . . . . . . . . . . . . . . 15 (๐œ‘ โ†’ (1 ยท ๐น) = ๐น)
406405ad2antrr 722 . . . . . . . . . . . . . 14 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (1 ยท ๐น) = ๐น)
407402, 404, 4063eqtr3d 2778 . . . . . . . . . . . . 13 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ ๐ต = ๐น)
408401, 407jca 510 . . . . . . . . . . . 12 (((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โˆง (๐ต / ๐น) = 1) โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น))
409408ex 411 . . . . . . . . . . 11 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ ((๐ต / ๐น) = 1 โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น)))
410392, 409syld 47 . . . . . . . . . 10 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (((๐ต / ๐น)โ†‘2) = 1 โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น)))
411377, 410mpd 15 . . . . . . . . 9 ((๐œ‘ โˆง (๐ต / ๐น) = (๐ด / ๐ธ)) โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น))
412411ex 411 . . . . . . . 8 (๐œ‘ โ†’ ((๐ต / ๐น) = (๐ด / ๐ธ) โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น)))
413323, 412sylbird 259 . . . . . . 7 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) = (๐ด ยท ๐น) โ†’ (๐ด = ๐ธ โˆง ๐ต = ๐น)))
414320, 413mtod 197 . . . . . 6 (๐œ‘ โ†’ ยฌ (๐ต ยท ๐ธ) = (๐ด ยท ๐น))
415414neqned 2945 . . . . 5 (๐œ‘ โ†’ (๐ต ยท ๐ธ) โ‰  (๐ด ยท ๐น))
416110, 111, 415subne0d 11584 . . . 4 (๐œ‘ โ†’ ((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) โ‰  0)
417112, 16, 416, 17divne0d 12010 . . 3 (๐œ‘ โ†’ (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โ‰  0)
418 nnabscl 15276 . . 3 (((((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โˆˆ โ„ค โˆง (((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ) โ‰  0) โ†’ (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„•)
419319, 417, 418syl2anc 582 . 2 (๐œ‘ โ†’ (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„•)
420 oveq1 7418 . . . . 5 (๐‘Ž = (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โ†’ (๐‘Žโ†‘2) = ((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2))
421420oveq1d 7426 . . . 4 (๐‘Ž = (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โ†’ ((๐‘Žโ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))))
422421eqeq1d 2732 . . 3 (๐‘Ž = (absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โ†’ (((๐‘Žโ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1 โ†” (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1))
423 oveq1 7418 . . . . . 6 (๐‘ = (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โ†’ (๐‘โ†‘2) = ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))
424423oveq2d 7427 . . . . 5 (๐‘ = (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โ†’ (๐ท ยท (๐‘โ†‘2)) = (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2)))
425424oveq2d 7427 . . . 4 (๐‘ = (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โ†’ (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))))
426425eqeq1d 2732 . . 3 (๐‘ = (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โ†’ ((((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1 โ†” (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = 1))
427422, 426rspc2ev 3623 . 2 (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ)) โˆˆ โ„• โˆง (absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ)) โˆˆ โ„• โˆง (((absโ€˜(((๐ด ยท ๐ธ) โˆ’ (๐ท ยท (๐ต ยท ๐น))) / ๐ถ))โ†‘2) โˆ’ (๐ท ยท ((absโ€˜(((๐ต ยท ๐ธ) โˆ’ (๐ด ยท ๐น)) / ๐ถ))โ†‘2))) = 1) โ†’ โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘ โˆˆ โ„• ((๐‘Žโ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1)
428289, 419, 274, 427syl3anc 1369 1 (๐œ‘ โ†’ โˆƒ๐‘Ž โˆˆ โ„• โˆƒ๐‘ โˆˆ โ„• ((๐‘Žโ†‘2) โˆ’ (๐ท ยท (๐‘โ†‘2))) = 1)
Colors of variables: wff setvar class
Syntax hints:  ยฌ wn 3   โ†’ wi 4   โ†” wb 205   โˆง wa 394   โˆง w3a 1085   = wceq 1539   โˆˆ wcel 2104   โ‰  wne 2938  โˆƒwrex 3068   class class class wbr 5147  โ€˜cfv 6542  (class class class)co 7411  โ„‚cc 11110  โ„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   ยท cmul 11117   < clt 11252   โ‰ค cle 11253   โˆ’ cmin 11448  -cneg 11449   / cdiv 11875  โ„•cn 12216  2c2 12271  โ„คcz 12562  โ„šcq 12936  โ„+crp 12978   mod cmo 13838  โ†‘cexp 14031  โˆšcsqrt 15184  abscabs 15185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-z 12563  df-uz 12827  df-rp 12979  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187
This theorem is referenced by:  pellex  41875
  Copyright terms: Public domain W3C validator