Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  factwoffsmonot Structured version   Visualization version   GIF version

Theorem factwoffsmonot 41614
Description: A factorial with offset is monotonely increasing. (Contributed by metakunt, 20-Apr-2024.)
Assertion
Ref Expression
factwoffsmonot (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘‹ + ๐‘)) โ‰ค (!โ€˜(๐‘Œ + ๐‘)))

Proof of Theorem factwoffsmonot
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 7422 . . . 4 (๐‘ฅ = 0 โ†’ (๐‘‹ + ๐‘ฅ) = (๐‘‹ + 0))
21fveq2d 6895 . . 3 (๐‘ฅ = 0 โ†’ (!โ€˜(๐‘‹ + ๐‘ฅ)) = (!โ€˜(๐‘‹ + 0)))
3 oveq2 7422 . . . 4 (๐‘ฅ = 0 โ†’ (๐‘Œ + ๐‘ฅ) = (๐‘Œ + 0))
43fveq2d 6895 . . 3 (๐‘ฅ = 0 โ†’ (!โ€˜(๐‘Œ + ๐‘ฅ)) = (!โ€˜(๐‘Œ + 0)))
52, 4breq12d 5155 . 2 (๐‘ฅ = 0 โ†’ ((!โ€˜(๐‘‹ + ๐‘ฅ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฅ)) โ†” (!โ€˜(๐‘‹ + 0)) โ‰ค (!โ€˜(๐‘Œ + 0))))
6 oveq2 7422 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘‹ + ๐‘ฅ) = (๐‘‹ + ๐‘ฆ))
76fveq2d 6895 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (!โ€˜(๐‘‹ + ๐‘ฅ)) = (!โ€˜(๐‘‹ + ๐‘ฆ)))
8 oveq2 7422 . . . 4 (๐‘ฅ = ๐‘ฆ โ†’ (๐‘Œ + ๐‘ฅ) = (๐‘Œ + ๐‘ฆ))
98fveq2d 6895 . . 3 (๐‘ฅ = ๐‘ฆ โ†’ (!โ€˜(๐‘Œ + ๐‘ฅ)) = (!โ€˜(๐‘Œ + ๐‘ฆ)))
107, 9breq12d 5155 . 2 (๐‘ฅ = ๐‘ฆ โ†’ ((!โ€˜(๐‘‹ + ๐‘ฅ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฅ)) โ†” (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))))
11 oveq2 7422 . . . 4 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (๐‘‹ + ๐‘ฅ) = (๐‘‹ + (๐‘ฆ + 1)))
1211fveq2d 6895 . . 3 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (!โ€˜(๐‘‹ + ๐‘ฅ)) = (!โ€˜(๐‘‹ + (๐‘ฆ + 1))))
13 oveq2 7422 . . . 4 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (๐‘Œ + ๐‘ฅ) = (๐‘Œ + (๐‘ฆ + 1)))
1413fveq2d 6895 . . 3 (๐‘ฅ = (๐‘ฆ + 1) โ†’ (!โ€˜(๐‘Œ + ๐‘ฅ)) = (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
1512, 14breq12d 5155 . 2 (๐‘ฅ = (๐‘ฆ + 1) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฅ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฅ)) โ†” (!โ€˜(๐‘‹ + (๐‘ฆ + 1))) โ‰ค (!โ€˜(๐‘Œ + (๐‘ฆ + 1)))))
16 oveq2 7422 . . . 4 (๐‘ฅ = ๐‘ โ†’ (๐‘‹ + ๐‘ฅ) = (๐‘‹ + ๐‘))
1716fveq2d 6895 . . 3 (๐‘ฅ = ๐‘ โ†’ (!โ€˜(๐‘‹ + ๐‘ฅ)) = (!โ€˜(๐‘‹ + ๐‘)))
18 oveq2 7422 . . . 4 (๐‘ฅ = ๐‘ โ†’ (๐‘Œ + ๐‘ฅ) = (๐‘Œ + ๐‘))
1918fveq2d 6895 . . 3 (๐‘ฅ = ๐‘ โ†’ (!โ€˜(๐‘Œ + ๐‘ฅ)) = (!โ€˜(๐‘Œ + ๐‘)))
2017, 19breq12d 5155 . 2 (๐‘ฅ = ๐‘ โ†’ ((!โ€˜(๐‘‹ + ๐‘ฅ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฅ)) โ†” (!โ€˜(๐‘‹ + ๐‘)) โ‰ค (!โ€˜(๐‘Œ + ๐‘))))
21 facwordi 14272 . . 3 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜๐‘‹) โ‰ค (!โ€˜๐‘Œ))
22 nn0cn 12504 . . . . . 6 (๐‘‹ โˆˆ โ„•0 โ†’ ๐‘‹ โˆˆ โ„‚)
23 addrid 11416 . . . . . 6 (๐‘‹ โˆˆ โ„‚ โ†’ (๐‘‹ + 0) = ๐‘‹)
2422, 23syl 17 . . . . 5 (๐‘‹ โˆˆ โ„•0 โ†’ (๐‘‹ + 0) = ๐‘‹)
2524fveq2d 6895 . . . 4 (๐‘‹ โˆˆ โ„•0 โ†’ (!โ€˜(๐‘‹ + 0)) = (!โ€˜๐‘‹))
26253ad2ant1 1131 . . 3 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜(๐‘‹ + 0)) = (!โ€˜๐‘‹))
27 nn0cn 12504 . . . . . 6 (๐‘Œ โˆˆ โ„•0 โ†’ ๐‘Œ โˆˆ โ„‚)
28 addrid 11416 . . . . . 6 (๐‘Œ โˆˆ โ„‚ โ†’ (๐‘Œ + 0) = ๐‘Œ)
2927, 28syl 17 . . . . 5 (๐‘Œ โˆˆ โ„•0 โ†’ (๐‘Œ + 0) = ๐‘Œ)
3029fveq2d 6895 . . . 4 (๐‘Œ โˆˆ โ„•0 โ†’ (!โ€˜(๐‘Œ + 0)) = (!โ€˜๐‘Œ))
31303ad2ant2 1132 . . 3 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜(๐‘Œ + 0)) = (!โ€˜๐‘Œ))
3221, 26, 313brtr4d 5174 . 2 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜(๐‘‹ + 0)) โ‰ค (!โ€˜(๐‘Œ + 0)))
33 nn0cn 12504 . . . . . . 7 (๐‘ฆ โˆˆ โ„•0 โ†’ ๐‘ฆ โˆˆ โ„‚)
34 ax-1cn 11188 . . . . . . . 8 1 โˆˆ โ„‚
35 addass 11217 . . . . . . . 8 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) = (๐‘‹ + (๐‘ฆ + 1)))
3634, 35mp3an3 1447 . . . . . . 7 ((๐‘‹ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) = (๐‘‹ + (๐‘ฆ + 1)))
3722, 33, 36syl2an 595 . . . . . 6 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) = (๐‘‹ + (๐‘ฆ + 1)))
3837fveq2d 6895 . . . . 5 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘‹ + (๐‘ฆ + 1))))
39383ad2antl1 1183 . . . 4 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘‹ + (๐‘ฆ + 1))))
4039adantr 480 . . 3 ((((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘‹ + (๐‘ฆ + 1))))
41 nn0addcl 12529 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘‹ + ๐‘ฆ) โˆˆ โ„•0)
42413adant2 1129 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘‹ + ๐‘ฆ) โˆˆ โ„•0)
4342adantr 480 . . . . . . . . . 10 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (๐‘‹ + ๐‘ฆ) โˆˆ โ„•0)
44 nn0addcl 12529 . . . . . . . . . . . 12 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„•0)
45443adant1 1128 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„•0)
4645adantr 480 . . . . . . . . . 10 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„•0)
47 nn0re 12503 . . . . . . . . . . . 12 (๐‘‹ โˆˆ โ„•0 โ†’ ๐‘‹ โˆˆ โ„)
48 nn0re 12503 . . . . . . . . . . . 12 (๐‘Œ โˆˆ โ„•0 โ†’ ๐‘Œ โˆˆ โ„)
49 nn0re 12503 . . . . . . . . . . . 12 (๐‘ฆ โˆˆ โ„•0 โ†’ ๐‘ฆ โˆˆ โ„)
50 leadd1 11704 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„ โˆง ๐‘Œ โˆˆ โ„ โˆง ๐‘ฆ โˆˆ โ„) โ†’ (๐‘‹ โ‰ค ๐‘Œ โ†” (๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ)))
5147, 48, 49, 50syl3an 1158 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘‹ โ‰ค ๐‘Œ โ†” (๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ)))
5251biimpa 476 . . . . . . . . . 10 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ))
53 facwordi 14272 . . . . . . . . . 10 (((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โˆง (๐‘Œ + ๐‘ฆ) โˆˆ โ„•0 โˆง (๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ)) โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)))
5443, 46, 52, 53syl3anc 1369 . . . . . . . . 9 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)))
55543an1rs 1357 . . . . . . . 8 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)))
56 nn0re 12503 . . . . . . . . . . . . 13 ((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (๐‘‹ + ๐‘ฆ) โˆˆ โ„)
5743, 56syl 17 . . . . . . . . . . . 12 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (๐‘‹ + ๐‘ฆ) โˆˆ โ„)
58 nn0re 12503 . . . . . . . . . . . . 13 ((๐‘Œ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„)
5946, 58syl 17 . . . . . . . . . . . 12 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„)
6057, 59jca 511 . . . . . . . . . . 11 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ ((๐‘‹ + ๐‘ฆ) โˆˆ โ„ โˆง (๐‘Œ + ๐‘ฆ) โˆˆ โ„))
61 1re 11236 . . . . . . . . . . . 12 1 โˆˆ โ„
62 leadd1 11704 . . . . . . . . . . . 12 (((๐‘‹ + ๐‘ฆ) โˆˆ โ„ โˆง (๐‘Œ + ๐‘ฆ) โˆˆ โ„ โˆง 1 โˆˆ โ„) โ†’ ((๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ) โ†” ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)))
6361, 62mp3an3 1447 . . . . . . . . . . 11 (((๐‘‹ + ๐‘ฆ) โˆˆ โ„ โˆง (๐‘Œ + ๐‘ฆ) โˆˆ โ„) โ†’ ((๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ) โ†” ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)))
6460, 63syl 17 . . . . . . . . . 10 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ ((๐‘‹ + ๐‘ฆ) โ‰ค (๐‘Œ + ๐‘ฆ) โ†” ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)))
6552, 64mpbid 231 . . . . . . . . 9 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1))
66653an1rs 1357 . . . . . . . 8 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1))
6755, 66jca 511 . . . . . . 7 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆง ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)))
68 faccl 14266 . . . . . . . . . . . . . . 15 ((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„•)
69 nnre 12241 . . . . . . . . . . . . . . 15 ((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„• โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„)
7041, 68, 693syl 18 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„)
71703adant2 1129 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„)
72 nngt0 12265 . . . . . . . . . . . . . . . 16 ((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„• โ†’ 0 < (!โ€˜(๐‘‹ + ๐‘ฆ)))
7341, 68, 723syl 18 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 0 < (!โ€˜(๐‘‹ + ๐‘ฆ)))
74 0re 11238 . . . . . . . . . . . . . . . . 17 0 โˆˆ โ„
75 ltle 11324 . . . . . . . . . . . . . . . . 17 ((0 โˆˆ โ„ โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„) โ†’ (0 < (!โ€˜(๐‘‹ + ๐‘ฆ)) โ†’ 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))))
7674, 75mpan 689 . . . . . . . . . . . . . . . 16 ((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„ โ†’ (0 < (!โ€˜(๐‘‹ + ๐‘ฆ)) โ†’ 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))))
7770, 76syl 17 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (0 < (!โ€˜(๐‘‹ + ๐‘ฆ)) โ†’ 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))))
7873, 77mpd 15 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ)))
79783adant2 1129 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ)))
8071, 79jca 511 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„ โˆง 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))))
81 faccl 14266 . . . . . . . . . . . . . 14 ((๐‘Œ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„•)
82 nnre 12241 . . . . . . . . . . . . . 14 ((!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„• โ†’ (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„)
8344, 81, 823syl 18 . . . . . . . . . . . . 13 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„)
84833adant1 1128 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„)
8580, 84jca 511 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„ โˆง 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))) โˆง (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„))
86 1nn0 12510 . . . . . . . . . . . . . . . . 17 1 โˆˆ โ„•0
87 nn0addcl 12529 . . . . . . . . . . . . . . . . 17 (((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โˆง 1 โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„•0)
8886, 87mpan2 690 . . . . . . . . . . . . . . . 16 ((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„•0)
8941, 88syl 17 . . . . . . . . . . . . . . 15 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„•0)
90 nn0re 12503 . . . . . . . . . . . . . . 15 (((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„•0 โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„)
9189, 90syl 17 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„)
92913adant2 1129 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„)
93 nn0ge0 12519 . . . . . . . . . . . . . . 15 (((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„•0 โ†’ 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1))
9489, 93syl 17 . . . . . . . . . . . . . 14 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1))
95943adant2 1129 . . . . . . . . . . . . 13 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1))
9692, 95jca 511 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„ โˆง 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1)))
97 nn0readdcl 12560 . . . . . . . . . . . . . 14 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (๐‘Œ + ๐‘ฆ) โˆˆ โ„)
98 1red 11237 . . . . . . . . . . . . . 14 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ 1 โˆˆ โ„)
9997, 98readdcld 11265 . . . . . . . . . . . . 13 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘Œ + ๐‘ฆ) + 1) โˆˆ โ„)
100993adant1 1128 . . . . . . . . . . . 12 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘Œ + ๐‘ฆ) + 1) โˆˆ โ„)
10196, 100jca 511 . . . . . . . . . . 11 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„ โˆง 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1)) โˆง ((๐‘Œ + ๐‘ฆ) + 1) โˆˆ โ„))
10285, 101jca 511 . . . . . . . . . 10 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„ โˆง 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))) โˆง (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„) โˆง ((((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„ โˆง 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1)) โˆง ((๐‘Œ + ๐‘ฆ) + 1) โˆˆ โ„)))
103 lemul12a 12094 . . . . . . . . . 10 (((((!โ€˜(๐‘‹ + ๐‘ฆ)) โˆˆ โ„ โˆง 0 โ‰ค (!โ€˜(๐‘‹ + ๐‘ฆ))) โˆง (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆˆ โ„) โˆง ((((๐‘‹ + ๐‘ฆ) + 1) โˆˆ โ„ โˆง 0 โ‰ค ((๐‘‹ + ๐‘ฆ) + 1)) โˆง ((๐‘Œ + ๐‘ฆ) + 1) โˆˆ โ„)) โ†’ (((!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆง ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
104102, 103syl 17 . . . . . . . . 9 ((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆง ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
1051043expa 1116 . . . . . . . 8 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆง ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
1061053adantl3 1166 . . . . . . 7 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (((!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ)) โˆง ((๐‘‹ + ๐‘ฆ) + 1) โ‰ค ((๐‘Œ + ๐‘ฆ) + 1)) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
10767, 106mpd 15 . . . . . 6 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1)))
108 facp1 14261 . . . . . . . . . 10 ((๐‘‹ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)))
10943, 108syl 17 . . . . . . . . 9 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)))
110 facp1 14261 . . . . . . . . . 10 ((๐‘Œ + ๐‘ฆ) โˆˆ โ„•0 โ†’ (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1)))
11146, 110syl 17 . . . . . . . . 9 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1)))
112109, 111jca 511 . . . . . . . 8 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ ((!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โˆง (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
113 breq12 5147 . . . . . . . 8 (((!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โˆง (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))) โ†’ ((!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) โ†” ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
114112, 113syl 17 . . . . . . 7 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โˆง ๐‘‹ โ‰ค ๐‘Œ) โ†’ ((!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) โ†” ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
1151143an1rs 1357 . . . . . 6 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) โ†” ((!โ€˜(๐‘‹ + ๐‘ฆ)) ยท ((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค ((!โ€˜(๐‘Œ + ๐‘ฆ)) ยท ((๐‘Œ + ๐‘ฆ) + 1))))
116107, 115mpbird 257 . . . . 5 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)))
117116adantr 480 . . . 4 ((((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)))
118 addass 11217 . . . . . . . . 9 ((๐‘Œ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง 1 โˆˆ โ„‚) โ†’ ((๐‘Œ + ๐‘ฆ) + 1) = (๐‘Œ + (๐‘ฆ + 1)))
11934, 118mp3an3 1447 . . . . . . . 8 ((๐‘Œ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚) โ†’ ((๐‘Œ + ๐‘ฆ) + 1) = (๐‘Œ + (๐‘ฆ + 1)))
12027, 33, 119syl2an 595 . . . . . . 7 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ ((๐‘Œ + ๐‘ฆ) + 1) = (๐‘Œ + (๐‘ฆ + 1)))
121120fveq2d 6895 . . . . . 6 ((๐‘Œ โˆˆ โ„•0 โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
1221213ad2antl2 1184 . . . . 5 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โ†’ (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
123122adantr 480 . . . 4 ((((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))) โ†’ (!โ€˜((๐‘Œ + ๐‘ฆ) + 1)) = (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
124117, 123breqtrd 5168 . . 3 ((((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))) โ†’ (!โ€˜((๐‘‹ + ๐‘ฆ) + 1)) โ‰ค (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
12540, 124eqbrtrrd 5166 . 2 ((((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ฆ โˆˆ โ„•0) โˆง (!โ€˜(๐‘‹ + ๐‘ฆ)) โ‰ค (!โ€˜(๐‘Œ + ๐‘ฆ))) โ†’ (!โ€˜(๐‘‹ + (๐‘ฆ + 1))) โ‰ค (!โ€˜(๐‘Œ + (๐‘ฆ + 1))))
1265, 10, 15, 20, 32, 125nn0indd 12681 1 (((๐‘‹ โˆˆ โ„•0 โˆง ๐‘Œ โˆˆ โ„•0 โˆง ๐‘‹ โ‰ค ๐‘Œ) โˆง ๐‘ โˆˆ โ„•0) โ†’ (!โ€˜(๐‘‹ + ๐‘)) โ‰ค (!โ€˜(๐‘Œ + ๐‘)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1085   = wceq 1534   โˆˆ wcel 2099   class class class wbr 5142  โ€˜cfv 6542  (class class class)co 7414  โ„‚cc 11128  โ„cr 11129  0cc0 11130  1c1 11131   + caddc 11133   ยท cmul 11135   < clt 11270   โ‰ค cle 11271  โ„•cn 12234  โ„•0cn0 12494  !cfa 14256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  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 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-er 8718  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-nn 12235  df-n0 12495  df-z 12581  df-uz 12845  df-seq 13991  df-fac 14257
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator