Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  divalglemex Unicode version

Theorem divalglemex 10466
 Description: Lemma for divalg 10468. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.)
Assertion
Ref Expression
divalglemex
Distinct variable groups:   ,,   ,,

Proof of Theorem divalglemex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpl1 942 . . . 4
2 simpl2 943 . . . . . 6
32znegcld 8552 . . . . 5
4 simpr 108 . . . . . 6
52zred 8550 . . . . . . 7
65lt0neg1d 7683 . . . . . 6
74, 6mpbid 145 . . . . 5
8 elnnz 8442 . . . . 5
93, 7, 8sylanbrc 408 . . . 4
10 divalglemnn 10462 . . . 4
111, 9, 10syl2anc 403 . . 3
12 simplr 497 . . . . . . . 8
1312znegcld 8552 . . . . . . 7
14 simpr1 945 . . . . . . 7
15 simpr2 946 . . . . . . . 8
16 simpll2 979 . . . . . . . . . . 11
1716ad2antrr 472 . . . . . . . . . 10
1817zcnd 8551 . . . . . . . . 9
1918absnegd 10213 . . . . . . . 8
2015, 19breqtrd 3817 . . . . . . 7
21 simpr3 947 . . . . . . . 8
2212zcnd 8551 . . . . . . . . . 10
23 mulneg12 7568 . . . . . . . . . 10
2422, 18, 23syl2anc 403 . . . . . . . . 9
2524oveq1d 5558 . . . . . . . 8
2621, 25eqtr4d 2117 . . . . . . 7
27 oveq1 5550 . . . . . . . . . . 11
2827oveq1d 5558 . . . . . . . . . 10
2928eqeq2d 2093 . . . . . . . . 9
30293anbi3d 1250 . . . . . . . 8
3130rspcev 2702 . . . . . . 7
3213, 14, 20, 26, 31syl13anc 1172 . . . . . 6
3332ex 113 . . . . 5
3433rexlimdva 2478 . . . 4
3534reximdva 2464 . . 3
3611, 35mpd 13 . 2
37 simpr 108 . . 3
38 simpl3 944 . . 3
3937, 38pm2.21ddne 2329 . 2
40 simpl1 942 . . 3
41 simpl2 943 . . . 4
42 simpr 108 . . . 4
43 elnnz 8442 . . . 4
4441, 42, 43sylanbrc 408 . . 3
45 divalglemnn 10462 . . 3
4640, 44, 45syl2anc 403 . 2
47 ztri3or0 8474 . . 3